cryptol-2.4.0: Cryptol: The Language of Cryptography

Cryptol.Prims.Eval

Description

Synopsis

# Documentation

Make a numeric constant.

Arguments

 :: Integer bit size of the resulting word -> Integer base -> Integer exponent -> Integer

Create a packed word

Arguments

 :: Integer base -> Integer exponent mask -> Integer modulus -> Integer

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

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

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

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

divWrap :: Integral a => a -> a -> a Source #

modWrap :: Integral a => a -> a -> a Source #

Lexicographic ordering on two values.

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

Process two elements based on their lexicographic ordering.

joinV :: Nat' -> Nat' -> TValue -> Value -> Value Source #

Join a sequence of sequences into a single sequence.

Split implementation.

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

Split into infinitely many chunks

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

Split into finitely many chunks

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

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

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

Arguments

 :: (Integer -> Integer -> Integer -> Integer) The function may assume its arguments are masked. It is responsible for masking its result if needed. -> (Nat' -> TValue -> [Value] -> Integer -> [Value]) -> Value

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

Indexing operations that return one element.

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

Indexing operations that return many elements.

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