what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Serialize.SETokens

Description

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

Synopsis

- data Atom
  - = AId Text
  - | AStr (Some StringInfoRepr) Text
  - | AInt Integer
  - | ANat Natural
  - | AReal Rational
  - | AFloat (Some FloatPrecisionRepr) BigFloat
  - | ABV Int Integer
  - | ABool Bool
- string :: Some StringInfoRepr -> Text -> SExpr
- ident :: Text -> SExpr
- int :: Integer -> SExpr
- nat :: Natural -> SExpr
- bitvec :: Natural -> Integer -> SExpr
- bool :: Bool -> SExpr
- real :: Rational -> SExpr
- float :: FloatPrecisionRepr fpp -> BigFloat -> SExpr
- string' :: Some StringInfoRepr -> String -> SExpr
- ident' :: String -> SExpr
- printAtom :: Atom -> Text
- printSExpr :: Seq String -> SExpr -> Text
- parseSExpr :: Text -> Either String SExpr

# Documentation

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 Source # show :: Atom -> String Source # showList :: [Atom] -> ShowS Source #
Eq Atom Source # |
Instance details Defined in What4.Serialize.SETokens Methods (==) :: Atom -> Atom -> Bool Source # (/=) :: Atom -> Atom -> Bool Source #
Ord Atom Source # |
Instance details Defined in What4.Serialize.SETokens Methods compare :: Atom -> Atom -> Ordering Source # (<) :: Atom -> Atom -> Bool Source # (<=) :: Atom -> Atom -> Bool Source # (>) :: Atom -> Atom -> Bool Source # (>=) :: Atom -> Atom -> Bool Source # max :: Atom -> Atom -> Atom Source # min :: Atom -> Atom -> Atom Source #

string :: Some StringInfoRepr -> Text -> SExpr Source #

ident :: Text -> SExpr Source #

Lift an unquoted identifier.

int :: Integer -> SExpr Source #

Lift an integer.

nat :: Natural -> SExpr Source #

Lift a natural

bitvec :: Natural -> Integer -> SExpr Source #

Lift a bitvector.

bool :: Bool -> SExpr Source #

Lift a boolean.

real :: Rational -> SExpr Source #

Lift a real

float :: FloatPrecisionRepr fpp -> BigFloat -> SExpr Source #

Lift a float

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

ident' :: String -> SExpr Source #

printAtom :: Atom -> Text 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.

parseSExpr :: Text -> Either String SExpr Source #