What4.Serialize.Parser

A parser for an s-expression representation of what4 expressions

Documentation

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

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

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

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

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

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

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

readBaseTypes :: forall m. MonadError String m => SExpr -> m (Some (Assignment BaseTypeRepr))

data Atom

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

Show Atom

Defined in What4.Serialize.SETokens

Methods

showsPrec :: Int -> Atom -> ShowS

show :: Atom -> String

showList :: [Atom] -> ShowS

Eq Atom

Defined in What4.Serialize.SETokens

Methods

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

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

Ord Atom

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

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

type Item (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)

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

type Item (WellFormedSExpr atom) = WellFormedSExpr atom

data Config sym

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

data SomeSymFn t

Constructors

forall dom ret. SomeSymFn (SymFn t dom ret)

type SExpr = WellFormedSExpr Atom

parseSExpr :: Text -> Either String SExpr

printSExpr :: Seq String -> SExpr -> Text

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