module Prelude.List

import Builtins

import Prelude.Algebra
import Prelude.Basics
import Prelude.Bool
import Prelude.Interfaces
import Prelude.Foldable
import Prelude.Functor
import Prelude.Maybe
import Prelude.Uninhabited
import Prelude.Nat

%access public export
%default total

infix 5 \\
infixr 7 ::,++

||| Generic lists
%elim data List : (elem : Type) -> Type where
  ||| Empty list
  Nil : List elem
  ||| A non-empty list, consisting of a head element and the rest of
  ||| the list.
  (::) : (x : elem) -> (xs : List elem) -> List elem

-- Name hints for interactive editing
%name List xs, ys, zs, ws

-- Usage hints for erasure analysis
%used List.(::) x
%used List.(::) xs

--------------------------------------------------------------------------------
-- Syntactic tests
--------------------------------------------------------------------------------

||| Returns `True` iff the argument is empty
isNil : List a -> Bool
isNil []      = True
isNil (x::xs) = False

||| Returns `True` iff the argument is not empty
isCons : List a -> Bool
isCons []      = False
isCons (x::xs) = True

--------------------------------------------------------------------------------
-- Decidable Predicates
--------------------------------------------------------------------------------

||| Satisfiable if `xs` is non-empty (e.g., if `xs` is a cons).
data NonEmpty : (xs : List a) -> Type where
    ||| The proof that a cons cell is non-empty
    IsNonEmpty : NonEmpty (x :: xs)

Uninhabited (NonEmpty []) where
  uninhabited IsNonEmpty impossible

||| Decide whether a list is non-empty
nonEmpty : (xs : List a) -> Dec (NonEmpty xs)
nonEmpty [] = No absurd
nonEmpty (x :: xs) = Yes IsNonEmpty

||| Satisfiable if `k` is a valid index into `xs`
|||
||| @ k the potential index
||| @ xs the list into which k may be an index
data InBounds : (k : Nat) -> (xs : List a) -> Type where
    ||| Z is a valid index into any cons cell
    InFirst : InBounds Z (x :: xs)
    ||| Valid indices can be extended
    InLater : InBounds k xs -> InBounds (S k) (x :: xs)

Uninhabited (InBounds k []) where
    uninhabited InFirst impossible

||| Decide whether `k` is a valid index into `xs`
inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)
inBounds k [] = No uninhabited
inBounds Z (x :: xs) = Yes InFirst
inBounds (S k) (x :: xs) with (inBounds k xs)
  inBounds (S k) (x :: xs) | (Yes prf) = Yes (InLater prf)
  inBounds (S k) (x :: xs) | (No contra)
      = No (\p => case p of
                       InLater y => contra y)

--------------------------------------------------------------------------------
-- Length
--------------------------------------------------------------------------------

||| Compute the length of a list.
|||
||| Runs in linear time
length : List a -> Nat
length []      = 0
length (x::xs) = 1 + length xs

--------------------------------------------------------------------------------
-- Indexing into lists
--------------------------------------------------------------------------------

||| Find a particular element of a list.
|||
||| @ ok a proof that the index is within bounds
index : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} -> a
index Z     (x :: xs) {ok} = x
index (S k) (x :: xs) {ok = InLater p} = index k xs

||| Attempt to find a particular element of a list.
|||
||| If the provided index is out of bounds, return Nothing.
index' : (n : Nat) -> (l : List a) -> Maybe a
index' Z     (x::xs) = Just x
index' (S n) (x::xs) = index' n xs
index' _     []      = Nothing

||| Get the first element of a non-empty list
||| @ ok proof that the list is non-empty
head : (l : List a) -> {auto ok : NonEmpty l} -> a
head []      {ok=IsNonEmpty} impossible
head (x::xs) {ok=p}    = x

||| Attempt to get the first element of a list. If the list is empty, return
||| `Nothing`.
head' : (l : List a) -> Maybe a
head' []      = Nothing
head' (x::xs) = Just x

