Copyright	(c) 2013-2015 Galois, Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	None
Language	Haskell98

Cryptol.Symbolic.Prims

Description

Synopsis

Documentation

traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b) Source

evalECon :: ECon -> Value Source

selectV :: (Integer -> Value) -> Value -> Value Source

replicateV Source

Arguments

:: Integer	number of elements
-> TValue	type of element
-> Value	element
-> Value

nth :: a -> [a] -> Int -> a Source

nthV :: Value -> Value -> Integer -> Value Source

mapV :: Bool -> (Value -> Value) -> Value -> Value Source

catV :: Value -> Value -> Value Source

dropV :: Integer -> Value -> Value Source

takeV :: Integer -> Value -> Value Source

ecDemoteV :: Value Source

Make a numeric constant. { val, bits } (fin val, fin bits, bits >= width val) => [bits]

data TypeVal Source

An easy-to-use alternative representation for type TValue.

Constructors

TVBit
TVSeq Int TypeVal
TVStream TypeVal
TVTuple [TypeVal]
TVRecord [(Name, TypeVal)]
TVFun TypeVal TypeVal

toTypeVal :: TValue -> TypeVal Source

type Binary = TValue -> Value -> Value -> Value Source

type Unary = TValue -> Value -> Value Source

arithBinary :: (SWord -> SWord -> SWord) -> Binary Source

Models functions of type `{a} (Arith a) => a -> a -> a`

arithUnary :: (SWord -> SWord) -> Unary Source

Models functions of type `{a} (Arith a) => a -> a`

sExp :: SWord -> SWord -> SWord Source

sLg2 :: SWord -> SWord Source

Ceiling (log_2 x)

cmpValue :: (SBool -> SBool -> a -> a) -> (SWord -> SWord -> a -> a) -> Value -> Value -> a -> a Source

cmpEq :: SWord -> SWord -> SBool -> SBool Source

cmpNotEq :: SWord -> SWord -> SBool -> SBool Source

cmpLt :: SWord -> SWord -> SBool -> SBool Source

cmpGt :: SWord -> SWord -> SBool -> SBool Source

cmpLtEq :: SWord -> SWord -> SBool -> SBool Source

cmpGtEq :: SWord -> SWord -> SBool -> SBool Source

cmpBinary :: (SBool -> SBool -> SBool -> SBool) -> (SWord -> SWord -> SBool -> SBool) -> SBool -> Binary Source

errorV :: String -> TValue -> Value Source

zeroV :: TValue -> Value Source

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

Join a sequence of sequences into a single sequence.

ecSplitV :: Value Source

Split implementation.

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

Split into infinitely many chunks

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

Split into finitely many chunks

logicBinary :: (SBool -> SBool -> SBool) -> (SWord -> SWord -> SWord) -> Binary Source

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

logicUnary :: (SBool -> SBool) -> (SWord -> SWord) -> Unary Source

fromThenV :: Value Source

fromToV :: Value Source

fromThenToV :: Value Source

addPoly :: [SBool] -> [SBool] -> [SBool] Source

Add two polynomials

ites :: SBool -> [SBool] -> [SBool] -> [SBool] Source

degree :: [SBool] -> Int Source

mdp :: [SBool] -> [SBool] -> ([SBool], [SBool]) Source

idx :: [SBool] -> Int -> SBool Source

divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool]) Source