Cryptol.Symbolic.Value

Documentation

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

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

Instances

Show TValue

Defined in Cryptol.Eval.Type

Methods

showsPrec :: Int -> TValue -> ShowS

show :: TValue -> String

showList :: [TValue] -> ShowS

Generic TValue

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

Defined in Cryptol.Eval.Type

Methods

rnf :: TValue -> ()

type Rep TValue

Defined in Cryptol.Eval.Type

type Rep TValue = D1 (MetaData "TValue" "Cryptol.Eval.Type" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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)))))

isTBit :: TValue -> Bool

True if the evaluated value is Bit

tvSeq :: Nat' -> TValue -> TValue

Produce a sequence type value

data GenValue b w i

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

(Show b, Show w, Show i) => Show (GenValue b w i)

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)

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)

Defined in Cryptol.Eval.Value

Methods

rnf :: GenValue b w i -> ()

type Rep (GenValue b w i)

Defined in Cryptol.Eval.Value

type Rep (GenValue b w i) = D1 (MetaData "GenValue" "Cryptol.Eval.Value" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

A type lambda that expects a Type.

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

Generate a stream.

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)

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

Extract a bit value.

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

Extract a function from a value.

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

Extract a polymorphic function from a value.

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

Extract a tuple from a value.

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

Extract a record from a value.

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

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)

Extract a sequence.

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

Extract a packed word.

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)

Orphan instances

BitWord SBool SWord SInteger

Methods

ppBit :: SBool -> Doc

ppWord :: PPOpts -> SWord -> Doc

ppInteger :: PPOpts -> SInteger -> Doc

wordAsChar :: SWord -> Maybe Char

wordLen :: SWord -> Integer

bitLit :: Bool -> SBool

wordLit :: Integer -> Integer -> SWord

integerLit :: Integer -> SInteger

wordBit :: SWord -> Integer -> SBool

wordUpdate :: SWord -> Integer -> SBool -> SWord

packWord :: [SBool] -> SWord

unpackWord :: SWord -> [SBool]

joinWord :: SWord -> SWord -> SWord

splitWord :: Integer -> Integer -> SWord -> (SWord, SWord)

extractWord :: Integer -> Integer -> SWord -> SWord

wordPlus :: SWord -> SWord -> SWord

wordMinus :: SWord -> SWord -> SWord

wordMult :: SWord -> SWord -> SWord

wordToInt :: SWord -> SInteger

intPlus :: SInteger -> SInteger -> SInteger

intMinus :: SInteger -> SInteger -> SInteger

intMult :: SInteger -> SInteger -> SInteger

intModPlus :: Integer -> SInteger -> SInteger -> SInteger

intModMinus :: Integer -> SInteger -> SInteger -> SInteger

intModMult :: Integer -> SInteger -> SInteger -> SInteger

wordFromInt :: Integer -> SInteger -> SWord