||| Get the tail of a non-empty list.
||| @ ok proof that the list is non-empty
tail : (l : List a) -> {auto ok : NonEmpty l} -> List a
tail []      {ok=IsNonEmpty} impossible
tail (x::xs) {ok=p}    = xs

||| Attempt to get the tail of a list.
|||
||| If the list is empty, return `Nothing`.
tail' : (l : List a) -> Maybe (List a)
tail' []      = Nothing
tail' (x::xs) = Just xs

||| Retrieve the last element of a non-empty list.
||| @ ok proof that the list is non-empty
last : (l : List a) -> {auto ok : NonEmpty l} -> a
last []         {ok=IsNonEmpty} impossible
last [x]        {ok=p}    = x
last (x::y::ys) {ok=p}    = last (y::ys) {ok=IsNonEmpty}

||| Attempt to retrieve the last element of a non-empty list.
|||
||| If the list is empty, return `Nothing`.
last' : (l : List a) -> Maybe a
last' []      = Nothing
last' (x::xs) =
  case xs of
    []      => Just x
    y :: ys => last' xs

||| Return all but the last element of a non-empty list.
||| @ ok proof that the list is non-empty
init : (l : List a) -> {auto ok : NonEmpty l} -> List a
init []         {ok=IsNonEmpty} impossible
init [x]        {ok=p}    = []
init (x::y::ys) {ok=p}    = x :: init (y::ys) {ok=IsNonEmpty}

||| Attempt to Return all but the last element of a list.
|||
||| If the list is empty, return `Nothing`.
init' : (l : List a) -> Maybe (List a)
init' []      = Nothing
init' (x::xs) =
  case xs of
    []    => Just []
    y::ys =>
      case init' $ y::ys of
        Nothing => Nothing
        Just j  => Just $ x :: j

--------------------------------------------------------------------------------
-- Sublists
--------------------------------------------------------------------------------

||| Take the first `n` elements of `xs`
|||
||| If there are not enough elements, return the whole list.
||| @ n how many elements to take
||| @ xs the list to take them from
take : (n : Nat) -> (xs : List a) -> List a
take Z     xs      = []
take (S n) []      = []
take (S n) (x::xs) = x :: take n xs

||| Drop the first `n` elements of `xs`
|||
||| If there are not enough elements, return the empty list.
||| @ n how many elements to drop
||| @ xs the list to drop them from
drop : (n : Nat) -> (xs : List a) -> List a
drop Z     xs      = xs
drop (S n) []      = []
drop (S n) (x::xs) = drop n xs

||| Take the longest prefix of a list such that all elements satisfy some
||| Boolean predicate.
|||
||| @ p the predicate
takeWhile : (p : a -> Bool) -> List a -> List a
takeWhile p []      = []
takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []

||| Remove the longest prefix of a list such that all removed elements satisfy some
||| Boolean predicate.
|||
||| @ p the predicate
dropWhile : (p : a -> Bool) -> List a -> List a
dropWhile p []      = []
dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs

--------------------------------------------------------------------------------
-- Misc.
--------------------------------------------------------------------------------

||| Simply-typed recursion operator for lists.
|||
||| @ nil what to return at the end of the list
||| @ cons what to do at each step of recursion
||| @ xs the list to recurse over
list : (nil : Lazy b) -> (cons : Lazy (a -> List a -> b)) -> (xs : List a) -> b
list nil cons []      = nil
list nil cons (x::xs) = cons x xs

--------------------------------------------------------------------------------
-- Building (bigger) lists
--------------------------------------------------------------------------------

||| Append two lists
(++) : List a -> List a -> List a
(++) []      right = right
(++) (x::xs) right = x :: (xs ++ right)

||| Construct a list with `n` copies of `x`
||| @ n how many copies
||| @ x the element to replicate
replicate : (n : Nat) -> (x : a) -> List a
replicate Z     x = []
replicate (S n) x = x :: replicate n x

--------------------------------------------------------------------------------
-- Instances
--------------------------------------------------------------------------------

(Eq a) => Eq (List a) where
  (==) []      []      = True
  (==) (x::xs) (y::ys) =
    if x == y then
      xs == ys
    else
      False
  (==) _ _ = False


