Copyright | (c) 2013-2015 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Language | Haskell98 |
- 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
- 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 [(Name, TValue)]
- tvSeq :: TValue -> TValue -> TValue
- data GenValue b w
- lam :: (GenValue b w -> GenValue b w) -> GenValue b w
- tlam :: (TValue -> GenValue b w) -> GenValue b w
- toStream :: [GenValue b w] -> GenValue b w
- toFinSeq :: TValue -> [GenValue b w] -> GenValue b w
- toSeq :: TValue -> TValue -> [GenValue b w] -> GenValue b w
- fromVBit :: GenValue b w -> b
- fromVFun :: GenValue b w -> GenValue b w -> GenValue b w
- fromVPoly :: GenValue b w -> TValue -> GenValue b w
- fromVTuple :: GenValue b w -> [GenValue b w]
- fromVRecord :: GenValue b w -> [(Name, GenValue b w)]
- lookupRecord :: Name -> GenValue b w -> GenValue b w
- fromSeq :: BitWord b w => GenValue b w -> [GenValue b w]
- fromVWord :: BitWord b w => GenValue b w -> w
- evalPanic :: String -> [String] -> a
- iteValue :: SBool -> Value -> Value -> Value
- mergeValue :: Bool -> SBool -> Value -> Value -> Value
Documentation
literalSWord :: Int -> Integer -> SWord Source
fromBitsLE :: [SBool] -> SWord Source
An evaluated type. These types do not contain type variables, type synonyms, or type functions.
toNumTValue :: Nat' -> TValue Source
Generic value type, parameterized by bit and word types.
toSeq :: TValue -> TValue -> [GenValue b w] -> GenValue b w Source
Construct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.
fromVPoly :: GenValue b w -> TValue -> GenValue b w Source
Extract a polymorphic function from a value.
fromVTuple :: GenValue b w -> [GenValue b w] Source
Extract a tuple from a value.
fromVRecord :: GenValue b w -> [(Name, GenValue b w)] Source
Extract a record from a value.
lookupRecord :: Name -> GenValue b w -> GenValue b w Source
Lookup a field in a record.