| Copyright | (c) 2013-2016 Galois, Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell98 |
Cryptol.Symbolic.Value
Contents
Description
- 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
- isTBit :: TValue -> Bool
- tvSeq :: Nat' -> TValue -> TValue
- data GenValue b w
- lam :: (GenValue b w -> GenValue b w) -> GenValue b w
- tlam :: (TValue -> GenValue b w) -> GenValue b w
- nlam :: (Nat' -> GenValue b w) -> GenValue b w
- toStream :: [GenValue b w] -> GenValue b w
- toFinSeq :: TValue -> [GenValue b w] -> GenValue b w
- toSeq :: Nat' -> TValue -> [GenValue b w] -> GenValue b w
- finNat' :: Nat' -> Integer
- fromVBit :: GenValue b w -> b
- fromVFun :: GenValue b w -> GenValue b w -> GenValue b w
- fromVPoly :: GenValue b w -> TValue -> GenValue b w
- fromVNumPoly :: GenValue b w -> Nat' -> GenValue b w
- fromVTuple :: GenValue b w -> [GenValue b w]
- fromVRecord :: GenValue b w -> [(Ident, GenValue b w)]
- lookupRecord :: Ident -> 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
fromBitsLE :: [SBool] -> SWord Source #
An evaluated type of kind *. These types do not contain type variables, type synonyms, or type functions.
Generic value type, parameterized by bit and word types.
tlam :: (TValue -> GenValue b w) -> GenValue b w Source #
A type lambda that expects a Type of kind *.
toSeq :: Nat' -> 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.
fromVNumPoly :: GenValue b w -> Nat' -> 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.