Ord a => Ord (List a) where
  compare [] [] = EQ
  compare [] _ = LT
  compare _ [] = GT
  compare (x::xs) (y::ys) =
    if x /= y then
      compare x y
    else
      compare xs ys

Semigroup (List a) where
  (<+>) = (++)

Monoid (List a) where
  neutral = []

Functor List where
  map f []      = []
  map f (x::xs) = f x :: map f xs

--------------------------------------------------------------------------------
-- Zips and unzips
--------------------------------------------------------------------------------

||| Combine two lists elementwise using some function. If they are different
||| lengths, the result is truncated to the length of the shorter list.
||| @ f the function to combine elements with
||| @ l the first list
||| @ r the second list
zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) -> List c
zipWith f []      (y::ys) = []
zipWith f (x::xs) []      = []
zipWith f []      []      = []
zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

||| Combine three lists elementwise using some function. If they are different
||| lengths, the result is truncated to the length of the shortest list.
||| @ f the function to combine elements with
||| @ x the first list
||| @ y the second list
||| @ z the third list
zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
           (z : List c) -> List d
zipWith3 f _       []      (z::zs) = []
zipWith3 f _       (y::ys) []      = []
zipWith3 f []      (y::ys) _       = []
zipWith3 f (x::xs) []      _       = []
zipWith3 f []      []      []      = []
zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs

||| Combine two lists elementwise into pairs
zip : (l : List a) -> (r : List b) -> List (a, b)
zip = zipWith (\x,y => (x, y))

||| Combine three lists elementwise into tuples
zip3 : (x : List a) -> (y : List b) -> (z : List c) -> List (a, b, c)
zip3 = zipWith3 (\x,y,z => (x, y, z))

||| Split a list of pairs into two lists
unzip : List (a, b) -> (List a, List b)
unzip []           = ([], [])
unzip ((l, r)::xs) with (unzip xs)
  | (lefts, rights) = (l::lefts, r::rights)

||| Split a list of triples into three lists
unzip3 : List (a, b, c) -> (List a, List b, List c)
unzip3 []              = ([], [], [])
unzip3 ((l, c, r)::xs) with (unzip3 xs)
  | (lefts, centres, rights) = (l::lefts, c::centres, r::rights)

--------------------------------------------------------------------------------
-- Maps
--------------------------------------------------------------------------------

||| Apply a partial function to the elements of a list, keeping the ones at which
||| it is defined.
mapMaybe : (a -> Maybe b) -> List a -> List b
mapMaybe f []      = []
mapMaybe f (x::xs) =
  case f x of
    Nothing => mapMaybe f xs
    Just j  => j :: mapMaybe f xs

--------------------------------------------------------------------------------
-- Folds
--------------------------------------------------------------------------------

Foldable List where
  foldr c n [] = n
  foldr c n (x::xs) = c x (foldr c n xs)

  foldl f q [] = q
  foldl f q (x::xs) = foldl f (f q x) xs

--------------------------------------------------------------------------------
-- Special folds
--------------------------------------------------------------------------------

||| Convert any Foldable structure to a list.
toList : Foldable t => t a -> List a
toList = foldr (::) []

--------------------------------------------------------------------------------
-- Transformations
--------------------------------------------------------------------------------

||| Return the elements of a list in reverse order.
reverse : List a -> List a
reverse = reverse' []
  where
    reverse' : List a -> List a -> List a
    reverse' acc []      = acc
    reverse' acc (x::xs) = reverse' (x::acc) xs

||| Insert some separator between the elements of a list.
|||
||| ````idris example
||| with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
||| ````
|||
intersperse : a -> List a -> List a
intersperse sep []      = []
intersperse sep (x::xs) = x :: intersperse' sep xs
  where
    intersperse' : a -> List a -> List a
    intersperse' sep []      = []
    intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys

||| Given a separator list and some more lists, produce a new list by
||| placing the separator between each of the lists.
|||
||| @ sep the separator
||| @ xss the lists between which the separator will be placed
intercalate : (sep : List a) -> (xss : List (List a)) -> List a
intercalate sep xss = concat $ intersperse sep xss

