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 | Safe
Language | Haskell98

Cryptol.Eval.Value

Description

Synopsis

- 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 = BV !Integer !Integer
- mkBv :: Integer -> Integer -> BV
- 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)
- type Value = GenValue Bool BV
- newtype TValue = TValue {
  - tValTy :: Type
  }
- data PPOpts = PPOpts {
  - useAscii :: Bool
  - useBase :: Int
  - useInfLength :: Int
  }
- 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
  - packWord :: [b] -> w
  - unpackWord :: w -> [b]
- 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
- toStream :: [GenValue b w] -> GenValue b w
- toFinSeq :: TValue -> [GenValue b w] -> GenValue b w
- boolToWord :: [Bool] -> Value
- toSeq :: TValue -> TValue -> [GenValue b w] -> GenValue b w
- toPackedSeq :: TValue -> 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
- fromVTuple :: GenValue b w -> [GenValue b w]
- fromVRecord :: GenValue b w -> [(Name, GenValue b w)]
- lookupRecord :: Name -> GenValue b w -> GenValue b w
- toExpr :: Type -> Value -> Maybe Expr

# Documentation

isTBit :: TValue -> Bool Source

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

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

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

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

tvSeq :: TValue -> TValue -> TValue Source

numTValue :: TValue -> Nat' Source

toNumTValue :: Nat' -> TValue Source

finTValue :: TValue -> Integer Source

data BV Source

Constructors

BV !Integer !Integer | width, value The value may contain junk bits

Instances

BitWord Bool BV Source |
PP (WithBase Value) Source |

mkBv :: Integer -> Integer -> BV Source

Smart constructor for `BV`s that checks for the width limit

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 |

type Value = GenValue Bool BV Source

newtype TValue Source

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

Constructors

TValue |

Fields

tValTy :: Type

Instances

Show TValue Source |

data PPOpts Source

Constructors

PPOpts |

Fields

useAscii :: Bool
useBase :: Int
useInfLength :: Int

defaultPPOpts :: PPOpts Source

ppValue :: PPOpts -> Value -> Doc Source

asciiMode :: PPOpts -> Integer -> Bool Source

integerToChar :: Integer -> Char Source

data WithBase a Source

Constructors

WithBase PPOpts a |

Instances

Functor WithBase Source |
PP (WithBase Value) Source |
PP (WithBase EvalEnv) Source |

ppWord :: PPOpts -> BV -> Doc Source

class BitWord b w where Source

Methods

packWord :: [b] -> w Source

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.

Instances

BitWord Bool BV Source |

mask Source

Arguments

:: Integer | Bit-width
-> Integer | Value
-> Integer | Masked result

word :: Integer -> Integer -> Value Source

Create a packed word of n bits.

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

boolToWord :: [Bool] -> Value Source

This is strict!

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.

toPackedSeq :: TValue -> 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.

fromVBit :: GenValue b w -> b Source

Extract a bit value.

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

Extract a sequence.

fromStr :: Value -> String Source

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.

vWordLen :: Value -> Maybe Integer Source

fromWord :: Value -> Integer Source

Turn a value into an integer represented by w bits.

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.

toExpr :: Type -> Value -> Maybe Expr Source

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.