From 0a1ec9405686b286d87bf8101343611b925bf630 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sun, 22 Nov 2020 09:34:48 -0800 Subject: [PATCH] Switch from `ansi-wl-pprint` to the `prettyprinter` package. This patch converts packages `what4`, `what4-abc`, and `what4-blt`. --- what4-abc/src/What4/Solver/ABC.hs | 29 +++-- what4-abc/what4-abc.cabal | 2 +- what4-blt/src/What4/Solver/BLT.hs | 18 +-- what4-blt/what4-blt.cabal | 2 +- what4/src/What4/BaseTypes.hs | 8 +- what4/src/What4/Concrete.hs | 30 +++-- what4/src/What4/Config.hs | 60 +++++---- what4/src/What4/Expr/App.hs | 12 +- what4/src/What4/Expr/Builder.hs | 72 +++++------ what4/src/What4/Expr/MATLAB.hs | 129 ++++++++++---------- what4/src/What4/Expr/VarIdentification.hs | 6 +- what4/src/What4/FunctionName.hs | 4 +- what4/src/What4/Interface.hs | 4 +- what4/src/What4/InterpretedFloatingPoint.hs | 4 +- what4/src/What4/ProgramLoc.hs | 26 ++-- what4/src/What4/Protocol/Online.hs | 6 +- what4/src/What4/Protocol/PolyRoot.hs | 10 +- what4/src/What4/Protocol/SMTLib2.hs | 28 +++-- what4/src/What4/Protocol/SMTWriter.hs | 48 +++++--- what4/src/What4/Solver/Adapter.hs | 4 +- what4/src/What4/Solver/Boolector.hs | 3 +- what4/src/What4/Solver/CVC4.hs | 5 +- what4/src/What4/Solver/DReal.hs | 3 +- what4/src/What4/Solver/STP.hs | 3 +- what4/src/What4/Solver/Yices.hs | 14 +-- what4/src/What4/Solver/Z3.hs | 5 +- what4/what4.cabal | 2 +- 27 files changed, 288 insertions(+), 249 deletions(-) diff --git a/what4-abc/src/What4/Solver/ABC.hs b/what4-abc/src/What4/Solver/ABC.hs index 7057799a..22adb9f9 100644 --- a/what4-abc/src/What4/Solver/ABC.hs +++ b/what4-abc/src/What4/Solver/ABC.hs @@ -70,11 +70,11 @@ import qualified Data.Set as Set import qualified Data.Text as T import Foreign.C.Types import Numeric.Natural +import Prettyprinter import System.Directory import System.IO import qualified System.IO.Streams as Streams import System.Process -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) import What4.BaseTypes import What4.Concrete @@ -108,7 +108,7 @@ abcQbfIterations = configOption BaseIntegerRepr "abc.qbf_max_iterations" abcOptions :: [ConfigDesc] abcOptions = [ opt abcQbfIterations (ConcreteInteger (toInteger (maxBound :: CInt))) - (text "Max number of iterations to run ABC's QBF solver") + ("Max number of iterations to run ABC's QBF solver" :: T.Text) ] abcAdapter :: SolverAdapter st @@ -132,7 +132,7 @@ satCommand = configOption knownRepr "sat_command" genericSatOptions :: [ConfigDesc] genericSatOptions = [ opt satCommand (ConcreteString "glucose $1") - (text "Generic SAT solving command to run") + ("Generic SAT solving command to run" :: T.Text) ] genericSatAdapter :: SolverAdapter st @@ -249,16 +249,20 @@ eval' ntk e = do failAt :: ProgramLoc -> String -> IO a failAt l msg = fail $ show $ - text msg <$$> - text "From term created at" <+> pretty (plSourceLoc l) + vcat + [ text msg + , text "From term created at" <+> pretty (plSourceLoc l) + ] failTerm :: Expr t tp -> String -> IO a failTerm e nm = do fail $ show $ - text "The" <+> text nm <+> text "created at" + vcat + [ text "The" <+> text nm <+> text "created at" <+> pretty (plSourceLoc (exprLoc e)) - <+> text "is not supported by ABC:" <$$> - indent 2 (ppExpr e) + <+> text "is not supported by ABC:" + , indent 2 (ppExpr e) + ] bitblastPred :: Network t s -> NonceAppExpr t tp -> IO (NameType s tp) bitblastPred h e = do @@ -731,8 +735,10 @@ checkSupportedByAbc vars = do let errors = Fold.toList (vars^.varErrors) -- Check no errors where reported in result. when (not (null errors)) $ do - fail $ show $ text "This formula is not supported by abc:" <$$> - indent 2 (vcat errors) + fail $ show $ vcat + [ text "This formula is not supported by abc:" + , indent 2 (vcat errors) + ] checkNoLatches :: MonadFail m => CollectedVarInfo t -> m () checkNoLatches vars = do @@ -1039,3 +1045,6 @@ getInputCount ntk = GIA.inputCount (gia ntk) -- | Return number of outputs so far in network. getOutputCount :: Network t s -> IO Int getOutputCount ntk = length <$> readIORef (revOutputs ntk) + +text :: String -> Doc ann +text = pretty diff --git a/what4-abc/what4-abc.cabal b/what4-abc/what4-abc.cabal index c0f4f55b..a0099a6e 100644 --- a/what4-abc/what4-abc.cabal +++ b/what4-abc/what4-abc.cabal @@ -20,7 +20,6 @@ library base >= 4.7 && < 4.15, aig, abcBridge >= 0.11, - ansi-wl-pprint, bv-sized >= 1.0.0, containers, what4 >= 0.4, @@ -29,6 +28,7 @@ library lens, mtl, parameterized-utils, + prettyprinter >= 1.7.0, process, text, transformers, diff --git a/what4-blt/src/What4/Solver/BLT.hs b/what4-blt/src/What4/Solver/BLT.hs index b8e6bc86..08e7bf3e 100644 --- a/what4-blt/src/What4/Solver/BLT.hs +++ b/what4-blt/src/What4/Solver/BLT.hs @@ -77,7 +77,7 @@ import qualified Data.Text as T import Data.Traversable import Data.Typeable import System.IO (hPutStrLn, stderr) -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) +import Prettyprinter import qualified Data.Parameterized.HashTable as PH import Data.Parameterized.Nonce @@ -106,7 +106,7 @@ bltParams = configOption knownRepr "blt_params" bltOptions :: [ConfigDesc] bltOptions = [ opt bltParams (ConcreteString (UnicodeLiteral "")) - (text "Command-line parameters to send to BLT") + ("Command-line parameters to send to BLT" :: T.Text) ] bltAdapter :: SolverAdapter t @@ -415,8 +415,10 @@ assume h (NonceAppExpr (nonceExprApp -> Annotation _ _ x)) = assume h x assume _ (NonceAppExpr e) = fail . show $ - text "Unsupported term created at" <+> pretty (plSourceLoc l) <> - text ":" <$$> indent 2 (pretty (NonceAppExpr e)) + vcat + [ "Unsupported term created at" <+> pretty (plSourceLoc l) <> ":" + , indent 2 (pretty (NonceAppExpr e)) + ] where l = nonceExprLoc e assume h (BoolExpr b l) @@ -447,9 +449,11 @@ assume h b@(AppExpr ba) = appLEq x' y' _ -> unsupported where - unsupported = fail $ show $ - text "Unsupported term created at" <+> pretty (plSourceLoc l) <> - text ":" <$$> indent 2 (pretty b) + unsupported = + fail $ show $ vcat + [ "Unsupported term created at" <+> pretty (plSourceLoc l) <> ":" + , indent 2 (pretty b) + ] l = appExprLoc ba appLEq lhs rhs = let (lhs', rhs') = normalizeLEQ lhs rhs in diff --git a/what4-blt/what4-blt.cabal b/what4-blt/what4-blt.cabal index 55ccddc5..4abcb057 100644 --- a/what4-blt/what4-blt.cabal +++ b/what4-blt/what4-blt.cabal @@ -18,12 +18,12 @@ Description: library build-depends: base >= 4.7 && < 4.15, - ansi-wl-pprint, blt >= 0.12.1, containers, what4 >= 0.4, lens >= 1.2, parameterized-utils, + prettyprinter >= 1.7.0, text, transformers diff --git a/what4/src/What4/BaseTypes.hs b/what4/src/What4/BaseTypes.hs index 029c5f82..2ba07adb 100644 --- a/what4/src/What4/BaseTypes.hs +++ b/what4/src/What4/BaseTypes.hs @@ -84,7 +84,7 @@ import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.NatRepr import Data.Parameterized.TH.GADT import GHC.TypeNats as TypeNats -import Text.PrettyPrint.ANSI.Leijen +import Prettyprinter -------------------------------------------------------------------------------- -- KnownCtx @@ -290,19 +290,19 @@ instance Hashable (StringInfoRepr si) where hashWithSalt = $(structuralHashWithSalt [t|StringInfoRepr|] []) instance Pretty (BaseTypeRepr bt) where - pretty = text . show + pretty = pretty . show instance Show (BaseTypeRepr bt) where showsPrec = $(structuralShowsPrec [t|BaseTypeRepr|]) instance ShowF BaseTypeRepr instance Pretty (FloatPrecisionRepr fpp) where - pretty = text . show + pretty = pretty . show instance Show (FloatPrecisionRepr fpp) where showsPrec = $(structuralShowsPrec [t|FloatPrecisionRepr|]) instance ShowF FloatPrecisionRepr instance Pretty (StringInfoRepr si) where - pretty = text . show + pretty = pretty . show instance Show (StringInfoRepr si) where showsPrec = $(structuralShowsPrec [t|StringInfoRepr|]) instance ShowF StringInfoRepr diff --git a/what4/src/What4/Concrete.hs b/what4/src/What4/Concrete.hs index 03eb6d74..cad4c8c7 100644 --- a/what4/src/What4/Concrete.hs +++ b/what4/src/What4/Concrete.hs @@ -52,7 +52,7 @@ import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import qualified Numeric as N import Numeric.Natural -import qualified Text.PrettyPrint.ANSI.Leijen as PP +import qualified Prettyprinter as PP import qualified Data.BitVector.Sized as BV import Data.Parameterized.Classes @@ -148,26 +148,30 @@ instance OrdF ConcreteVal where instance Ord (ConcreteVal tp) where compare x y = toOrdering (compareF x y) +-- | Pretty-print a rational number. +ppRational :: Rational -> PP.Doc ann +ppRational x = PP.pretty (show x) + -- | Pretty-print a concrete value -ppConcrete :: ConcreteVal tp -> PP.Doc +ppConcrete :: ConcreteVal tp -> PP.Doc ann ppConcrete = \case - ConcreteBool x -> PP.text (show x) - ConcreteNat x -> PP.text (show x) - ConcreteInteger x -> PP.text (show x) - ConcreteReal x -> PP.text (show x) - ConcreteString x -> PP.text (show x) - ConcreteBV w x -> PP.text ("0x" ++ (N.showHex (BV.asUnsigned x) (":[" ++ show w ++ "]"))) - ConcreteComplex (r :+ i) -> PP.text "complex(" PP.<> PP.text (show r) PP.<> PP.text ", " PP.<> PP.text (show i) PP.<> PP.text ")" - ConcreteStruct xs -> PP.text "struct(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete xs)) PP.<> PP.text ")" - ConcreteArray _ def xs0 -> go (Map.toAscList xs0) (PP.text "constArray(" PP.<> ppConcrete def PP.<> PP.text ")") + ConcreteBool x -> PP.pretty x + ConcreteNat x -> PP.pretty x + ConcreteInteger x -> PP.pretty x + ConcreteReal x -> ppRational x + ConcreteString x -> PP.pretty (show x) + ConcreteBV w x -> PP.pretty ("0x" ++ (N.showHex (BV.asUnsigned x) (":[" ++ show w ++ "]"))) + ConcreteComplex (r :+ i) -> PP.pretty "complex(" PP.<> ppRational r PP.<> PP.pretty ", " PP.<> ppRational i PP.<> PP.pretty ")" + ConcreteStruct xs -> PP.pretty "struct(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete xs)) PP.<> PP.pretty ")" + ConcreteArray _ def xs0 -> go (Map.toAscList xs0) (PP.pretty "constArray(" PP.<> ppConcrete def PP.<> PP.pretty ")") where go [] doc = doc go ((i,x):xs) doc = ppUpd i x (go xs doc) ppUpd i x doc = - PP.text "update(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete i)) + PP.pretty "update(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete i)) PP.<> PP.comma PP.<> ppConcrete x PP.<> PP.comma PP.<> doc - PP.<> PP.text ")" + PP.<> PP.pretty ")" diff --git a/what4/src/What4/Config.hs b/what4/src/What4/Config.hs index e088b9f8..24160793 100644 --- a/what4/src/What4/Config.hs +++ b/what4/src/What4/Config.hs @@ -176,7 +176,7 @@ import Numeric.Natural import System.IO ( Handle, hPutStr ) import System.IO.Error ( ioeGetErrorString ) -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>)) +import Prettyprinter hiding (Unbounded) import What4.BaseTypes import What4.Concrete @@ -253,8 +253,8 @@ configOptionType (ConfigOption tp _) = tp -- attempting to alter the option setting. data OptionSetResult = OptionSetResult - { optionSetError :: !(Maybe Doc) - , optionSetWarnings :: !(Seq Doc) + { optionSetError :: !(Maybe (Doc ())) + , optionSetWarnings :: !(Seq (Doc ())) } instance Semigroup OptionSetResult where @@ -272,11 +272,11 @@ optOK :: OptionSetResult optOK = OptionSetResult{ optionSetError = Nothing, optionSetWarnings = mempty } -- | Reject the new option value with an error message. -optErr :: Doc -> OptionSetResult +optErr :: Doc () -> OptionSetResult optErr x = OptionSetResult{ optionSetError = Just x, optionSetWarnings = mempty } -- | Accept the given option value, but report a warning message. -optWarn :: Doc -> OptionSetResult +optWarn :: Doc () -> OptionSetResult optWarn x = OptionSetResult{ optionSetError = Nothing, optionSetWarnings = Seq.singleton x } @@ -312,7 +312,7 @@ data OptionStyle (tp :: BaseType) = -- If the validation fails, the operation should return a result -- describing why validation failed. Optionally, warnings may also be returned. - , opt_help :: Doc + , opt_help :: Doc () -- ^ Documentation for the option to be displayed in the event a user asks for information -- about this option. This message should contain information relevant to all options in this -- style (e.g., its type and range of expected values), not necessarily @@ -330,7 +330,7 @@ defaultOpt tp = OptionStyle { opt_type = tp , opt_onset = \_ _ -> return mempty - , opt_help = empty + , opt_help = mempty , opt_default_value = Nothing } @@ -341,7 +341,7 @@ set_opt_onset :: (Maybe (ConcreteVal tp) -> ConcreteVal tp -> IO OptionSetResult set_opt_onset f s = s { opt_onset = f } -- | Update the @opt_help@ field. -set_opt_help :: Doc +set_opt_help :: Doc () -> OptionStyle tp -> OptionStyle tp set_opt_help v s = s { opt_help = v } @@ -395,7 +395,7 @@ checkBound lo hi a = checkLo lo a && checkHi a hi checkHi x (Inclusive y) = x <= y checkHi x (Exclusive y) = x < y -docInterval :: Show a => Bound a -> Bound a -> Doc +docInterval :: Show a => Bound a -> Bound a -> Doc ann docInterval lo hi = docLo lo <> text ", " <> docHi hi where docLo Unbounded = text "(-∞" docLo (Exclusive r) = text "(" <> text (show r) @@ -450,7 +450,7 @@ integerWithMaxOptSty hi = integerWithRangeOptSty Unbounded hi enumOptSty :: Set Text -> OptionStyle (BaseStringType Unicode) enumOptSty elts = stringOptSty & set_opt_onset vf & set_opt_help help - where help = group (text "one of: " <+> align (sep $ map (dquotes . text . Text.unpack) $ Set.toList elts)) + where help = group (text "one of: " <+> align (sep $ map (dquotes . pretty) $ Set.toList elts)) vf :: Maybe (ConcreteVal (BaseStringType Unicode)) -> ConcreteVal (BaseStringType Unicode) -> IO OptionSetResult @@ -459,7 +459,7 @@ enumOptSty elts = stringOptSty & set_opt_onset vf | otherwise = return $ optErr $ text "invalid setting" <+> text (show x) <+> text ", expected one of:" <+> - align (sep (map (text . Text.unpack) $ Set.toList elts)) + align (sep (map pretty $ Set.toList elts)) -- | A configuration syle for options that must be one of a fixed set of text values. -- Associated with each string is a validation/callback action that will be run @@ -469,7 +469,7 @@ listOptSty -> OptionStyle (BaseStringType Unicode) listOptSty values = stringOptSty & set_opt_onset vf & set_opt_help help - where help = group (text "one of: " <+> align (sep $ map (dquotes . text . Text.unpack . fst) $ Map.toList values)) + where help = group (text "one of: " <+> align (sep $ map (dquotes . pretty . fst) $ Map.toList values)) vf :: Maybe (ConcreteVal (BaseStringType Unicode)) -> ConcreteVal (BaseStringType Unicode) -> IO OptionSetResult @@ -478,7 +478,7 @@ listOptSty values = stringOptSty & set_opt_onset vf (return $ optErr $ text "invalid setting" <+> text (show x) <+> text ", expected one of:" <+> - align (sep (map (text . Text.unpack . fst) $ Map.toList values))) + align (sep (map (pretty . fst) $ Map.toList values))) (Map.lookup x values) @@ -505,12 +505,12 @@ executablePathOptSty = stringOptSty & set_opt_onset vf -- an @OptionStyle@ describing the sort of option it is, and an optional -- help message describing the semantics of this option. data ConfigDesc where - ConfigDesc :: ConfigOption tp -> OptionStyle tp -> Maybe Doc -> ConfigDesc + ConfigDesc :: ConfigOption tp -> OptionStyle tp -> Maybe (Doc ()) -> ConfigDesc -- | The most general method for construcing a normal `ConfigDesc`. mkOpt :: ConfigOption tp -- ^ Fixes the name and the type of this option -> OptionStyle tp -- ^ Define the style of this option - -> Maybe Doc -- ^ Help text + -> Maybe (Doc ()) -- ^ Help text -> Maybe (ConcreteVal tp) -- ^ A default value for this option -> ConfigDesc mkOpt o sty h def = ConfigDesc o sty{ opt_default_value = def } h @@ -577,7 +577,7 @@ data ConfigLeaf where ConfigLeaf :: !(OptionStyle tp) {- Style for this option -} -> IORef (Maybe (ConcreteVal tp)) {- State of the option -} -> - Maybe Doc {- Help text for the option -} -> + Maybe (Doc ()) {- Help text for the option -} -> ConfigLeaf -- | Main configuration data type. It is organized as a trie based on the @@ -689,7 +689,7 @@ builtInOpts :: Integer -> [ConfigDesc] builtInOpts initialVerbosity = [ opt verbosity (ConcreteInteger initialVerbosity) - (text "Verbosity of the simulator: higher values produce more detailed informational and debugging output.") + ("Verbosity of the simulator: higher values produce more detailed informational and debugging output." :: Text) ] -- | Return an operation that will consult the current value of the @@ -715,7 +715,7 @@ class Opt (tp :: BaseType) (a :: Type) | tp -> a where -- | Set the value of an option. Return any generated warnings. -- Throw an exception if a validation error occurs. - setOpt :: OptionSetting tp -> a -> IO [Doc] + setOpt :: OptionSetting tp -> a -> IO [Doc ()] setOpt x v = trySetOpt x v >>= checkOptSetResult -- | Get the current value of an option. Throw an exception @@ -726,7 +726,7 @@ class Opt (tp :: BaseType) (a :: Type) | tp -> a where -- | Throw an exception if the given @OptionSetResult@ indidcates -- an error. Otherwise, return any generated warnings. -checkOptSetResult :: OptionSetResult -> IO [Doc] +checkOptSetResult :: OptionSetResult -> IO [Doc ()] checkOptSetResult res = case optionSetError res of Just msg -> fail (show msg) @@ -830,16 +830,19 @@ getConfigValues prefix (Config cfg) = toList <$> execWriterT (traverseSubtree ps f m) -ppSetting :: [Text] -> Maybe (ConcreteVal tp) -> Doc -ppSetting nm v = fill 30 (text (Text.unpack (Text.intercalate "." nm)) - <> maybe empty (\x -> text " = " <> ppConcrete x) v +ppSetting :: [Text] -> Maybe (ConcreteVal tp) -> Doc ann +ppSetting nm v = fill 30 (pretty (Text.intercalate "." nm) + <> maybe mempty (\x -> text " = " <> ppConcrete x) v ) -ppOption :: [Text] -> OptionStyle tp -> Maybe (ConcreteVal tp) -> Maybe Doc -> Doc +ppOption :: [Text] -> OptionStyle tp -> Maybe (ConcreteVal tp) -> Maybe (Doc ()) -> Doc () ppOption nm sty x help = - group (ppSetting nm x indent 2 (opt_help sty)) <$$> maybe empty (indent 2) help + vcat + [ group $ fillCat [ppSetting nm x, indent 2 (opt_help sty)] + , maybe mempty (indent 2) help + ] -ppConfigLeaf :: [Text] -> ConfigLeaf -> IO Doc +ppConfigLeaf :: [Text] -> ConfigLeaf -> IO (Doc ()) ppConfigLeaf nm (ConfigLeaf sty ref help) = do x <- readIORef ref return $ ppOption nm sty x help @@ -851,12 +854,15 @@ ppConfigLeaf nm (ConfigLeaf sty ref help) = configHelp :: Text -> Config -> - IO [Doc] + IO [Doc ()] configHelp prefix (Config cfg) = do m <- readIORef cfg let ps = Text.splitOn "." prefix - f :: [Text] -> ConfigLeaf -> WriterT (Seq Doc) IO ConfigLeaf + f :: [Text] -> ConfigLeaf -> WriterT (Seq (Doc ())) IO ConfigLeaf f nm leaf = do d <- liftIO (ppConfigLeaf nm leaf) tell (Seq.singleton d) return leaf toList <$> (execWriterT (traverseSubtree ps f m)) + +text :: String -> Doc ann +text = pretty diff --git a/what4/src/What4/Expr/App.hs b/what4/src/What4/Expr/App.hs index 70aad22b..7149873d 100644 --- a/what4/src/What4/Expr/App.hs +++ b/what4/src/What4/Expr/App.hs @@ -55,7 +55,7 @@ import Data.Ratio (numerator, denominator) import Data.Text (Text) import qualified Data.Text as Text import Numeric.Natural -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) +import Prettyprinter hiding (Unbounded) import What4.BaseTypes import What4.Interface @@ -1380,12 +1380,12 @@ ppNonceApp ppFn a0 = do where resolve f_nm = prettyApp "apply" (f_nm : toListFC exprPrettyArg a) instance ShowF e => Pretty (App e u) where - pretty a = text (Text.unpack nm) <+> sep (ppArg <$> args) + pretty a = pretty nm <+> sep (ppArg <$> args) where (nm, args) = ppApp' a - ppArg :: PrettyArg e -> Doc - ppArg (PrettyArg e) = text (showF e) - ppArg (PrettyText txt) = text (Text.unpack txt) - ppArg (PrettyFunc fnm fargs) = parens (text (Text.unpack fnm) <+> sep (ppArg <$> fargs)) + ppArg :: PrettyArg e -> Doc ann + ppArg (PrettyArg e) = pretty (showF e) + ppArg (PrettyText txt) = pretty txt + ppArg (PrettyFunc fnm fargs) = parens (pretty fnm <+> sep (ppArg <$> fargs)) instance ShowF e => Show (App e u) where show = show . pretty diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs index 8d39a68d..0e88d8ea 100644 --- a/what4/src/What4/Expr/Builder.hs +++ b/what4/src/What4/Expr/Builder.hs @@ -208,8 +208,7 @@ import qualified Data.Text as Text import Data.Word (Word64) import GHC.Generics (Generic) import Numeric.Natural -import qualified Text.PrettyPrint.ANSI.Leijen as PP -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) +import Prettyprinter hiding (Unbounded) import What4.BaseTypes import What4.Concrete @@ -868,44 +867,44 @@ instance Pretty (Expr t tp) where -- | @AppPPExpr@ represents a an application, and it may be let bound. -data AppPPExpr +data AppPPExpr ann = APE { apeIndex :: !PPIndex , apeLoc :: !ProgramLoc , apeName :: !Text - , apeExprs :: ![PPExpr] + , apeExprs :: ![PPExpr ann] , apeLength :: !Int -- ^ Length of AppPPExpr not including parenthesis. } -data PPExpr - = FixedPPExpr !Doc ![Doc] !Int +data PPExpr ann + = FixedPPExpr !(Doc ann) ![Doc ann] !Int -- ^ A fixed doc with length. - | AppPPExpr !AppPPExpr + | AppPPExpr !(AppPPExpr ann) -- ^ A doc that can be let bound. -- | Pretty print a AppPPExpr -apeDoc :: AppPPExpr -> (Doc, [Doc]) -apeDoc a = (text (Text.unpack (apeName a)), ppExprDoc True <$> apeExprs a) +apeDoc :: AppPPExpr ann -> (Doc ann, [Doc ann]) +apeDoc a = (pretty (apeName a), ppExprDoc True <$> apeExprs a) -textPPExpr :: Text -> PPExpr -textPPExpr t = FixedPPExpr (text (Text.unpack t)) [] (Text.length t) +textPPExpr :: Text -> PPExpr ann +textPPExpr t = FixedPPExpr (pretty t) [] (Text.length t) -stringPPExpr :: String -> PPExpr -stringPPExpr t = FixedPPExpr (text t) [] (length t) +stringPPExpr :: String -> PPExpr ann +stringPPExpr t = FixedPPExpr (pretty t) [] (length t) -- | Get length of Expr including parens. -ppExprLength :: PPExpr -> Int +ppExprLength :: PPExpr ann -> Int ppExprLength (FixedPPExpr _ [] n) = n ppExprLength (FixedPPExpr _ _ n) = n + 2 ppExprLength (AppPPExpr a) = apeLength a + 2 -parenIf :: Bool -> Doc -> [Doc] -> Doc +parenIf :: Bool -> Doc ann -> [Doc ann] -> Doc ann parenIf _ h [] = h parenIf False h l = hsep (h:l) parenIf True h l = parens (hsep (h:l)) -- | Pretty print PPExpr -ppExprDoc :: Bool -> PPExpr -> Doc +ppExprDoc :: Bool -> PPExpr ann -> Doc ann ppExprDoc b (FixedPPExpr d a _) = parenIf b d a ppExprDoc b (AppPPExpr a) = uncurry (parenIf b) (apeDoc a) @@ -920,28 +919,29 @@ defaultPPExprOpts = } -- | Pretty print an 'Expr' using let bindings to create the term. -ppExpr :: Expr t tp -> Doc +ppExpr :: Expr t tp -> Doc ann ppExpr e | Prelude.null bindings = ppExprDoc False r | otherwise = - text "let" <+> align (vcat bindings) PP.<$> - text " in" <+> align (ppExprDoc False r) + vsep + [ text "let" <+> align (vcat bindings) + , text " in" <+> align (ppExprDoc False r) ] where (bindings,r) = runST (ppExpr' e defaultPPExprOpts) instance ShowF (Expr t) -- | Pretty print the top part of an element. -ppExprTop :: Expr t tp -> Doc +ppExprTop :: Expr t tp -> Doc ann ppExprTop e = ppExprDoc False r where (_,r) = runST (ppExpr' e defaultPPExprOpts) -- | Contains the elements before, the index, doc, and width and -- the elements after. -type SplitPPExprList = Maybe ([PPExpr], AppPPExpr, [PPExpr]) +type SplitPPExprList ann = Maybe ([PPExpr ann], AppPPExpr ann, [PPExpr ann]) -findExprToRemove :: [PPExpr] -> SplitPPExprList +findExprToRemove :: [PPExpr ann] -> SplitPPExprList ann findExprToRemove exprs0 = go [] exprs0 Nothing - where go :: [PPExpr] -> [PPExpr] -> SplitPPExprList -> SplitPPExprList + where go :: [PPExpr ann] -> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann go _ [] mr = mr go prev (e@FixedPPExpr{} : exprs) mr = do go (e:prev) exprs mr @@ -951,7 +951,7 @@ findExprToRemove exprs0 = go [] exprs0 Nothing go (AppPPExpr a:prev) exprs (Just (reverse prev, a, exprs)) -ppExpr' :: forall t tp s . Expr t tp -> PPExprOpts -> ST s ([Doc], PPExpr) +ppExpr' :: forall t tp s ann. Expr t tp -> PPExprOpts -> ST s ([Doc ann], PPExpr ann) ppExpr' e0 o = do let max_width = ppExpr_maxWidth o let use_decimal = ppExpr_useDecimal o @@ -966,11 +966,11 @@ ppExpr' e0 o = do bindingsRef <- newSTRef Seq.empty - visited <- H.new :: ST s (H.HashTable s PPIndex PPExpr) + visited <- H.new :: ST s (H.HashTable s PPIndex (PPExpr ann)) visited_fns <- H.new :: ST s (H.HashTable s Word64 Text) let -- Add a binding to the list of bindings - addBinding :: AppPPExpr -> ST s PPExpr + addBinding :: AppPPExpr ann -> ST s (PPExpr ann) addBinding a = do let idx = apeIndex a cnt <- Seq.length <$> readSTRef bindingsRef @@ -983,8 +983,9 @@ ppExpr' e0 o = do ExprPPIndex e -> "v" ++ show e RatPPIndex _ -> "r" ++ show cnt let lhs = parenIf False (text nm) (text <$> args) - let doc = text "--" <+> pretty (plSourceLoc (apeLoc a)) <$$> - lhs <+> text "=" <+> uncurry (parenIf False) (apeDoc a) + let doc = vcat + [ text "--" <+> pretty (plSourceLoc (apeLoc a)) + , lhs <+> text "=" <+> uncurry (parenIf False) (apeDoc a) ] modifySTRef' bindingsRef (Seq.|> doc) let len = length nm + sum ((\arg_s -> length arg_s + 1) <$> args) let nm_expr = FixedPPExpr (text nm) (map text args) len @@ -992,8 +993,8 @@ ppExpr' e0 o = do return nm_expr let fixLength :: Int - -> [PPExpr] - -> ST s ([PPExpr], Int) + -> [PPExpr ann] + -> ST s ([PPExpr ann], Int) fixLength cur_width exprs | cur_width > max_width , Just (prev_e, a, next_e) <- findExprToRemove exprs = do @@ -1004,7 +1005,7 @@ ppExpr' e0 o = do return $! (exprs, cur_width) -- Pretty print an argument. - let renderArg :: PrettyArg (Expr t) -> ST s PPExpr + let renderArg :: PrettyArg (Expr t) -> ST s (PPExpr ann) renderArg (PrettyArg e) = getBindings e renderArg (PrettyText txt) = return (textPPExpr txt) renderArg (PrettyFunc nm args) = @@ -1018,7 +1019,7 @@ ppExpr' e0 o = do -> ProgramLoc -> Text -> [PrettyArg (Expr t)] - -> ST s AppPPExpr + -> ST s (AppPPExpr ann) renderApp idx loc nm args = Ex.assert (not (Prelude.null args)) $ do exprs0 <- traverse renderArg args -- Get width not including parenthesis of outer app. @@ -1034,7 +1035,7 @@ ppExpr' e0 o = do cacheResult :: PPIndex -> ProgramLoc -> PrettyApp (Expr t) - -> ST s PPExpr + -> ST s (PPExpr ann) cacheResult _ _ (nm,[]) = do return (textPPExpr nm) cacheResult idx loc (nm,args) = do @@ -1073,7 +1074,7 @@ ppExpr' e0 o = do -- Collect definitions for all applications that occur multiple times -- in term. - getBindings :: Expr t u -> ST s PPExpr + getBindings :: Expr t u -> ST s (PPExpr ann) getBindings (SemiRingLiteral sr x l) = case sr of SR.SemiRingNatRepr -> @@ -4696,3 +4697,6 @@ mkFreshUninterpFnApp sym str_fn_name args ret_type = do let arg_types = fmapFC exprType args fn <- freshTotalUninterpFn sym fn_name arg_types ret_type applySymFn sym fn args + +text :: String -> Doc ann +text = pretty diff --git a/what4/src/What4/Expr/MATLAB.hs b/what4/src/What4/Expr/MATLAB.hs index 4d2510ab..51186bda 100644 --- a/what4/src/What4/Expr/MATLAB.hs +++ b/what4/src/What4/Expr/MATLAB.hs @@ -45,7 +45,7 @@ import Data.Parameterized.Classes import Data.Parameterized.Context as Ctx import Data.Parameterized.TH.GADT import Data.Parameterized.TraversableFC -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) +import Prettyprinter import What4.BaseTypes import What4.Interface @@ -664,71 +664,74 @@ matlabSolverReturnType f = CplxCosFn -> knownRepr CplxTanFn -> knownRepr -ppMatlabSolverFn :: IsExpr f => MatlabSolverFn f a r -> Doc +ppMatlabSolverFn :: IsExpr f => MatlabSolverFn f a r -> Doc ann ppMatlabSolverFn f = case f of - BoolOrFn -> text "bool_or" - IsIntegerFn -> text "is_integer" - NatLeFn -> text "nat_le" - IntLeFn -> text "int_le" - BVToNatFn w -> parens $ text "bv_to_nat" <+> text (show w) - SBVToIntegerFn w -> parens $ text "sbv_to_int" <+> text (show w) - NatToIntegerFn -> text "nat_to_integer" - IntegerToNatFn -> text "integer_to_nat" - IntegerToRealFn -> text "integer_to_real" - RealToIntegerFn -> text "real_to_integer" - PredToIntegerFn -> text "pred_to_integer" - NatSeqFn b i -> parens $ text "nat_seq" <+> printSymExpr b <+> printSymExpr i - RealSeqFn b i -> parens $ text "real_seq" <+> printSymExpr b <+> printSymExpr i + BoolOrFn -> pretty "bool_or" + IsIntegerFn -> pretty "is_integer" + NatLeFn -> pretty "nat_le" + IntLeFn -> pretty "int_le" + BVToNatFn w -> parens $ pretty "bv_to_nat" <+> ppNatRepr w + SBVToIntegerFn w -> parens $ pretty "sbv_to_int" <+> ppNatRepr w + NatToIntegerFn -> pretty "nat_to_integer" + IntegerToNatFn -> pretty "integer_to_nat" + IntegerToRealFn -> pretty "integer_to_real" + RealToIntegerFn -> pretty "real_to_integer" + PredToIntegerFn -> pretty "pred_to_integer" + NatSeqFn b i -> parens $ pretty "nat_seq" <+> printSymExpr b <+> printSymExpr i + RealSeqFn b i -> parens $ pretty "real_seq" <+> printSymExpr b <+> printSymExpr i IndicesInRange _ bnds -> - parens (text "indices_in_range" <+> sep (toListFC printSymExpr bnds)) - IsEqFn{} -> text "is_eq" - - BVIsNonZeroFn w -> parens $ text "bv_is_nonzero" <+> text (show w) - ClampedIntNegFn w -> parens $ text "clamped_int_neg" <+> text (show w) - ClampedIntAbsFn w -> parens $ text "clamped_neg_abs" <+> text (show w) - ClampedIntAddFn w -> parens $ text "clamped_int_add" <+> text (show w) - ClampedIntSubFn w -> parens $ text "clamped_int_sub" <+> text (show w) - ClampedIntMulFn w -> parens $ text "clamped_int_mul" <+> text (show w) - ClampedUIntAddFn w -> parens $ text "clamped_uint_add" <+> text (show w) - ClampedUIntSubFn w -> parens $ text "clamped_uint_sub" <+> text (show w) - ClampedUIntMulFn w -> parens $ text "clamped_uint_mul" <+> text (show w) - - IntSetWidthFn i o -> parens $ text "int_set_width" <+> text (show i) <+> text (show o) - UIntSetWidthFn i o -> parens $ text "uint_set_width" <+> text (show i) <+> text (show o) - UIntToIntFn i o -> parens $ text "uint_to_int" <+> text (show i) <+> text (show o) - IntToUIntFn i o -> parens $ text "int_to_uint" <+> text (show i) <+> text (show o) - - RealCosFn -> text "real_cos" - RealSinFn -> text "real_sin" - RealIsNonZeroFn -> text "real_is_nonzero" - - RealToSBVFn w -> parens $ text "real_to_sbv" <+> text (show w) - RealToUBVFn w -> parens $ text "real_to_sbv" <+> text (show w) - PredToBVFn w -> parens $ text "pred_to_bv" <+> text (show w) - - CplxIsNonZeroFn -> text "cplx_is_nonzero" - CplxIsRealFn -> text "cplx_is_real" - RealToComplexFn -> text "real_to_complex" - RealPartOfCplxFn -> text "real_part_of_complex" - ImagPartOfCplxFn -> text "imag_part_of_complex" - - CplxNegFn -> text "cplx_neg" - CplxAddFn -> text "cplx_add" - CplxSubFn -> text "cplx_sub" - CplxMulFn -> text "cplx_mul" - - CplxRoundFn -> text "cplx_round" - CplxFloorFn -> text "cplx_floor" - CplxCeilFn -> text "cplx_ceil" - CplxMagFn -> text "cplx_mag" - CplxSqrtFn -> text "cplx_sqrt" - CplxExpFn -> text "cplx_exp" - CplxLogFn -> text "cplx_log" - CplxLogBaseFn b -> parens $ text "cplx_log_base" <+> text (show b) - CplxSinFn -> text "cplx_sin" - CplxCosFn -> text "cplx_cos" - CplxTanFn -> text "cplx_tan" + parens (pretty "indices_in_range" <+> sep (toListFC printSymExpr bnds)) + IsEqFn{} -> pretty "is_eq" + + BVIsNonZeroFn w -> parens $ pretty "bv_is_nonzero" <+> ppNatRepr w + ClampedIntNegFn w -> parens $ pretty "clamped_int_neg" <+> ppNatRepr w + ClampedIntAbsFn w -> parens $ pretty "clamped_neg_abs" <+> ppNatRepr w + ClampedIntAddFn w -> parens $ pretty "clamped_int_add" <+> ppNatRepr w + ClampedIntSubFn w -> parens $ pretty "clamped_int_sub" <+> ppNatRepr w + ClampedIntMulFn w -> parens $ pretty "clamped_int_mul" <+> ppNatRepr w + ClampedUIntAddFn w -> parens $ pretty "clamped_uint_add" <+> ppNatRepr w + ClampedUIntSubFn w -> parens $ pretty "clamped_uint_sub" <+> ppNatRepr w + ClampedUIntMulFn w -> parens $ pretty "clamped_uint_mul" <+> ppNatRepr w + + IntSetWidthFn i o -> parens $ pretty "int_set_width" <+> pretty (show i) <+> pretty (show o) + UIntSetWidthFn i o -> parens $ pretty "uint_set_width" <+> pretty (show i) <+> pretty (show o) + UIntToIntFn i o -> parens $ pretty "uint_to_int" <+> pretty (show i) <+> pretty (show o) + IntToUIntFn i o -> parens $ pretty "int_to_uint" <+> pretty (show i) <+> pretty (show o) + + RealCosFn -> pretty "real_cos" + RealSinFn -> pretty "real_sin" + RealIsNonZeroFn -> pretty "real_is_nonzero" + + RealToSBVFn w -> parens $ pretty "real_to_sbv" <+> ppNatRepr w + RealToUBVFn w -> parens $ pretty "real_to_sbv" <+> ppNatRepr w + PredToBVFn w -> parens $ pretty "pred_to_bv" <+> ppNatRepr w + + CplxIsNonZeroFn -> pretty "cplx_is_nonzero" + CplxIsRealFn -> pretty "cplx_is_real" + RealToComplexFn -> pretty "real_to_complex" + RealPartOfCplxFn -> pretty "real_part_of_complex" + ImagPartOfCplxFn -> pretty "imag_part_of_complex" + + CplxNegFn -> pretty "cplx_neg" + CplxAddFn -> pretty "cplx_add" + CplxSubFn -> pretty "cplx_sub" + CplxMulFn -> pretty "cplx_mul" + + CplxRoundFn -> pretty "cplx_round" + CplxFloorFn -> pretty "cplx_floor" + CplxCeilFn -> pretty "cplx_ceil" + CplxMagFn -> pretty "cplx_mag" + CplxSqrtFn -> pretty "cplx_sqrt" + CplxExpFn -> pretty "cplx_exp" + CplxLogFn -> pretty "cplx_log" + CplxLogBaseFn b -> parens $ pretty "cplx_log_base" <+> pretty (show b) + CplxSinFn -> pretty "cplx_sin" + CplxCosFn -> pretty "cplx_cos" + CplxTanFn -> pretty "cplx_tan" + +ppNatRepr :: NatRepr w -> Doc ann +ppNatRepr w = pretty (show w) -- | Test 'MatlabSolverFn' values for equality. testSolverFnEq :: TestEquality f diff --git a/what4/src/What4/Expr/VarIdentification.hs b/what4/src/What4/Expr/VarIdentification.hs index afb4d935..97422414 100644 --- a/what4/src/What4/Expr/VarIdentification.hs +++ b/what4/src/What4/Expr/VarIdentification.hs @@ -57,7 +57,7 @@ import qualified Data.Sequence as Seq import Data.Set (Set) import qualified Data.Set as Set import Data.Word -import Text.PrettyPrint.ANSI.Leijen +import Prettyprinter (Doc) import What4.BaseTypes import What4.Expr.AppTheory @@ -96,7 +96,7 @@ data CollectedVarInfo t , _forallQuantifiers :: !(QuantifierInfoMap t) , _latches :: !(Set (Some (ExprBoundVar t))) -- | List of errors found during parsing. - , _varErrors :: !(Seq Doc) + , _varErrors :: !(Seq (Doc ())) } -- | Describes types of functionality required by solver based on the problem. @@ -121,7 +121,7 @@ forallQuantifiers = lens _forallQuantifiers (\s v -> s { _forallQuantifiers = v latches :: Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t))) latches = lens _latches (\s v -> s { _latches = v }) -varErrors :: Simple Lens (CollectedVarInfo t) (Seq Doc) +varErrors :: Simple Lens (CollectedVarInfo t) (Seq (Doc ())) varErrors = lens _varErrors (\s v -> s { _varErrors = v }) -- | Return variables needed to define element as a predicate diff --git a/what4/src/What4/FunctionName.hs b/what4/src/What4/FunctionName.hs index 53348b5a..1cf290fe 100644 --- a/what4/src/What4/FunctionName.hs +++ b/what4/src/What4/FunctionName.hs @@ -21,7 +21,7 @@ module What4.FunctionName import Data.Hashable import Data.String import qualified Data.Text as Text -import qualified Text.PrettyPrint.ANSI.Leijen as PP +import qualified Prettyprinter as PP ------------------------------------------------------------------------ -- FunctionName @@ -38,7 +38,7 @@ instance Show FunctionName where show (FunctionName nm) = Text.unpack nm instance PP.Pretty FunctionName where - pretty (FunctionName nm) = PP.text (Text.unpack nm) + pretty (FunctionName nm) = PP.pretty nm -- | Name of function for starting simulator. startFunctionName :: FunctionName diff --git a/what4/src/What4/Interface.hs b/what4/src/What4/Interface.hs index 4b83f05f..427da197 100644 --- a/what4/src/What4/Interface.hs +++ b/what4/src/What4/Interface.hs @@ -183,7 +183,7 @@ import Data.Ratio import Data.Scientific (Scientific) import GHC.Generics (Generic) import Numeric.Natural -import Text.PrettyPrint.ANSI.Leijen (Doc) +import Prettyprinter (Doc) import What4.BaseTypes import What4.Config @@ -348,7 +348,7 @@ class HasAbsValue e => IsExpr e where BaseBVRepr w -> w -- | Print a sym expression for debugging or display purposes. - printSymExpr :: e tp -> Doc + printSymExpr :: e tp -> Doc ann newtype ArrayResultWrapper f idx tp = diff --git a/what4/src/What4/InterpretedFloatingPoint.hs b/what4/src/What4/InterpretedFloatingPoint.hs index fcf5d264..47b146c1 100644 --- a/what4/src/What4/InterpretedFloatingPoint.hs +++ b/what4/src/What4/InterpretedFloatingPoint.hs @@ -50,7 +50,7 @@ import Data.Parameterized.TH.GADT import Data.Ratio import Data.Word ( Word16, Word64 ) import GHC.TypeNats -import Text.PrettyPrint.ANSI.Leijen +import Prettyprinter import What4.BaseTypes import What4.Interface @@ -97,7 +97,7 @@ instance Hashable (FloatInfoRepr fi) where hashWithSalt = $(structuralHashWithSalt [t|FloatInfoRepr|] []) instance Pretty (FloatInfoRepr fi) where - pretty = text . show + pretty = pretty . show instance Show (FloatInfoRepr fi) where showsPrec = $(structuralShowsPrec [t|FloatInfoRepr|]) instance ShowF FloatInfoRepr diff --git a/what4/src/What4/ProgramLoc.hs b/what4/src/What4/ProgramLoc.hs index 2b4fea3a..771a8c8b 100644 --- a/what4/src/What4/ProgramLoc.hs +++ b/what4/src/What4/ProgramLoc.hs @@ -38,7 +38,7 @@ import Data.Text (Text) import qualified Data.Text as Text import Data.Word import Numeric (showHex) -import qualified Text.PrettyPrint.ANSI.Leijen as PP +import qualified Prettyprinter as PP import What4.FunctionName @@ -73,23 +73,23 @@ startOfFile path = sourcePos path 1 0 instance PP.Pretty Position where pretty (SourcePos path l c) = - PP.text (Text.unpack path) - PP.<> PP.colon PP.<> PP.int l - PP.<> PP.colon PP.<> PP.int c + PP.pretty path + PP.<> PP.colon PP.<> PP.pretty l + PP.<> PP.colon PP.<> PP.pretty c pretty (BinaryPos path addr) = - PP.text (Text.unpack path) PP.<> PP.colon PP.<> - PP.text "0x" PP.<> PP.text (showHex addr "") - pretty (OtherPos txt) = PP.text (Text.unpack txt) - pretty InternalPos = PP.text "internal" + PP.pretty path PP.<> PP.colon PP.<> + PP.pretty "0x" PP.<> PP.pretty (showHex addr "") + pretty (OtherPos txt) = PP.pretty txt + pretty InternalPos = PP.pretty "internal" -ppNoFileName :: Position -> PP.Doc +ppNoFileName :: Position -> PP.Doc ann ppNoFileName (SourcePos _ l c) = - PP.int l PP.<> PP.colon PP.<> PP.int c + PP.pretty l PP.<> PP.colon PP.<> PP.pretty c ppNoFileName (BinaryPos _ addr) = - PP.text (showHex addr "") + PP.pretty (showHex addr "") ppNoFileName (OtherPos msg) = - PP.text (Text.unpack msg) -ppNoFileName InternalPos = PP.text "internal" + PP.pretty msg +ppNoFileName InternalPos = PP.pretty "internal" ------------------------------------------------------------------------ -- Posd diff --git a/what4/src/What4/Protocol/Online.hs b/what4/src/What4/Protocol/Online.hs index a3cd89f8..75e3223c 100644 --- a/what4/src/What4/Protocol/Online.hs +++ b/what4/src/What4/Protocol/Online.hs @@ -48,12 +48,12 @@ import Data.Proxy import Data.IORef import Data.Text (Text) import qualified Data.Text.Lazy as LazyText +import Prettyprinter import System.Exit import System.IO import qualified System.IO.Streams as Streams import System.Process (ProcessHandle, terminateProcess, waitForProcess) -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>)) import What4.Expr import What4.Interface (SolverEvent(..)) @@ -361,7 +361,7 @@ getUnsatAssumptions :: SMTReadWriter solver => SolverProcess scope solver -> IO getUnsatAssumptions proc = do let conn = solverConn proc unless (supportedFeatures conn `hasProblemFeature` useUnsatAssumptions) $ - fail $ show $ text (smtWriterName conn) <+> text "is not configured to produce UNSAT assumption lists" + fail $ show $ pretty (smtWriterName conn) <+> pretty "is not configured to produce UNSAT assumption lists" addCommandNoAck conn (getUnsatAssumptionsCommand conn) smtUnsatAssumptionsResult conn (solverResponse proc) @@ -372,7 +372,7 @@ getUnsatCore :: SMTReadWriter solver => SolverProcess scope solver -> IO [Text] getUnsatCore proc = do let conn = solverConn proc unless (supportedFeatures conn `hasProblemFeature` useUnsatCores) $ - fail $ show $ text (smtWriterName conn) <+> text "is not configured to produce UNSAT cores" + fail $ show $ pretty (smtWriterName conn) <+> pretty "is not configured to produce UNSAT cores" addCommandNoAck conn (getUnsatCoreCommand conn) smtUnsatCoreResult conn (solverResponse proc) diff --git a/what4/src/What4/Protocol/PolyRoot.hs b/what4/src/What4/Protocol/PolyRoot.hs index 692fe58a..aefd889d 100644 --- a/what4/src/What4/Protocol/PolyRoot.hs +++ b/what4/src/What4/Protocol/PolyRoot.hs @@ -32,7 +32,7 @@ import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Vector as V -import Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>)) +import Prettyprinter as PP atto_angle :: Atto.Parser a -> Atto.Parser a atto_angle p = Atto.char '<' *> p <* Atto.char '>' @@ -47,19 +47,19 @@ newtype SingPoly coef = SingPoly (V.Vector coef) instance (Ord coef, Num coef, Pretty coef) => Pretty (SingPoly coef) where pretty (SingPoly v) = case V.findIndex (/= 0) v of - Nothing -> text "0" + Nothing -> pretty "0" Just j -> go (V.length v - 1) where ppc c | c < 0 = parens (pretty c) | otherwise = pretty c - ppi 1 = text "*x" - ppi i = text "*x^" <> pretty i + ppi 1 = pretty "*x" + ppi i = pretty "*x^" <> pretty i go 0 = ppc (v V.! 0) go i | seq i False = error "pretty SingPoly" | i == j = ppc (v V.! i) <> ppi i | v V.! i == 0 = go (i-1) - | otherwise = ppc (v V.! i) <> ppi i <+> text "+" <+> go (i-1) + | otherwise = ppc (v V.! i) <> ppi i <+> pretty "+" <+> go (i-1) fromList :: [c] -> SingPoly c fromList = SingPoly . V.fromList diff --git a/what4/src/What4/Protocol/SMTLib2.hs b/what4/src/What4/Protocol/SMTLib2.hs index 825d3d99..124dacc4 100644 --- a/what4/src/What4/Protocol/SMTLib2.hs +++ b/what4/src/What4/Protocol/SMTLib2.hs @@ -121,7 +121,7 @@ import qualified System.IO.Streams as Streams import qualified System.IO.Streams.Attoparsec.Text as Streams import Data.Versions (Version(..)) import qualified Data.Versions as Versions -import qualified Text.PrettyPrint.ANSI.Leijen as PP +import qualified Prettyprinter as PP import Prelude hiding (writeFile) @@ -1167,14 +1167,17 @@ solverMaxVersions = [] data SolverVersionCheckError = UnparseableVersion Versions.ParsingError -ppSolverVersionCheckError :: SolverVersionCheckError -> PP.Doc -ppSolverVersionCheckError = - (PP.text "Unexpected error while checking solver version: " PP.<$$>) . - \case - UnparseableVersion parseErr -> PP.cat $ map PP.text - [ "Couldn't parse solver version number: " - , show parseErr - ] +ppSolverVersionCheckError :: SolverVersionCheckError -> PP.Doc ann +ppSolverVersionCheckError err = + PP.vsep + [ "Unexpected error while checking solver version:" + , case err of + UnparseableVersion parseErr -> + PP.hsep $ map PP.pretty + [ "Couldn't parse solver version number:" + , show parseErr + ] + ] data SolverVersionError = SolverVersionError @@ -1184,9 +1187,10 @@ data SolverVersionError = } deriving (Eq, Ord) -ppSolverVersionError :: SolverVersionError -> PP.Doc -ppSolverVersionError err = PP.vcat $ map PP.text - [ "Solver did not meet version bound restrictions: " +ppSolverVersionError :: SolverVersionError -> PP.Doc ann +ppSolverVersionError err = + PP.vsep $ map PP.pretty + [ "Solver did not meet version bound restrictions:" , "Lower bound (inclusive): " ++ na (show <$> vMin err) , "Upper bound (non-inclusive): " ++ na (show <$> vMax err) , "Actual version: " ++ show (vActual err) diff --git a/what4/src/What4/Protocol/SMTWriter.hs b/what4/src/What4/Protocol/SMTWriter.hs index 5bbb5766..0ee24d4e 100644 --- a/what4/src/What4/Protocol/SMTWriter.hs +++ b/what4/src/What4/Protocol/SMTWriter.hs @@ -132,7 +132,7 @@ import qualified Data.Text.Lazy as Lazy import Data.Word import Numeric.Natural -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>)) +import Prettyprinter hiding (Unbounded) import System.IO.Streams (OutputStream, InputStream) import qualified System.IO.Streams as Streams @@ -1484,9 +1484,11 @@ sbvIntTerm w0 x0 = sumExpr (signed_offset : go w0 x0 (natValue w0 - 2)) unsupportedTerm :: MonadFail m => Expr t tp -> m a unsupportedTerm e = fail $ show $ - text "Cannot generate solver output for term generated at" - <+> pretty (plSourceLoc (exprLoc e)) <> text ":" <$$> - indent 2 (pretty e) + vcat + [ text "Cannot generate solver output for term generated at" + <+> pretty (plSourceLoc (exprLoc e)) <> text ":" + , indent 2 (pretty e) + ] -- | Checks whether a variable is supported. -- @@ -1575,22 +1577,24 @@ checkArgumentTypes conn types = do -- | This generates an error message from a solver and a type error. -- -- It issed for error reporting -type SMTSource = String -> BaseTypeError -> Doc +type SMTSource ann = String -> BaseTypeError -> Doc ann -ppBaseTypeError :: BaseTypeError -> Doc +ppBaseTypeError :: BaseTypeError -> Doc ann ppBaseTypeError ComplexTypeUnsupported = text "complex values" ppBaseTypeError ArrayUnsupported = text "arrays encoded as a functions" ppBaseTypeError (StringTypeUnsupported (Some si)) = text ("string values " ++ show si) -eltSource :: Expr t tp -> SMTSource +eltSource :: Expr t tp -> SMTSource ann eltSource e solver_name cause = - text solver_name <+> - text "does not support" <+> ppBaseTypeError cause <> - text ", and cannot interpret the term generated at" <+> - pretty (plSourceLoc (exprLoc e)) <> text ":" <$$> - indent 2 (pretty e) <> text "." - -fnSource :: SolverSymbol -> ProgramLoc -> SMTSource + vcat + [ text solver_name <+> + text "does not support" <+> ppBaseTypeError cause <> + text ", and cannot interpret the term generated at" <+> + pretty (plSourceLoc (exprLoc e)) <> text ":" + , indent 2 (pretty e) <> text "." + ] + +fnSource :: SolverSymbol -> ProgramLoc -> SMTSource ann fnSource fn_name loc solver_name cause = text solver_name <+> text "does not support" <+> ppBaseTypeError cause <> @@ -1603,7 +1607,7 @@ fnSource fn_name loc solver_name cause = -- returned by functions. evalFirstClassTypeRepr :: MonadFail m => WriterConn t h - -> SMTSource + -> SMTSource ann -> BaseTypeRepr tp -> m (TypeMap tp) evalFirstClassTypeRepr conn src base_tp = @@ -1895,10 +1899,13 @@ appSMTExpr ae = do let ytp = smtExprType ye let checkArrayType z (FnArrayTypeMap{}) = do - fail $ show $ text (smtWriterName conn) <+> - text "does not support checking equality for the array generated at" - <+> pretty (plSourceLoc (exprLoc z)) <> text ":" <$$> - indent 2 (pretty z) + fail $ show $ + vcat + [ text (smtWriterName conn) <+> + text "does not support checking equality for the array generated at" + <+> pretty (plSourceLoc (exprLoc z)) <> text ":" + , indent 2 (pretty z) + ] checkArrayType _ _ = return () checkArrayType x xtp @@ -3059,3 +3066,6 @@ smtExprGroundEvalFn conn smtFns = do return $ GroundEvalFn cachedEval + +text :: String -> Doc ann +text = pretty diff --git a/what4/src/What4/Solver/Adapter.hs b/what4/src/What4/Solver/Adapter.hs index 774602b1..153752d7 100644 --- a/what4/src/What4/Solver/Adapter.hs +++ b/what4/src/What4/Solver/Adapter.hs @@ -29,7 +29,7 @@ import Data.IORef import qualified Data.Map as Map import qualified Data.Text as T import System.IO -import qualified Text.PrettyPrint.ANSI.Leijen as PP +import qualified Prettyprinter as PP import What4.BaseTypes @@ -129,7 +129,7 @@ solverAdapterOptions xs@(def:_) = vals ref = Map.fromList (map (f ref) xs) sty ref = mkOpt defaultSolverAdapter (listOptSty (vals ref)) - (Just (PP.text "Indicates which solver to use for check-sat queries")) + (Just (PP.pretty "Indicates which solver to use for check-sat queries")) (Just (ConcreteString (UnicodeLiteral (T.pack (solver_adapter_name def))))) -- | Test the ability to interact with a solver by peforming a check-sat query diff --git a/what4/src/What4/Solver/Boolector.hs b/what4/src/What4/Solver/Boolector.hs index cb42cf8a..633ade95 100644 --- a/what4/src/What4/Solver/Boolector.hs +++ b/what4/src/What4/Solver/Boolector.hs @@ -28,7 +28,6 @@ module What4.Solver.Boolector import Control.Monad import Data.Bits ( (.|.) ) -import qualified Text.PrettyPrint.ANSI.Leijen as PP import What4.BaseTypes import What4.Config @@ -57,7 +56,7 @@ boolectorOptions = [ mkOpt boolectorPath executablePathOptSty - (Just (PP.text "Path to boolector executable")) + (Just "Path to boolector executable") (Just (ConcreteString "boolector")) ] diff --git a/what4/src/What4/Solver/CVC4.hs b/what4/src/What4/Solver/CVC4.hs index 56004584..442e6628 100644 --- a/what4/src/What4/Solver/CVC4.hs +++ b/what4/src/What4/Solver/CVC4.hs @@ -33,7 +33,6 @@ import Data.Bits import Data.String import System.IO import qualified System.IO.Streams as Streams -import qualified Text.PrettyPrint.ANSI.Leijen as PP import What4.BaseTypes import What4.Config @@ -72,12 +71,12 @@ cvc4Options :: [ConfigDesc] cvc4Options = [ mkOpt cvc4Path executablePathOptSty - (Just (PP.text "Path to CVC4 executable")) + (Just "Path to CVC4 executable") (Just (ConcreteString "cvc4")) , intWithRangeOpt cvc4RandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1) , mkOpt cvc4Timeout integerOptSty - (Just (PP.text "Per-check timeout in milliseconds (zero is none)")) + (Just "Per-check timeout in milliseconds (zero is none)") (Just (ConcreteInteger 0)) ] diff --git a/what4/src/What4/Solver/DReal.hs b/what4/src/What4/Solver/DReal.hs index c54b9556..6ded04e8 100644 --- a/what4/src/What4/Solver/DReal.hs +++ b/what4/src/What4/Solver/DReal.hs @@ -45,7 +45,6 @@ import System.IO.Error import qualified System.IO.Streams as Streams import qualified System.IO.Streams.Attoparsec as Streams import System.Process -import qualified Text.PrettyPrint.ANSI.Leijen as PP import What4.BaseTypes import What4.Config @@ -73,7 +72,7 @@ drealOptions = [ mkOpt drealPath executablePathOptSty - (Just (PP.text "Path to dReal executable")) + (Just "Path to dReal executable") (Just (ConcreteString "dreal")) ] diff --git a/what4/src/What4/Solver/STP.hs b/what4/src/What4/Solver/STP.hs index 3787c722..c8c2d1bd 100644 --- a/what4/src/What4/Solver/STP.hs +++ b/what4/src/What4/Solver/STP.hs @@ -23,7 +23,6 @@ module What4.Solver.STP ) where import Data.Bits -import qualified Text.PrettyPrint.ANSI.Leijen as PP import What4.BaseTypes import What4.Config @@ -55,7 +54,7 @@ stpOptions :: [ConfigDesc] stpOptions = [ mkOpt stpPath executablePathOptSty - (Just (PP.text "Path to STP executable.")) + (Just "Path to STP executable.") (Just (ConcreteString "stp")) , intWithRangeOpt stpRandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1) ] diff --git a/what4/src/What4/Solver/Yices.hs b/what4/src/What4/Solver/Yices.hs index 3fea541e..3fddaed3 100644 --- a/what4/src/What4/Solver/Yices.hs +++ b/what4/src/What4/Solver/Yices.hs @@ -99,7 +99,7 @@ import System.Exit import System.IO import qualified System.IO.Streams as Streams import qualified System.IO.Streams.Attoparsec.Text as Streams -import qualified Text.PrettyPrint.ANSI.Leijen as PP +import qualified Prettyprinter as PP import What4.BaseTypes import What4.Config @@ -935,22 +935,22 @@ yicesOptions = [ mkOpt yicesPath executablePathOptSty - (Just (PP.text "Yices executable path")) + (Just "Yices executable path") (Just (ConcreteString "yices")) , mkOpt yicesEnableMCSat boolOptSty - (Just (PP.text "Enable the Yices MCSAT solving engine")) + (Just "Enable the Yices MCSAT solving engine") (Just (ConcreteBool False)) , mkOpt yicesEnableInteractive boolOptSty - (Just (PP.text "Enable Yices interactive mode (needed to support timeouts)")) + (Just "Enable Yices interactive mode (needed to support timeouts)") (Just (ConcreteBool False)) , mkOpt yicesGoalTimeout integerOptSty - (Just (PP.text "Set a per-goal timeout")) + (Just "Set a per-goal timeout") (Just (ConcreteInteger 0)) ] ++ yicesInternalOptions @@ -1073,8 +1073,8 @@ checkSupportedByYices p = do -- Check no errors where reported in result. let errors = toList (varInfo^.varErrors) when (not (null errors)) $ do - fail $ show $ PP.text "This formula is not supported by yices:" PP.<$$> - PP.indent 2 (PP.vcat errors) + fail $ show $ + PP.vcat ["This formula is not supported by yices:", PP.indent 2 (PP.vcat errors)] return $! varInfo^.problemFeatures diff --git a/what4/src/What4/Solver/Z3.hs b/what4/src/What4/Solver/Z3.hs index a26c16dd..21d842fe 100644 --- a/what4/src/What4/Solver/Z3.hs +++ b/what4/src/What4/Solver/Z3.hs @@ -31,7 +31,6 @@ import Control.Monad ( when ) import Data.Bits import Data.String import System.IO -import qualified Text.PrettyPrint.ANSI.Leijen as PP import What4.BaseTypes import What4.Concrete @@ -63,12 +62,12 @@ z3Options = [ mkOpt z3Path executablePathOptSty - (Just (PP.text "Z3 executable path")) + (Just "Z3 executable path") (Just (ConcreteString "z3")) , mkOpt z3Timeout integerOptSty - (Just (PP.text "Per-check timeout in milliseconds (zero is none)")) + (Just "Per-check timeout in milliseconds (zero is none)") (Just (ConcreteInteger 0)) ] diff --git a/what4/what4.cabal b/what4/what4.cabal index b7ffa255..6e304a15 100644 --- a/what4/what4.cabal +++ b/what4/what4.cabal @@ -52,7 +52,6 @@ library build-depends: base >= 4.8 && < 5, attoparsec >= 0.13, - ansi-wl-pprint >= 0.6.8, bimap >= 0.2, bifunctors >= 5, bv-sized >= 1.0.0, @@ -73,6 +72,7 @@ library mtl >= 2.2.1, panic >= 0.3, parameterized-utils >= 2.1 && < 2.2, + prettyprinter >= 1.7.0, process >= 1.2, scientific >= 0.3.6, temporary >= 1.2,