Cryptol.Eval.Value

Documentation

data BV

Concrete bitvector values: width, value Invariant: The value must be within the range 0 .. 2^width-1

Constructors

BV !Integer !Integer

Instances

Show BV

Defined in Cryptol.Eval.Value

Methods

showsPrec :: Int -> BV -> ShowS

show :: BV -> String

showList :: [BV] -> ShowS

Generic BV

Defined in Cryptol.Eval.Value

Associated Types

type Rep BV :: Type -> Type

Methods

from :: BV -> Rep BV x

to :: Rep BV x -> BV

NFData BV

Defined in Cryptol.Eval.Value

Methods

rnf :: BV -> ()

EvalPrims Bool BV Integer

Defined in Cryptol.Prims.Eval

Methods

evalPrim :: Decl -> GenValue Bool BV Integer

iteValue :: Bool -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer)

BitWord Bool BV Integer

Defined in Cryptol.Eval.Value

Methods

ppBit :: Bool -> Doc

ppWord :: PPOpts -> BV -> Doc

ppInteger :: PPOpts -> Integer -> Doc

wordAsChar :: BV -> Maybe Char

wordLen :: BV -> Integer

bitLit :: Bool -> Bool

wordLit :: Integer -> Integer -> BV

integerLit :: Integer -> Integer

wordBit :: BV -> Integer -> Bool

wordUpdate :: BV -> Integer -> Bool -> BV

packWord :: [Bool] -> BV

unpackWord :: BV -> [Bool]

joinWord :: BV -> BV -> BV

splitWord :: Integer -> Integer -> BV -> (BV, BV)

extractWord :: Integer -> Integer -> BV -> BV

wordPlus :: BV -> BV -> BV

wordMinus :: BV -> BV -> BV

wordMult :: BV -> BV -> BV

wordToInt :: BV -> Integer

intPlus :: Integer -> Integer -> Integer

intMinus :: Integer -> Integer -> Integer

intMult :: Integer -> Integer -> Integer

intModPlus :: Integer -> Integer -> Integer -> Integer

intModMinus :: Integer -> Integer -> Integer -> Integer

intModMult :: Integer -> Integer -> Integer -> Integer

wordFromInt :: Integer -> Integer -> BV

type Rep BV

Defined in Cryptol.Eval.Value

type Rep BV = D1 (MetaData "BV" "Cryptol.Eval.Value" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "BV" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer)))

binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV

Apply an integer function to the values of bitvectors. This function assumes both bitvectors are the same width.

unaryBV :: (Integer -> Integer) -> BV -> BV

Apply an integer function to the values of a bitvector. This function assumes the function will not require masking.

bvVal :: BV -> Integer

mkBv :: Integer -> Integer -> BV

Smart constructor for BVs that checks for the width limit

data SeqMap b w i

A sequence map represents a mapping from nonnegative integer indices to values. These are used to represent both finite and infinite sequences.

Constructors

IndexSeqMap !(Integer -> Eval (GenValue b w i))

UpdateSeqMap !(Map Integer (Eval (GenValue b w i))) !(Integer -> Eval (GenValue b w i))

Instances

NFData (SeqMap b w i)

Defined in Cryptol.Eval.Value

Methods

rnf :: SeqMap b w i -> ()

lookupSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i)

type SeqValMap = SeqMap Bool BV Integer

finiteSeqMap :: [Eval (GenValue b w i)] -> SeqMap b w i

Generate a finite sequence map from a list of values

infiniteSeqMap :: [Eval (GenValue b w i)] -> Eval (SeqMap b w i)

Generate an infinite sequence map from a stream of values

enumerateSeqMap :: Integral n => n -> SeqMap b w i -> [Eval (GenValue b w i)]

Create a finite list of length n of the values from [0..n-1] in the given the sequence emap.

streamSeqMap :: SeqMap b w i -> [Eval (GenValue b w i)]

Create an infinite stream of all the values in a sequence map

reverseSeqMap

Arguments

:: Integer

Size of the sequence map

-> SeqMap b w i

-> SeqMap b w i

Reverse the order of a finite sequence map

updateSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i

concatSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i -> SeqMap b w i

Concatenate the first n values of the first sequence map onto the beginning of the second sequence map.

splitSeqMap :: Integer -> SeqMap b w i -> (SeqMap b w i, SeqMap b w i)

Given a number n and a sequence map, return two new sequence maps: the first containing the values from `[0..n-1]` and the next containing the values from n onward.

dropSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i

Drop the first n elements of the given SeqMap.

memoMap :: SeqMap b w i -> Eval (SeqMap b w i)

Given a sequence map, return a new sequence map that is memoized using a finite map memo table.

zipSeqMap :: (GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)) -> SeqMap b w i -> SeqMap b w i -> Eval (SeqMap b w i)

Apply the given evaluation function pointwise to the two given sequence maps.

mapSeqMap :: (GenValue b w i -> Eval (GenValue b w i)) -> SeqMap b w i -> Eval (SeqMap b w i)

Apply the given function to each value in the given sequence map

data WordValue b w i

For efficiency reasons, we handle finite sequences of bits as special cases in the evaluator. In cases where we know it is safe to do so, we prefer to used a "packed word" representation of bit sequences. This allows us to rely directly on Integer types (in the concrete evaluator) and SBV's Word types (in the symbolic simulator).

However, if we cannot be sure all the bits of the sequence will eventually be forced, we must instead rely on an explicit sequence of bits representation.

Constructors

WordVal !w

Packed word representation for bit sequences.

BitsVal !(Seq (Eval b))

Sequence of thunks representing bits.

LargeBitsVal !Integer !(SeqMap b w i)

A large bitvector sequence, represented as a SeqMap of bits.

Instances

Generic (WordValue b w i)

Defined in Cryptol.Eval.Value

Associated Types

type Rep (WordValue b w i) :: Type -> Type

Methods

from :: WordValue b w i -> Rep (WordValue b w i) x

to :: Rep (WordValue b w i) x -> WordValue b w i

(NFData w, NFData b) => NFData (WordValue b w i)

Defined in Cryptol.Eval.Value

Methods

rnf :: WordValue b w i -> ()

type Rep (WordValue b w i)

Defined in Cryptol.Eval.Value

type Rep (WordValue b w i) = D1 (MetaData "WordValue" "Cryptol.Eval.Value" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "WordVal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 w)) :+: (C1 (MetaCons "BitsVal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (Seq (Eval b)))) :+: C1 (MetaCons "LargeBitsVal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (SeqMap b w i)))))

largeBitSize :: Integer

An arbitrarily-chosen number of elements where we switch from a dense sequence representation of bit-level words to SeqMap representation.

asWordVal :: BitWord b w i => WordValue b w i -> Eval w

Force a word value into packed word form

asBitsMap :: BitWord b w i => WordValue b w i -> SeqMap b w i

Force a word value into a sequence of bits

enumerateWordValue :: BitWord b w i => WordValue b w i -> Eval [b]

Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in big-endian order.

enumerateWordValueRev :: BitWord b w i => WordValue b w i -> Eval [b]

Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in reverse of the usual order, which is little-endian order.

wordValueSize :: BitWord b w i => WordValue b w i -> Integer

Compute the size of a word value

checkedSeqIndex :: Seq a -> Integer -> Eval a

checkedIndex :: [a] -> Integer -> Eval a

indexWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b

Select an individual bit from a word value

updateWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)

Produce a new WordValue from the one given by updating the ith bit with the given bit value.

data GenValue b w i

Generic value type, parameterized by bit and word types.

NOTE: we maintain an important invariant regarding sequence types. VSeq must never be used for finite sequences of bits. Always use the VWord constructor instead! Infinite sequences of bits are handled by the VStream constructor, just as for other types.

Constructors

VRecord ![(Ident, Eval (GenValue b w i))]

 { .. }

VTuple ![Eval (GenValue b w i)]

 ( .. )

VBit !b

 Bit

VInteger !i

Integer or Z n

VSeq !Integer !(SeqMap b w i)

[n]a Invariant: VSeq is never a sequence of bits

VWord !Integer !(Eval (WordValue b w i))

 [n]Bit

