Cryptol.Symbolic.Value

Documentation

type SBool = SVal

type SWord = SVal

literalSWord :: Int -> Integer -> SWord

fromBitsLE :: [SBool] -> SWord

forallBV_ :: Int -> Symbolic SWord

existsBV_ :: Int -> Symbolic SWord

forallSBool_ :: Symbolic SBool

existsSBool_ :: Symbolic SBool

type Value = GenValue SBool SWord

data TValue

An evaluated type. These types do not contain type variables, type synonyms, or type functions.

Instances

Show TValue

Generic TValue

NFData TValue

type Rep TValue

numTValue :: TValue -> Nat'

toNumTValue :: Nat' -> TValue

finTValue :: TValue -> Integer

isTBit :: TValue -> Bool

isTFun :: TValue -> Maybe (TValue, TValue)

isTSeq :: TValue -> Maybe (TValue, TValue)

isTTuple :: TValue -> Maybe (Int, [TValue])

isTRec :: TValue -> Maybe [(Ident, TValue)]

tvSeq :: TValue -> TValue -> TValue

data GenValue b w

Generic value type, parameterized by bit and word types.

Constructors

VRecord [(Ident, GenValue b w)]

VTuple [GenValue b w]

VBit b

VSeq Bool [GenValue b w]

VWord w

VStream [GenValue b w]

VFun (GenValue b w -> GenValue b w)

VPoly (TValue -> GenValue b w)

Instances

PP (WithBase Value)

Generic (GenValue b w)

(NFData b, NFData w) => NFData (GenValue b w)

type Rep (GenValue b w)

lam :: (GenValue b w -> GenValue b w) -> GenValue b w

tlam :: (TValue -> GenValue b w) -> GenValue b w

A type lambda that expects a Type.

toStream :: [GenValue b w] -> GenValue b w

Generate a stream.

toFinSeq :: TValue -> [GenValue b w] -> GenValue b w

toSeq :: TValue -> TValue -> [GenValue b w] -> GenValue b w

Construct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.

fromVBit :: GenValue b w -> b

Extract a bit value.

fromVFun :: GenValue b w -> GenValue b w -> GenValue b w

Extract a function from a value.

fromVPoly :: GenValue b w -> TValue -> GenValue b w

Extract a polymorphic function from a value.

fromVTuple :: GenValue b w -> [GenValue b w]

Extract a tuple from a value.

fromVRecord :: GenValue b w -> [(Ident, GenValue b w)]

Extract a record from a value.

lookupRecord :: Ident -> GenValue b w -> GenValue b w

Lookup a field in a record.

fromSeq :: BitWord b w => GenValue b w -> [GenValue b w]

Extract a sequence.

fromVWord :: BitWord b w => GenValue b w -> w

Extract a packed word.

evalPanic :: String -> [String] -> a

iteValue :: SBool -> Value -> Value -> Value

mergeValue :: Bool -> SBool -> Value -> Value -> Value