||| Transposes rows and columns of a list of lists.
|||
||| ```idris example
||| with List transpose [[1, 2], [3, 4]]
||| ```
|||
||| This also works for non square scenarios, thus
||| involution does not always hold:
|||
|||     transpose [[], [1, 2]] = [[1], [2]]
|||     transpose (transpose [[], [1, 2]]) = [[1, 2]]
|||
||| TODO: Solution which satisfies the totality checker?
%assert_total
transpose : List (List a) -> List (List a)
transpose [] = []
transpose ([] :: xss) = transpose xss
transpose ((x::xs) :: xss) = (x :: (mapMaybe head' xss)) :: (transpose (xs :: (map (drop 1) xss)))

--------------------------------------------------------------------------------
-- Membership tests
--------------------------------------------------------------------------------

||| Check if something is a member of a list using a custom comparison.
elemBy : (a -> a -> Bool) -> a -> List a -> Bool
elemBy p e []      = False
elemBy p e (x::xs) =
  if p e x then
    True
  else
    elemBy p e xs

||| Check if something is a member of a list using the default Boolean equality.
elem : Eq a => a -> List a -> Bool
elem = elemBy (==)

||| Find associated information in a list using a custom comparison.
lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
lookupBy p e []      = Nothing
lookupBy p e (x::xs) =
  let (l, r) = x in
    if p e l then
      Just r
    else
      lookupBy p e xs

||| Find associated information in a list using Boolean equality.
lookup : Eq a => a -> List (a, b) -> Maybe b
lookup = lookupBy (==)

||| Check if any elements of the first list are found in the second, using
||| a custom comparison.
hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
hasAnyBy p elems []      = False
hasAnyBy p elems (x::xs) =
  if elemBy p x elems then
    True
  else
    hasAnyBy p elems xs

||| Check if any elements of the first list are found in the second, using
||| Boolean equality.
hasAny : Eq a => List a -> List a -> Bool
hasAny = hasAnyBy (==)

--------------------------------------------------------------------------------
-- Searching with a predicate
--------------------------------------------------------------------------------

||| Find the first element of a list that satisfies a predicate, or `Nothing` if none do.
find : (a -> Bool) -> List a -> Maybe a
find p []      = Nothing
find p (x::xs) =
  if p x then
    Just x
  else
    find p xs

||| Find the index of the first element of a list that satisfies a predicate, or
||| `Nothing` if none do.
findIndex : (a -> Bool) -> List a -> Maybe Nat
findIndex = findIndex' Z
  where
    findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat
    findIndex' cnt p []      = Nothing
    findIndex' cnt p (x::xs) =
      if p x then
        Just cnt
      else
        findIndex' (S cnt) p xs

||| Find the indices of all elements that satisfy some predicate.
findIndices : (a -> Bool) -> List a -> List Nat
findIndices = findIndices' Z
  where
    findIndices' : Nat -> (a -> Bool) -> List a -> List Nat
    findIndices' cnt p []      = []
    findIndices' cnt p (x::xs) =
      if p x then
        cnt :: findIndices' (S cnt) p xs
      else
        findIndices' (S cnt) p xs

||| Find the index of the first occurrence of an element in a list, using a custom equality test.
elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat
elemIndexBy p e = findIndex $ p e

||| Find the index of the first occurrence of an element in a list,
||| using the default equality test for the type of list elements.
elemIndex : Eq a => a -> List a -> Maybe Nat
elemIndex = elemIndexBy (==)

||| Find all indices for an element in a list, using a custom equality test.
elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat
elemIndicesBy p e = findIndices $ p e

||| Find all indices for an element in a list, using the default equality test for the type of list elements.
elemIndices : Eq a => a -> List a -> List Nat
elemIndices = elemIndicesBy (==)

--------------------------------------------------------------------------------
-- Filters
--------------------------------------------------------------------------------

||| filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; e.g.,
|||
||| ````idris example
||| filter (< 3) [Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z)))]
||| ````
|||
filter : (a -> Bool) -> List a -> List a
filter p []      = []
filter p (x::xs) =
  if p x then
    x :: filter p xs
  else
    filter p xs

