Act compiling

src/Act/CLI.hs

@@ -23,7 +23,7 @@ import Data.Map (Map)
 import Data.Maybe
 import qualified Data.Text as Text
 import qualified Data.Text.IO as TIO
-import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import Prettyprinter hiding (annotate, line')
 import GHC.Conc
 import GHC.Natural
 import Options.Generic
@@ -154,7 +154,7 @@ parseSolver s = case s of
                   Just s' -> case Text.unpack s' of
                               "z3" -> pure Solvers.Z3
                               "cvc5" -> pure Solvers.CVC5
-                              input -> render (text $ "unrecognised solver: " <> input) >> exitFailure
+                              input -> render (text $ "unrecognised solver: " <> Text.pack input) >> exitFailure
 
 prove :: FilePath -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
 prove file' solver' smttimeout' debug' = do
@@ -167,27 +167,27 @@ prove file' solver' smttimeout' debug' = do
       catErrors results = [e | e@SMT.Error {} <- results]
       catUnknowns results = [u | u@SMT.Unknown {} <- results]
 
-      (<->) :: Doc -> [Doc] -> Doc
+      (<->) :: DocAnsi -> [DocAnsi] -> DocAnsi
       x <-> y = x <$$> line <> (indent 2 . vsep $ y)
 
-      failMsg :: [SMT.SMTResult] -> Doc
+      failMsg :: [SMT.SMTResult] -> DocAnsi
       failMsg results
         | not . null . catUnknowns $ results
             = text "could not be proven due to a" <+> (yellow . text $ "solver timeout")
         | not . null . catErrors $ results
-            = (red . text $ "failed") <+> "due to solver errors:" <-> ((fmap (text . show)) . catErrors $ results)
+            = (red . text $ "failed") <+> "due to solver errors:" <-> ((fmap viaShow) . catErrors $ results)
         | otherwise
-            = (red . text $ "violated") <> colon <-> (fmap pretty . catModels $ results)
+            = (red . text $ "violated") <> colon <-> (fmap prettyAnsi . catModels $ results)
 
-      passMsg :: Doc
+      passMsg :: DocAnsi
       passMsg = (green . text $ "holds") <+> (bold . text $ "∎")
 
-      accumulateResults :: (Bool, Doc) -> (Query, [SMT.SMTResult]) -> (Bool, Doc)
+      accumulateResults :: (Bool, DocAnsi) -> (Query, [SMT.SMTResult]) -> (Bool, DocAnsi)
       accumulateResults (status, report) (query, results) = (status && holds, report <$$> msg <$$> smt)
         where
           holds = all isPass results
           msg = identifier query <+> if holds then passMsg else failMsg results
-          smt = if debug' then line <> getSMT query else empty
+          smt = if debug' then line <> getSMT query else emptyDoc
 
     solverInstance <- spawnSolver config
     pcResults <- mapM (runQuery solverInstance) (mkPostconditionQueries claims)
@@ -196,10 +196,10 @@ prove file' solver' smttimeout' debug' = do
 
     let
       invTitle = line <> (underline . bold . text $ "Invariants:") <> line
-      invOutput = foldl' accumulateResults (True, empty) invResults
+      invOutput = foldl' accumulateResults (True, emptyDoc) invResults
 
       pcTitle = line <> (underline . bold . text $ "Postconditions:") <> line
-      pcOutput = foldl' accumulateResults (True, empty) pcResults
+      pcOutput = foldl' accumulateResults (True, emptyDoc) pcResults
 
     render $ vsep
       [ ifExists invResults invTitle

src/Act/Consistency.hs

@@ -14,7 +14,7 @@ module Act.Consistency (
 import Prelude hiding (GT, LT)
 
 import Data.List
-import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import Prettyprinter
 import System.Exit (exitFailure)
 import Data.Maybe
 
@@ -83,7 +83,7 @@ mkCaseQuery props behvs@((Behaviour _ _ (Interface ifaceName decls) preconds _ _
         , _minitargs = []
         }
 mkCaseQuery _ [] = error "Internal error: behaviours cannot be empty"
-
+  
 -- | Checks nonoverlapping and exhaustiveness of cases
 checkCases :: Act -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
 checkCases (Act _ contracts) solver' smttimeout debug = do
@@ -109,10 +109,10 @@ checkCases (Act _ contracts) solver' smttimeout debug = do
       checkRes :: String -> (Id, SMT.SMTResult) -> IO ()
       checkRes check (name, res) =
         case res of
-          Sat model -> failMsg ("Cases are not " <> check <> " for behavior " <> name <> ".") (pretty model)
+          Sat model -> failMsg ("Cases are not " <> check <> " for behavior " <> name <> ".") (prettyAnsi model)
           Unsat -> pure ()
           Unknown -> errorMsg $ "Solver timeour. Cannot prove that cases are " <> check <> " for behavior " <> name <> "."
           SMT.Error _ err -> errorMsg $ "Solver error: " <> err <> "\nCannot prove that cases are " <>  check <> " for behavior " <> name <> "."
 
-      failMsg str model = render (red (text str) <> line <> model <> line) >> exitFailure
-      errorMsg str = render (text str <> line) >> exitFailure
+      failMsg str model = render (red (pretty str) <> line <> model <> line) >> exitFailure
+      errorMsg str = render (pretty str <> line) >> exitFailure

src/Act/Print.hs

@@ -6,9 +6,9 @@ module Act.Print where
 
 import Prelude hiding (GT, LT)
 import Data.ByteString.UTF8 (toString)
-import qualified Prettyprinter as PP
-import Prettyprinter.Render.Text (renderIO)
-import qualified Prettyprinter.Render.Terminal as RenderT
+import Prettyprinter hiding (brackets)
+import qualified Prettyprinter.Render.Terminal as Term
+import qualified Data.Text as Text
 
 import System.IO (stdout)
 import Data.Text qualified as T
@@ -231,25 +231,38 @@ prettyInvPred = prettyExp . untime . fst
 
 
 
+-- backwards compatibility with Text.PrettyPrint.ANSI.Leijen
+type DocAnsi = Doc Term.AnsiStyle
 
 -- | prints a Doc, with wider output than the built in `putDoc`
-render :: PP.Doc ann -> IO ()
+render :: DocAnsi -> IO ()
 render doc =
-  let opts = PP.LayoutOptions { PP.layoutPageWidth = PP.AvailablePerLine 120 0.9 } in
-  renderIO stdout (PP.layoutSmart opts doc)
+  let opts = LayoutOptions { layoutPageWidth = AvailablePerLine 120 0.9 } in
+  Term.renderIO stdout (layoutPretty opts doc)
 
+underline :: DocAnsi -> DocAnsi
+underline = annotate Term.underlined
 
--- backwards compatibility with Text.PrettyPrint.ANSI.Leijen
+red :: DocAnsi -> DocAnsi
+red = annotate (Term.color Term.Red)
+
+yellow :: DocAnsi -> DocAnsi
+yellow = annotate (Term.color Term.Yellow)
 
-type Doc = PP.Doc RenderT.AnsiStyle
+green :: DocAnsi -> DocAnsi
+green = annotate (Term.color Term.Green)
 
-underline :: Doc -> Doc
-underline = PP.annotate RenderT.underlined
+bold :: DocAnsi -> DocAnsi
+bold = annotate Term.bold
 
-bold :: Doc -> Doc
-bold = PP.annotate RenderT.bold
+(<$$>) :: Doc ann -> Doc ann -> Doc ann
+(<$$>) = \x y -> vsep [x,y]
 
-(<$$>) = \x y -> PP.vsep [x,y]
+string :: String -> DocAnsi
+string = pretty
 
+text :: Text.Text -> DocAnsi
+text = pretty
 
-
+class PrettyAnsi a where
+  prettyAnsi :: a -> DocAnsi

src/Act/SMT.hs

@@ -98,8 +98,8 @@ data SMTExp = SMTExp
   }
   deriving (Show)
 
-instance Pretty SMTExp where
-  pretty e = vsep [storage, calldata, environment, assertions]
+instance PrettyAnsi SMTExp where
+  prettyAnsi e = vsep [storage, calldata, environment, assertions]
     where
       storage = pretty ";STORAGE:" <$$> (vsep . (fmap pretty) . nubOrd . _storage $ e) <> line
       calldata = pretty ";CALLDATA:" <$$> (vsep . (fmap pretty) . nubOrd . _calldata $ e) <> line
@@ -139,8 +139,8 @@ data Model = Model
   }
   deriving (Show)
 
-instance Pretty Model where
-  pretty (Model prestate poststate (ifaceName, args) environment initargs) =
+instance PrettyAnsi Model where
+  prettyAnsi (Model prestate poststate (ifaceName, args) environment initargs) =
     (underline . pretty $ "counterexample:") <$$> line
       <> (indent 2
         (    calldata'
@@ -335,7 +335,7 @@ runQuery solver query@(Inv (Invariant _ _ _ predicate) (ctor, ctorSMT) behvs) =
 checkSat :: SolverInstance -> (SolverInstance -> IO Model) -> SMTExp -> IO SMTResult
 checkSat solver modelFn smt = do
   -- render (pretty smt)
-  err <- sendLines solver ("(reset)" : (lines . show . pretty $ smt))
+  err <- sendLines solver ("(reset)" : (lines . show . prettyAnsi $ smt))
   case err of
     Nothing -> do
       sat <- sendCommand solver "(check-sat)"
@@ -731,21 +731,21 @@ isFail _ = True
 isPass :: SMTResult -> Bool
 isPass = not . isFail
 
-getBehvName :: Query -> Doc
+getBehvName :: Query -> DocAnsi
 getBehvName (Postcondition (Ctor _) _ _) = (pretty "the") <+> (bold . pretty $ "constructor")
 getBehvName (Postcondition (Behv behv) _ _) = (pretty "behaviour") <+> (bold . pretty $ _name behv)
 getBehvName (Inv {}) = error "Internal Error: invariant queries do not have an associated behaviour"
 
-identifier :: Query -> Doc
+identifier :: Query -> DocAnsi
 identifier q@(Inv (Invariant _ _ _ e) _ _)    = (bold . pretty . prettyInvPred $ e) <+> pretty "of" <+> (bold . pretty . getQueryContract $ q)
 identifier q@Postcondition {} = (bold . pretty . prettyExp . target $ q) <+> pretty "in" <+> getBehvName q <+> pretty "of" <+> (bold . pretty . getQueryContract $ q)
 
-getSMT :: Query -> Doc
-getSMT (Postcondition _ _ smt) = pretty smt
-getSMT (Inv _ (_, csmt) behvs) = pretty "; constructor" <$$> sep' <$$> line <> pretty csmt <$$> vsep (fmap formatBehv behvs)
+getSMT :: Query -> DocAnsi
+getSMT (Postcondition _ _ smt) = prettyAnsi smt
+getSMT (Inv _ (_, csmt) behvs) = pretty "; constructor" <$$> sep' <$$> line <> prettyAnsi csmt <$$> vsep (fmap formatBehv behvs)
   where
-    formatBehv (b, smt) = line <> pretty "; behaviour: " <> (pretty . _name $ b) <$$> sep' <$$> line <> pretty smt
+    formatBehv (b, smt) = line <> pretty "; behaviour: " <> (pretty . _name $ b) <$$> sep' <$$> line <> prettyAnsi smt
     sep' = pretty "; -------------------------------"
 
-ifExists :: Foldable t => t a -> Doc -> Doc
+ifExists :: Foldable t => t a -> DocAnsi -> DocAnsi
 ifExists a b = if null a then emptyDoc else b