mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 17:33:13 +03:00
56824291b2
This ensures that all applications of partial type functions are well-defined. Fixes #416.
723 lines
20 KiB
Plaintext
723 lines
20 KiB
Plaintext
/*
|
|
* Copyright (c) 2013-2016 Galois, Inc.
|
|
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
*/
|
|
|
|
module Cryptol where
|
|
|
|
/**
|
|
* The value corresponding to a numeric type.
|
|
*/
|
|
primitive demote : {val, rep} Literal val rep => rep
|
|
|
|
infixr 5 ==>
|
|
infixr 10 \/
|
|
infixr 15 /\
|
|
infix 20 ==, ===, !=, !==
|
|
infix 30 >, >=, <, <=, <$, >$, <=$, >=$
|
|
infixr 40 ||
|
|
infixl 45 ^
|
|
infixr 50 &&
|
|
infixr 60 #
|
|
infixl 70 <<, <<<, >>, >>>, >>$
|
|
infixl 80 +, -
|
|
infixl 90 *, /, %, /$, %$
|
|
infixr 95 ^^
|
|
infixl 100 @, @@, !, !!
|
|
|
|
/**
|
|
* Add two values.
|
|
* * For words, addition uses modulo arithmetic.
|
|
* * Structured values are added element-wise.
|
|
*/
|
|
primitive (+) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* For words, subtraction uses modulo arithmetic.
|
|
* Structured values are subtracted element-wise. Defined as:
|
|
* a - b = a + negate b
|
|
* See also: `negate'.
|
|
*/
|
|
primitive (-) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* For words, multiplies two words, modulus 2^^a.
|
|
* Structured values are multiplied element-wise.
|
|
*/
|
|
primitive (*) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* For words, divides two words, modulus 2^^a.
|
|
* Structured values are divided element-wise.
|
|
*/
|
|
primitive (/) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* For words, takes the modulus of two words, modulus 2^^a.
|
|
* Over structured values, operates element-wise.
|
|
* Be careful, as this will often give unexpected results due to interaction of
|
|
* the two moduli.
|
|
*/
|
|
primitive (%) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* For words, takes the exponent of two words, modulus 2^^a.
|
|
* Over structured values, operates element-wise.
|
|
* Be careful, due to its fast-growing nature, exponentiation is prone to
|
|
* interacting poorly with defaulting.
|
|
*/
|
|
primitive (^^) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* Log base two.
|
|
*
|
|
* For words, computes the ceiling of log, base 2, of a number.
|
|
* Over structured values, operates element-wise.
|
|
*/
|
|
primitive lg2 : {a} (Arith a) => a -> a
|
|
|
|
|
|
type Bool = Bit
|
|
|
|
/**
|
|
* The constant True. Corresponds to the bit value 1.
|
|
*/
|
|
primitive True : Bit
|
|
|
|
/**
|
|
* The constant False. Corresponds to the bit value 0.
|
|
*/
|
|
primitive False : Bit
|
|
|
|
/**
|
|
* Returns the twos complement of its argument.
|
|
* Over structured values, operates element-wise.
|
|
* negate a = ~a + 1
|
|
*/
|
|
primitive negate : {a} (Arith a) => a -> a
|
|
|
|
/**
|
|
* Bitwise complement. The prefix notation '~ x'
|
|
* is syntactic sugar for 'complement x'.
|
|
*/
|
|
primitive complement : {a} (Logic a) => a -> a
|
|
|
|
/**
|
|
* Less-than. Only works on comparable arguments.
|
|
*
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
primitive (<) : {a} (Cmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Greater-than of two comparable arguments.
|
|
*
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
primitive (>) : {a} (Cmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Less-than or equal of two comparable arguments.
|
|
*
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
primitive (<=) : {a} (Cmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Greater-than or equal of two comparable arguments.
|
|
*
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
primitive (>=) : {a} (Cmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Compares any two values of the same type for equality.
|
|
*/
|
|
primitive (==) : {a} (Cmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Compares any two values of the same type for inequality.
|
|
*/
|
|
primitive (!=) : {a} (Cmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Compare the outputs of two functions for equality.
|
|
*/
|
|
(===) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)
|
|
f === g = \ x -> f x == g x
|
|
|
|
/**
|
|
* Compare the outputs of two functions for inequality.
|
|
*/
|
|
(!==) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)
|
|
f !== g = \x -> f x != g x
|
|
|
|
/**
|
|
* Returns the smaller of two comparable arguments.
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
min : {a} (Cmp a) => a -> a -> a
|
|
min x y = if x < y then x else y
|
|
|
|
/**
|
|
* Returns the greater of two comparable arguments.
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
max : {a} (Cmp a) => a -> a -> a
|
|
max x y = if x > y then x else y
|
|
|
|
|
|
/**
|
|
* 2's complement signed less-than.
|
|
*/
|
|
primitive (<$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* 2's complement signed greater-than.
|
|
*/
|
|
(>$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
x >$ y = y <$ x
|
|
|
|
/**
|
|
* 2's complement signed less-than-or-equal.
|
|
*/
|
|
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
x <=$ y = ~(y <$ x)
|
|
|
|
/**
|
|
* 2's complement signed greater-than-or-equal.
|
|
*/
|
|
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
x >=$ y = ~(x <$ y)
|
|
|
|
/**
|
|
* 2's complement signed division. Division rounds toward 0.
|
|
*/
|
|
primitive (/$) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* 2's complement signed remainder. Division rounds toward 0.
|
|
*/
|
|
primitive (%$) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* Unsigned carry. Returns true if the unsigned addition of the given
|
|
* bitvector arguments would result in an unsigned overflow.
|
|
*/
|
|
primitive carry : {n} (fin n) => [n] -> [n] -> Bit
|
|
|
|
/**
|
|
* Signed carry. Returns true if the 2's complement signed addition of the
|
|
* given bitvector arguments would result in a signed overflow.
|
|
*/
|
|
primitive scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
|
|
|
|
/**
|
|
* Signed borrow. Returns true if the 2's complement signed subtraction of the
|
|
* given bitvector arguments would result in a signed overflow.
|
|
*/
|
|
sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
|
|
sborrow x y = ( x <$ (x-y) ) ^ y@0
|
|
|
|
/**
|
|
* Zero extension of a bitvector.
|
|
*/
|
|
zext : {m, n} (fin m, m >= n) => [n] -> [m]
|
|
zext x = zero # x
|
|
|
|
/**
|
|
* Sign extension of a bitvector.
|
|
*/
|
|
sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
|
|
sext x = newbits # x
|
|
where newbits = if x@0 then ~zero else zero
|
|
|
|
/**
|
|
* Short-cutting boolean conjuction function.
|
|
* If the first argument is False, the second argument
|
|
* is not evaluated.
|
|
*/
|
|
(/\) : Bit -> Bit -> Bit
|
|
x /\ y = if x then y else False
|
|
|
|
/**
|
|
* Short-cutting boolean disjuction function.
|
|
* If the first argument is True, the second argument
|
|
* is not evaluated.
|
|
*/
|
|
(\/) : Bit -> Bit -> Bit
|
|
x \/ y = if x then True else y
|
|
|
|
/**
|
|
* Short-cutting logical implication.
|
|
* If the first argument is False, the second argument is
|
|
* not evaluated.
|
|
*/
|
|
(==>) : Bit -> Bit -> Bit
|
|
a ==> b = if a then b else True
|
|
|
|
/**
|
|
* Logical `and' over bits. Extends element-wise over sequences, tuples.
|
|
*/
|
|
primitive (&&) : {a} (Logic a) => a -> a -> a
|
|
|
|
/**
|
|
* Logical `or' over bits. Extends element-wise over sequences, tuples.
|
|
*/
|
|
primitive (||) : {a} (Logic a) => a -> a -> a
|
|
|
|
/**
|
|
* Logical `exclusive or' over bits. Extends element-wise over sequences, tuples.
|
|
*/
|
|
primitive (^) : {a} (Logic a) => a -> a -> a
|
|
|
|
/**
|
|
* Gives an arbitrary shaped value whose bits are all False.
|
|
* ~zero likewise gives an arbitrary shaped value whose bits are all True.
|
|
*/
|
|
primitive zero : {a} (Zero a) => a
|
|
|
|
/**
|
|
* Converts a bitvector to a non-negative integer in the range 0 to 2^^n-1.
|
|
*/
|
|
primitive toInteger : {bits} (fin bits) => [bits] -> Integer
|
|
|
|
/**
|
|
* Converts an unbounded integer to another arithmetic type. When converting
|
|
* to the bitvector type [n], the value is reduced modulo 2^^n.
|
|
*/
|
|
primitive fromInteger : {a} (Arith a) => Integer -> a
|
|
|
|
/**
|
|
* Converts an integer modulo n to an unbounded integer in the range 0 to n-1.
|
|
*/
|
|
primitive fromZ : {n} (fin n, n >= 1) => Z n -> Integer
|
|
|
|
/**
|
|
* Left shift. The first argument is the sequence to shift, the second is the
|
|
* number of positions to shift by.
|
|
*/
|
|
primitive (<<) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
|
|
|
|
/**
|
|
* Right shift. The first argument is the sequence to shift, the second is the
|
|
* number of positions to shift by.
|
|
*/
|
|
primitive (>>) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
|
|
|
|
/**
|
|
* Left rotate. The first argument is the sequence to rotate, the second is the
|
|
* number of positions to rotate by.
|
|
*/
|
|
primitive (<<<) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
|
|
|
|
/**
|
|
* Right rotate. The first argument is the sequence to rotate, the second is
|
|
* the number of positions to rotate by.
|
|
*/
|
|
primitive (>>>) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
|
|
|
|
/**
|
|
* 2's complement signed (arithmetic) right shift. The first argument
|
|
* is the sequence to shift (considered as a signed value),
|
|
* the second argument is the number of positions to shift
|
|
* by (considered as an unsigned value).
|
|
*/
|
|
primitive (>>$) : {n, ix} (fin n, n >= 1, fin ix) => [n] -> [ix] -> [n]
|
|
|
|
|
|
|
|
/**
|
|
* Concatenates two sequences. On bitvectors, the most-significant bits
|
|
* are in the left argument, and the least-significant bits are in the right.
|
|
*/
|
|
primitive (#) : {front, back, a} (fin front) => [front]a -> [back]a
|
|
-> [front + back] a
|
|
|
|
/**
|
|
* Splits a sequence into a pair of sequences.
|
|
* 'splitAt z = (x, y)' iff 'x # y = z'.
|
|
*/
|
|
primitive splitAt : {front, back, a} (fin front) => [front + back]a
|
|
-> ([front]a, [back]a)
|
|
|
|
/**
|
|
* Concatenates a list of sequences.
|
|
* 'join' is the inverse function to 'split'.
|
|
*/
|
|
primitive join : {parts, each, a} (fin each) => [parts][each]a
|
|
-> [parts * each]a
|
|
|
|
/**
|
|
* Splits a sequence into 'parts' groups with 'each' elements.
|
|
* 'split' is the inverse function to 'join'.
|
|
*/
|
|
primitive split : {parts, each, a} (fin each) => [parts * each]a
|
|
-> [parts][each]a
|
|
|
|
/**
|
|
* Reverses the elements in a sequence.
|
|
*/
|
|
primitive reverse : {n, a} (fin n) => [n]a -> [n]a
|
|
|
|
/**
|
|
* Transposes a matrix.
|
|
* Satisfies the property 'transpose m @ i @ j == m @ j @ i'.
|
|
*/
|
|
primitive transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
|
|
|
|
/**
|
|
* Index operator. The first argument is a sequence. The second argument is
|
|
* the zero-based index of the element to select from the sequence.
|
|
*/
|
|
primitive (@) : {n, a, ix} (fin ix) => [n]a -> [ix] -> a
|
|
|
|
/**
|
|
* Bulk index operator. The first argument is a sequence. The second argument
|
|
* is a sequence of the zero-based indices of the elements to select.
|
|
*/
|
|
(@@) : {n, k, ix, a} (fin ix) => [n]a -> [k][ix] -> [k]a
|
|
xs @@ is = [ xs @ i | i <- is ]
|
|
|
|
/**
|
|
* Reverse index operator. The first argument is a finite sequence. The second
|
|
* argument is the zero-based index of the element to select, starting from the
|
|
* end of the sequence.
|
|
*/
|
|
primitive (!) : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a
|
|
|
|
/**
|
|
* Bulk reverse index operator. The first argument is a finite sequence. The
|
|
* second argument is a sequence of the zero-based indices of the elements to
|
|
* select, starting from the end of the sequence.
|
|
*/
|
|
(!!) : {n, k, ix, a} (fin n, fin ix) => [n]a -> [k][ix] -> [k]a
|
|
xs !! is = [ xs ! i | i <- is ]
|
|
|
|
/**
|
|
* Update the given sequence with new value at the given index position.
|
|
* The first argument is a sequence. The second argument is the zero-based
|
|
* index of the element to update, starting from the front of the sequence.
|
|
* The third argument is the new element. The return value is the
|
|
* initial sequence updated so that the indicated index has the given value.
|
|
*/
|
|
primitive update : {n, a, ix} (fin ix) => [n]a -> [ix] -> a -> [n]a
|
|
|
|
/**
|
|
* Update the given sequence with new value at the given index position.
|
|
* The first argument is a sequence. The second argument is the zero-based
|
|
* index of the element to update, starting from the end of the sequence.
|
|
* The third argument is the new element. The return value is the
|
|
* initial sequence updated so that the indicated index has the given value.
|
|
*/
|
|
primitive updateEnd : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a -> [n]a
|
|
|
|
/**
|
|
* Perform a series of updates to a sequence. The first argument is
|
|
* the initial sequence to update. The second argument is a sequence
|
|
* of indices, and the third argument is a sequence of values.
|
|
* This function applies the 'update' function in sequence with the
|
|
* given update pairs.
|
|
*/
|
|
updates : {n, k, ix, a} (fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a
|
|
updates xs0 idxs vals = xss!0
|
|
where
|
|
xss = [ xs0 ] #
|
|
[ update xs i b
|
|
| xs <- xss
|
|
| i <- idxs
|
|
| b <- vals
|
|
]
|
|
|
|
/**
|
|
* Perform a series of updates to a sequence. The first argument is
|
|
* the initial sequence to update. The second argument is a sequence
|
|
* of indices, and the third argument is a sequence of values.
|
|
* This function applies the 'updateEnd' function in sequence with the
|
|
* given update pairs.
|
|
*/
|
|
updatesEnd : {n, k, ix, a} (fin n, fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a
|
|
updatesEnd xs0 idxs vals = xss!0
|
|
where
|
|
xss = [ xs0 ] #
|
|
[ updateEnd xs i b
|
|
| xs <- xss
|
|
| i <- idxs
|
|
| b <- vals
|
|
]
|
|
|
|
/**
|
|
* A finite arithmetic sequence starting with 'first' and 'next',
|
|
* stopping when the values would wrap around modulo '2^^bits'.
|
|
*
|
|
* '[a,b..]' is syntactic sugar for 'fromThen`{first=a,next=b}'.
|
|
* '[a..]' is syntactic sugar for 'fromThen`{first=a,next=a+1}'.
|
|
*/
|
|
primitive fromThen : {first, next, bits, len}
|
|
( fin first, fin next, fin bits
|
|
, bits >= width first, bits >= width next
|
|
, first != next
|
|
, lengthFromThen first next bits == len) => [len][bits]
|
|
|
|
/**
|
|
* A finite sequence counting up from 'first' to 'last'.
|
|
*
|
|
* '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'.
|
|
*/
|
|
primitive fromTo : {first, last, a} (fin last, last >= first, Literal last a) =>
|
|
[1 + (last - first)]a
|
|
|
|
/**
|
|
* A finite arithmetic sequence starting with 'first' and 'next',
|
|
* stopping when the values reach or would skip over 'last'.
|
|
*
|
|
* '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'.
|
|
*/
|
|
primitive fromThenTo : {first, next, last, a, len}
|
|
( fin first, fin next, fin last
|
|
, Literal first a, Literal next a, Literal last a
|
|
, first != next
|
|
, lengthFromThenTo first next last == len) => [len]a
|
|
|
|
/**
|
|
* An infinite sequence counting up from the given starting value.
|
|
* '[x...]' is syntactic sugar for 'infFrom x'.
|
|
*/
|
|
primitive infFrom : {a} (Arith a) => a -> [inf]a
|
|
|
|
/**
|
|
* An infinite arithmetic sequence starting with the given two values.
|
|
* '[x,y...]' is syntactic sugar for 'infFromThen x y'.
|
|
*/
|
|
primitive infFromThen : {a} (Arith a) => a -> a -> [inf]a
|
|
|
|
primitive error : {a, len} (fin len) => [len][8] -> a
|
|
|
|
|
|
/**
|
|
* Performs multiplication of polynomials over GF(2).
|
|
*/
|
|
pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
|
|
pmult x y = last zs
|
|
where
|
|
zs = [0] # [ (z << 1) ^ (if yi then 0 # x else 0) | yi <- y | z <- zs ]
|
|
|
|
/**
|
|
* Performs division of polynomials over GF(2).
|
|
*/
|
|
pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
|
|
pdiv x y = [ z ! degree | z <- zs ]
|
|
where
|
|
degree : [width v]
|
|
degree = last (ds : [1 + v]_)
|
|
where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]
|
|
|
|
reduce : [v] -> [v]
|
|
reduce u = if u ! degree then u ^ y else u
|
|
|
|
zs : [u][v]
|
|
zs = [ tail (reduce z # [xi]) | z <- [0] # zs | xi <- x ]
|
|
|
|
/**
|
|
* Performs modulus of polynomials over GF(2).
|
|
*/
|
|
pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
|
|
pmod x y = if y == 0 then 0/0 else last zs
|
|
where
|
|
degree : [width v]
|
|
degree = last (ds : [2 + v]_)
|
|
where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]
|
|
|
|
reduce : [1 + v] -> [1 + v]
|
|
reduce u = if u ! degree then u ^ y else u
|
|
|
|
powers : [inf][1 + v]
|
|
powers = [reduce 1] # [ reduce (p << 1) | p <- powers ]
|
|
|
|
zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]
|
|
|
|
/**
|
|
* Generates random values from a seed. When called with a function, currently
|
|
* generates a function that always returns zero.
|
|
*/
|
|
primitive random : {a} [256] -> a
|
|
|
|
type String n = [n][8]
|
|
type Word n = [n]
|
|
type Char = [8]
|
|
|
|
take : {front, back, a} (fin front) => [front + back]a -> [front]a
|
|
take (x # _) = x
|
|
|
|
drop : {front, back, a} (fin front) => [front + back]a -> [back]a
|
|
drop ((_ : [front] _) # y) = y
|
|
|
|
tail : {n, a} [1 + n]a -> [n]a
|
|
tail xs = drop`{1} xs
|
|
|
|
/**
|
|
* Return the left-most element of a sequence.
|
|
*/
|
|
head : {n, a} [1 + n]a -> a
|
|
head xs = xs @ 0
|
|
|
|
/**
|
|
* Return the right-most element of a sequence.
|
|
*/
|
|
last : {n, a} (fin n) => [1 + n]a -> a
|
|
last xs = xs ! 0
|
|
|
|
width : {bits, n, a} (fin n, fin bits, bits >= width n) => [n]a -> [bits]
|
|
width _ = `n
|
|
|
|
undefined : {a} a
|
|
undefined = error "undefined"
|
|
|
|
groupBy : {each, parts, a} (fin each) => [parts * each]a -> [parts][each]a
|
|
groupBy = split`{parts=parts}
|
|
|
|
/**
|
|
* Define the base 2 logarithm function in terms of width
|
|
*/
|
|
type lg2 n = width (max n 1 - 1)
|
|
|
|
/**
|
|
* Debugging function for tracing. The first argument is a string,
|
|
* which is prepended to the printed value of the second argument.
|
|
* This combined string is then printed when the trace function is
|
|
* evaluated. The return value is equal to the third argument.
|
|
*
|
|
* The exact timing and number of times the trace message is printed
|
|
* depend on the internal details of the Cryptol evaluation order,
|
|
* which are unspecified. Thus, the output produced by this
|
|
* operation may be difficult to predict.
|
|
*/
|
|
primitive trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
|
|
|
|
/**
|
|
* Debugging function for tracing values. The first argument is a string,
|
|
* which is prepended to the printed value of the second argument.
|
|
* This combined string is then printed when the trace function is
|
|
* evaluated. The return value is equal to the second argument.
|
|
*
|
|
* The exact timing and number of times the trace message is printed
|
|
* depend on the internal details of the Cryptol evaluation order,
|
|
* which are unspecified. Thus, the output produced by this
|
|
* operation may be difficult to predict.
|
|
*/
|
|
traceVal : {n, a} (fin n) => [n][8] -> a -> a
|
|
traceVal msg x = trace msg x x
|
|
|
|
/* Functions previously in Cryptol::Extras */
|
|
|
|
/**
|
|
* Conjunction of all bits in a sequence.
|
|
*/
|
|
and : {n} (fin n) => [n]Bit -> Bit
|
|
and xs = ~zero == xs
|
|
|
|
/**
|
|
* Disjunction of all bits in a sequence.
|
|
*/
|
|
or : {n} (fin n) => [n]Bit -> Bit
|
|
or xs = zero != xs
|
|
|
|
/**
|
|
* Conjunction after applying a predicate to all elements.
|
|
*/
|
|
all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
|
|
all f xs = and (map f xs)
|
|
|
|
/**
|
|
* Disjunction after applying a predicate to all elements.
|
|
*/
|
|
any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
|
|
any f xs = or (map f xs)
|
|
|
|
/**
|
|
* Map a function over a sequence.
|
|
*/
|
|
map : {n, a, b} (a -> b) -> [n]a -> [n]b
|
|
map f xs = [f x | x <- xs]
|
|
|
|
/**
|
|
* Functional left fold.
|
|
*
|
|
* foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3
|
|
*/
|
|
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
|
|
foldl f acc xs = ys ! 0
|
|
where ys = [acc] # [f a x | a <- ys | x <- xs]
|
|
|
|
/**
|
|
* Functional right fold.
|
|
*
|
|
* foldr (-) 0 [1,2,3] = 0 - (1 - (2 - 3))
|
|
*/
|
|
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
|
|
foldr f acc xs = ys ! 0
|
|
where ys = [acc] # [f x a | a <- ys | x <- reverse xs]
|
|
|
|
/**
|
|
* Compute the sum of the values in the sequence.
|
|
*/
|
|
sum : {n, a} (fin n, Arith a) => [n]a -> a
|
|
sum xs = foldl (+) (fromInteger 0) xs
|
|
|
|
/**
|
|
* Scan left is like a foldl that also emits the intermediate values.
|
|
*/
|
|
scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [n+1]b
|
|
scanl f acc xs = ys
|
|
where ys = [acc] # [f a x | a <- ys | x <- xs]
|
|
|
|
/**
|
|
* Scan right is like a foldr that also emits the intermediate values.
|
|
*/
|
|
scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
|
|
scanr f acc xs = reverse ys
|
|
where ys = [acc] # [f x a | a <- ys | x <- reverse xs]
|
|
|
|
/**
|
|
* Repeat a value.
|
|
*/
|
|
repeat : {n, a} a -> [n]a
|
|
repeat x = [ x | _ <- zero : [n] ]
|
|
|
|
/**
|
|
* `elem x xs` Returns true if x is equal to a value in xs.
|
|
*/
|
|
elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
|
|
elem a xs = any (\x -> x == a) xs
|
|
|
|
/**
|
|
* Create a list of tuples from two lists.
|
|
*/
|
|
zip : {n, a, b} [n]a -> [n]b -> [n](a, b)
|
|
zip xs ys = [(x,y) | x <- xs | y <- ys]
|
|
|
|
/**
|
|
* Create a list by applying the function to each pair of elements in the input.
|
|
*/
|
|
zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c
|
|
zipWith f xs ys = [f x y | x <- xs | y <- ys]
|
|
|
|
/**
|
|
* Transform a function into uncurried form.
|
|
*/
|
|
uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c
|
|
uncurry f = \(a, b) -> f a b
|
|
|
|
/**
|
|
* Transform a function into curried form.
|
|
*/
|
|
curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
|
|
curry f = \a b -> f (a, b)
|
|
|
|
/**
|
|
* Map a function iteratively over a seed value, producing an infinite
|
|
* list of successive function applications.
|
|
*/
|
|
iterate : {a} (a -> a) -> a -> [inf]a
|
|
iterate f x = [x] # [ f v | v <- iterate f x ]
|