cryptol-3.0.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2020 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe-Inferred
Language | Haskell2010

Cryptol.Eval.Generic

Description

Synopsis

- mkLit :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym)
- ecNumberV :: Backend sym => sym -> Prim sym
- intV :: Backend sym => sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
- ratioV :: Backend sym => sym -> Prim sym
- ecFractionV :: Backend sym => sym -> Prim sym
- fromZV :: Backend sym => sym -> Prim sym
- type Binary sym = TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
- binary :: Backend sym => Binary sym -> Prim sym
- type Unary sym = TValue -> GenValue sym -> SEval sym (GenValue sym)
- unary :: Backend sym => Unary sym -> Prim sym
- type BinWord sym = Integer -> SWord sym -> SWord sym -> SEval sym (SWord sym)
- ringBinary :: forall sym. Backend sym => sym -> BinWord sym -> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) -> (Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) -> (SRational sym -> SRational sym -> SEval sym (SRational sym)) -> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym)) -> Binary sym
- type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym)
- ringUnary :: forall sym. Backend sym => sym -> UnaryWord sym -> (SInteger sym -> SEval sym (SInteger sym)) -> (Integer -> SInteger sym -> SEval sym (SInteger sym)) -> (SRational sym -> SEval sym (SRational sym)) -> (SFloat sym -> SEval sym (SFloat sym)) -> Unary sym
- ringNullary :: forall sym. Backend sym => sym -> (Integer -> SEval sym (SWord sym)) -> SEval sym (SInteger sym) -> (Integer -> SEval sym (SInteger sym)) -> SEval sym (SRational sym) -> (Integer -> Integer -> SEval sym (SFloat sym)) -> TValue -> SEval sym (GenValue sym)
- integralBinary :: forall sym. Backend sym => sym -> BinWord sym -> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) -> Binary sym
- fromIntegerV :: Backend sym => sym -> Prim sym
- addV :: Backend sym => sym -> Binary sym
- subV :: Backend sym => sym -> Binary sym
- negateV :: Backend sym => sym -> Unary sym
- mulV :: Backend sym => sym -> Binary sym
- divV :: Backend sym => sym -> Binary sym
- expV :: Backend sym => sym -> Prim sym
- computeExponent :: Backend sym => sym -> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
- modV :: Backend sym => sym -> Binary sym
- toIntegerV :: Backend sym => sym -> Prim sym
- recipV :: Backend sym => sym -> Prim sym
- fieldDivideV :: Backend sym => sym -> Prim sym
- roundOp :: Backend sym => sym -> String -> (SRational sym -> SEval sym (SInteger sym)) -> (SFloat sym -> SEval sym (SInteger sym)) -> Unary sym
- floorV :: Backend sym => sym -> Unary sym
- ceilingV :: Backend sym => sym -> Unary sym
- truncV :: Backend sym => sym -> Unary sym
- roundAwayV :: Backend sym => sym -> Unary sym
- roundToEvenV :: Backend sym => sym -> Unary sym
- andV :: Backend sym => sym -> Binary sym
- orV :: Backend sym => sym -> Binary sym
- xorV :: Backend sym => sym -> Binary sym
- complementV :: Backend sym => sym -> Unary sym
- lg2V :: Backend sym => sym -> Prim sym
- sdivV :: Backend sym => sym -> Prim sym
- smodV :: Backend sym => sym -> Prim sym
- toSignedIntegerV :: Backend sym => sym -> Prim sym
- cmpValue :: Backend sym => sym -> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a) -> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a) -> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) -> (Integer -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) -> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a) -> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a) -> TValue -> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a
- bitLessThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
- bitGreaterThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
- valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
- valLt :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
- valGt :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
- eqCombine :: Backend sym => sym -> SEval sym (SBit sym) -> SEval sym (SBit sym) -> SEval sym (SBit sym)
- lexCombine :: Backend sym => sym -> SEval sym (SBit sym) -> SEval sym (SBit sym) -> SEval sym (SBit sym) -> SEval sym (SBit sym)
- eqV :: Backend sym => sym -> Binary sym
- distinctV :: Backend sym => sym -> Binary sym
- lessThanV :: Backend sym => sym -> Binary sym
- lessThanEqV :: Backend sym => sym -> Binary sym
- greaterThanV :: Backend sym => sym -> Binary sym
- greaterThanEqV :: Backend sym => sym -> Binary sym
- signedLessThanV :: Backend sym => sym -> Binary sym
- zeroV :: forall sym. Backend sym => sym -> TValue -> SEval sym (GenValue sym)
- joinSeq :: Backend sym => sym -> Nat' -> Integer -> TValue -> SEval sym (SeqMap sym (GenValue sym)) -> SEval sym (GenValue sym)
- joinV :: Backend sym => sym -> Nat' -> Integer -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
- takeV :: Backend sym => sym -> Nat' -> Nat' -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
- dropV :: Backend sym => sym -> Integer -> Nat' -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
- splitV :: Backend sym => sym -> Nat' -> Integer -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
- reverseV :: forall sym. Backend sym => sym -> Integer -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
- transposeV :: Backend sym => sym -> Nat' -> Nat' -> TValue -> GenValue sym -> SEval sym (GenValue sym)
- ccatV :: Backend sym => sym -> Integer -> Nat' -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
- logicBinary :: forall sym. Backend sym => sym -> (SBit sym -> SBit sym -> SEval sym (SBit sym)) -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> Binary sym
- logicUnary :: forall sym. Backend sym => sym -> (SBit sym -> SEval sym (SBit sym)) -> (SWord sym -> SEval sym (SWord sym)) -> Unary sym
- assertIndexInBounds :: Backend sym => sym -> Nat' -> Either (SInteger sym) (WordValue sym) -> SEval sym ()
- indexPrim :: Backend sym => sym -> IndexDirection -> (Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> SInteger sym -> SEval sym (GenValue sym)) -> (Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> Integer -> [IndexSegment sym] -> SEval sym (GenValue sym)) -> Prim sym
- updatePrim :: Backend sym => sym -> (Nat' -> TValue -> WordValue sym -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (WordValue sym)) -> (Nat' -> TValue -> SeqMap sym (GenValue sym) -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym (GenValue sym))) -> Prim sym
- fromToV :: Backend sym => sym -> Prim sym
- fromThenToV :: Backend sym => sym -> Prim sym
- fromToLessThanV :: Backend sym => sym -> Prim sym
- fromToByV :: Backend sym => sym -> Prim sym
- fromToByLessThanV :: Backend sym => sym -> Prim sym
- fromToDownByV :: Backend sym => sym -> Prim sym
- fromToDownByGreaterThanV :: Backend sym => sym -> Prim sym
- infFromV :: Backend sym => sym -> Prim sym
- infFromThenV :: Backend sym => sym -> Prim sym
- shiftLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer
- shiftRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer
- rotateLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer
- rotateRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer
- logicShift :: Backend sym => sym -> String -> (sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)) -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Prim sym
- intShifter :: Backend sym => sym -> String -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Nat' -> TValue -> GenValue sym -> SInteger sym -> SEval sym (GenValue sym)
- wordShifter :: Backend sym => sym -> String -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Nat' -> TValue -> GenValue sym -> WordValue sym -> SEval sym (GenValue sym)
- shiftShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
- rotateShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
- sshrV :: Backend sym => sym -> Prim sym
- errorV :: forall sym. Backend sym => sym -> TValue -> String -> SEval sym (GenValue sym)
- valueToChar :: Backend sym => sym -> GenValue sym -> SEval sym Char
- valueToString :: Backend sym => sym -> GenValue sym -> SEval sym String
- foldlV :: Backend sym => sym -> Prim sym
- foldl'V :: Backend sym => sym -> Prim sym
- scanlV :: forall sym. Backend sym => sym -> Prim sym
- randomV :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym)
- parmapV :: Backend sym => sym -> Prim sym
- sparkParMap :: Backend sym => sym -> (SEval sym a -> SEval sym (GenValue sym)) -> Integer -> SeqMap sym a -> SEval sym (SeqMap sym (GenValue sym))
- fpConst :: Backend sym => (Integer -> Integer -> SEval sym (SFloat sym)) -> Prim sym
- fpBinArithV :: Backend sym => sym -> FPArith2 sym -> Prim sym
- fpRndMode :: Backend sym => sym -> SEval sym (SWord sym)
- fpRndRNE :: Backend sym => sym -> SEval sym (SWord sym)
- fpRndRNA :: Backend sym => sym -> SEval sym (SWord sym)
- fpRndRTP :: Backend sym => sym -> SEval sym (SWord sym)
- fpRndRTN :: Backend sym => sym -> SEval sym (SWord sym)
- fpRndRTZ :: Backend sym => sym -> SEval sym (SWord sym)
- genericFloatTable :: Backend sym => sym -> Map PrimIdent (Prim sym)
- genericPrimTable :: Backend sym => sym -> IO EvalOpts -> Map PrimIdent (Prim sym)