VStream !(SeqMap b w i)

 [inf]a

VFun (Eval (GenValue b w i) -> Eval (GenValue b w i))

functions

VPoly (TValue -> Eval (GenValue b w i))

polymorphic values (kind *)

VNumPoly (Nat' -> Eval (GenValue b w i))

polymorphic values (kind #)

Instances

(Show b, Show w, Show i) => Show (GenValue b w i)

Defined in Cryptol.Eval.Value

Methods

showsPrec :: Int -> GenValue b w i -> ShowS

show :: GenValue b w i -> String

showList :: [GenValue b w i] -> ShowS

Generic (GenValue b w i)

Defined in Cryptol.Eval.Value

Associated Types

type Rep (GenValue b w i) :: Type -> Type

Methods

from :: GenValue b w i -> Rep (GenValue b w i) x

to :: Rep (GenValue b w i) x -> GenValue b w i

(NFData b, NFData i, NFData w) => NFData (GenValue b w i)

Defined in Cryptol.Eval.Value

Methods

rnf :: GenValue b w i -> ()

type Rep (GenValue b w i)

Defined in Cryptol.Eval.Value

type Rep (GenValue b w i) = D1 (MetaData "GenValue" "Cryptol.Eval.Value" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (((C1 (MetaCons "VRecord" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(Ident, Eval (GenValue b w i))])) :+: C1 (MetaCons "VTuple" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Eval (GenValue b w i)]))) :+: (C1 (MetaCons "VBit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b)) :+: (C1 (MetaCons "VInteger" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 i)) :+: C1 (MetaCons "VSeq" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (SeqMap b w i)))))) :+: ((C1 (MetaCons "VWord" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (Eval (WordValue b w i)))) :+: C1 (MetaCons "VStream" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (SeqMap b w i)))) :+: (C1 (MetaCons "VFun" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Eval (GenValue b w i) -> Eval (GenValue b w i)))) :+: (C1 (MetaCons "VPoly" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TValue -> Eval (GenValue b w i)))) :+: C1 (MetaCons "VNumPoly" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Nat' -> Eval (GenValue b w i))))))))

forceWordValue :: WordValue b w i -> Eval ()

Force the evaluation of a word value

forceValue :: GenValue b w i -> Eval ()

Force the evaluation of a value

type Value = GenValue Bool BV Integer

defaultPPOpts :: PPOpts

atFst :: Functor f => (a -> f b) -> (a, c) -> f (b, c)

atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b)

ppValue :: forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc

asciiMode :: PPOpts -> Integer -> Bool

integerToChar :: Integer -> Char

ppBV :: PPOpts -> BV -> Doc

class BitWord b w i | b -> w, w -> i, i -> b where

This type class defines a collection of operations on bits and words that are necessary to define generic evaluator primitives that operate on both concrete and symbolic values uniformly.

Methods

ppBit :: b -> Doc

Pretty-print an individual bit

ppWord :: PPOpts -> w -> Doc

Pretty-print a word value

ppInteger :: PPOpts -> i -> Doc

Pretty-print an integer value

wordAsChar :: w -> Maybe Char

Attempt to render a word value as an ASCII character. Return Nothing if the character value is unknown (e.g., for symbolic values).

wordLen :: w -> Integer

The number of bits in a word value.

bitLit :: Bool -> b

Construct a literal bit value from a boolean.

wordLit

Arguments

:: Integer

Width

-> Integer

Value

-> w

Construct a literal word value given a bit width and a value.

integerLit

Arguments

:: Integer

Value

-> i

Construct a literal integer value from the given integer.

wordBit :: w -> Integer -> b

Extract the numbered bit from the word.

NOTE: this assumes that the sequence of bits is big-endian and finite, so the bit numbered 0 is the most significant bit.

wordUpdate :: w -> Integer -> b -> w

Update the numbered bit in the word.

NOTE: this assumes that the sequence of bits is big-endian and finite, so the bit numbered 0 is the most significant bit.

packWord :: [b] -> w

Construct a word value from a finite sequence of bits. 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]

Deconstruct a packed word value in to a finite sequence of bits. 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.

joinWord :: w -> w -> w

Concatenate the two given word values. NOTE: the first argument represents the more-significant bits

splitWord

Arguments

:: Integer

left width

-> Integer

right width

-> w

-> (w, w)

Take the most-significant bits, and return those bits and the remainder. The first element of the pair is the most significant bits. The two integer sizes must sum to the length of the given word value.

extractWord

Arguments

:: Integer

Number of bits to take

-> Integer

starting bit

-> w

-> w

Extract a subsequence of bits from a packed word value. The first integer argument is the number of bits in the resulting word. The second integer argument is the number of less-significant digits to discard. Stated another way, the operation `extractWord n i w` is equivalent to first shifting w right by i bits, and then truncating to n bits.

wordPlus :: w -> w -> w

2's complement addition of packed words. The arguments must have equal bit width, and the result is of the same width. Overflow is silently discarded.

wordMinus :: w -> w -> w

2's complement subtraction of packed words. The arguments must have equal bit width, and the result is of the same width. Overflow is silently discarded.

wordMult :: w -> w -> w

2's complement multiplication of packed words. The arguments must have equal bit width, and the result is of the same width. The high bits of the multiplication are silently discarded.

wordToInt :: w -> i

Construct an integer value from the given packed word.

intPlus :: i -> i -> i

Addition of unbounded integers.

intMinus :: i -> i -> i

Subtraction of unbounded integers.

intMult :: i -> i -> i

Multiplication of unbounded integers.

intModPlus :: Integer -> i -> i -> i

Addition of integers modulo n, for a concrete positive integer n.

intModMinus :: Integer -> i -> i -> i

Subtraction of integers modulo n, for a concrete positive integer n.

intModMult :: Integer -> i -> i -> i

Multiplication of integers modulo n, for a concrete positive integer n.

wordFromInt :: Integer -> i -> w

Construct a packed word of the specified width from an integer value.

Instances

BitWord Bool BV Integer

Defined in Cryptol.Eval.Value

Methods

ppBit :: Bool -> Doc

ppWord :: PPOpts -> BV -> Doc

ppInteger :: PPOpts -> Integer -> Doc

wordAsChar :: BV -> Maybe Char

wordLen :: BV -> Integer

bitLit :: Bool -> Bool

wordLit :: Integer -> Integer -> BV

integerLit :: Integer -> Integer

wordBit :: BV -> Integer -> Bool

wordUpdate :: BV -> Integer -> Bool -> BV

packWord :: [Bool] -> BV

unpackWord :: BV -> [Bool]

joinWord :: BV -> BV -> BV

splitWord :: Integer -> Integer -> BV -> (BV, BV)

extractWord :: Integer -> Integer -> BV -> BV

wordPlus :: BV -> BV -> BV

wordMinus :: BV -> BV -> BV

wordMult :: BV -> BV -> BV

wordToInt :: BV -> Integer

intPlus :: Integer -> Integer -> Integer

intMinus :: Integer -> Integer -> Integer

intMult :: Integer -> Integer -> Integer

intModPlus :: Integer -> Integer -> Integer -> Integer

intModMinus :: Integer -> Integer -> Integer -> Integer

intModMult :: Integer -> Integer -> Integer -> Integer

wordFromInt :: Integer -> Integer -> BV

BitWord SBool SWord SInteger

Defined in Cryptol.Symbolic.Value

Methods

ppBit :: SBool -> Doc

ppWord :: PPOpts -> SWord -> Doc

ppInteger :: PPOpts -> SInteger -> Doc

wordAsChar :: SWord -> Maybe Char

wordLen :: SWord -> Integer

bitLit :: Bool -> SBool

wordLit :: Integer -> Integer -> SWord

integerLit :: Integer -> SInteger

wordBit :: SWord -> Integer -> SBool

wordUpdate :: SWord -> Integer -> SBool -> SWord

packWord :: [SBool] -> SWord

unpackWord :: SWord -> [SBool]

joinWord :: SWord -> SWord -> SWord

splitWord :: Integer -> Integer -> SWord -> (SWord, SWord)

extractWord :: Integer -> Integer -> SWord -> SWord

wordPlus :: SWord -> SWord -> SWord

wordMinus :: SWord -> SWord -> SWord

wordMult :: SWord -> SWord -> SWord

wordToInt :: SWord -> SInteger

intPlus :: SInteger -> SInteger -> SInteger

intMinus :: SInteger -> SInteger -> SInteger

intMult :: SInteger -> SInteger -> SInteger

intModPlus :: Integer -> SInteger -> SInteger -> SInteger

intModMinus :: Integer -> SInteger -> SInteger -> SInteger

intModMult :: Integer -> SInteger -> SInteger -> SInteger

wordFromInt :: Integer -> SInteger -> SWord

class BitWord b w i => EvalPrims b w i where

This class defines additional operations necessary to define generic evaluation functions.

Methods

evalPrim :: Decl -> GenValue b w i

Eval prim binds primitive declarations to the primitive values that implement them.

iteValue

Arguments

:: b

Test bit

-> Eval (GenValue b w i)

'then' value

-> Eval (GenValue b w i)

'else' value

-> Eval (GenValue b w i)

ifthenelse operation. Choose either the 'then' value or the 'else' value depending on the value of the test bit.

Instances

EvalPrims Bool BV Integer

Defined in Cryptol.Prims.Eval

Methods

evalPrim :: Decl -> GenValue Bool BV Integer

iteValue :: Bool -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer)

