Add options to the kore term pretty printer (#3963)

Add the following options when pretty printing terms:

* `decode` - decode symbol labels and strip the `Lbl` prefix
* `truncate` - truncate long domain values
* `infix` - try to re-assemble infix notation from the holes in label
syntax (may not always be correct). For example:
   ```
... Uncertain about match with rule. Remainder: #range(
Eq#VarB1:SortBytes{} , Eq#VarS2:SortInt{} , Eq#VarW2:SortInt{} ) ==
buf("32", lookup(VarCONTRACT-FAKEETH_STORAGE:SortMap{}, keccak(
buf("32", VarCALLER_ID:SortInt{}) +Bytes
"\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL"
))), #range( Eq#VarB1:SortBytes{} , Eq#VarS1:SortInt{} ,
Eq#VarW1:SortInt{} ) == buf("32",
lookup(VarCONTRACT-FAKEETH_STORAGE:SortMap{}, keccak( buf("32",
VarCONTRACT_ID:SortInt{}) +Bytes buf("32", keccak( buf("32",
VarCALLER_ID:SortInt{}) +Bytes
"\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\SOH"
)) )))
   ```

These can now be passed to the server via the `--pretty-print` flag.
E.g. `--pretty-print truncated,decode` will preserve current behaviour
(and is set as default when no explicit option is provided)

---------

Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

booster/library/Booster/Builtin/Base.hs

@@ -21,6 +21,7 @@ import Data.Text.Encoding qualified as Text
 import Prettyprinter (pretty)
 
 import Booster.Pattern.Base
+import Booster.Pattern.Pretty
 import Booster.Pattern.Util
 import Booster.Prettyprinter
 
@@ -68,5 +69,5 @@ t `shouldHaveSort` s
         throwE $
             Text.unlines
                 [ "Argument term has unexpected sort (expected " <> Text.decodeLatin1 s <> "):"
-                , renderText (pretty t)
+                , renderText (pretty (PrettyWithModifiers @['Decoded, 'Truncated] t))
                 ]

booster/library/Booster/Builtin/KEQUAL.hs

@@ -22,6 +22,7 @@ import Prettyprinter
 import Booster.Builtin.Base
 import Booster.Pattern.Base
 import Booster.Pattern.Bool
+import Booster.Pattern.Pretty
 import Booster.Pattern.Util (isConstructorSymbol, sortOfTerm)
 import Booster.Prettyprinter (renderText)
 
@@ -40,8 +41,8 @@ iteHook args
         unless (sortOfTerm thenVal == sortOfTerm elseVal) $
             throwE . Text.unlines $
                 [ "Different sorts in alternatives:"
-                , renderText $ pretty thenVal
-                , renderText $ pretty elseVal
+                , renderText $ pretty (PrettyWithModifiers @['Decoded, 'Truncated] thenVal)
+                , renderText $ pretty (PrettyWithModifiers @['Decoded, 'Truncated] elseVal)
                 ]
         case cond of
             TrueBool -> pure $ Just thenVal

booster/library/Booster/CLOptions.hs

@@ -28,6 +28,7 @@ import Text.Read (readMaybe)
 
 import Booster.GlobalState (EquationOptions (..))
 import Booster.Log.Context (ContextFilter, ctxt, readContextFilter)
+import Booster.Pattern.Pretty
 import Booster.SMT.Interface (SMTOptions (..), defaultSMTOptions)
 import Booster.SMT.LowLevelCodec qualified as SMT (parseSExpr)
 import Booster.Trace (CustomUserEventType)
@@ -48,6 +49,7 @@ data CLOptions = CLOptions
     , smtOptions :: Maybe SMTOptions
     , equationOptions :: EquationOptions
     , indexCells :: [Text]
+    , prettyPrintOptions :: [ModifierT]
     , -- developer options below
       eventlogEnabledUserEvents :: [CustomUserEventType]
     }
@@ -162,6 +164,14 @@ clOptionsParser =
                 <> help "Names of configuration cells to index rewrite rules with (default: 'k')"
                 <> value []
             )
