| Copyright | (c) 2013-2016 Galois, Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell98 |
Cryptol.Eval.Value
Description
- isTBit :: TValue -> Bool
- isTSeq :: TValue -> Maybe (Nat', TValue)
- isTFun :: TValue -> Maybe (TValue, TValue)
- isTTuple :: TValue -> Maybe (Int, [TValue])
- isTRec :: TValue -> Maybe [(Ident, TValue)]
- tvSeq :: Nat' -> TValue -> TValue
- finNat' :: Nat' -> Integer
- data BV = BV !Integer !Integer
- mkBv :: Integer -> Integer -> BV
- data GenValue b w
- type Value = GenValue Bool BV
- data TValue
- tValTy :: TValue -> Type
- data PPOpts = PPOpts {}
- defaultPPOpts :: PPOpts
- ppValue :: PPOpts -> Value -> Doc
- asciiMode :: PPOpts -> Integer -> Bool
- integerToChar :: Integer -> Char
- data WithBase a = WithBase PPOpts a
- ppWord :: PPOpts -> BV -> Doc
- class BitWord b w where
- mask :: Integer -> Integer -> Integer
- word :: Integer -> Integer -> Value
- 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
- boolToWord :: [Bool] -> Value
- toSeq :: Nat' -> TValue -> [GenValue b w] -> GenValue b w
- toPackedSeq :: Nat' -> TValue -> [Value] -> Value
- fromVBit :: GenValue b w -> b
- fromSeq :: BitWord b w => GenValue b w -> [GenValue b w]
- fromStr :: Value -> String
- fromVWord :: BitWord b w => GenValue b w -> w
- vWordLen :: Value -> Maybe Integer
- fromWord :: Value -> Integer
- 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
- toExpr :: PrimMap -> Type -> Value -> Maybe Expr
Documentation
width, value Invariant: The value must be within the range 0 .. 2^width-1
Generic value type, parameterized by bit and word types.
An evaluated type of kind *. These types do not contain type variables, type synonyms, or type functions.
integerToChar :: Integer -> Char Source #
class BitWord b w where Source #
Minimal complete definition
Methods
NOTE this assumes that the sequence of bits is big-endian and finite, so the first element of the list will be the most significant bit.
unpackWord :: w -> [b] Source #
NOTE this produces a list of bits that represent a big-endian word, so the most significant bit is the first element of the list.
tlam :: (TValue -> GenValue b w) -> GenValue b w Source #
A type lambda that expects a Type of kind *.
boolToWord :: [Bool] -> Value Source #
This is strict!
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.
toPackedSeq :: Nat' -> TValue -> [Value] -> Value Source #
Construct one of: * a word, when the sequence is finite and the elements are bits * a sequence, when the sequence is finite but the elements aren't bits * a stream, when the sequence is not finite
NOTE: do not use this constructor in the case where the thing may be a finite, but recursive, sequence.
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.