||| A filtered list is no longer than its input
filterSmaller : (xs : _) -> LTE (length (filter p xs)) (length xs)
filterSmaller [] = LTEZero
filterSmaller {p} (x :: xs) with (p x)
  filterSmaller {p = p} (x :: xs) | False = lteSuccRight (filterSmaller xs)
  filterSmaller {p = p} (x :: xs) | True = LTESucc (filterSmaller xs)


||| The nubBy function behaves just like nub, except it uses a user-supplied equality predicate instead of the overloaded == function.
nubBy : (a -> a -> Bool) -> List a -> List a
nubBy = nubBy' []
  where
    nubBy' : List a -> (a -> a -> Bool) -> List a -> List a
    nubBy' acc p []      = []
    nubBy' acc p (x::xs) =
      if elemBy p x acc then
        nubBy' acc p xs
      else
        x :: nubBy' (x::acc) p xs

||| O(n^2). The nub function removes duplicate elements from a list. In
||| particular, it keeps only the first occurrence of each element. It is a
||| special case of nubBy, which allows the programmer to supply their own
||| equality test.
|||
||| ```idris example
||| nub (the (List _) [1,2,1,3])
||| ```
nub : Eq a => List a -> List a
nub = nubBy (==)

||| The deleteBy function behaves like delete, but takes a user-supplied equality predicate.
deleteBy : (a -> a -> Bool) -> a -> List a -> List a
deleteBy _  _ []      = []
deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys

||| `delete x` removes the first occurrence of `x` from its list argument. For
||| example,
|||
|||````idris example
|||delete 'a' ['b', 'a', 'n', 'a', 'n', 'a']
|||````
|||
||| It is a special case of deleteBy, which allows the programmer to supply
||| their own equality test.
delete : (Eq a) => a -> List a -> List a
delete = deleteBy (==)

||| The `\\` function is list difference (non-associative). In the result of
||| `xs \\ ys`, the first occurrence of each element of ys in turn (if any) has
||| been removed from `xs`, e.g.,
|||
||| ```idris example
||| (([1,2] ++ [2,3]) \\ [1,2])
||| ```
(\\) : (Eq a) => List a -> List a -> List a
(\\) =  foldl (flip delete)

||| The unionBy function returns the union of two lists by user-supplied equality predicate.
unionBy : (a -> a -> Bool) -> List a -> List a -> List a
unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

||| Compute the union of two lists according to their `Eq` implementation.
|||
||| ```idris example
||| union ['d', 'o', 'g'] ['c', 'o', 'w']
||| ```
|||
union : (Eq a) => List a -> List a -> List a
union = unionBy (==)

--------------------------------------------------------------------------------
-- Splitting and breaking lists
--------------------------------------------------------------------------------

||| Given a list and a predicate, returns a pair consisting of the longest
||| prefix of the list that satisfies a predicate and the rest of the list.
|||
||| ```idris example
||| span (<3) [1,2,3,2,1]
||| ```
span : (a -> Bool) -> List a -> (List a, List a)
span p []      = ([], [])
span p (x::xs) =
  if p x then
    let (ys, zs) = span p xs in
      (x::ys, zs)
  else
    ([], x::xs)

||| Given a list and a predicate, returns a pair consisting of the longest
||| prefix of the list that does not satisfy a predicate and the rest of the
||| list.
|||
||| ```idris example
||| break (>=3) [1,2,3,2,1]
||| ```
break : (a -> Bool) -> List a -> (List a, List a)
break p = span (not . p)

||| Split on any elements that satisfy the given predicate.
|||
||| ```idris example
||| split (<2) [2,0,3,1,4]
||| ```
split : (a -> Bool) -> List a -> List (List a)
split p xs =
  case break p xs of
    (chunk, [])          => [chunk]
    (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest)

||| A tuple where the first element is a List of the n first elements and
||| the second element is a List of the remaining elements of the list
||| It is equivalent to (take n xs, drop n xs)
||| @ n   the index to split at
||| @ xs  the list to split in two
splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
splitAt n xs = (take n xs, drop n xs)

