cryptol-2.2.6: Cryptol: The Language of Cryptography

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

- traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b)
- evalECon :: ECon -> Value
- selectV :: (Integer -> Value) -> Value -> Value
- replicateV :: Integer -> TValue -> Value -> Value
- nth :: a -> [a] -> Int -> a
- nthV :: Value -> Value -> Integer -> Value
- mapV :: Bool -> (Value -> Value) -> Value -> Value
- catV :: Value -> Value -> Value
- dropV :: Integer -> Value -> Value
- takeV :: Integer -> Value -> Value
- ecDemoteV :: Value
- data TypeVal
  - = TVBit
  - | TVSeq Int TypeVal
  - | TVStream TypeVal
  - | TVTuple [TypeVal]
  - | TVRecord [(Name, TypeVal)]
  - | TVFun TypeVal TypeVal
- toTypeVal :: TValue -> TypeVal
- type Binary = TValue -> Value -> Value -> Value
- type Unary = TValue -> Value -> Value
- arithBinary :: (SWord -> SWord -> SWord) -> Binary
- arithUnary :: (SWord -> SWord) -> Unary
- sExp :: SWord -> SWord -> SWord
- sLg2 :: SWord -> SWord
- cmpValue :: (SBool -> SBool -> a -> a) -> (SWord -> SWord -> a -> a) -> Value -> Value -> a -> a
- cmpEq :: SWord -> SWord -> SBool -> SBool
- cmpNotEq :: SWord -> SWord -> SBool -> SBool
- cmpLt :: SWord -> SWord -> SBool -> SBool
- cmpGt :: SWord -> SWord -> SBool -> SBool
- cmpLtEq :: SWord -> SWord -> SBool -> SBool
- cmpGtEq :: SWord -> SWord -> SBool -> SBool
- cmpBinary :: (SBool -> SBool -> SBool -> SBool) -> (SWord -> SWord -> SBool -> SBool) -> SBool -> Binary
- errorV :: String -> TValue -> Value
- zeroV :: TValue -> Value
- joinV :: TValue -> TValue -> TValue -> Value -> Value
- ecSplitV :: Value
- infChunksOf :: Integer -> [a] -> [[a]]
- finChunksOf :: Integer -> Integer -> [a] -> [[a]]
- logicBinary :: (SBool -> SBool -> SBool) -> (SWord -> SWord -> SWord) -> Binary
- logicUnary :: (SBool -> SBool) -> (SWord -> SWord) -> Unary
- fromThenV :: Value
- fromToV :: Value
- fromThenToV :: Value
- addPoly :: [SBool] -> [SBool] -> [SBool]
- ites :: SBool -> [SBool] -> [SBool] -> [SBool]
- degree :: [SBool] -> Int
- mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
- idx :: [SBool] -> Int -> SBool
- divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])

# 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