# Documentation

mkLit :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym) Source #

Make a numeric literal value at the given type.

ecNumberV :: Backend sym => sym -> Prim sym Source #

Make a numeric constant.

intV :: Backend sym => sym -> SInteger sym -> TValue -> SEval sym (GenValue sym) Source #

ratioV :: Backend sym => sym -> Prim sym Source #

ecFractionV :: Backend sym => sym -> Prim sym Source #

fromZV :: Backend sym => sym -> Prim sym Source #

type Binary sym = TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym) Source #

binary :: Backend sym => Binary sym -> Prim sym Source #

type Unary sym = TValue -> GenValue sym -> SEval sym (GenValue sym) Source #

unary :: Backend sym => Unary sym -> Prim sym Source #

type BinWord sym = Integer -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

ringBinary :: forall sym. Backend sym => sym -> BinWord sym -> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) -> (Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) -> (SRational sym -> SRational sym -> SEval sym (SRational sym)) -> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym)) -> Binary sym Source #

type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym) Source #

ringUnary :: forall sym. Backend sym => sym -> UnaryWord sym -> (SInteger sym -> SEval sym (SInteger sym)) -> (Integer -> SInteger sym -> SEval sym (SInteger sym)) -> (SRational sym -> SEval sym (SRational sym)) -> (SFloat sym -> SEval sym (SFloat sym)) -> Unary sym Source #