||| The partition function takes a predicate a list and returns the pair of lists of elements which do and do not satisfy the predicate, respectively; e.g.,
|||
||| ```idris example
||| partition (<3) [0, 1, 2, 3, 4, 5]
||| ```
partition : (a -> Bool) -> List a -> (List a, List a)
partition p []      = ([], [])
partition p (x::xs) =
  let (lefts, rights) = partition p xs in
    if p x then
      (x::lefts, rights)
    else
      (lefts, x::rights)

||| The inits function returns all initial segments of the argument, shortest
||| first. For example,
|||
||| ```idris example
||| inits [1,2,3]
||| ```
inits : List a -> List (List a)
inits xs = [] :: case xs of
  []        => []
  x :: xs'  => map (x ::) (inits xs')

||| The tails function returns all final segments of the argument, longest
||| first. For example,
|||
||| ```idris example
||| tails [1,2,3] == [[1,2,3], [2,3], [3], []]
|||```
tails : List a -> List (List a)
tails xs = xs :: case xs of
  []        => []
  _ :: xs'  => tails xs'

||| Split on the given element.
|||
||| ```idris example
||| splitOn 0 [1,0,2,0,0,3]
||| ```
|||
splitOn : Eq a => a -> List a -> List (List a)
splitOn a = split (== a)

||| Replaces all occurences of the first argument with the second argument in a list.
|||
||| ```idris example
||| replaceOn '-' ',' ['1', '-', '2', '-', '3']
||| ```
|||
replaceOn : Eq a => a -> a -> List a -> List a
replaceOn a b l = map (\c => if c == a then b else c) l

--------------------------------------------------------------------------------
-- Predicates
--------------------------------------------------------------------------------

||| Check whether a list is a prefix of another according to a user-supplied equality test.
|||
||| @ eq the equality comparison
||| @ left the potential prefix
||| @ right the list that may have `left` as its prefix
isPrefixOfBy : (eq : a -> a -> Bool) -> (left, right : List a) -> Bool
isPrefixOfBy p [] right        = True
isPrefixOfBy p left []         = False
isPrefixOfBy p (x::xs) (y::ys) =
  if p x y then
    isPrefixOfBy p xs ys
  else
    False

||| The isPrefixOf function takes two lists and returns True iff the first list is a prefix of the second.
isPrefixOf : Eq a => List a -> List a -> Bool
isPrefixOf = isPrefixOfBy (==)

isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)

||| The isSuffixOf function takes two lists and returns True iff the first list is a suffix of the second.
isSuffixOf : Eq a => List a -> List a -> Bool
isSuffixOf = isSuffixOfBy (==)

||| The isInfixOf function takes two lists and returns True iff the first list is contained, wholly and intact, anywhere within the second.
|||
||| ```idris example
||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']
||| ```
||| ```idris example
||| isInfixOf ['b','d'] ['a', 'b', 'c', 'd']
||| ```
|||
isInfixOf : Eq a => List a -> List a -> Bool
isInfixOf n h = any (isPrefixOf n) (tails h)

--------------------------------------------------------------------------------
-- Sorting
--------------------------------------------------------------------------------

||| Check whether a list is sorted with respect to the default ordering for the type of its elements.
sorted : Ord a => List a -> Bool
sorted []      = True
sorted (x::xs) =
  case xs of
    Nil     => True
    (y::ys) => x <= y && sorted (y::ys)

||| Merge two sorted lists using an arbitrary comparison
||| predicate. Note that the lists must have been sorted using this
||| predicate already.
mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
mergeBy order []      right   = right
mergeBy order left    []      = left
mergeBy order (x::xs) (y::ys) =
  case order x y of
       LT => x :: mergeBy order xs (y::ys)
       _  => y :: mergeBy order (x::xs) ys

||| Merge two sorted lists using the default ordering for the type of their elements.
merge : Ord a => List a -> List a -> List a
merge = mergeBy compare