EvalPrims SBool SWord SInteger

Defined in Cryptol.Symbolic.Prims

Methods

evalPrim :: Decl -> GenValue SBool SWord SInteger

iteValue :: SBool -> Eval (GenValue SBool SWord SInteger) -> Eval (GenValue SBool SWord SInteger) -> Eval (GenValue SBool SWord SInteger)

mask

Arguments

:: Integer

Bit-width

-> Integer

Value

-> Integer

Masked result

word :: BitWord b w i => Integer -> Integer -> GenValue b w i

Create a packed word of n bits.

lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i

wlam :: BitWord b w i => (w -> Eval (GenValue b w i)) -> GenValue b w i

Functions that assume word inputs

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

A type lambda that expects a Type.

nlam :: (Nat' -> GenValue b w i) -> GenValue b w i

A type lambda that expects a Type of kind #.

toStream :: [GenValue b w i] -> Eval (GenValue b w i)

Generate a stream.

toFinSeq :: BitWord b w i => Integer -> TValue -> [GenValue b w i] -> GenValue b w i

boolToWord :: [Bool] -> Value

This is strict!

toSeq :: BitWord b w i => Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i)

Construct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.

mkSeq :: Nat' -> TValue -> SeqMap b w i -> GenValue b w i

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 i -> b