ringNullary :: forall sym. Backend sym => sym -> (Integer -> SEval sym (SWord sym)) -> SEval sym (SInteger sym) -> (Integer -> SEval sym (SInteger sym)) -> SEval sym (SRational sym) -> (Integer -> Integer -> SEval sym (SFloat sym)) -> TValue -> SEval sym (GenValue sym) Source #

integralBinary :: forall sym. Backend sym => sym -> BinWord sym -> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) -> Binary sym Source #

fromIntegerV :: Backend sym => sym -> Prim sym Source #

Convert an unbounded integer to a value in Ring

addV :: Backend sym => sym -> Binary sym Source #

subV :: Backend sym => sym -> Binary sym Source #

negateV :: Backend sym => sym -> Unary sym Source #

mulV :: Backend sym => sym -> Binary sym Source #

divV :: Backend sym => sym -> Binary sym Source #

expV :: Backend sym => sym -> Prim sym Source #

computeExponent :: Backend sym => sym -> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym) Source #

modV :: Backend sym => sym -> Binary sym Source #

toIntegerV :: Backend sym => sym -> Prim sym Source #

Convert a word to a non-negative integer.

recipV :: Backend sym => sym -> Prim sym Source #

fieldDivideV :: Backend sym => sym -> Prim sym Source #

roundOp :: Backend sym => sym -> String -> (SRational sym -> SEval sym (SInteger sym)) -> (SFloat sym -> SEval sym (SInteger sym)) -> Unary sym Source #

floorV :: Backend sym => sym -> Unary sym Source #

ceilingV :: Backend sym => sym -> Unary sym Source #

truncV :: Backend sym => sym -> Unary sym Source #

roundAwayV :: Backend sym => sym -> Unary sym Source #

roundToEvenV :: Backend sym => sym -> Unary sym Source #

andV :: Backend sym => sym -> Binary sym Source #

