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

Cryptol.Symbolic.Value

Contents

- Orphan instances

Description

Synopsis

- type SBool = SVal
- type SWord = SVal
- literalSWord :: Int -> Integer -> SWord
- fromBitsLE :: [SBool] -> SWord
- forallBV_ :: Int -> Symbolic SWord
- existsBV_ :: Int -> Symbolic SWord
- forallSBool_ :: Symbolic SBool
- existsSBool_ :: Symbolic SBool
- type Value = GenValue SBool SWord
- data TValue
  - = TVBit
  - | TVSeq Integer TValue
  - | TVStream TValue
  - | TVTuple [TValue]
  - | TVRec [(Ident, TValue)]
  - | TVFun TValue TValue
- isTBit :: TValue -> Bool
- tvSeq :: Nat' -> TValue -> TValue
- 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)
- 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
- toSeq :: Nat' -> TValue -> [GenValue b w] -> GenValue b w
- finNat' :: Nat' -> Integer
- fromVBit :: GenValue b w -> b
- 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
- fromSeq :: BitWord b w => GenValue b w -> [GenValue b w]
- fromVWord :: BitWord b w => GenValue b w -> w
- evalPanic :: String -> [String] -> a
- iteValue :: SBool -> Value -> Value -> Value
- mergeValue :: Bool -> SBool -> Value -> Value -> Value

# Documentation

type SBool = SVal Source #

type SWord = SVal Source #

literalSWord :: Int -> Integer -> SWord Source #

fromBitsLE :: [SBool] -> SWord Source #

forallBV_ :: Int -> Symbolic SWord Source #

existsBV_ :: Int -> Symbolic SWord Source #

forallSBool_ :: Symbolic SBool Source #

existsSBool_ :: Symbolic SBool Source #

type Value = GenValue SBool SWord 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)))))))

isTBit :: TValue -> Bool Source #

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

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))))))))

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 #

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.

finNat' :: Nat' -> Integer Source #

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.

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.

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.

evalPanic :: String -> [String] -> a Source #

iteValue :: SBool -> Value -> Value -> Value Source #

mergeValue :: Bool -> SBool -> Value -> Value -> Value Source #

# Orphan instances

BitWord SBool SWord Source # |
Methods packWord :: [SBool] -> SWord Source # unpackWord :: SWord -> [SBool] Source #