Cryptol.Eval.Value

Documentation

isTBit :: TValue -> Bool

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

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

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

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

tvSeq :: TValue -> TValue -> TValue

numTValue :: TValue -> Nat'

toNumTValue :: Nat' -> TValue

finTValue :: TValue -> Integer

data BV

Constructors

BV !Integer !Integer

width, value The value may contain junk bits

Instances

BitWord Bool BV

PP (WithBase Value)

mkBv :: Integer -> Integer -> BV

Smart constructor for BVs that checks for the width limit

data GenValue b w

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)

type Value = GenValue Bool BV

newtype TValue

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

Constructors

TValue

Fields

tValTy :: Type

Instances

Show TValue

data PPOpts

Constructors

PPOpts

Fields

useAscii :: Bool

useBase :: Int

useInfLength :: Int

defaultPPOpts :: PPOpts

ppValue :: PPOpts -> Value -> Doc

asciiMode :: PPOpts -> Integer -> Bool

integerToChar :: Integer -> Char

data WithBase a

Constructors

WithBase PPOpts a

Instances

Functor WithBase

PP (WithBase Value)

PP (WithBase EvalEnv)

ppWord :: PPOpts -> BV -> Doc

class BitWord b w where

Methods

packWord :: [b] -> w

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]

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.

Instances

BitWord Bool BV

BitWord SBool SWord

mask

Arguments

:: Integer

Bit-width

-> Integer

Value

-> Integer

Masked result

word :: Integer -> Integer -> Value

Create a packed word of n bits.

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

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

A type lambda that expects a Type.

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

Generate a stream.

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

boolToWord :: [Bool] -> Value

This is strict!

toSeq :: TValue -> TValue -> [GenValue b w] -> GenValue b w

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 :: TValue -> TValue -> [Value] -> Value

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.

fromVBit :: GenValue b w -> b

Extract a bit value.

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

Extract a sequence.

fromStr :: Value -> String

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

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

vWordLen :: Value -> Maybe Integer

fromWord :: Value -> Integer

Turn a value into an integer represented by w bits.

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

Extract a function from a value.

fromVPoly :: GenValue b w -> TValue -> GenValue b w

Extract a polymorphic function from a value.

fromVTuple :: GenValue b w -> [GenValue b w]

Extract a tuple from a value.

fromVRecord :: GenValue b w -> [(Name, GenValue b w)]

Extract a record from a value.

lookupRecord :: Name -> GenValue b w -> GenValue b w

Lookup a field in a record.

toExpr :: Type -> Value -> 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.