Cryptol.Prims.Eval

Documentation

evalECon :: ECon -> Value

ecDemoteV :: Value

Make a numeric constant.

divModPoly :: Integer -> Int -> Integer -> Int -> (Integer, Integer)

modExp

Arguments

:: Integer

bit size of the resulting word

-> Integer

base

-> Integer

exponent

-> Integer

Create a packed word

doubleAndAdd

Arguments

:: Integer

base

-> Integer

exponent mask

-> Integer

modulus

-> Integer

type GenBinary b w = TValue -> GenValue b w -> GenValue b w -> GenValue b w

type Binary = GenBinary Bool BV

binary :: GenBinary b w -> GenValue b w

type GenUnary b w = TValue -> GenValue b w -> GenValue b w

type Unary = GenUnary Bool BV

unary :: GenUnary b w -> GenValue b w

liftBinArith :: (Integer -> Integer -> Integer) -> BinArith

Turn a normal binop on Integers into one that can also deal with a bitsize.

type BinArith = Integer -> Integer -> Integer -> Integer

arithBinary :: BinArith -> Binary

arithUnary :: (Integer -> Integer) -> Unary

lg2 :: Integer -> Integer

divWrap :: Integral a => a -> a -> a

modWrap :: Integral a => a -> a -> a

lexCompare :: TValue -> Value -> Value -> Ordering

Lexicographic ordering on two values.

zipLexCompare :: [TValue] -> [Value] -> [Value] -> Ordering

cmpOrder :: (Ordering -> Bool) -> Binary

Process two elements based on their lexicographic ordering.

withOrder :: (Ordering -> TValue -> Value -> Value -> Value) -> Binary

maxV :: Ordering -> TValue -> Value -> Value -> Value

minV :: Ordering -> TValue -> Value -> Value -> Value

funCmp :: (Ordering -> Bool) -> Value

zeroV :: TValue -> Value

joinV :: TValue -> TValue -> TValue -> Value -> Value

Join a sequence of sequences into a single sequence.

splitAtV :: TValue -> TValue -> TValue -> Value -> Value

ecSplitV :: Value

Split implementation.

infChunksOf :: Integer -> [a] -> [[a]]

Split into infinitely many chunks

finChunksOf :: Integer -> Integer -> [a] -> [[a]]

Split into finitely many chunks

ccatV :: TValue -> TValue -> TValue -> Value -> Value -> Value

logicBinary :: (forall a. Bits a => a -> a -> a) -> Binary

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

logicUnary :: (forall a. Bits a => a -> a) -> Unary

logicShift

Arguments

:: (Integer -> Integer -> Int -> Integer)

the Integer value (argument 2) may contain junk bits, but the Int (argument 3) will always be clean

-> (TValue -> TValue -> [Value] -> Int -> [Value])

-> Value

shiftLW :: Integer -> Integer -> Int -> Integer

shiftLS :: TValue -> TValue -> [Value] -> Int -> [Value]

shiftRW :: Integer -> Integer -> Int -> Integer

shiftRS :: TValue -> TValue -> [Value] -> Int -> [Value]

rotateLW :: Integer -> Integer -> Int -> Integer

rotateLS :: TValue -> TValue -> [Value] -> Int -> [Value]

rotateRW :: Integer -> Integer -> Int -> Integer

rotateRS :: TValue -> TValue -> [Value] -> Int -> [Value]

indexPrimOne :: (Maybe Integer -> [Value] -> Integer -> Value) -> Value

Indexing operations that return one element.

indexFront :: Maybe Integer -> [Value] -> Integer -> Value

indexBack :: Maybe Integer -> [Value] -> Integer -> Value

indexPrimMany :: (Maybe Integer -> [Value] -> [Integer] -> [Value]) -> Value

Indexing operations that return many elements.

indexFrontRange :: Maybe Integer -> [Value] -> [Integer] -> [Value]

indexBackRange :: Maybe Integer -> [Value] -> [Integer] -> [Value]

fromThenV :: Value

fromToV :: Value

fromThenToV :: Value

randomV :: TValue -> Integer -> Value

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

tlamN :: (Nat' -> GenValue b w) -> GenValue b w