What4.Serialize.SETokens

Definition of the S-Expression tokens used to (de)serialize What4 expressions.

Documentation

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

string :: Some StringInfoRepr -> Text -> SExpr

ident :: Text -> SExpr

Lift an unquoted identifier.

int :: Integer -> SExpr

Lift an integer.

nat :: Natural -> SExpr

Lift a natural

bitvec :: Natural -> Integer -> SExpr

Lift a bitvector.

bool :: Bool -> SExpr

Lift a boolean.

real :: Rational -> SExpr

Lift a real

float :: FloatPrecisionRepr fpp -> BigFloat -> SExpr

Lift a float

string' :: Some StringInfoRepr -> String -> SExpr

ident' :: String -> SExpr

printAtom :: Atom -> Text

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.

parseSExpr :: Text -> Either String SExpr