@@ -47,25 +47,35 @@ isCons (x::xs) = True
4747-- Decidable Predicates
4848--------------------------------------------------------------------------------
4949
50−data NonEmpty : List a -> Type where
51− IsNonEmpty : NonEmpty (x :: xs)
50+||| Satisfiable if `xs` is non-empty (e.g., if `xs` is a cons).
51+data NonEmpty : (xs : List a) -> Type where
52+ ||| The proof that a cons cell is non-empty
53+ IsNonEmpty : NonEmpty (x :: xs)
5254
5355private
5456nonEmptyNil : NonEmpty [] -> Void
5557nonEmptyNil IsNonEmpty impossible
5658
59+||| Decide whether a list is non-empty
5760nonEmpty : (xs : List a) -> Dec (NonEmpty xs)
5861nonEmpty [] = No nonEmptyNil
5962nonEmpty (x :: xs) = Yes IsNonEmpty
6063
61−data InBounds : Nat -> List a -> Type where
62− InFirst : InBounds Z (x :: xs)
63− InLater : InBounds k xs -> InBounds (S k) (x :: xs)
64+||| Satisfiable if `k` is a valid index into `xs`
65+|||
66+||| @ k the potential index
67+||| @ xs the list into which k may be an index
68+data InBounds : (k : Nat) -> (xs : List a) -> Type where
69+ ||| Z is a valid index into any cons cell
70+ InFirst : InBounds Z (x :: xs)
71+ ||| Valid indices can be extended
72+ InLater : InBounds k xs -> InBounds (S k) (x :: xs)
6473
6574instance Uninhabited (InBounds k []) where
6675 uninhabited InFirst impossible
6776
68−inBounds : (n : Nat) -> (xs : List a) -> Dec (InBounds n xs)
77+||| Decide whether `k` is a valid index into `xs`
78+inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)
6979inBounds k [] = No uninhabited
7080inBounds Z (x :: xs) = Yes InFirst
7181inBounds (S k) (x :: xs) with (inBounds k xs)
@@ -339,7 +349,7 @@ mapMaybe f (x::xs) =
339349instance Foldable List where
340350 foldr c n [] = n
341351 foldr c n (x::xs) = c x (foldr c n xs)
342−
352+
343353 foldl f q [] = q
344354 foldl f q (x::xs) = foldl f (f q x) xs
345355
@@ -377,8 +387,13 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
377387 intersperse' sep [] = []
378388 intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
379389
380−intercalate : List a -> List (List a) -> List a
381−intercalate sep l = concat $ intersperse sep l
390+||| Given a separator list and some more lists, produce a new list by
391+||| placing the separator between each of the lists.
392+|||
393+||| @ sep the separator
394+||| @ xss the lists between which the separator will be placed
395+intercalate : (sep : List a) -> (xss : List (List a)) -> List a
396+intercalate sep xss = concat $ intersperse sep xss
382397
383398||| Transposes rows and columns of a list of lists.
384399|||
@@ -483,15 +498,20 @@ findIndices = findIndices' Z
483498 else
484499 findIndices' (S cnt) p xs
485500
501+||| Find the index of the first occurrence of an element in a list, using a custom equality test.
486502elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat
487503elemIndexBy p e = findIndex $ p e
488504
505+||| Find the index of the first occurrence of an element in a list,
506+||| using the default equality test for the type of list elements.
489507elemIndex : Eq a => a -> List a -> Maybe Nat
490508elemIndex = elemIndexBy (==)
491509
510+||| Find all indices for an element in a list, using a custom equality test.
492511elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat
493512elemIndicesBy p e = findIndices $ p e
494513
514+||| Find all indices for an element in a list, using the default equality test for the type of list elements.
495515elemIndices : Eq a => a -> List a -> List Nat
496516elemIndices = elemIndicesBy (==)
497517
@@ -682,7 +702,12 @@ replaceOn a b l = map (\c => if c == a then b else c) l
682702-- Predicates
683703--------------------------------------------------------------------------------
684704
685−isPrefixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
705+||| Check whether a list is a prefix of another according to a user-supplied equality test.
706+|||
707+||| @ eq the equality comparison
708+||| @ left the potential prefix
709+||| @ right the list that may have `left` as its prefix
710+isPrefixOfBy : (eq : a -> a -> Bool) -> (left, right : List a) -> Bool
686711isPrefixOfBy p [] right = True
687712isPrefixOfBy p left [] = False
688713isPrefixOfBy p (x::xs) (y::ys) =
@@ -718,6 +743,7 @@ isInfixOf n h = any (isPrefixOf n) (tails h)
718743-- Sorting
719744--------------------------------------------------------------------------------
720745
746+||| Check whether a list is sorted with respect to the default ordering for the type of its elements.
721747sorted : Ord a => List a -> Bool
722748sorted [] = True
723749sorted (x::xs) =
@@ -725,6 +751,9 @@ sorted (x::xs) =
725751 Nil => True
726752 (y::ys) => x <= y && sorted (y::ys)
727753
754+||| Merge two sorted lists using an arbitrary comparison
755+||| predicate. Note that the lists must have been sorted using this
756+||| predicate already.
728757mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
729758mergeBy order [] right = right
730759mergeBy order left [] = left
@@ -733,15 +762,21 @@ mergeBy order (x::xs) (y::ys) =
733762 then x :: mergeBy order xs (y::ys)
734763 else y :: mergeBy order (x::xs) ys
735764
765+||| Merge two sorted lists using the default ordering for the type of their elements.
736766merge : Ord a => List a -> List a -> List a
737767merge = mergeBy compare
738768
739−sort : Ord a => List a -> List a
740−sort [] = []
741−sort [x] = [x]
742−sort xs = let (x, y) = split xs in
743− merge (sort (assert_smaller xs x))
744− (sort (assert_smaller xs y)) -- not structurally smaller, hence assert
769+||| Sort a list using some arbitrary comparison predicate.
770+|||
771+||| @ cmp how to compare elements
772+||| @ xs the list to sort
773+sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
774+sortBy cmp [] = []
775+sortBy cmp [x] = [x]
776+sortBy cmp xs = let (x, y) = split xs in
777+ mergeBy cmp
778+ (sortBy cmp (assert_smaller xs x))
779+ (sortBy cmp (assert_smaller xs y)) -- not structurally smaller, hence assert
745780 where
746781 splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)
747782 splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))
@@ -750,6 +785,10 @@ sort xs = let (x, y) = split xs in
750785 split : List a -> (List a, List a)
751786 split xs = splitRec xs xs id
752787
788+||| Sort a list using the default ordering for the type of its elements.
789+sort : Ord a => List a -> List a
790+sort = sortBy compare
791+
753792--------------------------------------------------------------------------------
754793-- Conversions
755794--------------------------------------------------------------------------------
@@ -763,6 +802,7 @@ listToMaybe (x::xs) = Just x
763802-- Misc
764803--------------------------------------------------------------------------------
765804
805+||| Keep the `Just` elements in a list, discarding the `Nothing` elements.
766806catMaybes : List (Maybe a) -> List a
767807catMaybes [] = []
768808catMaybes (x::xs) =
@@ -836,6 +876,7 @@ hasAnyByNilFalse p (x::xs) =
836876hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
837877hasAnyNilFalse l = rewrite (hasAnyByNilFalse (==) l) in Refl
838878
879+||| Implement foldl using foldr, for a later equality proof.
839880foldlAsFoldr : (b -> a -> b) -> b -> List a -> b
840881foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z
841882