what4-1.6.2: Solver-agnostic symbolic values support for issuing queries
Safe HaskellSafe-Inferred
LanguageHaskell2010

What4.Serialize.Parser

Description

A parser for an s-expression representation of what4 expressions

Synopsis

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 #

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

IsList (WellFormedSExpr atom) 
Instance details

Defined in Data.SCargot.Repr

Associated Types

type Item (WellFormedSExpr atom) #

Read atom => Read (WellFormedSExpr atom) 
Instance details

Defined in Data.SCargot.Repr

Show atom => Show (WellFormedSExpr atom) 
Instance details

Defined in Data.SCargot.Repr

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

data Config sym Source #

Constructors

Config 

Fields

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

data SomeSymFn t Source #

Constructors

forall dom ret. SomeSymFn (SymFn t dom ret) 

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.