From 629717a0902e03de09ed9d8476f1ffdf682ebaf5 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 19 Nov 2020 17:42:16 -0800 Subject: [PATCH 1/5] Switch from ansi-wl-pprint to the prettyprinter package. Fixes #105. --- saw-core/saw-core.cabal | 3 +- saw-core/src/Verifier/SAW/FiniteValue.hs | 4 +- saw-core/src/Verifier/SAW/Module.hs | 1 - saw-core/src/Verifier/SAW/Term/Pretty.hs | 94 +++++++++++++++--------- saw-core/src/Verifier/SAW/Typechecker.hs | 6 +- 5 files changed, 67 insertions(+), 41 deletions(-) diff --git a/saw-core/saw-core.cabal b/saw-core/saw-core.cabal index 1240c04eef..ffd460c1e2 100644 --- a/saw-core/saw-core.cabal +++ b/saw-core/saw-core.cabal @@ -25,7 +25,6 @@ library build-depends: base == 4.*, - ansi-wl-pprint, array, bytestring, containers, @@ -41,6 +40,8 @@ library panic, parameterized-utils, pretty, + prettyprinter >= 1.7.0, + prettyprinter-ansi-terminal >= 1.1.2, random, rme, template-haskell, diff --git a/saw-core/src/Verifier/SAW/FiniteValue.hs b/saw-core/src/Verifier/SAW/FiniteValue.hs index 292f906938..8a29ad55ce 100644 --- a/saw-core/src/Verifier/SAW/FiniteValue.hs +++ b/saw-core/src/Verifier/SAW/FiniteValue.hs @@ -20,13 +20,13 @@ import Data.Map (Map) import qualified Data.Map as Map import Numeric.Natural (Natural) +import Prettyprinter hiding (Doc) + import qualified Verifier.SAW.Recognizer as R import Verifier.SAW.SharedTerm import Verifier.SAW.TypedAST import Verifier.SAW.Term.Pretty -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) - -- | Finite types that can be encoded as bits for a SAT/SMT solver. data FiniteType = FTBit diff --git a/saw-core/src/Verifier/SAW/Module.hs b/saw-core/src/Verifier/SAW/Module.hs index ec15cadaa7..a5697e1c37 100644 --- a/saw-core/src/Verifier/SAW/Module.hs +++ b/saw-core/src/Verifier/SAW/Module.hs @@ -81,7 +81,6 @@ import qualified Data.Map.Strict as Map import Data.HashMap.Strict (HashMap) import qualified Data.HashMap.Strict as HMap import GHC.Generics (Generic) -import Text.PrettyPrint.ANSI.Leijen (Doc) import qualified Language.Haskell.TH.Syntax as TH diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index 08fbd0d7b2..ecfce0d353 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -15,7 +15,8 @@ Portability : non-portable (language extensions) -} module Verifier.SAW.Term.Pretty - ( PPOpts(..) + ( Doc + , PPOpts(..) , defaultPPOpts , depthPPOpts , ppNat @@ -30,6 +31,7 @@ module Verifier.SAW.Term.Pretty , OccurrenceMap , shouldMemoizeTerm , ppName + , text, char, integer ) where import Data.Maybe (isJust) @@ -40,10 +42,12 @@ import Data.Foldable (Foldable) #endif import qualified Data.Foldable as Fold import qualified Data.Text as Text +import qualified Data.Text.Lazy as Text.Lazy import qualified Data.Vector as V import Numeric (showIntAtBase) -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) -import qualified Text.PrettyPrint.ANSI.Leijen as PPL ((<$>)) +import Prettyprinter hiding (Doc) +import qualified Prettyprinter (Doc) +import Prettyprinter.Render.Terminal import Text.URI import Data.IntMap.Strict (IntMap) @@ -51,6 +55,7 @@ import qualified Data.IntMap.Strict as IntMap import Verifier.SAW.Term.Functor +type Doc = Prettyprinter.Doc AnsiStyle -------------------------------------------------------------------------------- -- * Pretty-Printing Options and Precedences @@ -199,12 +204,12 @@ instance MonadReader PPState PPM where ask = PPM ask local f (PPM m) = PPM $ local f m --- | Color a document, using the supplied function (1st argument), if the +-- | Color a document, using the supplied style (1st argument), if the -- 'ppColor' option is set -maybeColorM :: (Doc -> Doc) -> Doc -> PPM Doc -maybeColorM f d = +maybeColorM :: AnsiStyle -> Doc -> PPM Doc +maybeColorM style d = (ppColor <$> ppOpts <$> ask) >>= \b -> - return ((if b then f else id) d) + return ((if b then annotate style else id) d) -- | Look up the given local variable by deBruijn index to get its name varLookupM :: DeBruijnIndex -> PPM String @@ -266,8 +271,20 @@ withMemoVar global_p idx f = -- * The Pretty-Printing of Specific Constructs -------------------------------------------------------------------------------- +text :: String -> Doc +text = pretty + +char :: Char -> Doc +char = pretty + +integer :: Integer -> Doc +integer = pretty + +int :: Int -> Doc +int = pretty + (<<$>>) :: Doc -> Doc -> Doc -x <<$>> y = (PPL.<$>) x y +x <<$>> y = vsep [x, y] -- | Pretty-print an identifier ppIdent :: Ident -> Doc @@ -276,13 +293,13 @@ ppIdent i = text (show i) -- | Pretty-print an integer in the correct base ppNat :: PPOpts -> Integer -> Doc ppNat (PPOpts{..}) i - | ppBase > 36 = integer i + | ppBase > 36 = pretty i | otherwise = prefix <> text value where prefix = case ppBase of 2 -> text "0b" 8 -> text "0o" - 10 -> empty + 10 -> mempty 16 -> text "0x" _ -> text "0" <> char '<' <> int ppBase <> char '>' @@ -291,7 +308,7 @@ ppNat (PPOpts{..}) i -- | Pretty-print a memoization variable ppMemoVar :: MemoVar -> Doc -ppMemoVar mv = text "x@" <> integer (toInteger mv) +ppMemoVar mv = text "x@" <> pretty (toInteger mv) -- | Pretty-print a type constraint (also known as an ascription) @x : tp@ ppTypeConstraint :: Doc -> Doc -> Doc @@ -304,18 +321,20 @@ ppAppList _ f [] = f ppAppList p f args = ppParensPrec p PrecApp $ group $ hang 2 $ vsep (f : args) -- | Pretty-print "let x1 = t1 ... xn = tn in body" -ppLetBlock :: [(MemoVar,Doc)] -> Doc -> Doc +ppLetBlock :: [(MemoVar, Doc)] -> Doc -> Doc ppLetBlock defs body = - text "let" <+> lbrace <+> align (vcat (map ppEqn defs)) <$$> - indent 4 rbrace <$$> - text " in" <+> body + vcat + [ text "let" <+> lbrace <+> align (vcat (map ppEqn defs)) + , indent 4 rbrace + , text " in" <+> body + ] where ppEqn (var,d) = ppMemoVar var <+> char '=' <+> d -- | Pretty-print pairs as "(x, y)" ppPair :: Prec -> Doc -> Doc -> Doc -ppPair prec x y = ppParensPrec prec PrecNone (group (x <> char ',' <$$> y)) +ppPair prec x y = ppParensPrec prec PrecNone (group (vcat [x <> char ',', y])) -- | Pretty-print pair types as "x * y" ppPairType :: Prec -> Doc -> Doc -> Doc @@ -328,7 +347,7 @@ ppPairType prec x y = ppParensPrec prec PrecProd (x <+> char '*' <+> y) -- -- * @{ fld1 op val1, ..., fldn op valn }@ otherwise, where @op@ is @::@ for -- types and @=@ for values. -ppRecord :: Bool -> [(String,Doc)] -> Doc +ppRecord :: Bool -> [(String, Doc)] -> Doc ppRecord type_p alist = (if type_p then (char '#' <>) else id) $ encloseSep lbrace rbrace comma $ map ppField alist @@ -349,8 +368,7 @@ ppArrayValue = list ppLambda :: Doc -> (String, Doc) -> Doc ppLambda tp (name, body) = group $ hang 2 $ - text "\\" <> parens (ppTypeConstraint (text name) tp) - <+> text "->" PPL.<$> body + vsep [text "\\" <> parens (ppTypeConstraint (text name) tp) <+> text "->", body] -- | Pretty-print a pi abstraction as @(x :: tp) -> body@, or as @tp -> body@ if -- @x == "_"@ @@ -369,16 +387,18 @@ ppDef d tp (Just body) = ppTypeConstraint d tp <+> equals <+> body -- > c1 (x1_1:tp1_1) .. (x1_N:tp1_N) : tp1 -- > ... -- > } -ppDataType :: Ident -> (Doc, ((Doc,Doc), [Doc])) -> Doc +ppDataType :: Ident -> (Doc, ((Doc, Doc), [Doc])) -> Doc ppDataType d (params, ((d_ctx,d_tp), ctors)) = - group $ (group - ((text "data" <+> ppIdent d <+> params <+> text ":" <+> - (d_ctx <+> text "->" <+> d_tp)) - <<$>> (text "where" <+> lbrace))) - <<$>> - vcat (map (<> semi) ctors) - <$$> - rbrace + group $ + vcat + [ (group + ((text "data" <+> ppIdent d <+> params <+> text ":" <+> + (d_ctx <+> text "->" <+> d_tp)) + <<$>> (text "where" <+> lbrace))) + <<$>> + vcat (map (<> semi) ctors) + , rbrace + ] -------------------------------------------------------------------------------- @@ -424,7 +444,7 @@ ppFlatTermF prec tf = ArrayValue _ args -> ppArrayValue <$> mapM (ppTerm' PrecNone) (V.toList args) StringLit s -> return $ text (show s) - ExtCns cns -> maybeColorM dullred $ ppName (ecName cns) + ExtCns cns -> maybeColorM (colorDull Red) $ ppName (ecName cns) ppName :: NameInfo -> Doc ppName (ModuleIdentifier i) = ppIdent i @@ -442,8 +462,8 @@ ppTermF prec (Pi x tp body) = ppParensPrec prec PrecLambda <$> (ppPi <$> ppTerm' PrecApp tp <*> ppTermInBinder PrecLambda x body) -ppTermF _ (LocalVar x) = (text <$> varLookupM x) >>= maybeColorM dullgreen -ppTermF _ (Constant ec _) = maybeColorM dullblue $ ppName (ecName ec) +ppTermF _ (LocalVar x) = (text <$> varLookupM x) >>= maybeColorM (colorDull Green) +ppTermF _ (Constant ec _) = maybeColorM (colorDull Blue) $ ppName (ecName ec) -- | Internal function to recursively pretty-print a term @@ -535,7 +555,7 @@ ppTermWithMemoTable prec global_p trm = ppLets occ_map_elems [] where -- Term and then add it to the memoization table of subsequent printing. The -- pretty-printing of these terms is reverse-accumulated in the second -- list. Finally, print trm with a let-binding for the bound terms. - ppLets :: [(TermIndex, (Term, Int))] -> [(MemoVar,Doc)] -> PPM Doc + ppLets :: [(TermIndex, (Term, Int))] -> [(MemoVar, Doc)] -> PPM Doc -- Special case: don't print let-binding if there are no bound vars ppLets [] [] = ppTerm' prec trm @@ -571,7 +591,7 @@ ppTermInBinder prec basename trm = -- tables for the inner computation; the justification is that this function is -- only used for printing datatypes, which we assume are not very big. ppWithBoundCtx :: [(String, Term)] -> PPM a -> PPM (Doc, a) -ppWithBoundCtx [] m = (empty ,) <$> m +ppWithBoundCtx [] m = (mempty ,) <$> m ppWithBoundCtx ((x,tp):ctx) m = (\tp_d (x', (ctx_d, ret)) -> (parens (ppTypeConstraint (text x') tp_d) <+> ctx_d, ret)) @@ -586,16 +606,20 @@ ppTerm opts trm = runPPM opts $ ppTermWithMemoTable PrecNone True trm ppTermDepth :: Int -> Term -> Doc ppTermDepth depth t = ppTerm (depthPPOpts depth) t +renderDoc :: Doc -> String +renderDoc doc = Text.Lazy.unpack (renderLazy (layoutPretty opts doc)) + where opts = LayoutOptions (AvailablePerLine 80 0.8) + -- | Pretty-print a term and render it to a string, using the given options scPrettyTerm :: PPOpts -> Term -> String scPrettyTerm opts t = - flip displayS "" $ renderPretty 0.8 80 $ ppTerm opts t + renderDoc $ ppTerm opts t -- | Like 'scPrettyTerm', but also supply a context of bound names, where the -- most recently-bound variable is listed first in the context scPrettyTermInCtx :: PPOpts -> [String] -> Term -> String scPrettyTermInCtx opts ctx trm = - flip displayS "" $ renderPretty 0.8 80 $ runPPM opts $ + renderDoc $ runPPM opts $ flip (Fold.foldl' (\m x -> snd <$> withBoundVarM x m)) ctx $ ppTermWithMemoTable PrecNone False trm diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs index 30ad203d4f..a2fb7151ac 100644 --- a/saw-core/src/Verifier/SAW/Typechecker.hs +++ b/saw-core/src/Verifier/SAW/Typechecker.hs @@ -36,7 +36,8 @@ import Control.Applicative import Control.Monad.State import Data.List (findIndex) import qualified Data.Vector as V -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) + +import Prettyprinter hiding (Doc) import Verifier.SAW.Utils (internalError) @@ -44,6 +45,7 @@ import Verifier.SAW.Module import Verifier.SAW.Position import Verifier.SAW.Term.Functor import Verifier.SAW.Term.CtxTerm +import Verifier.SAW.Term.Pretty (Doc, text) import Verifier.SAW.SharedTerm import Verifier.SAW.Recognizer import Verifier.SAW.SCTypeCheck @@ -64,7 +66,7 @@ inferCompleteTermCtx :: SharedContext -> Maybe ModuleName -> [(String,Term)] -> inferCompleteTermCtx sc mnm ctx t = do res <- runTCM (typeInferComplete t) sc mnm ctx case res of - Left err -> return $ Left $ vsep $ map string $ prettyTCError err + Left err -> return $ Left $ vsep $ map text $ prettyTCError err Right t' -> return $ Right $ typedVal t' -- | Look up the current module name, raising an error if it is not set From a581a5b7018d4092b3d5993f3596c17b7a4433b6 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sun, 22 Nov 2020 06:12:06 -0800 Subject: [PATCH 2/5] Use custom document style type for semantic prettyprinter annotations. --- saw-core/src/Verifier/SAW/Term/Pretty.hs | 61 ++++++++++++++++-------- 1 file changed, 41 insertions(+), 20 deletions(-) diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index ecfce0d353..b7bd3e2466 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -1,6 +1,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} @@ -55,7 +56,33 @@ import qualified Data.IntMap.Strict as IntMap import Verifier.SAW.Term.Functor -type Doc = Prettyprinter.Doc AnsiStyle +-------------------------------------------------------------------------------- +-- * Doc annotations + +data SawStyle + = GlobalDefStyle + | ConstantStyle + | ExtCnsStyle + | LocalVarStyle + | DataTypeStyle + | CtorAppStyle + | RecursorStyle + | FieldNameStyle + +-- TODO: assign colors for more styles +colorStyle :: SawStyle -> AnsiStyle +colorStyle = + \case + GlobalDefStyle -> mempty + ConstantStyle -> colorDull Blue + ExtCnsStyle -> colorDull Red + LocalVarStyle -> colorDull Green + DataTypeStyle -> mempty + CtorAppStyle -> mempty + RecursorStyle -> mempty + FieldNameStyle -> mempty + +type Doc = Prettyprinter.Doc SawStyle -------------------------------------------------------------------------------- -- * Pretty-Printing Options and Precedences @@ -204,13 +231,6 @@ instance MonadReader PPState PPM where ask = PPM ask local f (PPM m) = PPM $ local f m --- | Color a document, using the supplied style (1st argument), if the --- 'ppColor' option is set -maybeColorM :: AnsiStyle -> Doc -> PPM Doc -maybeColorM style d = - (ppColor <$> ppOpts <$> ask) >>= \b -> - return ((if b then annotate style else id) d) - -- | Look up the given local variable by deBruijn index to get its name varLookupM :: DeBruijnIndex -> PPM String varLookupM idx = @@ -313,7 +333,7 @@ ppMemoVar mv = text "x@" <> pretty (toInteger mv) -- | Pretty-print a type constraint (also known as an ascription) @x : tp@ ppTypeConstraint :: Doc -> Doc -> Doc ppTypeConstraint x tp = - hang 2 $ group (x <<$>> text ":" <+> tp) + hang 2 $ group $ vsep [annotate LocalVarStyle x, text ":" <+> tp] -- | Pretty-print an application to 0 or more arguments at the given precedence ppAppList :: Prec -> Doc -> [Doc] -> Doc @@ -409,7 +429,7 @@ ppDataType d (params, ((d_ctx,d_tp), ctors)) = ppFlatTermF :: Prec -> FlatTermF Term -> PPM Doc ppFlatTermF prec tf = case tf of - GlobalDef i -> return $ ppIdent i + GlobalDef i -> return $ annotate GlobalDefStyle $ ppIdent i UnitValue -> return $ text "(-empty-)" UnitType -> return $ text "#(-empty-)" PairValue x y -> ppPair prec <$> ppTerm' PrecLambda x <*> ppTerm' PrecNone y @@ -418,9 +438,9 @@ ppFlatTermF prec tf = PairRight t -> ppProj "2" <$> ppTerm' PrecArg t CtorApp c params args -> - ppAppList prec (ppIdent c) <$> mapM (ppTerm' PrecArg) (params ++ args) + ppAppList prec (annotate CtorAppStyle (ppIdent c)) <$> mapM (ppTerm' PrecArg) (params ++ args) DataTypeApp dt params args -> - ppAppList prec (ppIdent dt) <$> mapM (ppTerm' PrecArg) (params ++ args) + ppAppList prec (annotate DataTypeStyle (ppIdent dt)) <$> mapM (ppTerm' PrecArg) (params ++ args) RecursorApp d params p_ret cs_fs ixs arg -> do params_pp <- mapM (ppTerm' PrecArg) params p_ret_pp <- ppTerm' PrecArg p_ret @@ -428,7 +448,7 @@ ppFlatTermF prec tf = ixs_pp <- mapM (ppTerm' PrecArg) ixs arg_pp <- ppTerm' PrecArg arg return $ - ppAppList prec (ppIdent d <> text "#rec") + ppAppList prec (annotate RecursorStyle (ppIdent d <> text "#rec")) (params_pp ++ [p_ret_pp] ++ [tupled $ zipWith (\(c,_) f_pp -> ppIdent c <<$>> text "=>" <<$>> f_pp) @@ -444,7 +464,7 @@ ppFlatTermF prec tf = ArrayValue _ args -> ppArrayValue <$> mapM (ppTerm' PrecNone) (V.toList args) StringLit s -> return $ text (show s) - ExtCns cns -> maybeColorM (colorDull Red) $ ppName (ecName cns) + ExtCns cns -> pure $ annotate ExtCnsStyle $ ppName (ecName cns) ppName :: NameInfo -> Doc ppName (ModuleIdentifier i) = ppIdent i @@ -462,8 +482,8 @@ ppTermF prec (Pi x tp body) = ppParensPrec prec PrecLambda <$> (ppPi <$> ppTerm' PrecApp tp <*> ppTermInBinder PrecLambda x body) -ppTermF _ (LocalVar x) = (text <$> varLookupM x) >>= maybeColorM (colorDull Green) -ppTermF _ (Constant ec _) = maybeColorM (colorDull Blue) $ ppName (ecName ec) +ppTermF _ (LocalVar x) = annotate LocalVarStyle <$> text <$> varLookupM x +ppTermF _ (Constant ec _) = pure $ annotate ConstantStyle $ ppName (ecName ec) -- | Internal function to recursively pretty-print a term @@ -606,20 +626,21 @@ ppTerm opts trm = runPPM opts $ ppTermWithMemoTable PrecNone True trm ppTermDepth :: Int -> Term -> Doc ppTermDepth depth t = ppTerm (depthPPOpts depth) t -renderDoc :: Doc -> String -renderDoc doc = Text.Lazy.unpack (renderLazy (layoutPretty opts doc)) +renderDoc :: (SawStyle -> AnsiStyle) -> Doc -> String +renderDoc style doc = Text.Lazy.unpack (renderLazy (reAnnotateS style (layoutPretty opts doc))) where opts = LayoutOptions (AvailablePerLine 80 0.8) -- | Pretty-print a term and render it to a string, using the given options scPrettyTerm :: PPOpts -> Term -> String scPrettyTerm opts t = - renderDoc $ ppTerm opts t + renderDoc (if ppColor opts then colorStyle else const mempty) $ ppTerm opts t -- | Like 'scPrettyTerm', but also supply a context of bound names, where the -- most recently-bound variable is listed first in the context scPrettyTermInCtx :: PPOpts -> [String] -> Term -> String scPrettyTermInCtx opts ctx trm = - renderDoc $ runPPM opts $ + renderDoc (if ppColor opts then colorStyle else const mempty) $ + runPPM opts $ flip (Fold.foldl' (\m x -> snd <$> withBoundVarM x m)) ctx $ ppTermWithMemoTable PrecNone False trm From 784fb0cdd8d05f99a97f0ba2baf3d717328a0efc Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sun, 22 Nov 2020 06:12:24 -0800 Subject: [PATCH 3/5] Remove mentions of `ansi-wl-pprint` from cabal files. --- saw-core-what4/saw-core-what4.cabal | 1 - saw-core/saw-core.cabal | 1 - 2 files changed, 2 deletions(-) diff --git a/saw-core-what4/saw-core-what4.cabal b/saw-core-what4/saw-core-what4.cabal index 69a30330af..717ee17f65 100644 --- a/saw-core-what4/saw-core-what4.cabal +++ b/saw-core-what4/saw-core-what4.cabal @@ -15,7 +15,6 @@ Description: library build-depends: - ansi-wl-pprint, base == 4.*, bv-sized >= 1.0.0, containers, diff --git a/saw-core/saw-core.cabal b/saw-core/saw-core.cabal index ffd460c1e2..e1384c9010 100644 --- a/saw-core/saw-core.cabal +++ b/saw-core/saw-core.cabal @@ -119,7 +119,6 @@ test-suite test-sawcore , time , unordered-containers , vector - , ansi-wl-pprint , QuickCheck >= 2.7 , tasty , tasty-ant-xml >= 1.1.0 From a1c42e06100d7009abe08237e90a7395b2198889 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sun, 22 Nov 2020 07:03:41 -0800 Subject: [PATCH 4/5] Rename `Doc` type synonym to `SawDoc`. type SawDoc = Doc SawStyle This lets later packages import `Verifier.SAW.Term.Pretty` without conflicting with the `Prettyprinter` module. --- saw-core/src/Verifier/SAW/FiniteValue.hs | 4 +- saw-core/src/Verifier/SAW/Module.hs | 2 +- saw-core/src/Verifier/SAW/Term/Pretty.hs | 79 ++++++++++++------------ saw-core/src/Verifier/SAW/Typechecker.hs | 6 +- 4 files changed, 45 insertions(+), 46 deletions(-) diff --git a/saw-core/src/Verifier/SAW/FiniteValue.hs b/saw-core/src/Verifier/SAW/FiniteValue.hs index 8a29ad55ce..17f7271efd 100644 --- a/saw-core/src/Verifier/SAW/FiniteValue.hs +++ b/saw-core/src/Verifier/SAW/FiniteValue.hs @@ -102,10 +102,10 @@ instance Show FirstOrderValue where commaSep ss = foldr (.) id (intersperse (showString ",") ss) showField (field, v) = showString field . showString " = " . shows v -ppFiniteValue :: PPOpts -> FiniteValue -> Doc +ppFiniteValue :: PPOpts -> FiniteValue -> SawDoc ppFiniteValue opts fv = ppFirstOrderValue opts (toFirstOrderValue fv) -ppFirstOrderValue :: PPOpts -> FirstOrderValue -> Doc +ppFirstOrderValue :: PPOpts -> FirstOrderValue -> SawDoc ppFirstOrderValue opts = loop where loop fv = case fv of diff --git a/saw-core/src/Verifier/SAW/Module.hs b/saw-core/src/Verifier/SAW/Module.hs index a5697e1c37..982308ba48 100644 --- a/saw-core/src/Verifier/SAW/Module.hs +++ b/saw-core/src/Verifier/SAW/Module.hs @@ -467,7 +467,7 @@ allModuleCtors modmap = concatMap moduleCtors (HMap.elems modmap) -- | Pretty-print a 'Module' -ppModule :: PPOpts -> Module -> Doc +ppModule :: PPOpts -> Module -> SawDoc ppModule opts m = ppPPModule opts (PPModule (moduleImportNames m) (map toDecl $ moduleDecls m)) where diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index b7bd3e2466..9c5fa0b490 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -16,7 +16,7 @@ Portability : non-portable (language extensions) -} module Verifier.SAW.Term.Pretty - ( Doc + ( SawDoc , PPOpts(..) , defaultPPOpts , depthPPOpts @@ -46,8 +46,7 @@ import qualified Data.Text as Text import qualified Data.Text.Lazy as Text.Lazy import qualified Data.Vector as V import Numeric (showIntAtBase) -import Prettyprinter hiding (Doc) -import qualified Prettyprinter (Doc) +import Prettyprinter import Prettyprinter.Render.Terminal import Text.URI @@ -82,7 +81,7 @@ colorStyle = RecursorStyle -> mempty FieldNameStyle -> mempty -type Doc = Prettyprinter.Doc SawStyle +type SawDoc = Doc SawStyle -------------------------------------------------------------------------------- -- * Pretty-Printing Options and Precedences @@ -143,7 +142,7 @@ precContains PrecNone PrecNone = True -- 'PrecArg', meaning we are pretty-printing the argument of an application, and -- @p2@ is 'PrecLambda', meaning the construct we are pretty-printing is a -- lambda or pi abstraction) then add parentheses. -ppParensPrec :: Prec -> Prec -> Doc -> Doc +ppParensPrec :: Prec -> Prec -> SawDoc -> SawDoc ppParensPrec p1 p2 d | precContains p1 p2 = d | otherwise = parens $ align d @@ -291,27 +290,27 @@ withMemoVar global_p idx f = -- * The Pretty-Printing of Specific Constructs -------------------------------------------------------------------------------- -text :: String -> Doc +text :: String -> SawDoc text = pretty -char :: Char -> Doc +char :: Char -> SawDoc char = pretty -integer :: Integer -> Doc +integer :: Integer -> SawDoc integer = pretty -int :: Int -> Doc +int :: Int -> SawDoc int = pretty -(<<$>>) :: Doc -> Doc -> Doc +(<<$>>) :: SawDoc -> SawDoc -> SawDoc x <<$>> y = vsep [x, y] -- | Pretty-print an identifier -ppIdent :: Ident -> Doc +ppIdent :: Ident -> SawDoc ppIdent i = text (show i) -- | Pretty-print an integer in the correct base -ppNat :: PPOpts -> Integer -> Doc +ppNat :: PPOpts -> Integer -> SawDoc ppNat (PPOpts{..}) i | ppBase > 36 = pretty i | otherwise = prefix <> text value @@ -327,21 +326,21 @@ ppNat (PPOpts{..}) i digits = "0123456789abcdefghijklmnopqrstuvwxyz" -- | Pretty-print a memoization variable -ppMemoVar :: MemoVar -> Doc +ppMemoVar :: MemoVar -> SawDoc ppMemoVar mv = text "x@" <> pretty (toInteger mv) -- | Pretty-print a type constraint (also known as an ascription) @x : tp@ -ppTypeConstraint :: Doc -> Doc -> Doc +ppTypeConstraint :: SawDoc -> SawDoc -> SawDoc ppTypeConstraint x tp = hang 2 $ group $ vsep [annotate LocalVarStyle x, text ":" <+> tp] -- | Pretty-print an application to 0 or more arguments at the given precedence -ppAppList :: Prec -> Doc -> [Doc] -> Doc +ppAppList :: Prec -> SawDoc -> [SawDoc] -> SawDoc ppAppList _ f [] = f ppAppList p f args = ppParensPrec p PrecApp $ group $ hang 2 $ vsep (f : args) -- | Pretty-print "let x1 = t1 ... xn = tn in body" -ppLetBlock :: [(MemoVar, Doc)] -> Doc -> Doc +ppLetBlock :: [(MemoVar, SawDoc)] -> SawDoc -> SawDoc ppLetBlock defs body = vcat [ text "let" <+> lbrace <+> align (vcat (map ppEqn defs)) @@ -353,11 +352,11 @@ ppLetBlock defs body = -- | Pretty-print pairs as "(x, y)" -ppPair :: Prec -> Doc -> Doc -> Doc +ppPair :: Prec -> SawDoc -> SawDoc -> SawDoc ppPair prec x y = ppParensPrec prec PrecNone (group (vcat [x <> char ',', y])) -- | Pretty-print pair types as "x * y" -ppPairType :: Prec -> Doc -> Doc -> Doc +ppPairType :: Prec -> SawDoc -> SawDoc -> SawDoc ppPairType prec x y = ppParensPrec prec PrecProd (x <+> char '*' <+> y) -- | Pretty-print records (if the flag is 'False') or record types (if the flag @@ -367,7 +366,7 @@ ppPairType prec x y = ppParensPrec prec PrecProd (x <+> char '*' <+> y) -- -- * @{ fld1 op val1, ..., fldn op valn }@ otherwise, where @op@ is @::@ for -- types and @=@ for values. -ppRecord :: Bool -> [(String, Doc)] -> Doc +ppRecord :: Bool -> [(String, SawDoc)] -> SawDoc ppRecord type_p alist = (if type_p then (char '#' <>) else id) $ encloseSep lbrace rbrace comma $ map ppField alist @@ -376,29 +375,29 @@ ppRecord type_p alist = op_str = if type_p then ":" else "=" -- | Pretty-print a projection / selector "x.f" -ppProj :: String -> Doc -> Doc +ppProj :: String -> SawDoc -> SawDoc ppProj sel doc = doc <> char '.' <> text sel -- | Pretty-print an array value @[v1, ..., vn]@ -ppArrayValue :: [Doc] -> Doc +ppArrayValue :: [SawDoc] -> SawDoc ppArrayValue = list -- | Pretty-print a lambda abstraction as @\(x :: tp) -> body@, where the -- variable name to use for @x@ is bundled with @body@ -ppLambda :: Doc -> (String, Doc) -> Doc +ppLambda :: SawDoc -> (String, SawDoc) -> SawDoc ppLambda tp (name, body) = group $ hang 2 $ vsep [text "\\" <> parens (ppTypeConstraint (text name) tp) <+> text "->", body] -- | Pretty-print a pi abstraction as @(x :: tp) -> body@, or as @tp -> body@ if -- @x == "_"@ -ppPi :: Doc -> (String, Doc) -> Doc +ppPi :: SawDoc -> (String, SawDoc) -> SawDoc ppPi tp (name, body) = lhs <<$>> text "->" <+> body where lhs = if name == "_" then tp else parens (ppTypeConstraint (text name) tp) -- | Pretty-print a definition @d :: tp = body@ -ppDef :: Doc -> Doc -> Maybe Doc -> Doc +ppDef :: SawDoc -> SawDoc -> Maybe SawDoc -> SawDoc ppDef d tp Nothing = ppTypeConstraint d tp ppDef d tp (Just body) = ppTypeConstraint d tp <+> equals <+> body @@ -407,7 +406,7 @@ ppDef d tp (Just body) = ppTypeConstraint d tp <+> equals <+> body -- > c1 (x1_1:tp1_1) .. (x1_N:tp1_N) : tp1 -- > ... -- > } -ppDataType :: Ident -> (Doc, ((Doc, Doc), [Doc])) -> Doc +ppDataType :: Ident -> (SawDoc, ((SawDoc, SawDoc), [SawDoc])) -> SawDoc ppDataType d (params, ((d_ctx,d_tp), ctors)) = group $ vcat @@ -426,7 +425,7 @@ ppDataType d (params, ((d_ctx,d_tp), ctors)) = -------------------------------------------------------------------------------- -- | Pretty-print a built-in atomic construct -ppFlatTermF :: Prec -> FlatTermF Term -> PPM Doc +ppFlatTermF :: Prec -> FlatTermF Term -> PPM SawDoc ppFlatTermF prec tf = case tf of GlobalDef i -> return $ annotate GlobalDefStyle $ ppIdent i @@ -466,12 +465,12 @@ ppFlatTermF prec tf = StringLit s -> return $ text (show s) ExtCns cns -> pure $ annotate ExtCnsStyle $ ppName (ecName cns) -ppName :: NameInfo -> Doc +ppName :: NameInfo -> SawDoc ppName (ModuleIdentifier i) = ppIdent i ppName (ImportedName absName _) = text (Text.unpack (render absName)) -- | Pretty-print a non-shared term -ppTermF :: Prec -> TermF Term -> PPM Doc +ppTermF :: Prec -> TermF Term -> PPM SawDoc ppTermF prec (FTermF ftf) = ppFlatTermF prec ftf ppTermF prec (App e1 e2) = ppAppList prec <$> ppTerm' PrecApp e1 <*> mapM (ppTerm' PrecArg) [e2] @@ -487,7 +486,7 @@ ppTermF _ (Constant ec _) = pure $ annotate ConstantStyle $ ppName (ecName ec) -- | Internal function to recursively pretty-print a term -ppTerm' :: Prec -> Term -> PPM Doc +ppTerm' :: Prec -> Term -> PPM SawDoc ppTerm' prec = atNextDepthM (text "...") . ppTerm'' where ppTerm'' (Unshared tf) = ppTermF prec tf ppTerm'' (STApp {stAppIndex = idx, stAppTermF = tf}) = @@ -557,7 +556,7 @@ shouldMemoizeTerm t = -- table to memoize the printing. Also print the table itself as a sequence of -- let-bindings for the entries in the memoization table. If the flag is true, -- compute a global table, otherwise compute a local table. -ppTermWithMemoTable :: Prec -> Bool -> Term -> PPM Doc +ppTermWithMemoTable :: Prec -> Bool -> Term -> PPM SawDoc ppTermWithMemoTable prec global_p trm = ppLets occ_map_elems [] where -- Generate an occurrence map for trm, filtering out terms that only occur @@ -575,7 +574,7 @@ ppTermWithMemoTable prec global_p trm = ppLets occ_map_elems [] where -- Term and then add it to the memoization table of subsequent printing. The -- pretty-printing of these terms is reverse-accumulated in the second -- list. Finally, print trm with a let-binding for the bound terms. - ppLets :: [(TermIndex, (Term, Int))] -> [(MemoVar, Doc)] -> PPM Doc + ppLets :: [(TermIndex, (Term, Int))] -> [(MemoVar, SawDoc)] -> PPM SawDoc -- Special case: don't print let-binding if there are no bound vars ppLets [] [] = ppTerm' prec trm @@ -599,7 +598,7 @@ ppTermWithMemoTable prec global_p trm = ppLets occ_map_elems [] where -- -- Also, pretty-print let-bindings around the term for all subterms that occur -- more than once at the same binding level. -ppTermInBinder :: Prec -> String -> Term -> PPM (String, Doc) +ppTermInBinder :: Prec -> String -> Term -> PPM (String, SawDoc) ppTermInBinder prec basename trm = let nm = if basename == "_" && inBitSet 0 (looseVars trm) then "_x" else basename in @@ -610,7 +609,7 @@ ppTermInBinder prec basename trm = -- pretty-printing of the context. Note: we do not use any local memoization -- tables for the inner computation; the justification is that this function is -- only used for printing datatypes, which we assume are not very big. -ppWithBoundCtx :: [(String, Term)] -> PPM a -> PPM (Doc, a) +ppWithBoundCtx :: [(String, Term)] -> PPM a -> PPM (SawDoc, a) ppWithBoundCtx [] m = (mempty ,) <$> m ppWithBoundCtx ((x,tp):ctx) m = (\tp_d (x', (ctx_d, ret)) -> @@ -619,27 +618,27 @@ ppWithBoundCtx ((x,tp):ctx) m = -- | Pretty-print a term, also adding let-bindings for all subterms that occur -- more than once at the same binding level -ppTerm :: PPOpts -> Term -> Doc +ppTerm :: PPOpts -> Term -> SawDoc ppTerm opts trm = runPPM opts $ ppTermWithMemoTable PrecNone True trm -- | Pretty-print a term, but only to a maximum depth -ppTermDepth :: Int -> Term -> Doc +ppTermDepth :: Int -> Term -> SawDoc ppTermDepth depth t = ppTerm (depthPPOpts depth) t -renderDoc :: (SawStyle -> AnsiStyle) -> Doc -> String -renderDoc style doc = Text.Lazy.unpack (renderLazy (reAnnotateS style (layoutPretty opts doc))) +renderSawDoc :: (SawStyle -> AnsiStyle) -> SawDoc -> String +renderSawDoc style doc = Text.Lazy.unpack (renderLazy (reAnnotateS style (layoutPretty opts doc))) where opts = LayoutOptions (AvailablePerLine 80 0.8) -- | Pretty-print a term and render it to a string, using the given options scPrettyTerm :: PPOpts -> Term -> String scPrettyTerm opts t = - renderDoc (if ppColor opts then colorStyle else const mempty) $ ppTerm opts t + renderSawDoc (if ppColor opts then colorStyle else const mempty) $ ppTerm opts t -- | Like 'scPrettyTerm', but also supply a context of bound names, where the -- most recently-bound variable is listed first in the context scPrettyTermInCtx :: PPOpts -> [String] -> Term -> String scPrettyTermInCtx opts ctx trm = - renderDoc (if ppColor opts then colorStyle else const mempty) $ + renderSawDoc (if ppColor opts then colorStyle else const mempty) $ runPPM opts $ flip (Fold.foldl' (\m x -> snd <$> withBoundVarM x m)) ctx $ ppTermWithMemoTable PrecNone False trm @@ -664,7 +663,7 @@ data PPDecl | PPDefDecl Ident Term (Maybe Term) -- | Pretty-print a 'PPModule' -ppPPModule :: PPOpts -> PPModule -> Doc +ppPPModule :: PPOpts -> PPModule -> SawDoc ppPPModule opts (PPModule importNames decls) = vcat $ concat $ fmap (map (<> line)) $ [ map ppImport importNames diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs index a2fb7151ac..26926daeab 100644 --- a/saw-core/src/Verifier/SAW/Typechecker.hs +++ b/saw-core/src/Verifier/SAW/Typechecker.hs @@ -45,7 +45,7 @@ import Verifier.SAW.Module import Verifier.SAW.Position import Verifier.SAW.Term.Functor import Verifier.SAW.Term.CtxTerm -import Verifier.SAW.Term.Pretty (Doc, text) +import Verifier.SAW.Term.Pretty (SawDoc, text) import Verifier.SAW.SharedTerm import Verifier.SAW.Recognizer import Verifier.SAW.SCTypeCheck @@ -56,13 +56,13 @@ import Debug.Trace -- | Infer the type of an untyped term and complete it to a 'Term', all in the -- empty typing context inferCompleteTerm :: SharedContext -> Maybe ModuleName -> Un.Term -> - IO (Either Doc Term) + IO (Either SawDoc Term) inferCompleteTerm sc mnm t = inferCompleteTermCtx sc mnm [] t -- | Infer the type of an untyped term and complete it to a 'Term' in a given -- typing context inferCompleteTermCtx :: SharedContext -> Maybe ModuleName -> [(String,Term)] -> - Un.Term -> IO (Either Doc Term) + Un.Term -> IO (Either SawDoc Term) inferCompleteTermCtx sc mnm ctx t = do res <- runTCM (typeInferComplete t) sc mnm ctx case res of From 056ac76c3ba0cdafe0ea054131da8d48660448c9 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 24 Nov 2020 09:50:18 -0800 Subject: [PATCH 5/5] Use standard prettyprinter combinators instead of locally-defined ones. --- saw-core/src/Verifier/SAW/FiniteValue.hs | 12 +-- saw-core/src/Verifier/SAW/Term/Pretty.hs | 94 ++++++++++-------------- saw-core/src/Verifier/SAW/Typechecker.hs | 5 +- 3 files changed, 49 insertions(+), 62 deletions(-) diff --git a/saw-core/src/Verifier/SAW/FiniteValue.hs b/saw-core/src/Verifier/SAW/FiniteValue.hs index 17f7271efd..788a16d5c8 100644 --- a/saw-core/src/Verifier/SAW/FiniteValue.hs +++ b/saw-core/src/Verifier/SAW/FiniteValue.hs @@ -110,16 +110,16 @@ ppFirstOrderValue opts = loop where loop fv = case fv of FOVBit b - | b -> text "True" - | otherwise -> text "False" - FOVInt i -> integer i - FOVIntMod _ i -> integer i + | b -> pretty "True" + | otherwise -> pretty "False" + FOVInt i -> pretty i + FOVIntMod _ i -> pretty i FOVWord _w i -> ppNat opts i FOVVec _ xs -> brackets (sep (punctuate comma (map loop xs))) - FOVArray{} -> text $ show $ firstOrderTypeOf fv + FOVArray{} -> viaShow $ firstOrderTypeOf fv FOVTuple xs -> parens (sep (punctuate comma (map loop xs))) FOVRec xs -> braces (sep (punctuate comma (map ppField (Map.toList xs)))) - where ppField (f,x) = pretty f <+> char '=' <+> loop x + where ppField (f,x) = pretty f <+> pretty '=' <+> loop x -- | Smart constructor diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index 9c5fa0b490..6833839422 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -17,6 +17,7 @@ Portability : non-portable (language extensions) module Verifier.SAW.Term.Pretty ( SawDoc + , SawStyle(..) , PPOpts(..) , defaultPPOpts , depthPPOpts @@ -32,7 +33,6 @@ module Verifier.SAW.Term.Pretty , OccurrenceMap , shouldMemoizeTerm , ppName - , text, char, integer ) where import Data.Maybe (isJust) @@ -42,7 +42,6 @@ import Control.Monad.State.Strict as State import Data.Foldable (Foldable) #endif import qualified Data.Foldable as Fold -import qualified Data.Text as Text import qualified Data.Text.Lazy as Text.Lazy import qualified Data.Vector as V import Numeric (showIntAtBase) @@ -290,49 +289,34 @@ withMemoVar global_p idx f = -- * The Pretty-Printing of Specific Constructs -------------------------------------------------------------------------------- -text :: String -> SawDoc -text = pretty - -char :: Char -> SawDoc -char = pretty - -integer :: Integer -> SawDoc -integer = pretty - -int :: Int -> SawDoc -int = pretty - -(<<$>>) :: SawDoc -> SawDoc -> SawDoc -x <<$>> y = vsep [x, y] - -- | Pretty-print an identifier ppIdent :: Ident -> SawDoc -ppIdent i = text (show i) +ppIdent = viaShow -- | Pretty-print an integer in the correct base ppNat :: PPOpts -> Integer -> SawDoc ppNat (PPOpts{..}) i | ppBase > 36 = pretty i - | otherwise = prefix <> text value + | otherwise = prefix <> pretty value where prefix = case ppBase of - 2 -> text "0b" - 8 -> text "0o" + 2 -> pretty "0b" + 8 -> pretty "0o" 10 -> mempty - 16 -> text "0x" - _ -> text "0" <> char '<' <> int ppBase <> char '>' + 16 -> pretty "0x" + _ -> pretty "0" <> pretty '<' <> pretty ppBase <> pretty '>' value = showIntAtBase (toInteger ppBase) (digits !!) i "" digits = "0123456789abcdefghijklmnopqrstuvwxyz" -- | Pretty-print a memoization variable ppMemoVar :: MemoVar -> SawDoc -ppMemoVar mv = text "x@" <> pretty (toInteger mv) +ppMemoVar mv = pretty "x@" <> pretty mv -- | Pretty-print a type constraint (also known as an ascription) @x : tp@ ppTypeConstraint :: SawDoc -> SawDoc -> SawDoc ppTypeConstraint x tp = - hang 2 $ group $ vsep [annotate LocalVarStyle x, text ":" <+> tp] + hang 2 $ group $ vsep [annotate LocalVarStyle x, pretty ":" <+> tp] -- | Pretty-print an application to 0 or more arguments at the given precedence ppAppList :: Prec -> SawDoc -> [SawDoc] -> SawDoc @@ -343,21 +327,21 @@ ppAppList p f args = ppParensPrec p PrecApp $ group $ hang 2 $ vsep (f : args) ppLetBlock :: [(MemoVar, SawDoc)] -> SawDoc -> SawDoc ppLetBlock defs body = vcat - [ text "let" <+> lbrace <+> align (vcat (map ppEqn defs)) + [ pretty "let" <+> lbrace <+> align (vcat (map ppEqn defs)) , indent 4 rbrace - , text " in" <+> body + , pretty " in" <+> body ] where - ppEqn (var,d) = ppMemoVar var <+> char '=' <+> d + ppEqn (var,d) = ppMemoVar var <+> pretty '=' <+> d -- | Pretty-print pairs as "(x, y)" ppPair :: Prec -> SawDoc -> SawDoc -> SawDoc -ppPair prec x y = ppParensPrec prec PrecNone (group (vcat [x <> char ',', y])) +ppPair prec x y = ppParensPrec prec PrecNone (group (vcat [x <> pretty ',', y])) -- | Pretty-print pair types as "x * y" ppPairType :: Prec -> SawDoc -> SawDoc -> SawDoc -ppPairType prec x y = ppParensPrec prec PrecProd (x <+> char '*' <+> y) +ppPairType prec x y = ppParensPrec prec PrecProd (x <+> pretty '*' <+> y) -- | Pretty-print records (if the flag is 'False') or record types (if the flag -- is 'True'), where the latter are preceded by the string @#@, either as: @@ -368,15 +352,15 @@ ppPairType prec x y = ppParensPrec prec PrecProd (x <+> char '*' <+> y) -- types and @=@ for values. ppRecord :: Bool -> [(String, SawDoc)] -> SawDoc ppRecord type_p alist = - (if type_p then (char '#' <>) else id) $ + (if type_p then (pretty '#' <>) else id) $ encloseSep lbrace rbrace comma $ map ppField alist where - ppField (fld, rhs) = group (nest 2 (text fld <+> text op_str <<$>> rhs)) + ppField (fld, rhs) = group (nest 2 (vsep [pretty fld <+> pretty op_str, rhs])) op_str = if type_p then ":" else "=" -- | Pretty-print a projection / selector "x.f" ppProj :: String -> SawDoc -> SawDoc -ppProj sel doc = doc <> char '.' <> text sel +ppProj sel doc = doc <> pretty '.' <> pretty sel -- | Pretty-print an array value @[v1, ..., vn]@ ppArrayValue :: [SawDoc] -> SawDoc @@ -387,14 +371,14 @@ ppArrayValue = list ppLambda :: SawDoc -> (String, SawDoc) -> SawDoc ppLambda tp (name, body) = group $ hang 2 $ - vsep [text "\\" <> parens (ppTypeConstraint (text name) tp) <+> text "->", body] + vsep [pretty "\\" <> parens (ppTypeConstraint (pretty name) tp) <+> pretty "->", body] -- | Pretty-print a pi abstraction as @(x :: tp) -> body@, or as @tp -> body@ if -- @x == "_"@ ppPi :: SawDoc -> (String, SawDoc) -> SawDoc -ppPi tp (name, body) = lhs <<$>> text "->" <+> body +ppPi tp (name, body) = vsep [lhs, pretty "->" <+> body] where - lhs = if name == "_" then tp else parens (ppTypeConstraint (text name) tp) + lhs = if name == "_" then tp else parens (ppTypeConstraint (pretty name) tp) -- | Pretty-print a definition @d :: tp = body@ ppDef :: SawDoc -> SawDoc -> Maybe SawDoc -> SawDoc @@ -410,12 +394,14 @@ ppDataType :: Ident -> (SawDoc, ((SawDoc, SawDoc), [SawDoc])) -> SawDoc ppDataType d (params, ((d_ctx,d_tp), ctors)) = group $ vcat - [ (group - ((text "data" <+> ppIdent d <+> params <+> text ":" <+> - (d_ctx <+> text "->" <+> d_tp)) - <<$>> (text "where" <+> lbrace))) - <<$>> - vcat (map (<> semi) ctors) + [ vsep + [ (group . vsep) + [ pretty "data" <+> ppIdent d <+> params <+> pretty ":" <+> + (d_ctx <+> pretty "->" <+> d_tp) + , pretty "where" <+> lbrace + ] + , vcat (map (<> semi) ctors) + ] , rbrace ] @@ -429,8 +415,8 @@ ppFlatTermF :: Prec -> FlatTermF Term -> PPM SawDoc ppFlatTermF prec tf = case tf of GlobalDef i -> return $ annotate GlobalDefStyle $ ppIdent i - UnitValue -> return $ text "(-empty-)" - UnitType -> return $ text "#(-empty-)" + UnitValue -> return $ pretty "(-empty-)" + UnitType -> return $ pretty "#(-empty-)" PairValue x y -> ppPair prec <$> ppTerm' PrecLambda x <*> ppTerm' PrecNone y PairType x y -> ppPairType prec <$> ppTerm' PrecApp x <*> ppTerm' PrecProd y PairLeft t -> ppProj "1" <$> ppTerm' PrecArg t @@ -447,10 +433,10 @@ ppFlatTermF prec tf = ixs_pp <- mapM (ppTerm' PrecArg) ixs arg_pp <- ppTerm' PrecArg arg return $ - ppAppList prec (annotate RecursorStyle (ppIdent d <> text "#rec")) + ppAppList prec (annotate RecursorStyle (ppIdent d <> pretty "#rec")) (params_pp ++ [p_ret_pp] ++ [tupled $ - zipWith (\(c,_) f_pp -> ppIdent c <<$>> text "=>" <<$>> f_pp) + zipWith (\(c,_) f_pp -> vsep [ppIdent c, pretty "=>", f_pp]) cs_fs fs_pp] ++ ixs_pp ++ [arg_pp]) RecordType alist -> @@ -458,16 +444,16 @@ ppFlatTermF prec tf = RecordValue alist -> ppRecord False <$> mapM (\(fld,t) -> (fld,) <$> ppTerm' PrecNone t) alist RecordProj e fld -> ppProj fld <$> ppTerm' PrecArg e - Sort s -> return $ text (show s) + Sort s -> return $ viaShow s NatLit i -> ppNat <$> (ppOpts <$> ask) <*> return (toInteger i) ArrayValue _ args -> ppArrayValue <$> mapM (ppTerm' PrecNone) (V.toList args) - StringLit s -> return $ text (show s) + StringLit s -> return $ viaShow s ExtCns cns -> pure $ annotate ExtCnsStyle $ ppName (ecName cns) ppName :: NameInfo -> SawDoc ppName (ModuleIdentifier i) = ppIdent i -ppName (ImportedName absName _) = text (Text.unpack (render absName)) +ppName (ImportedName absName _) = pretty (render absName) -- | Pretty-print a non-shared term ppTermF :: Prec -> TermF Term -> PPM SawDoc @@ -481,13 +467,13 @@ ppTermF prec (Pi x tp body) = ppParensPrec prec PrecLambda <$> (ppPi <$> ppTerm' PrecApp tp <*> ppTermInBinder PrecLambda x body) -ppTermF _ (LocalVar x) = annotate LocalVarStyle <$> text <$> varLookupM x +ppTermF _ (LocalVar x) = annotate LocalVarStyle <$> pretty <$> varLookupM x ppTermF _ (Constant ec _) = pure $ annotate ConstantStyle $ ppName (ecName ec) -- | Internal function to recursively pretty-print a term ppTerm' :: Prec -> Term -> PPM SawDoc -ppTerm' prec = atNextDepthM (text "...") . ppTerm'' where +ppTerm' prec = atNextDepthM (pretty "...") . ppTerm'' where ppTerm'' (Unshared tf) = ppTermF prec tf ppTerm'' (STApp {stAppIndex = idx, stAppTermF = tf}) = do maybe_memo_var <- memoLookupM idx @@ -613,7 +599,7 @@ ppWithBoundCtx :: [(String, Term)] -> PPM a -> PPM (SawDoc, a) ppWithBoundCtx [] m = (mempty ,) <$> m ppWithBoundCtx ((x,tp):ctx) m = (\tp_d (x', (ctx_d, ret)) -> - (parens (ppTypeConstraint (text x') tp_d) <+> ctx_d, ret)) + (parens (ppTypeConstraint (pretty x') tp_d) <+> ctx_d, ret)) <$> ppTerm' PrecNone tp <*> withBoundVarM x (ppWithBoundCtx ctx m) -- | Pretty-print a term, also adding let-bindings for all subterms that occur @@ -670,11 +656,11 @@ ppPPModule opts (PPModule importNames decls) = , map (runPPM opts . ppDecl) decls ] where - ppImport nm = text $ "import " ++ show nm + ppImport nm = pretty $ "import " ++ show nm ppDecl (PPTypeDecl dtName dtParams dtIndices dtSort dtCtors) = ppDataType dtName <$> ppWithBoundCtx dtParams ((,) <$> - ppWithBoundCtx dtIndices (return $ text $ show dtSort) <*> + ppWithBoundCtx dtIndices (return $ viaShow dtSort) <*> mapM (\(ctorName,ctorType) -> ppTypeConstraint (ppIdent ctorName) <$> ppTerm' PrecNone ctorType) diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs index 26926daeab..b0439fe81c 100644 --- a/saw-core/src/Verifier/SAW/Typechecker.hs +++ b/saw-core/src/Verifier/SAW/Typechecker.hs @@ -45,7 +45,7 @@ import Verifier.SAW.Module import Verifier.SAW.Position import Verifier.SAW.Term.Functor import Verifier.SAW.Term.CtxTerm -import Verifier.SAW.Term.Pretty (SawDoc, text) +import Verifier.SAW.Term.Pretty (SawDoc) import Verifier.SAW.SharedTerm import Verifier.SAW.Recognizer import Verifier.SAW.SCTypeCheck @@ -66,7 +66,8 @@ inferCompleteTermCtx :: SharedContext -> Maybe ModuleName -> [(String,Term)] -> inferCompleteTermCtx sc mnm ctx t = do res <- runTCM (typeInferComplete t) sc mnm ctx case res of - Left err -> return $ Left $ vsep $ map text $ prettyTCError err + -- TODO: avoid intermediate 'String's from 'prettyTCError' + Left err -> return $ Left $ vsep $ map pretty $ prettyTCError err Right t' -> return $ Right $ typedVal t' -- | Look up the current module name, raising an error if it is not set