| 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 {}
- 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
- 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.
Controls how expressions and functions are serialized.
Constructors
| Config | |
Fields
| |
Constructors
| Result | |
Fields
| |
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.
type SExpr = WellFormedSExpr 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. |
data SomeExprSymFn t Source #
Constructors
| forall dom ret. SomeExprSymFn (ExprSymFn t dom ret) |
Instances
| Show (SomeExprSymFn t) Source # | |
Defined in What4.Serialize.Printer Methods showsPrec :: Int -> SomeExprSymFn t -> ShowS # show :: SomeExprSymFn t -> String # showList :: [SomeExprSymFn t] -> ShowS # | |
| Eq (SomeExprSymFn t) Source # | |
Defined in What4.Serialize.Printer Methods (==) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool # (/=) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool # | |
| Ord (SomeExprSymFn t) Source # | |
Defined in What4.Serialize.Printer Methods compare :: SomeExprSymFn t -> SomeExprSymFn t -> Ordering # (<) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool # (<=) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool # (>) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool # (>=) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool # max :: SomeExprSymFn t -> SomeExprSymFn t -> SomeExprSymFn t # min :: SomeExprSymFn t -> SomeExprSymFn t -> SomeExprSymFn t # | |
data WellFormedSExpr atom #
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
ppFreeVarEnv :: VarNameEnv t -> String Source #
ppFreeSymFnEnv :: FnNameEnv t -> String Source #
pattern L :: [WellFormedSExpr t] -> WellFormedSExpr t #
A shorter alias for WFSList
>>>L [A "pachy", A "derm"]WFSList [WFSAtom "pachy",WFSAtom "derm"]
pattern A :: t -> WellFormedSExpr t #
A shorter alias for WFSAtom
>>>A "elephant"WFSAtom "elephant"