what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Serialize.Printer

Synopsis

- serializeExpr :: Expr t tp -> SExpr
- serializeExprWithConfig :: Config -> Expr t tp -> Result t
- serializeSymFn :: ExprSymFn t dom ret -> SExpr
- serializeSymFnWithConfig :: Config -> ExprSymFn t dom ret -> Result t
- serializeBaseType :: BaseTypeRepr tp -> SExpr
- convertBaseTypes :: Assignment BaseTypeRepr tps -> [SExpr]
- data Config = Config {
  - cfgAllowFreeVars :: Bool
  - cfgAllowFreeSymFns :: Bool
  }
- data Result t = Result {
  - resSExpr :: WellFormedSExpr Atom
  - resFreeVarEnv :: VarNameEnv t
  - resSymFnEnv :: FnNameEnv t
  }
- printSExpr :: Seq String -> SExpr -> Text
- defaultConfig :: Config
- type SExpr = WellFormedSExpr Atom
- data Atom
  - = AId Text
  - | AStr (Some StringInfoRepr) Text
  - | AInt Integer
  - | ANat Natural
  - | AReal Rational
  - | AFloat (Some FloatPrecisionRepr) BigFloat
  - | ABV Int Integer
  - | ABool Bool
- data SomeExprSymFn t = forall dom ret. SomeExprSymFn (ExprSymFn t dom ret)
- data WellFormedSExpr atom
  - = WFSList [WellFormedSExpr atom]
  - | WFSAtom atom
- ident :: Text -> SExpr
- int :: Integer -> SExpr
- string :: Some StringInfoRepr -> Text -> SExpr
- bitvec :: Natural -> Integer -> SExpr
- bool :: Bool -> SExpr
- nat :: Natural -> SExpr
- real :: Rational -> SExpr
- ppFreeVarEnv :: VarNameEnv t -> String
- ppFreeSymFnEnv :: FnNameEnv t -> String
- pattern L :: [WellFormedSExpr t] -> WellFormedSExpr t
- pattern A :: t -> WellFormedSExpr t

# Documentation

serializeExpr :: Expr t tp -> SExpr Source #

Serialize a What4 Expr as a well-formed s-expression (i.e., one which contains no improper lists). Equivalent to `(resSExpr (serializeExpr' defaultConfig))`. Sharing in the AST is achieved via a top-level let-binding around the emitted expression (unless there are no terms with non-atomic terms which can be shared).

serializeExprWithConfig :: Config -> Expr t tp -> Result t Source #

Serialize a What4 Expr as a well-formed s-expression (i.e., one which contains no improper lists) according to the configuration. Sharing in the AST is achieved via a top-level let-binding around the emitted expression (unless there are no terms with non-atomic terms which can be shared).

serializeSymFn :: ExprSymFn t dom ret -> SExpr Source #

Serialize a What4 ExprSymFn as a well-formed s-expression (i.e., one which contains no improper lists). Equivalent to `(resSExpr (serializeSymFn' defaultConfig))`. Sharing in the AST is achieved via a top-level let-binding around the emitted expression (unless there are no terms with non-atomic terms which can be shared).

serializeSymFnWithConfig :: Config -> ExprSymFn t dom ret -> Result t Source #

Serialize a What4 ExprSymFn as a well-formed s-expression (i.e., one which contains no improper lists) according to the configuration. Sharing in the AST is achieved via a top-level let-binding around the emitted expression (unless there are no terms with non-atomic terms which can be shared).

serializeBaseType :: BaseTypeRepr tp -> SExpr Source #

convertBaseTypes :: Assignment BaseTypeRepr tps -> [SExpr] Source #

Convert an Assignment of base types into a list of base types SExpr, where the left-to-right syntactic ordering of the types is maintained.

data Config Source #

Controls how expressions and functions are serialized.

Constructors

Config |

Fields

- cfgAllowFreeVars :: Bool

  When `True`, any free What4 `ExprBoundVar` encountered is simply serialized with a unique name, and the mapping from What4 ExprBoundVar to unique names is returned after serialization. When False, an error is raised when a "free" `ExprBoundVar` is encountered.

- cfgAllowFreeSymFns :: Bool

  When `True`, any encountered What4 `ExprSymFn` during serialization is simply assigned a unique name and the mapping from What4 ExprSymFn to unique name is returned after serialization. When @False, encountered ExprSymFns are serialized at the top level of the expression in a `(letfn ([f ...]) ...)`.

data Result t Source #

Constructors

Result |

Fields

- resSExpr :: WellFormedSExpr Atom

  The serialized term.

