cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 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 (Nat', TValue)
- isTFun :: TValue -> Maybe (TValue, TValue)
- isTTuple :: TValue -> Maybe (Int, [TValue])
- isTRec :: TValue -> Maybe [(Ident, TValue)]
- tvSeq :: Nat' -> TValue -> TValue
- finNat' :: Nat' -> Integer
- data BV = BV !Integer !Integer
- mkBv :: Integer -> Integer -> BV
- data GenValue b w
  - = VRecord [(Ident, 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)
  - | VNumPoly (Nat' -> GenValue b w)
- type Value = GenValue Bool BV
- data TValue
  - = TVBit
  - | TVSeq Integer TValue
  - | TVStream TValue
  - | TVTuple [TValue]
  - | TVRec [(Ident, TValue)]
  - | TVFun TValue TValue
- tValTy :: TValue -> 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
- 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
- nlam :: (Nat' -> 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 :: Nat' -> TValue -> [GenValue b w] -> GenValue b w
- toPackedSeq :: Nat' -> 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
- fromVNumPoly :: GenValue b w -> Nat' -> GenValue b w
- fromVTuple :: GenValue b w -> [GenValue b w]
- fromVRecord :: GenValue b w -> [(Ident, GenValue b w)]
- lookupRecord :: Ident -> GenValue b w -> GenValue b w
- toExpr :: PrimMap -> Type -> Value -> Maybe Expr

# Documentation

isTBit :: TValue -> Bool Source #

isTSeq :: TValue -> Maybe (Nat', TValue) Source #

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

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

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

tvSeq :: Nat' -> TValue -> TValue Source #

finNat' :: Nat' -> Integer Source #

data BV Source #

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

Constructors

BV !Integer !Integer |

Instances

Generic BV Source # |
Associated Types type Rep BV :: * -> * # Methods from :: BV -> Rep BV x # to :: Rep BV x -> BV #
NFData BV Source # |
Methods rnf :: BV -> () #
BitWord Bool BV Source # |
Methods packWord :: [Bool] -> BV Source # unpackWord :: BV -> [Bool] Source #
PP (WithBase Value) Source # |
Methods ppPrec :: Int -> WithBase Value -> Doc Source #
type Rep BV Source # |
type Rep BV = D1 (MetaData "BV" "Cryptol.Eval.Value" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "BV" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer))))

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 [(Ident, 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) |
VNumPoly (Nat' -> GenValue b w) |

Instances

PP (WithBase Value) Source # |
Methods ppPrec :: Int -> WithBase Value -> Doc Source #
Generic (GenValue b w) Source # |
Associated Types type Rep (GenValue b w) :: * -> * # Methods from :: GenValue b w -> Rep (GenValue b w) x # to :: Rep (GenValue b w) x -> GenValue b w #
(NFData w, NFData b) => NFData (GenValue b w) Source # |
Methods rnf :: GenValue b w -> () #
type Rep (GenValue b w) Source # |

type Rep (GenValue b w) = D1 (MetaData "GenValue" "Cryptol.Eval.Value" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "VRecord" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Ident, GenValue b w)]))) (C1 (MetaCons "VTuple" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [GenValue b w])))) ((:+:) (C1 (MetaCons "VBit" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 b))) (C1 (MetaCons "VSeq" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [GenValue b w])))))) ((:+:) ((:+:) (C1 (MetaCons "VWord" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 w))) (C1 (MetaCons "VStream" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [GenValue b w])))) ((:+:) (C1 (MetaCons "VFun" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (GenValue b w -> GenValue b w)))) ((:+:) (C1 (MetaCons "VPoly" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TValue -> GenValue b w)))) (C1 (MetaCons "VNumPoly" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Nat' -> GenValue b w))))))))

type Value = GenValue Bool BV Source #

data TValue Source #

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

Constructors

TVBit |
TVSeq Integer TValue |

TVStream TValue

inf
  t

TVTuple [TValue] |
TVRec [(Ident, TValue)] |
TVFun TValue TValue |

Instances

Show TValue Source # |
Methods showsPrec :: Int -> TValue -> ShowS # show :: TValue -> String # showList :: [TValue] -> ShowS #
Generic TValue Source # |
Associated Types type Rep TValue :: * -> * # Methods from :: TValue -> Rep TValue x # to :: Rep TValue x -> TValue #
NFData TValue Source # |
Methods rnf :: TValue -> () #
type Rep TValue Source # |

type Rep TValue = D1 (MetaData "TValue" "Cryptol.Eval.Value" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) ((:+:) (C1 (MetaCons "TVBit" PrefixI False) U1) ((:+:) (C1 (MetaCons "TVSeq" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TValue)))) (C1 (MetaCons "TVStream" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TValue))))) ((:+:) (C1 (MetaCons "TVTuple" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TValue]))) ((:+:) (C1 (MetaCons "TVRec" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Ident, TValue)]))) (C1 (MetaCons "TVFun" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TValue)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TValue)))))))

tValTy :: TValue -> Type 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 # |
Methods fmap :: (a -> b) -> WithBase a -> WithBase b # (<$) :: a -> WithBase b -> WithBase a #
PP (WithBase Value) Source # |
Methods ppPrec :: Int -> WithBase Value -> Doc Source #
PP (WithBase EvalEnv) Source # |
Methods ppPrec :: Int -> WithBase EvalEnv -> Doc Source #

ppWord :: PPOpts -> BV -> Doc Source #

class BitWord b w where Source #

Minimal complete definition

packWord, unpackWord

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 # |
Methods packWord :: [Bool] -> BV Source # unpackWord :: BV -> [Bool] 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` of kind *.

nlam :: (Nat' -> GenValue b w) -> GenValue b w Source #

A type lambda that expects a `Type` of kind #.

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 :: Nat' -> 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 :: Nat' -> 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.

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.

fromVNumPoly :: GenValue b w -> Nat' -> 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 -> [(Ident, GenValue b w)] Source #

Extract a record from a value.

lookupRecord :: Ident -> GenValue b w -> GenValue b w Source #

Lookup a field in a record.

toExpr :: PrimMap -> 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.