orV :: Backend sym => sym -> Binary sym Source #

xorV :: Backend sym => sym -> Binary sym Source #

complementV :: Backend sym => sym -> Unary sym Source #

lg2V :: Backend sym => sym -> Prim sym Source #

sdivV :: Backend sym => sym -> Prim sym Source #

smodV :: Backend sym => sym -> Prim sym Source #

toSignedIntegerV :: Backend sym => sym -> Prim sym Source #

cmpValue :: Backend sym => sym -> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a) -> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a) -> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) -> (Integer -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) -> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a) -> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a) -> TValue -> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a Source #

bitLessThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #

bitGreaterThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #

valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym) Source #

valLt :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym) Source #

valGt :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym) Source #

eqCombine :: Backend sym => sym -> SEval sym (SBit sym) -> SEval sym (SBit sym) -> SEval sym (SBit sym) Source #

lexCombine :: Backend sym => sym -> SEval sym (SBit sym) -> SEval sym (SBit sym) -> SEval sym (SBit sym) -> SEval sym (SBit sym) Source #

eqV :: Backend sym => sym -> Binary sym Source #

distinctV :: Backend sym => sym -> Binary sym Source #

lessThanV :: Backend sym => sym -> Binary sym Source #

lessThanEqV :: Backend sym => sym -> Binary sym Source #

greaterThanV :: Backend sym => sym -> Binary sym Source #

greaterThanEqV :: Backend sym => sym -> Binary sym Source #

signedLessThanV :: Backend sym => sym -> Binary sym Source #

zeroV :: forall sym. Backend sym => sym -> TValue -> SEval sym (GenValue sym) Source #

joinSeq :: Backend sym => sym -> Nat' -> Integer -> TValue -> SEval sym (SeqMap sym (GenValue sym)) -> SEval sym (GenValue sym) Source #

joinV :: Backend sym => sym -> Nat' -> Integer -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #

Join a sequence of sequences into a single sequence.

takeV :: Backend sym => sym -> Nat' -> Nat' -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #

dropV :: Backend sym => sym -> Integer -> Nat' -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #

splitV :: Backend sym => sym -> Nat' -> Integer -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #

Split implementation.

reverseV :: forall sym. Backend sym => sym -> Integer -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #

transposeV :: Backend sym => sym -> Nat' -> Nat' -> TValue -> GenValue sym -> SEval sym (GenValue sym) Source #

ccatV :: Backend sym => sym -> Integer -> Nat' -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #

logicBinary :: forall sym. Backend sym => sym -> (SBit sym -> SBit sym -> SEval sym (SBit sym)) -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> Binary sym Source #

Merge two values given a binop. This is used for and, or and xor.

logicUnary :: forall sym. Backend sym => sym -> (SBit sym -> SEval sym (SBit sym)) -> (SWord sym -> SEval sym (SWord sym)) -> Unary sym Source #

assertIndexInBounds Source #

Arguments

:: Backend sym |
=> sym |
-> Nat' | Sequence size bounds
-> Either (SInteger sym) (WordValue sym) | Index value
-> SEval sym () |

indexPrim :: Backend sym => sym -> IndexDirection -> (Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> SInteger sym -> SEval sym (GenValue sym)) -> (Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> Integer -> [IndexSegment sym] -> SEval sym (GenValue sym)) -> Prim sym Source #

Indexing operations.

updatePrim :: Backend sym => sym -> (Nat' -> TValue -> WordValue sym -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (WordValue sym)) -> (Nat' -> TValue -> SeqMap sym (GenValue sym) -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym (GenValue sym))) -> Prim sym Source #

fromToV :: Backend sym => sym -> Prim sym Source #

fromThenToV :: Backend sym => sym -> Prim sym Source #

fromToLessThanV :: Backend sym => sym -> Prim sym Source #

fromToByV :: Backend sym => sym -> Prim sym Source #

fromToByLessThanV :: Backend sym => sym -> Prim sym Source #

fromToDownByV :: Backend sym => sym -> Prim sym Source #

fromToDownByGreaterThanV :: Backend sym => sym -> Prim sym Source #