+        <*> option
+            (eitherReader $ mapM (readModifierT . trim) . splitOn ",")
+            ( metavar "PRETTY_PRINT"
+                <> value [Decoded, Truncated]
+                <> long "pretty-print"
+                <> help "Prety print options for kore terms: decode, infix, truncated"
+                <> showDefault
+            )
         -- developer options below
         <*> many
             ( option
@@ -201,6 +211,13 @@ clOptionsParser =
         "json" -> Right Json
         other -> Left $ other <> ": Unsupported log format"
 
+    readModifierT :: String -> Either String ModifierT
+    readModifierT = \case
+        "truncated" -> Right Truncated
+        "infix" -> Right Infix
+        "decoded" -> Right Decoded
+        other -> Left $ other <> ": Unsupported prettry printer option"
+
     readTimeStampFormat :: String -> Either String TimestampFormat
     readTimeStampFormat = \case
         "pretty" -> Right Pretty

booster/library/Booster/Definition/Ceil.hs

@@ -16,6 +16,7 @@ import Booster.Pattern.Base
 import Booster.LLVM as LLVM (API, simplifyBool)
 import Booster.Log
 import Booster.Pattern.Bool
+import Booster.Pattern.Pretty
 import Booster.Pattern.Util (isConcrete, sortOfTerm)
 import Booster.Util (Flag (..))
 import Control.DeepSeq (NFData)
@@ -43,20 +44,20 @@ data ComputeCeilSummary = ComputeCeilSummary
     deriving stock (Eq, Ord, Show, GHC.Generic)
     deriving anyclass (NFData)
 
-instance Pretty ComputeCeilSummary where
-    pretty ComputeCeilSummary{rule, ceils} =
+instance FromModifiersT mods => Pretty (PrettyWithModifiers mods ComputeCeilSummary) where
+    pretty (PrettyWithModifiers ComputeCeilSummary{rule, ceils}) =
         Pretty.vsep $
             [ "\n\n----------------------------\n"
             , pretty $ sourceRef rule
-            , pretty rule.lhs
+            , pretty' @mods rule.lhs
             , "=>"
-            , pretty rule.rhs
+            , pretty' @mods rule.rhs
             ]
                 <> ( if null rule.requires
                         then []
                         else
                             [ "requires"
-                            , Pretty.indent 2 . Pretty.vsep $ map pretty $ Set.toList rule.requires
+                            , Pretty.indent 2 . Pretty.vsep $ map (pretty' @mods) $ Set.toList rule.requires
                             ]
                    )
                 <> [ Pretty.line
@@ -69,7 +70,9 @@ instance Pretty ComputeCeilSummary where
                         [ Pretty.line
                         , "computed ceils:"
                         , Pretty.indent 2 . Pretty.vsep $
-                            map (either pretty (\t -> "#Ceil(" Pretty.<+> pretty t Pretty.<+> ")")) (Set.toList ceils)
+                            map
+                                (either (pretty' @mods) (\t -> "#Ceil(" Pretty.<+> pretty' @mods t Pretty.<+> ")"))
+                                (Set.toList ceils)
                         ]
 
 computeCeilsDefinition ::
@@ -209,7 +212,7 @@ mkInKeys inKeysSymbols k m =
         Nothing ->
             error $
                 "in_keys for key sort '"
-                    <> show (pretty $ sortOfTerm k)
+                    <> show (pretty $ PrettyWithModifiers @'[Decoded, Truncated] $ sortOfTerm k)
                     <> "' and map sort '"
-                    <> show (pretty $ sortOfTerm m)
+                    <> show (pretty $ PrettyWithModifiers @'[Decoded, Truncated] $ sortOfTerm m)
                     <> "' does not exist."

booster/library/Booster/Definition/Util.hs

@@ -31,6 +31,7 @@ import Booster.Definition.Base
 import Booster.Definition.Ceil (ComputeCeilSummary (..))
 import Booster.Pattern.Base
 import Booster.Pattern.Index (CellIndex (..), TermIndex (..))
+import Booster.Pattern.Pretty
 import Booster.Prettyprinter
 import Booster.Util
 
@@ -92,7 +93,8 @@ prettySummary :: Bool -> Summary -> String
 prettySummary veryVerbose summary@Summary{computeCeilsSummary} =
     Pretty.renderString . layoutPrettyUnbounded $
         Pretty.vcat $
-            pretty summary : if veryVerbose then map pretty computeCeilsSummary else []
+            pretty summary
+                : if veryVerbose then map (pretty' @['Decoded, 'Truncated] $) computeCeilsSummary else []
 
 instance Pretty Summary where
     pretty summary =
@@ -146,7 +148,8 @@ instance Pretty Summary where
         prettyCellIndex None = "None"
 
         prettyCeilRule :: RewriteRule r -> Doc a
-        prettyCeilRule RewriteRule{lhs, rhs} = "#Ceil(" <+> pretty lhs <+> ") =>" <+> pretty rhs
+        prettyCeilRule RewriteRule{lhs, rhs} =
+            "#Ceil(" <+> pretty' @['Decoded, 'Truncated] lhs <+> ") =>" <+> pretty' @['Decoded, 'Truncated] rhs
 
 sourceRefText :: HasSourceRef a => a -> Text
 sourceRefText = renderOneLineText . pretty . sourceRef