/*
 * 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 number : {val, rep} Literal val rep => rep

/**
 * An alternative name for 'number', present for backward compatibility.
 */
demote : {val, rep} Literal val rep => rep
demote = number`{val}

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 @, @@, !, !!

// -----------------------------------------------------------------------------

/** A numeric type representing infinity. */
primitive type inf : #

/** The type of boolean values. */
primitive type Bit : *

/** The type of unbounded integers. */
primitive type Integer : *

/** 'Z n' is the type of integers, modulo 'n'. */
primitive type {n : #} (fin n, n >= 1) => Z n : *



/** Assert that two numeric types are equal. */
primitive type (==) : # -> # -> Prop

/** Assert that two numeric types are different. */
primitive type (!=) : # -> # -> Prop

/** Assert that the first numeric type is larger than, or equal to the second.*/
primitive type (>=) : # -> # -> Prop

/** Assert that a numeric type is a proper natural number (not 'inf'). */
primitive type fin : * -> Prop

/** Value types that have a notion of 'zero'. */
primitive type Zero : * -> Prop

/** Value types that support logical operations. */
primitive type Logic : * -> Prop

/** Value types that support arithmetic. */
primitive type Arith : * -> Prop

/** Value types that support unsigned comparisons. */
primitive type Cmp : * -> Prop

/** Value types that support signed comparisons. */
primitive type SignedCmp : * -> Prop

/** 'Literal n a' asserts that type 'a' contains the number 'n'. */
primitive type Literal : # -> * -> Prop



/** Add numeric types. */
primitive type (+) : # -> # -> #

/** Subtract numeric types. */
primitive type
  {m : #, n : # }
  (fin n, m >= n) =>
  m - n : #

/** Multiply numeric types. */
primitive type (*) : # -> # -> #

/** Divide numeric types, rounding down. */
primitive type
  { m : #, n : # }
  (fin m, n >= 1) =>
  m / n : #

/** Remainder of numeric type division. */
primitive type
  { m : #, n : # }
  (fin m, n >= 1) =>
  m % n : #

/** Exponentiate numeric types. */
primitive type (^^) : # -> # -> #

/** The number of bits required to represent the value of a numeric type. */
primitive type width : # -> #

/** The smaller of two numeric types. */
primitive type min : # -> # -> #

/** The larger of two numeric types. */
primitive type max : # -> # -> #

/** Divide numeric types, rounding up. */
primitive type
  { m : #, n : # }
  (fin m, fin n, n >= 1) =>
  m /^ n : #

/** How much we need to add to make a proper multiple of the second argument. */
primitive type
  { m : #, n : # }
  (fin m, fin n, n >= 1) =>
  m %^ n : #

/** The length of an enumeration. */
primitive type
  { start : #, next : #, last : # }
  (fin start, fin next, fin last, start != next) =>
  lengthFromThenTo start next last : #




// -----------------------------------------------------------------------------

/**
 * Assert that the first numeric type is less than or equal to the second.
 */
type constraint i <= j = (j >= i)

/**
 * Assert that the first numeric type is greater than the second.
 */
type constraint i > j = i >= j + 1

/**
 * Assert that the first numeric type is less than the second.
 */
type constraint i < j = j >= i + 1

/**
 * Add two values.
 *  * For type [n], addition is modulo 2^^n.
 *  * Structured values are added element-wise.
 */
primitive (+) : {a} (Arith a) => a -> a -> a

/**
 * Subtract two values.
 *  * For type [n], subtraction is modulo 2^^n.
 *  * Structured values are subtracted element-wise.
 *  * Satisfies 'a - b = a + negate b'.
 * See also: 'negate'.
 */
primitive (-) : {a} (Arith a) => a -> a -> a

/**
 * Multiply two values.
 *  * For type [n], multiplication is modulo 2^^n.
 *  * Structured values are multiplied element-wise.
 */
primitive (*) : {a} (Arith a) => a -> a -> a

/**
 * Divide two values, rounding down.
 *  * For type [n], the arguments are treated as unsigned.
 *  * Structured values are divided element-wise.
 *  * Division by zero is undefined.
 */
primitive (/) : {a} (Arith a) => a -> a -> a

/**
 * Compute the remainder from dividing two values.
 *  * For type [n], the arguments are treated as unsigned.
 *  * Structured values are combined element-wise.
 *  * Remainder of division by zero is undefined.
 *  * Satisfies 'x % y == x - (x / y) * y'.
 */
primitive (%) : {a} (Arith a) => a -> a -> a

/**
 * Compute the exponentiation of two values.
 *  * For type [n], the exponent is treated as unsigned,
 *    and the result is reduced modulo 2^^n.
 *  * For type Integer, negative powers are undefined.
 *  * Structured values are combined element-wise.
 */
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 two's complement of its argument.
 * Over structured values, operates element-wise.
 * The prefix notation '- x' is syntactic sugar
 * for 'negate x'.
 * Satisfies '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 conjunction 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 disjunction 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 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

/**
 * Produce a sequence using a generating function.
 * Satisfies 'generate f @ i == f i' for all 'i' between '0' and 'n-1'.
 *
 * Declarations of the form 'x @ i = e' are syntactic sugar for
 * 'x = generate (\i -> e)'.
 */
generate : {n, ix, a}
  (fin ix, n >= 1, ix >= width (n - 1)) => ([ix] -> a) -> [n]a
generate f = [ f i | i <- [0 .. n-1] ]

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

/**
 * Return the length of a sequence.  Note that the result depends only
 * on the type of the argument, not its value.
 */
length : {n, a, b} (fin n, Literal n b) => [n]a -> b
length _ = `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 ]