using NoStdLib

||| A right fold for lists.
|||   foldr(f, z, [a,b,c]) = f(a, f(b, f(c, z)))

!!!   foldr(~+~, 0, [1,2,3]) == 6
!!!   foldr(~+~, 0, [])      == 0

foldr : (a × b → b) × b × List(a) → b
foldr(f, z, []   ) = z
foldr(f, z, x::xs) = f(x, foldr(f, z, xs))

||| Append two lists into a single list.

!!!   append([], [])           == []
!!!   append([1,2,3], [])      == [1,2,3]
!!!   append([1,2,3], [4,5,6]) == [1,2,3,4,5,6]
!!!   ∀      xs : List(N). append([], xs) == xs
!!!   forall xs : List(N). append(xs, []) == xs

append : List(a) × List(a) → List(a)
append([],    ys) = ys
append(x::xs, ys) = x :: append(xs, ys)

||| Flatten a list of lists into a single list.

!!!   concat [[1,2],[3],[],[4,5,6]] == [1,2,3,4,5,6]

concat : List(List(a)) → List(a)
concat []      = []
concat (l::ls) = append(l, concat ls)

||| Apply a function to each element of a list, returning a new list
||| of the results.  Note, this is here just for illustration
||| purposes; it is much more efficient to use the builtin primitive
||| 'each' function (which also works on bags and sets).

!!!   eachlist(\x.x+1, []       ) == []
!!!   eachlist(\x.2,   "hello"  ) == [2,2,2,2,2]
!!!   eachlist(\x. 5x, [2,4,1,7]) == [10,20,5,35]

eachlist : (a → b) × List(a) → List(b)
eachlist(f, [])    = []
eachlist(f, x::xs) = f(x) :: eachlist(f, xs)

||| Take the first n elements of a list.
!!!   take(1, [true, false, true]) == [true]
!!!   take(3, [true, false]) == [true, false]
!!!   take(0, [true, false]) == ([] : List(Bool))

take : ℕ × List(a) → List(a)
take(0, _)         = []
take(_, [])        = []
take(n+1, x :: xs) = x :: take(n, xs)

||| The length of a list.
!!!   length [true, false, true] == 3
length : List(a) → ℕ
length [] = 0
length (_::l) = 1 + length l

||| The Cartesian product of two lists.
!!! listCP([1,2],[3,4]) == [(1,3), (1,4), (2,3), (2,4)]
!!! listCP([], [1,2,3]) == []
!!! listCP([1,2,3], []) == []
!!! ∀ xs : List(N), ys : List(N). length(listCP(xs,ys)) == length(xs) * length(ys)
listCP : List(a) * List(b) -> List(a * b)
listCP(as,bs) = concat(eachlist(\a. eachlist(\b. (a,b), bs), as))

zipWith : (a × b → c) × List(a) × List(b) -> List(c)
zipWith(_, [], _) = []
zipWith(_, _, []) = []
zipWith(f, a::as, b::bs) = f(a, b) :: zipWith(f, as, bs)

filterlist : (a -> Bool) × List(a) -> List(a)
filterlist(_, []) = []
filterlist(p, a :: as) =
  {? a :: filterlist(p, as)  if p a
  ,  filterlist(p, as)       otherwise
  ?}