From baba8f61db4081e7374e43b5671c2ece713c8ca5 Mon Sep 17 00:00:00 2001
From: David Raymond Christiansen <david@davidchristiansen.dk>
Date: Mon, 17 Aug 2015 20:47:55 -0700
Subject: [PATCH 1/2] Add sortBy on lists and documentation for sorting

---
 libs/prelude/Prelude/List.idr | 26 ++++++++++++++++++++------
 1 file changed, 20 insertions(+), 6 deletions(-)

diff --git a/libs/prelude/Prelude/List.idr b/libs/prelude/Prelude/List.idr
index 5d54525e7..54f023b66 100644
--- a/libs/prelude/Prelude/List.idr
+++ b/libs/prelude/Prelude/List.idr
@@ -718,6 +718,7 @@ 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) =
@@ -725,6 +726,9 @@ sorted (x::xs) =
     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
@@ -733,15 +737,21 @@ mergeBy order (x::xs) (y::ys) =
      then x :: mergeBy order xs (y::ys)
      else 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 : Ord a => List a -> List a
-sort []  = []
-sort [x] = [x]
-sort xs  = let (x, y) = split xs in
-    merge (sort (assert_smaller xs x)) 
-          (sort (assert_smaller xs y)) -- not structurally smaller, hence assert
+||| 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))
@@ -750,6 +760,10 @@ sort xs  = let (x, y) = split xs in
     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
 --------------------------------------------------------------------------------

From db83920876694b559847c7416ca075725e786aed Mon Sep 17 00:00:00 2001
From: David Raymond Christiansen <david@davidchristiansen.dk>
Date: Mon, 17 Aug 2015 21:02:20 -0700
Subject: [PATCH 2/2] Document all exports of Prelude.List

---
 libs/prelude/Prelude/List.idr | 47 +++++++++++++++++++++++++++--------
 1 file changed, 37 insertions(+), 10 deletions(-)

diff --git a/libs/prelude/Prelude/List.idr b/libs/prelude/Prelude/List.idr
index 54f023b66..619491c30 100644
--- a/libs/prelude/Prelude/List.idr
+++ b/libs/prelude/Prelude/List.idr
@@ -47,25 +47,35 @@ isCons (x::xs) = True
 -- Decidable Predicates
 --------------------------------------------------------------------------------
 
-data NonEmpty : List a -> Type where
-     IsNonEmpty : NonEmpty (x :: xs)
+||| 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)
 
 private
 nonEmptyNil : NonEmpty [] -> Void
 nonEmptyNil IsNonEmpty impossible
 
+||| Decide whether a list is non-empty
 nonEmpty : (xs : List a) -> Dec (NonEmpty xs)
 nonEmpty [] = No nonEmptyNil
 nonEmpty (x :: xs) = Yes IsNonEmpty
 
-data InBounds : Nat -> List a -> Type where
-     InFirst : InBounds Z (x :: xs)
-     InLater : InBounds k xs -> InBounds (S k) (x :: xs)
+||| 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)
 
 instance Uninhabited (InBounds k []) where
     uninhabited InFirst impossible
 
-inBounds : (n : Nat) -> (xs : List a) -> Dec (InBounds n xs)
+||| 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)
@@ -339,7 +349,7 @@ mapMaybe f (x::xs) =
 instance 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
 
@@ -377,8 +387,13 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
     intersperse' sep []      = []
     intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
 
-intercalate : List a -> List (List a) -> List a
-intercalate sep l = concat $ intersperse sep l
+||| 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.
 |||
@@ -483,15 +498,20 @@ findIndices = findIndices' Z
       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 (==)
 
@@ -682,7 +702,12 @@ replaceOn a b l = map (\c => if c == a then b else c) l
 -- Predicates
 --------------------------------------------------------------------------------
 
-isPrefixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
+||| 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) =
@@ -777,6 +802,7 @@ 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) =
@@ -850,6 +876,7 @@ hasAnyByNilFalse p (x::xs) =
 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