Make Pretty prettier (#4057)

The tool was not printing the substitution after internalising a pattern. Also switched it to using `Text` to print things and prettified the format a bit (infix printing, indentations).
runtimeverification · Oct 15, 2024 · 0bfbcff · 0bfbcff
1 parent 4872094
commit 0bfbcff
Show file tree

Hide file tree

Showing 2 changed files with 43 additions and 23 deletions.
diff --git a/dev-tools/package.yaml b/dev-tools/package.yaml
@@ -157,6 +157,7 @@ executables:
       - base
       - aeson
       - bytestring
+      - containers
       - hs-backend-booster
       - prettyprinter
       - text

diff --git a/dev-tools/pretty/Pretty.hs b/dev-tools/pretty/Pretty.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE PatternSynonyms #-}
 
 {- | Pretty printer for JSON KORE terms
@@ -9,8 +10,19 @@ module Main (
     main,
 ) where
 
+import Control.Monad (unless)
+import Control.Monad.Trans.Except
+import Data.Aeson (eitherDecode)
+import Data.ByteString.Lazy qualified as BS
+import Data.Map (Map)
+import Data.Map qualified as Map
+import Data.Text.IO qualified as Text
+import Prettyprinter
+import System.Environment (getArgs)
+
+import Booster.Pattern.Base (Term, Variable)
 import Booster.Pattern.Pretty
-import Booster.Prettyprinter (renderDefault)
+import Booster.Prettyprinter (renderDefault, renderText)
 import Booster.Syntax.Json (KoreJson (..))
 import Booster.Syntax.Json.Internalise (
     InternalisedPredicates (..),
@@ -21,12 +33,6 @@ import Booster.Syntax.Json.Internalise (
     pattern DisallowAlias,
  )
 import Booster.Syntax.ParsedKore (internalise, parseKoreDefinition)
-import Control.Monad.Trans.Except
-import Data.Aeson (eitherDecode)
-import Data.ByteString.Lazy qualified as BS
-import Data.Text.IO qualified as Text
-import Prettyprinter
-import System.Environment (getArgs)
 
 main :: IO ()
 main = do
@@ -40,24 +46,37 @@ main = do
         Left err -> putStrLn $ "Error: " ++ err
         Right KoreJson{term} -> do
             case runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing internalDef term of
-                Right (trm, preds, ceils, _subst, _unsupported) -> do
-                    putStrLn "Pretty-printing pattern: "
-                    putStrLn $ renderDefault $ pretty' @'[Decoded] trm
-                    putStrLn "Bool predicates: "
-                    mapM_ (putStrLn . renderDefault . pretty' @'[Decoded]) preds
-                    putStrLn "Ceil predicates: "
-                    mapM_ (putStrLn . renderDefault . pretty' @'[Decoded]) ceils
+                Right (trm, preds, ceils, subst, unsupported) -> do
+                    Text.putStrLn . renderText . vsep $
+                        [ "Pretty-printing pattern:"
+                        , pretty' @'[Decoded, Infix] trm
+                        , renderThings "Bool predicates:" preds
+                        , renderThings "Ceil predicates:" ceils
+                        , hang 2 $ "Substitution:" <> line <> showSubst subst
+                        ]
+                    unless (null unsupported) $ do
+                        putStrLn $ "...as well as " <> show (length unsupported) <> " unsupported parts:"
+                        mapM_ print unsupported
                 Left (NoTermFound _) ->
                     case runExcept $ internalisePredicates DisallowAlias CheckSubsorts Nothing internalDef [term] of
                         Left es -> error (show es)
                         Right ts -> do
-                            putStrLn "Pretty-printing predicates: "
-                            putStrLn "Bool predicates: "
-                            mapM_ (putStrLn . renderDefault . pretty' @'[Decoded]) ts.boolPredicates
-                            putStrLn "Ceil predicates: "
-                            mapM_ (putStrLn . renderDefault . pretty' @'[Decoded]) ts.ceilPredicates
-                            putStrLn "Substitution: "
-                            mapM_ (putStrLn . renderDefault . pretty' @'[Decoded]) ts.substitution
-                            putStrLn "Unsupported predicates: "
-                            mapM_ print ts.unsupported
+                            Text.putStrLn . renderText . vsep $
+                                [ "Pretty-printing predicates:"
+                                , renderThings "Bool predicates:" ts.boolPredicates
+                                , renderThings "Ceil predicates:" ts.ceilPredicates
+                                , hang 2 $ "Substitution:" <> line <> showSubst ts.substitution
+                                ]
+                            unless (null ts.unsupported) $ do
+                                putStrLn $ "...as well as " <> show (length ts.unsupported) <> " unsupported parts:"
+                                mapM_ print ts.unsupported
                 Left err -> error (show err)
+  where
+    showSubst :: Map Variable Term -> Doc ann
+    showSubst m =
+        vsep
+            [pretty' @'[Decoded] v <+> "->" <+> pretty' @'[Decoded, Infix] expr | (v, expr) <- Map.assocs m]
+
+    renderThings :: Pretty (PrettyWithModifiers '[Decoded, Infix] a) => Doc ann -> [a] -> Doc ann
+    renderThings heading [] = heading <> " -"
+    renderThings heading things = hang 2 $ vsep $ heading : map (pretty' @'[Decoded, Infix]) things