what4-1.6.3: Solver-agnostic symbolic values support for issuing queries
Safe HaskellNone
LanguageHaskell2010

What4.Serialize.Printer

Synopsis

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

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.

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.

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

show :: Atom -> String

showList :: [Atom] -> ShowS

Eq Atom Source # 
Instance details

Defined in What4.Serialize.SETokens

Methods

(==) :: Atom -> Atom -> Bool

(/=) :: Atom -> Atom -> Bool

Ord Atom Source # 
Instance details

Defined in What4.Serialize.SETokens

Methods

compare :: Atom -> Atom -> Ordering

(<) :: Atom -> Atom -> Bool

(<=) :: Atom -> Atom -> Bool

(>) :: Atom -> Atom -> Bool

(>=) :: Atom -> Atom -> Bool

max :: Atom -> Atom -> Atom

min :: Atom -> Atom -> Atom

data SomeExprSymFn t Source #

Constructors

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

show :: SomeExprSymFn t -> String

showList :: [SomeExprSymFn t] -> ShowS

Eq (SomeExprSymFn t) Source # 
Instance details

Defined in What4.Serialize.Printer

Methods

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

(/=) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool

Ord (SomeExprSymFn t) Source # 
Instance details

Defined in What4.Serialize.Printer

data WellFormedSExpr atom #

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

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 
Instance details

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 
Instance details

Defined in Data.SCargot.Repr

Methods

fmap :: (a -> b) -> WellFormedSExpr a -> WellFormedSExpr b

(<$) :: a -> WellFormedSExpr b -> WellFormedSExpr a

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)

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) 
Instance details

Defined in Data.SCargot.Repr

Methods

fromString :: String -> WellFormedSExpr atom

IsList (WellFormedSExpr atom) 
Instance details

Defined in Data.SCargot.Repr

Associated Types

type Item (WellFormedSExpr atom) 
Instance details

Defined in Data.SCargot.Repr

type Item (WellFormedSExpr atom) = WellFormedSExpr atom

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) 
Instance details

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) 
Instance details

Defined in Data.SCargot.Repr

Methods

showsPrec :: Int -> WellFormedSExpr atom -> ShowS

show :: WellFormedSExpr atom -> String

showList :: [WellFormedSExpr atom] -> ShowS

Eq atom => Eq (WellFormedSExpr atom) 
Instance details

Defined in Data.SCargot.Repr

Methods

(==) :: WellFormedSExpr atom -> WellFormedSExpr atom -> Bool

(/=) :: WellFormedSExpr atom -> WellFormedSExpr atom -> Bool

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 #

pattern A :: t -> WellFormedSExpr t #