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

What4.Serialize.Parser

Description

A parser for an s-expression representation of what4 expressions

Synopsis

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 #

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

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 #

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

data Config sym Source #

Constructors

Config 

Fields

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

data SomeSymFn t Source #

Constructors

SomeSymFn (SymFn t dom ret) 

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.