||| Sort a list using some arbitrary comparison predicate.
|||
||| @ cmp how to compare elements
||| @ xs the list to sort
sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
sortBy cmp []  = []
sortBy cmp [x] = [x]
sortBy cmp xs  = let (x, y) = split xs in
    mergeBy cmp
          (sortBy cmp (assert_smaller xs x))
          (sortBy cmp (assert_smaller xs y)) -- not structurally smaller, hence assert
  where
    splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)
    splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))
    splitRec _          ys      zs = (zs [], ys)

    split : List a -> (List a, List a)
    split xs = splitRec xs xs id

||| Sort a list using the default ordering for the type of its elements.
sort : Ord a => List a -> List a
sort = sortBy compare

--------------------------------------------------------------------------------
-- Conversions
--------------------------------------------------------------------------------

||| Either return the head of a list, or `Nothing` if it is empty.
listToMaybe : List a -> Maybe a
listToMaybe []      = Nothing
listToMaybe (x::xs) = Just x

--------------------------------------------------------------------------------
-- Misc
--------------------------------------------------------------------------------

||| Keep the `Just` elements in a list, discarding the `Nothing` elements.
catMaybes : List (Maybe a) -> List a
catMaybes []      = []
catMaybes (x::xs) =
  case x of
    Nothing => catMaybes xs
    Just j  => j :: catMaybes xs

--------------------------------------------------------------------------------
-- Properties
--------------------------------------------------------------------------------

||| The empty list is a right identity for append.
appendNilRightNeutral : (l : List a) ->
  l ++ [] = l
appendNilRightNeutral []      = Refl
appendNilRightNeutral (x::xs) =
  let inductiveHypothesis = appendNilRightNeutral xs in
    rewrite inductiveHypothesis in Refl

||| Appending lists is associative.
appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
  l ++ (c ++ r) = (l ++ c) ++ r
appendAssociative []      c r = Refl
appendAssociative (x::xs) c r =
  let inductiveHypothesis = appendAssociative xs c r in
    rewrite inductiveHypothesis in Refl

||| The length of two lists that are appended is the sum of the lengths
||| of the input lists.
lengthAppend : (left : List a) -> (right : List a) ->
  length (left ++ right) = length left + length right
lengthAppend []      right = Refl
lengthAppend (x::xs) right =
  let inductiveHypothesis = lengthAppend xs right in
    rewrite inductiveHypothesis in Refl

||| Mapping a function over a list doesn't change its length.
mapPreservesLength : (f : a -> b) -> (l : List a) ->
  length (map f l) = length l
mapPreservesLength f []      = Refl
mapPreservesLength f (x::xs) =
  let inductiveHypothesis = mapPreservesLength f xs in
    rewrite inductiveHypothesis in Refl

||| Mapping a function over two lists and appending them is equivalent
||| to appending them and then mapping the function.
mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->
  map f (l ++ r) = map f l ++ map f r
mapDistributesOverAppend f []      r = Refl
mapDistributesOverAppend f (x::xs) r =
  let inductiveHypothesis = mapDistributesOverAppend f xs r in
    rewrite inductiveHypothesis in Refl

||| Mapping two functions is the same as mapping their composition.
mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
  map f (map g l) = map (f . g) l
mapFusion f g []      = Refl
mapFusion f g (x::xs) =
  let inductiveHypothesis = mapFusion f g xs in
    rewrite inductiveHypothesis in Refl

||| No list contains an element of the empty list by any predicate.
hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
  hasAnyBy p [] l = False
hasAnyByNilFalse p []      = Refl
hasAnyByNilFalse p (x::xs) =
  let inductiveHypothesis = hasAnyByNilFalse p xs in
    rewrite inductiveHypothesis in Refl

||| No list contains an element of the empty list.
hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
hasAnyNilFalse l = rewrite (hasAnyByNilFalse (==) l) in Refl

||| Implement foldl using foldr, for a later equality proof.
foldlAsFoldr : (b -> a -> b) -> b -> List a -> b
foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z

||| The definition of foldl works the same as the default definition
||| in terms of foldr
foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs
foldlMatchesFoldr f q [] = Refl
foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs