cryptol-2.8.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Cryptol.Symbolic.Value

Description

 
Synopsis

Documentation

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

data TValue Source #

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

Instances

Instances details
Show TValue Source # 
Instance details

Defined in Cryptol.Eval.Type

Methods

showsPrec :: Int -> TValue -> ShowS

show :: TValue -> String

showList :: [TValue] -> ShowS

Generic TValue Source # 
Instance details

Defined in Cryptol.Eval.Type

Associated Types

type Rep TValue :: Type -> Type

Methods

from :: TValue -> Rep TValue x

to :: Rep TValue x -> TValue

NFData TValue Source # 
Instance details

Defined in Cryptol.Eval.Type

Methods

rnf :: TValue -> ()

type Rep TValue Source # 
Instance details

Defined in Cryptol.Eval.Type

type Rep TValue = D1 ('MetaData "TValue" "Cryptol.Eval.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (((C1 ('MetaCons "TVBit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TVInteger" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TVIntMod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "TVSeq" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TValue)))) :+: ((C1 ('MetaCons "TVStream" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TValue)) :+: C1 ('MetaCons "TVTuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TValue]))) :+: (C1 ('MetaCons "TVRec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Ident, TValue)])) :+: (C1 ('MetaCons "TVFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TValue) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TValue)) :+: C1 ('MetaCons "TVAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UserTC) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Either Nat' TValue]))))))

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

Integer or Z n

VSeq !Integer !(SeqMap b w i)

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

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

functions

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

polymorphic values (kind *)

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

polymorphic values (kind #)

Instances

Instances details
(Show b, Show w, Show i) => Show (GenValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

Methods

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

show :: GenValue b w i -> String

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

Generic (GenValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

Associated Types

type Rep (GenValue b w i) :: Type -> Type

Methods

from :: GenValue b w i -> Rep (GenValue b w i) x

to :: Rep (GenValue b w i) x -> GenValue b w i

(NFData b, NFData i, NFData w) => NFData (GenValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

Methods

rnf :: GenValue b w i -> ()

type Rep (GenValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

type Rep (GenValue b w i) = D1 ('MetaData "GenValue" "Cryptol.Eval.Value" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (((C1 ('MetaCons "VRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Ident, Eval (GenValue b w i))])) :+: C1 ('MetaCons "VTuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Eval (GenValue b w i)]))) :+: (C1 ('MetaCons "VBit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b)) :+: (C1 ('MetaCons "VInteger" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 i)) :+: C1 ('MetaCons "VSeq" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SeqMap b w i)))))) :+: ((C1 ('MetaCons "VWord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Eval (WordValue b w i)))) :+: C1 ('MetaCons "VStream" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SeqMap b w i)))) :+: (C1 ('MetaCons "VFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Eval (GenValue b w i) -> Eval (GenValue b w i)))) :+: (C1 ('MetaCons "VPoly" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TValue -> Eval (GenValue b w i)))) :+: C1 ('MetaCons "VNumPoly" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Nat' -> Eval (GenValue b w i))))))))

lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i Source #

tlam :: (TValue -> GenValue b w i) -> GenValue b w i Source #

A type lambda that expects a Type.

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

Generate a stream.

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

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

Extract a bit value.

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

Extract a function from a value.

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

Extract a polymorphic function from a value.

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

Extract a tuple from a value.

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

Extract a record from a value.

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

Lookup a field in a record.

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

Extract a sequence.

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

Extract a packed word.

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

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

Orphan instances