cryptol-2.2.2: Cryptol: The Language of Cryptography

Copyright(c) 2013-2015 Galois, Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell98

Cryptol.Symbolic.Value

Description

 

Synopsis

Documentation

data TValue Source

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

Instances

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) 

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.

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.