Extract a bit value.

fromVInteger :: GenValue b w i -> i

Extract an integer value.

fromVSeq :: GenValue b w i -> SeqMap b w i

Extract a finite sequence value.

fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i)

Extract a sequence.

fromStr :: Value -> Eval String

fromBit :: GenValue b w i -> Eval b

fromWordVal :: String -> GenValue b w i -> Eval (WordValue b w i)

fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w

Extract a packed word.

vWordLen :: BitWord b w i => GenValue b w i -> Maybe Integer

tryFromBits :: BitWord b w i => [Eval (GenValue b w i)] -> Maybe w

If the given list of values are all fully-evaluated thunks containing bits, return a packed word built from the same bits. However, if any value is not a fully-evaluated bit, return Nothing.

fromWord :: String -> Value -> Eval Integer

Turn a value into an integer represented by w bits.

fromVFun :: GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)

Extract a function from a value.

fromVPoly :: GenValue b w i -> TValue -> Eval (GenValue b w i)

Extract a polymorphic function from a value.

fromVNumPoly :: GenValue b w i -> Nat' -> Eval (GenValue b w i)

Extract a polymorphic function from a value.

fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)]

Extract a tuple from a value.

fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))]

Extract a record from a value.

lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i)

Lookup a field in a record.

toExpr :: PrimMap -> Type -> Value -> Eval (Maybe Expr)

Given an expected type, returns an expression that evaluates to this value, if we can determine it.

XXX: View patterns would probably clean up this definition a lot.