Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
Cryptol.Symbolic.Value
Contents
Description
Synopsis
- type SBool = SVal
- type SWord = SVal
- type SInteger = SVal
- literalSWord :: Int -> Integer -> SWord
- fromBitsLE :: [SBool] -> SWord
- forallBV_ :: Int -> Symbolic SWord
- existsBV_ :: Int -> Symbolic SWord
- forallSBool_ :: Symbolic SBool
- existsSBool_ :: Symbolic SBool
- forallSInteger_ :: Symbolic SBool
- existsSInteger_ :: Symbolic SBool
- type Value = GenValue SBool SWord SInteger
- data TValue
- isTBit :: TValue -> Bool
- tvSeq :: Nat' -> TValue -> TValue
- data GenValue b w i
- = VRecord ![(Ident, Eval (GenValue b w i))]
- | VTuple ![Eval (GenValue b w i)]
- | VBit !b
- | VInteger !i
- | VSeq !Integer !(SeqMap b w i)
- | VWord !Integer !(Eval (WordValue b w i))
- | VStream !(SeqMap b w i)
- | VFun (Eval (GenValue b w i) -> Eval (GenValue b w i))
- | VPoly (TValue -> Eval (GenValue b w i))
- | VNumPoly (Nat' -> Eval (GenValue b w i))
- lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
- tlam :: (TValue -> GenValue b w i) -> GenValue b w i
- toStream :: [GenValue b w i] -> Eval (GenValue b w i)
- toFinSeq :: BitWord b w i => Integer -> TValue -> [GenValue b w i] -> GenValue b w i
- toSeq :: BitWord b w i => Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i)
- fromVBit :: GenValue b w i -> b
- fromVFun :: GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
- fromVPoly :: GenValue b w i -> TValue -> Eval (GenValue b w i)
- fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)]
- fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))]
- lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i)
- fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i)
- fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w
- evalPanic :: String -> [String] -> a
- iteSValue :: SBool -> Value -> Value -> Eval Value
- mergeValue :: Bool -> SBool -> Value -> Value -> Eval Value
- mergeWord :: Bool -> SBool -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger
- mergeBit :: Bool -> SBool -> SBool -> SBool -> SBool
- mergeBits :: Bool -> SBool -> Seq (Eval SBool) -> Seq (Eval SBool) -> Seq (Eval SBool)
- mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger
- mergeWord' :: Bool -> SBool -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger)
Documentation
literalSWord :: Int -> Integer -> SWord Source #
fromBitsLE :: [SBool] -> SWord Source #
An evaluated type of kind *. These types do not contain type variables, type synonyms, or type functions.
Instances
Show TValue Source # | |
Generic TValue Source # | |
NFData TValue Source # | |
Defined in Cryptol.Eval.Type | |
type Rep TValue Source # | |
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])))))) |
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 |
|
VSeq !Integer !(SeqMap b w i) |
|
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
(Show b, Show w, Show i) => Show (GenValue b w i) Source # | |
Generic (GenValue b w i) Source # | |
(NFData b, NFData i, NFData w) => NFData (GenValue b w i) Source # | |
Defined in Cryptol.Eval.Value | |
type Rep (GenValue b w i) Source # | |
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)))))))) |
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.
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.
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.
mergeWord :: Bool -> SBool -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger Source #
mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger Source #
mergeWord' :: Bool -> SBool -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) Source #