cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 Galois, Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | None
Language | Haskell98

Cryptol.Symbolic.Value

Description

Synopsis

- 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
  - = VRecord [(Name, 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)
- 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

type SBool = SVal Source

type SWord = SVal Source

literalSWord :: Int -> Integer -> SWord Source

fromBitsLE :: [SBool] -> SWord Source

forallBV_ :: Int -> Symbolic SWord Source

existsBV_ :: Int -> Symbolic SWord Source

forallSBool_ :: Symbolic SBool Source

existsSBool_ :: Symbolic SBool Source

type Value = GenValue SBool SWord Source

data TValue Source

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

Instances

Show TValue Source |

numTValue :: TValue -> Nat' Source

toNumTValue :: Nat' -> TValue Source

finTValue :: TValue -> Integer Source

isTBit :: TValue -> Bool Source

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

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

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

isTRec :: TValue -> Maybe [(Name, TValue)] Source

tvSeq :: TValue -> TValue -> TValue Source

data GenValue b w Source

Generic value type, parameterized by bit and word types.

Constructors

VRecord [(Name, 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) Source |

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

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

A type lambda that expects a `Type`.

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

Generate a stream.

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

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.

fromVBit :: GenValue b w -> b Source

Extract a bit value.

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

Extract a function from a value.

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.

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

Extract a sequence.

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

Extract a packed word. Note that this does not clean-up any junk bits in the word.

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

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

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