Safe Haskell | None |
---|---|
Language | Haskell2010 |
What4.Serialize.Printer
Synopsis
- serializeExpr :: forall t (tp :: BaseType). Expr t tp -> SExpr
- serializeExprWithConfig :: forall t (tp :: BaseType). Config -> Expr t tp -> Result t
- serializeSymFn :: forall t (dom :: Ctx BaseType) (ret :: BaseType). ExprSymFn t dom ret -> SExpr
- serializeSymFnWithConfig :: forall t (dom :: Ctx BaseType) (ret :: BaseType). Config -> ExprSymFn t dom ret -> Result t
- serializeBaseType :: forall (tp :: BaseType). BaseTypeRepr tp -> SExpr
- convertBaseTypes :: forall (tps :: Ctx BaseType). 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
- data SomeExprSymFn t = 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 :: forall t (tp :: BaseType). 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 :: forall t (tp :: BaseType). 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 :: forall t (dom :: Ctx BaseType) (ret :: BaseType). 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 :: forall t (dom :: Ctx BaseType) (ret :: BaseType). 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 :: forall (tp :: BaseType). BaseTypeRepr tp -> SExpr Source #
convertBaseTypes :: forall (tps :: Ctx BaseType). 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
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 #
Constructors
WFSList [WellFormedSExpr atom] | |
WFSAtom atom |
Instances
Foldable WellFormedSExpr | |||||
Defined in Data.SCargot.Repr Methods fold :: Monoid m => WellFormedSExpr m -> m foldMap :: Monoid m => (a -> m) -> WellFormedSExpr a -> m foldMap' :: Monoid m => (a -> m) -> WellFormedSExpr a -> m foldr :: (a -> b -> b) -> b -> WellFormedSExpr a -> b foldr' :: (a -> b -> b) -> b -> WellFormedSExpr a -> b foldl :: (b -> a -> b) -> b -> WellFormedSExpr a -> b foldl' :: (b -> a -> b) -> b -> WellFormedSExpr a -> b foldr1 :: (a -> a -> a) -> WellFormedSExpr a -> a foldl1 :: (a -> a -> a) -> WellFormedSExpr a -> a toList :: WellFormedSExpr a -> [a] null :: WellFormedSExpr a -> Bool length :: WellFormedSExpr a -> Int elem :: Eq a => a -> WellFormedSExpr a -> Bool maximum :: Ord a => WellFormedSExpr a -> a minimum :: Ord a => WellFormedSExpr a -> a sum :: Num a => WellFormedSExpr a -> a product :: Num a => WellFormedSExpr a -> a | |||||
Traversable WellFormedSExpr | |||||
Defined in Data.SCargot.Repr Methods traverse :: Applicative f => (a -> f b) -> WellFormedSExpr a -> f (WellFormedSExpr b) sequenceA :: Applicative f => WellFormedSExpr (f a) -> f (WellFormedSExpr a) mapM :: Monad m => (a -> m b) -> WellFormedSExpr a -> m (WellFormedSExpr b) sequence :: Monad m => WellFormedSExpr (m a) -> m (WellFormedSExpr a) | |||||
Functor WellFormedSExpr | |||||
Defined in Data.SCargot.Repr Methods fmap :: (a -> b) -> WellFormedSExpr a -> WellFormedSExpr b (<$) :: a -> WellFormedSExpr b -> WellFormedSExpr a | |||||
Data atom => Data (WellFormedSExpr atom) | |||||
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) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WellFormedSExpr atom) toConstr :: WellFormedSExpr atom -> Constr dataTypeOf :: WellFormedSExpr atom -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WellFormedSExpr atom)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WellFormedSExpr atom)) gmapT :: (forall b. Data b => b -> b) -> WellFormedSExpr atom -> WellFormedSExpr atom gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WellFormedSExpr atom -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WellFormedSExpr atom -> r gmapQ :: (forall d. Data d => d -> u) -> WellFormedSExpr atom -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> WellFormedSExpr atom -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> WellFormedSExpr atom -> m (WellFormedSExpr atom) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WellFormedSExpr atom -> m (WellFormedSExpr atom) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WellFormedSExpr atom -> m (WellFormedSExpr atom) | |||||
IsString atom => IsString (WellFormedSExpr atom) | |||||
Defined in Data.SCargot.Repr Methods fromString :: String -> WellFormedSExpr atom | |||||
IsList (WellFormedSExpr atom) | |||||
Defined in Data.SCargot.Repr Associated Types
Methods fromList :: [Item (WellFormedSExpr atom)] -> WellFormedSExpr atom fromListN :: Int -> [Item (WellFormedSExpr atom)] -> WellFormedSExpr atom toList :: WellFormedSExpr atom -> [Item (WellFormedSExpr atom)] | |||||
Read atom => Read (WellFormedSExpr atom) | |||||
Defined in Data.SCargot.Repr Methods readsPrec :: Int -> ReadS (WellFormedSExpr atom) readList :: ReadS [WellFormedSExpr atom] readPrec :: ReadPrec (WellFormedSExpr atom) readListPrec :: ReadPrec [WellFormedSExpr atom] | |||||
Show atom => Show (WellFormedSExpr atom) | |||||
Defined in Data.SCargot.Repr Methods showsPrec :: Int -> WellFormedSExpr atom -> ShowS show :: WellFormedSExpr atom -> String showList :: [WellFormedSExpr atom] -> ShowS | |||||
Eq atom => Eq (WellFormedSExpr atom) | |||||
Defined in Data.SCargot.Repr Methods (==) :: WellFormedSExpr atom -> WellFormedSExpr atom -> Bool (/=) :: WellFormedSExpr atom -> WellFormedSExpr atom -> Bool | |||||
type Item (WellFormedSExpr atom) | |||||
Defined in Data.SCargot.Repr |
string :: Some StringInfoRepr -> Text -> SExpr Source #
ppFreeVarEnv :: VarNameEnv t -> String Source #
ppFreeSymFnEnv :: FnNameEnv t -> String Source #
pattern L :: [WellFormedSExpr t] -> WellFormedSExpr t #
pattern A :: t -> WellFormedSExpr t #