Safe Haskell	Safe-Inferred
Language	Haskell2010

What4.Serialize.Parser

Description

A parser for an s-expression representation of what4 expressions

Synopsis

deserializeExpr :: forall sym t st fs. sym ~ ExprBuilder t st fs => sym -> SExpr -> IO (Either String (Some (SymExpr 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))
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
- = 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 = forall dom ret. 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 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 fs. sym ~ ExprBuilder t st fs => sym -> Config sym -> SExpr -> IO (Either String (Some (SymExpr sym))) Source #

deserializeSymFn :: forall sym t st 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 fs. sym ~ ExprBuilder t st fs => sym -> Config sym -> SExpr -> IO (Either String (SomeSymFn sym)) Source #

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

readBaseTypes :: forall m. 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 # 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 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

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

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

forall dom ret. 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.