GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-12-01 20:23:10 +03:00
Code Issues Projects Releases Wiki Activity

Switch from ansi-wl-pprint to the prettyprinter package.

Browse Source 
This patch converts packages `what4`, `what4-abc`, and `what4-blt`.
This commit is contained in:
Brian Huffman 2020-11-22 09:34:48 -08:00
parent 419ed1d899
commit 0a1ec94056
27 changed files with 280 additions and 241 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
what4-abc/src/What4/Solver/ABC.hs
View File

@ -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

2
what4-abc/what4-abc.cabal
View File

@ -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,

18
what4-blt/src/What4/Solver/BLT.hs
View File

@ -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

2
what4-blt/what4-blt.cabal
View File

@ -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

8
what4/src/What4/BaseTypes.hs
View File

@ -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

30
what4/src/What4/Concrete.hs
View File

@ -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 ")"

60
what4/src/What4/Config.hs
View File

@ -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

12
what4/src/What4/Expr/App.hs
View File

@ -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

72
what4/src/What4/Expr/Builder.hs
View File

@ -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

115
what4/src/What4/Expr/MATLAB.hs
View File

@ -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"
parens (pretty "indices_in_range" <+> sep (toListFC printSymExpr bnds))
IsEqFn{} -> pretty "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)
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 $ 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)
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 -> text "real_cos"
RealSinFn -> text "real_sin"
RealIsNonZeroFn -> text "real_is_nonzero"
RealCosFn -> pretty "real_cos"
RealSinFn -> pretty "real_sin"
RealIsNonZeroFn -> pretty "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)
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 -> 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"
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 -> text "cplx_neg"
CplxAddFn -> text "cplx_add"
CplxSubFn -> text "cplx_sub"
CplxMulFn -> text "cplx_mul"
CplxNegFn -> pretty "cplx_neg"
CplxAddFn -> pretty "cplx_add"
CplxSubFn -> pretty "cplx_sub"
CplxMulFn -> pretty "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"
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

6
what4/src/What4/Expr/VarIdentification.hs
View File

@ -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

4
what4/src/What4/FunctionName.hs
View File

@ -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

4
what4/src/What4/Interface.hs
View File

@ -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 =

4
what4/src/What4/InterpretedFloatingPoint.hs
View File

@ -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

26
what4/src/What4/ProgramLoc.hs
View File

@ -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

6
what4/src/What4/Protocol/Online.hs
View File

@ -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)

10
what4/src/What4/Protocol/PolyRoot.hs
View File

@ -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

20
what4/src/What4/Protocol/SMTLib2.hs
View File

@ -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
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,8 +1187,9 @@ data SolverVersionError =
}
deriving (Eq, Ord)
ppSolverVersionError :: SolverVersionError -> PP.Doc
ppSolverVersionError err = PP.vcat $ map PP.text
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)

40
what4/src/What4/Protocol/SMTWriter.hs
View File

@ -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 <+>
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 "."
pretty (plSourceLoc (exprLoc e)) <> text ":"
, indent 2 (pretty e) <> text "."
]
fnSource :: SolverSymbol -> ProgramLoc -> SMTSource
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) <+>
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)
<+> 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

4
what4/src/What4/Solver/Adapter.hs
View File

@ -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

3
what4/src/What4/Solver/Boolector.hs
View File

@ -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"))
]

5
what4/src/What4/Solver/CVC4.hs
View File

@ -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))
]

3
what4/src/What4/Solver/DReal.hs
View File

@ -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"))
]

3
what4/src/What4/Solver/STP.hs
View File

@ -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)
]

14
what4/src/What4/Solver/Yices.hs
View File

@ -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

5
what4/src/What4/Solver/Z3.hs
View File

@ -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))
]

2
what4/what4.cabal
View File

@ -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,