infFromV :: Backend sym => sym -> Prim sym Source #

infFromThenV :: Backend sym => sym -> Prim sym Source #

shiftLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer Source #

shiftRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer Source #

rotateLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer Source #

rotateRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer Source #

logicShift Source #

Arguments

:: Backend sym |
=> sym |
-> String |
-> (sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)) | operation for range reduction on integers
-> (SWord sym -> SWord sym -> SEval sym (SWord sym)) | word shift operation for positive indices
-> (SWord sym -> SWord sym -> SEval sym (SWord sym)) | word shift operation for negative indices
-> (Nat' -> Integer -> Integer -> Maybe Integer) | reindexing operation for positive indices (sequence size, starting index, shift amount
-> (Nat' -> Integer -> Integer -> Maybe Integer) | reindexing operation for negative indices (sequence size, starting index, shift amount
-> Prim sym |

Generic implementation of shifting. Uses the provided word-level operation to perform the shift, when possible. Otherwise falls back on a barrel shifter that uses the provided reindexing operation to implement the concrete shifting operations. The reindex operation is given the size of the sequence, the requested index value for the new output sequence, and the amount to shift. The return value is an index into the original sequence if in bounds, and Nothing otherwise.

intShifter :: Backend sym => sym -> String -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Nat' -> TValue -> GenValue sym -> SInteger sym -> SEval sym (GenValue sym) Source #

wordShifter :: Backend sym => sym -> String -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Nat' -> TValue -> GenValue sym -> WordValue sym -> SEval sym (GenValue sym) Source #

shiftShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym) Source #

rotateShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym) Source #

sshrV :: Backend sym => sym -> Prim sym Source #

errorV :: forall sym. Backend sym => sym -> TValue -> String -> SEval sym (GenValue sym) Source #

valueToChar :: Backend sym => sym -> GenValue sym -> SEval sym Char Source #

Expect a word value. Mask it to an 8-bits ASCII value and return the associated character, if it is concrete. Otherwise, return a `?` character

valueToString :: Backend sym => sym -> GenValue sym -> SEval sym String Source #

foldlV :: Backend sym => sym -> Prim sym Source #

foldl'V :: Backend sym => sym -> Prim sym Source #

scanlV :: forall sym. Backend sym => sym -> Prim sym Source #

randomV :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym) Source #

Produce a random value with the given seed. If we do not support making values of the given type, return zero of that type. TODO: do better than returning zero

parmapV :: Backend sym => sym -> Prim sym Source #

sparkParMap :: Backend sym => sym -> (SEval sym a -> SEval sym (GenValue sym)) -> Integer -> SeqMap sym a -> SEval sym (SeqMap sym (GenValue sym)) Source #

fpConst :: Backend sym => (Integer -> Integer -> SEval sym (SFloat sym)) -> Prim sym Source #

A helper for definitng floating point constants.

fpBinArithV :: Backend sym => sym -> FPArith2 sym -> Prim sym Source #

Make a Cryptol value for a binary arithmetic function.

fpRndMode :: Backend sym => sym -> SEval sym (SWord sym) Source #

Rounding mode used in FP operations that do not specify it explicitly.

fpRndRNE :: Backend sym => sym -> SEval sym (SWord sym) Source #

Rounding mode used in FP operations that do not specify it explicitly.

fpRndRNA :: Backend sym => sym -> SEval sym (SWord sym) Source #

Rounding mode used in FP operations that do not specify it explicitly.

fpRndRTP :: Backend sym => sym -> SEval sym (SWord sym) Source #

Rounding mode used in FP operations that do not specify it explicitly.

fpRndRTN :: Backend sym => sym -> SEval sym (SWord sym) Source #

Rounding mode used in FP operations that do not specify it explicitly.

fpRndRTZ :: Backend sym => sym -> SEval sym (SWord sym) Source #

Rounding mode used in FP operations that do not specify it explicitly.

genericFloatTable :: Backend sym => sym -> Map PrimIdent (Prim sym) Source #

genericPrimTable :: Backend sym => sym -> IO EvalOpts -> Map PrimIdent (Prim sym) Source #