- resFreeVarEnv :: VarNameEnv t

  The free BoundVars that were encountered during serialization and their associated fresh name that was used to generate the s-expression.

- resSymFnEnv :: FnNameEnv t

  The SymFns that were encountered during serialization and their associated fresh name that was used to generate the s-expression.

printSExpr :: Seq String -> SExpr -> Text Source #

Generates the the S-expression tokens represented by the sexpr argument, preceeded by a list of strings output as comments.

defaultConfig :: Config Source #

type SExpr = WellFormedSExpr Atom Source #

data Atom Source #

Constructors

AId Text | An identifier.
AStr (Some StringInfoRepr) Text | A prefix followed by a string literal (.e.g, AStr "u" "Hello World" is serialize as `#u"Hello World"`).
AInt Integer | Integer (i.e., unbounded) literal.
ANat Natural | Natural (i.e., unbounded) literal
AReal Rational | Real (i.e., unbounded) literal.
AFloat (Some FloatPrecisionRepr) BigFloat | A floating point literal (with precision)
ABV Int Integer | Bitvector, width and then value.
ABool Bool | Boolean literal.

#### Instances

Instances details

Show Atom Source # |
Instance details Defined in What4.Serialize.SETokens Methods showsPrec :: Int -> Atom -> ShowS Source # show :: Atom -> String Source # showList :: [Atom] -> ShowS Source #
Eq Atom Source # |
Instance details Defined in What4.Serialize.SETokens Methods (==) :: Atom -> Atom -> Bool Source # (/=) :: Atom -> Atom -> Bool Source #
Ord Atom Source # |
Instance details Defined in What4.Serialize.SETokens Methods compare :: Atom -> Atom -> Ordering Source # (<) :: Atom -> Atom -> Bool Source # (<=) :: Atom -> Atom -> Bool Source # (>) :: Atom -> Atom -> Bool Source # (>=) :: Atom -> Atom -> Bool Source # max :: Atom -> Atom -> Atom Source # min :: Atom -> Atom -> Atom Source #

data SomeExprSymFn t Source #

Constructors

forall dom ret. SomeExprSymFn (ExprSymFn t dom ret) |

#### Instances

Instances details

Show (SomeExprSymFn t) Source # |
Instance details Defined in What4.Serialize.Printer Methods showsPrec :: Int -> SomeExprSymFn t -> ShowS Source # show :: SomeExprSymFn t -> String Source # showList :: [SomeExprSymFn t] -> ShowS Source #
Eq (SomeExprSymFn t) Source # |
Instance details Defined in What4.Serialize.Printer Methods (==) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source # (/=) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source #
Ord (SomeExprSymFn t) Source # |

Instance details

Defined in What4.Serialize.Printer

Methods

compare :: SomeExprSymFn t -> SomeExprSymFn t -> Ordering Source #

(<) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source #

(<=) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source #

(>) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source #

(>=) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source #

max :: SomeExprSymFn t -> SomeExprSymFn t -> SomeExprSymFn t Source #

min :: SomeExprSymFn t -> SomeExprSymFn t -> SomeExprSymFn t Source #

data WellFormedSExpr atom Source #

A well-formed s-expression is one which does not contain any dotted lists. This means that not every value of `SExpr a` can be converted to a `WellFormedSExpr a`, although the opposite is fine.

Constructors

WFSList [WellFormedSExpr atom] |
WFSAtom atom |

#### Instances

Instances details

Foldable WellFormedSExpr |

Instance details

Defined in Data.SCargot.Repr

Methods

fold :: Monoid m => WellFormedSExpr m -> m Source #

foldMap :: Monoid m => (a -> m) -> WellFormedSExpr a -> m Source #

foldMap' :: Monoid m => (a -> m) -> WellFormedSExpr a -> m Source #

foldr :: (a -> b -> b) -> b -> WellFormedSExpr a -> b Source #

foldr' :: (a -> b -> b) -> b -> WellFormedSExpr a -> b Source #

foldl :: (b -> a -> b) -> b -> WellFormedSExpr a -> b Source #

foldl' :: (b -> a -> b) -> b -> WellFormedSExpr a -> b Source #

foldr1 :: (a -> a -> a) -> WellFormedSExpr a -> a Source #

foldl1 :: (a -> a -> a) -> WellFormedSExpr a -> a Source #

toList :: WellFormedSExpr a -> [a] Source #

null :: WellFormedSExpr a -> Bool Source #

length :: WellFormedSExpr a -> Int Source #

elem :: Eq a => a -> WellFormedSExpr a -> Bool Source #

maximum :: Ord a => WellFormedSExpr a -> a Source #

minimum :: Ord a => WellFormedSExpr a -> a Source #

