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

Safe Haskell | None
Language | Haskell2010

What4.Serialize.Parser

Description

A parser for an s-expression representation of what4 expressions

Synopsis

- deserializeExpr :: forall sym t (st :: Type -> Type) fs. sym ~ ExprBuilder t st fs => sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
- deserializeExprWithConfig :: forall sym t (st :: Type -> Type) fs. sym ~ ExprBuilder t st fs => sym -> Config sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
- deserializeSymFn :: forall sym t (st :: Type -> Type) fs. sym ~ ExprBuilder t st fs => sym -> SExpr -> IO (Either String (SomeSymFn sym))
- deserializeSymFnWithConfig :: forall sym t (st :: Type -> Type) fs. sym ~ ExprBuilder t st fs => sym -> Config sym -> SExpr -> IO (Either String (SomeSymFn sym))
- deserializeBaseType :: SExpr -> Either String (Some BaseTypeRepr)
- readBaseTypes :: MonadError String m => SExpr -> m (Some (Assignment BaseTypeRepr))
- data Atom
  - = AId Text
  - | AStr (Some StringInfoRepr) Text
  - | AInt Integer
  - | ANat Natural
  - | AReal Rational
  - | AFloat (Some FloatPrecisionRepr) BigFloat
  - | ABV Int Integer
  - | ABool Bool
- data WellFormedSExpr atom
  - = WFSList [WellFormedSExpr atom]
  - | WFSAtom atom
- data Config sym = Config {
  - cSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
  - cExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
  }
- defaultConfig :: (IsSymExprBuilder sym, ShowF (SymExpr sym)) => sym -> Config sym
- data SomeSymFn t = SomeSymFn (SymFn t dom ret)
- type SExpr = WellFormedSExpr Atom
- parseSExpr :: Text -> Either String SExpr
- printSExpr :: Seq String -> SExpr -> Text

# Documentation

deserializeExpr :: forall sym t (st :: Type -> Type) fs. sym ~ ExprBuilder t st fs => sym -> SExpr -> IO (Either String (Some (SymExpr sym))) Source #

`(deserializeExpr sym)` is equivalent to `(deserializeExpr' (defaultConfig sym))`.

deserializeExprWithConfig :: forall sym t (st :: Type -> Type) fs. sym ~ ExprBuilder t st fs => sym -> Config sym -> SExpr -> IO (Either String (Some (SymExpr sym))) Source #

deserializeSymFn :: forall sym t (st :: Type -> Type) fs. sym ~ ExprBuilder t st fs => sym -> SExpr -> IO (Either String (SomeSymFn sym)) Source #

`(deserializeSymFn sym)` is equivalent to `(deserializeSymFn' (defaultConfig sym))`.

deserializeSymFnWithConfig :: forall sym t (st :: Type -> Type) fs. sym ~ ExprBuilder t st fs => sym -> Config sym -> SExpr -> IO (Either String (SomeSymFn sym)) Source #

deserializeBaseType :: SExpr -> Either String (Some BaseTypeRepr) Source #

readBaseTypes :: MonadError String m => SExpr -> m (Some (Assignment BaseTypeRepr)) 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 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

Functor WellFormedSExpr |
Instance details Defined in Data.SCargot.Repr Methods fmap :: (a -> b) -> WellFormedSExpr a -> WellFormedSExpr b Source # (<$) :: a -> WellFormedSExpr b -> WellFormedSExpr a Source #
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 #
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) |
Instance details Defined in Data.SCargot.Repr type Item (WellFormedSExpr atom) = WellFormedSExpr atom

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

data Config sym Source #

Constructors

Config |

Fields

- cSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))

  The mapping of names to defined What4 SymFns.

- cExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))

  The mapping of names to defined What4 expressions.

defaultConfig :: (IsSymExprBuilder sym, ShowF (SymExpr sym)) => sym -> Config sym Source #

data SomeSymFn t Source #

Constructors

SomeSymFn (SymFn t dom ret) |

type SExpr = WellFormedSExpr Atom Source #

parseSExpr :: Text -> Either String SExpr Source #

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.