cryptol-2.5.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell98

Cryptol.Symbolic.Value

Contents

Description

 

Synopsis

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.

Instances

isTBit :: TValue -> Bool Source #

True if the evaluated value is Bit

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

Produce a sequence type value

data GenValue b w Source #

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))]
 { .. }
VTuple ![Eval (GenValue b w)]
 ( .. )
VBit !b
 Bit
VSeq !Integer !(SeqMap b w)

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

VWord !Integer !(Eval (WordValue b w))
 [n]Bit
VStream !(SeqMap b w)
 [inf]a
VFun (Eval (GenValue b w) -> Eval (GenValue b w))

functions

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

polymorphic values (kind *)

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

polymorphic values (kind #)

Instances

(Show b, Show w) => Show (GenValue b w) Source # 

Methods

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

show :: GenValue b w -> String #

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

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.5.0-62ntwDPh16AFY461fF3rK" False) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "VRecord" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(Ident, Eval (GenValue b w))]))) (C1 (MetaCons "VTuple" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Eval (GenValue b w)])))) ((:+:) (C1 (MetaCons "VBit" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b))) (C1 (MetaCons "VSeq" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (SeqMap b w))))))) ((:+:) ((:+:) (C1 (MetaCons "VWord" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (Eval (WordValue b w)))))) (C1 (MetaCons "VStream" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (SeqMap b w))))) ((:+:) (C1 (MetaCons "VFun" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Eval (GenValue b w) -> Eval (GenValue b w))))) ((:+:) (C1 (MetaCons "VPoly" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TValue -> Eval (GenValue b w))))) (C1 (MetaCons "VNumPoly" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Nat' -> Eval (GenValue b w)))))))))

lam :: (Eval (GenValue b w) -> Eval (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] -> Eval (GenValue b w) Source #

Generate a stream.

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

toSeq :: BitWord b w => Nat' -> TValue -> [GenValue b w] -> Eval (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.

fromVBit :: GenValue b w -> b Source #

Extract a bit value.

fromVFun :: GenValue b w -> Eval (GenValue b w) -> Eval (GenValue b w) Source #

Extract a function from a value.

fromVPoly :: GenValue b w -> TValue -> Eval (GenValue b w) Source #

Extract a polymorphic function from a value.

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

Extract a tuple from a value.

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

Extract a record from a value.

lookupRecord :: Ident -> GenValue b w -> Eval (GenValue b w) Source #

Lookup a field in a record.

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

Extract a sequence.

fromVWord :: BitWord b w => String -> GenValue b w -> Eval w Source #

Extract a packed word.

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

iteSValue :: SBool -> Value -> Value -> Value Source #

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

mergeWord :: Bool -> SBool -> WordValue SBool SWord -> WordValue SBool SWord -> WordValue SBool SWord Source #

mergeBit :: Bool -> SBool -> SBool -> SBool -> SBool Source #

mergeBits :: Bool -> SBool -> Seq (Eval SBool) -> Seq (Eval SBool) -> Seq (Eval SBool) Source #

mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord -> SeqMap SBool SWord -> SeqMap SBool SWord Source #

Orphan instances