sum :: Num a => WellFormedSExpr a -> a Source #

product :: Num a => WellFormedSExpr a -> a Source #

Traversable WellFormedSExpr |
Instance details Defined in Data.SCargot.Repr Methods traverse :: Applicative f => (a -> f b) -> WellFormedSExpr a -> f (WellFormedSExpr b) Source # sequenceA :: Applicative f => WellFormedSExpr (f a) -> f (WellFormedSExpr a) Source # mapM :: Monad m => (a -> m b) -> WellFormedSExpr a -> m (WellFormedSExpr b) Source # sequence :: Monad m => WellFormedSExpr (m a) -> m (WellFormedSExpr a) Source #
Functor WellFormedSExpr |
Instance details Defined in Data.SCargot.Repr Methods fmap :: (a -> b) -> WellFormedSExpr a -> WellFormedSExpr b Source # (<$) :: a -> WellFormedSExpr b -> WellFormedSExpr a Source #
Data atom => Data (WellFormedSExpr atom) |

Instance details

Defined in Data.SCargot.Repr

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WellFormedSExpr atom -> c (WellFormedSExpr atom) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WellFormedSExpr atom) Source #

toConstr :: WellFormedSExpr atom -> Constr Source #

dataTypeOf :: WellFormedSExpr atom -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WellFormedSExpr atom)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WellFormedSExpr atom)) Source #

gmapT :: (forall b. Data b => b -> b) -> WellFormedSExpr atom -> WellFormedSExpr atom Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WellFormedSExpr atom -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WellFormedSExpr atom -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> WellFormedSExpr atom -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> WellFormedSExpr atom -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WellFormedSExpr atom -> m (WellFormedSExpr atom) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WellFormedSExpr atom -> m (WellFormedSExpr atom) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WellFormedSExpr atom -> m (WellFormedSExpr atom) Source #

IsString atom => IsString (WellFormedSExpr atom) |
Instance details Defined in Data.SCargot.Repr Methods fromString :: String -> WellFormedSExpr atom Source #
IsList (WellFormedSExpr atom) |
Instance details Defined in Data.SCargot.Repr Associated Types type Item (WellFormedSExpr atom) Source # Methods fromList :: [Item (WellFormedSExpr atom)] -> WellFormedSExpr atom Source # fromListN :: Int -> [Item (WellFormedSExpr atom)] -> WellFormedSExpr atom Source # toList :: WellFormedSExpr atom -> [Item (WellFormedSExpr atom)] Source #
Read atom => Read (WellFormedSExpr atom) |
Instance details Defined in Data.SCargot.Repr Methods readsPrec :: Int -> ReadS (WellFormedSExpr atom) Source # readList :: ReadS [WellFormedSExpr atom] Source # readPrec :: ReadPrec (WellFormedSExpr atom) Source # readListPrec :: ReadPrec [WellFormedSExpr atom] Source #
Show atom => Show (WellFormedSExpr atom) |
Instance details Defined in Data.SCargot.Repr Methods showsPrec :: Int -> WellFormedSExpr atom -> ShowS Source # show :: WellFormedSExpr atom -> String Source # showList :: [WellFormedSExpr atom] -> ShowS Source #
Eq atom => Eq (WellFormedSExpr atom) |
Instance details Defined in Data.SCargot.Repr Methods (==) :: WellFormedSExpr atom -> WellFormedSExpr atom -> Bool Source # (/=) :: WellFormedSExpr atom -> WellFormedSExpr atom -> Bool Source #
type Item (WellFormedSExpr atom) |
Instance details Defined in Data.SCargot.Repr type Item (WellFormedSExpr atom) = WellFormedSExpr atom

ident :: Text -> SExpr Source #

Lift an unquoted identifier.

int :: Integer -> SExpr Source #

Lift an integer.

string :: Some StringInfoRepr -> Text -> SExpr Source #

bitvec :: Natural -> Integer -> SExpr Source #

Lift a bitvector.

bool :: Bool -> SExpr Source #

Lift a boolean.

nat :: Natural -> SExpr Source #

Lift a natural

real :: Rational -> SExpr Source #

Lift a real

ppFreeVarEnv :: VarNameEnv t -> String Source #

ppFreeSymFnEnv :: FnNameEnv t -> String Source #

pattern L :: [WellFormedSExpr t] -> WellFormedSExpr t Source #

A shorter alias for `WFSList`

    >>> L [A "pachy", A "derm"]
    WFSList [WFSAtom "pachy",WFSAtom "derm"]

pattern A :: t -> WellFormedSExpr t Source #

A shorter alias for `WFSAtom`

    >>> A "elephant"
    WFSAtom "elephant"