Make Pretty prettier

runtimeverification · Oct 15, 2024 · de6ddad · de6ddad
1 parent 4872094
commit de6ddad
Show file tree

Hide file tree

Showing 2 changed files with 44 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,20 @@ 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 (Text)
+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 +34,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 +47,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
+                    mapM_ Text.putStrLn $
+                        ["Pretty-printing pattern:", renderText $ pretty' @'[Decoded] trm]
+                            <> renderThings "Bool predicates:" preds
+                            <> renderThings "Ceil predicates:" ceils
+                            <> ["Substitution:", 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
+                            mapM_ Text.putStrLn $
+                                "Pretty-printing predicates:"
+                                    : renderThings "Bool predicates:" ts.boolPredicates
+                                        <> renderThings "Ceil predicates:" ts.ceilPredicates
+                                        <> ["Substitution:", 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 -> Text
+    showSubst m =
+        renderText $
+            vsep
+                [ pretty' @'[Decoded] v <+> "->" <+> pretty' @'[Decoded] expr
+                | (v, expr) <- Map.assocs m
+                ]
+
+    renderThings :: Pretty (PrettyWithModifiers '[Decoded] a) => Text -> [a] -> [Text]
+    renderThings heading [] = [heading <> " -"]
+    renderThings heading things = heading : map (renderText . pretty' @'[Decoded]) things