@@ -47,25 +47,35 @@ isCons (x::xs) = True
47-- Decidable Predicates
47-- Decidable Predicates
48--------------------------------------------------------------------------------
48--------------------------------------------------------------------------------
50+||| Satisfiable if `xs` is non-empty (e.g., if `xs` is a cons).
50−data NonEmpty : List a -> Type where
51+data NonEmpty : (xs : List a) -> Type where
52+ ||| The proof that a cons cell is non-empty
51− IsNonEmpty : NonEmpty (x :: xs)
53+ IsNonEmpty : NonEmpty (x :: xs)
54nonEmptyNil : NonEmpty [] -> Void
56nonEmptyNil : NonEmpty [] -> Void
55nonEmptyNil IsNonEmpty impossible
57nonEmptyNil IsNonEmpty impossible
59+||| Decide whether a list is non-empty
57nonEmpty : (xs : List a) -> Dec (NonEmpty xs)
60nonEmpty : (xs : List a) -> Dec (NonEmpty xs)
58nonEmpty [] = No nonEmptyNil
61nonEmpty [] = No nonEmptyNil
59nonEmpty (x :: xs) = Yes IsNonEmpty
62nonEmpty (x :: xs) = Yes IsNonEmpty
64+||| Satisfiable if `k` is a valid index into `xs`
66+||| @ k the potential index
67+||| @ xs the list into which k may be an index
61−data InBounds : Nat -> List a -> Type where
68+data InBounds : (k : Nat) -> (xs : List a) -> Type where
69+ ||| Z is a valid index into any cons cell
62− InFirst : InBounds Z (x :: xs)
70+ InFirst : InBounds Z (x :: xs)
71+ ||| Valid indices can be extended
63− InLater : InBounds k xs -> InBounds (S k) (x :: xs)
72+ InLater : InBounds k xs -> InBounds (S k) (x :: xs)
65instance Uninhabited (InBounds k []) where
74instance Uninhabited (InBounds k []) where
66 uninhabited InFirst impossible
75 uninhabited InFirst impossible
77+||| Decide whether `k` is a valid index into `xs`
68−inBounds : (n : Nat) -> (xs : List a) -> Dec (InBounds n xs)
78+inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)
69inBounds k [] = No uninhabited
79inBounds k [] = No uninhabited
70inBounds Z (x :: xs) = Yes InFirst
80inBounds Z (x :: xs) = Yes InFirst
71inBounds (S k) (x :: xs) with (inBounds k xs)
81inBounds (S k) (x :: xs) with (inBounds k xs)
@@ -339,7 +349,7 @@ mapMaybe f (x::xs) =
339instance Foldable List where
349instance Foldable List where
340 foldr c n [] = n
350 foldr c n [] = n
341 foldr c n (x::xs) = c x (foldr c n xs)
351 foldr c n (x::xs) = c x (foldr c n xs)
343 foldl f q [] = q
353 foldl f q [] = q
344 foldl f q (x::xs) = foldl f (f q x) xs
354 foldl f q (x::xs) = foldl f (f q x) xs
@@ -377,8 +387,13 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
377 intersperse' sep [] = []
387 intersperse' sep [] = []
378 intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
388 intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
390+||| Given a separator list and some more lists, produce a new list by
391+||| placing the separator between each of the lists.
393+||| @ sep the separator
394+||| @ xss the lists between which the separator will be placed
380−intercalate : List a -> List (List a) -> List a
395+intercalate : (sep : List a) -> (xss : List (List a)) -> List a
381−intercalate sep l = concat $ intersperse sep l
396+intercalate sep xss = concat $ intersperse sep xss
383||| Transposes rows and columns of a list of lists.
398||| Transposes rows and columns of a list of lists.
@@ -483,15 +498,20 @@ findIndices = findIndices' Z
484 findIndices' (S cnt) p xs
499 findIndices' (S cnt) p xs
501+||| Find the index of the first occurrence of an element in a list, using a custom equality test.
486elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat
502elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat
487elemIndexBy p e = findIndex $ p e
503elemIndexBy p e = findIndex $ p e
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.
489elemIndex : Eq a => a -> List a -> Maybe Nat
507elemIndex : Eq a => a -> List a -> Maybe Nat
490elemIndex = elemIndexBy (==)
508elemIndex = elemIndexBy (==)
510+||| Find all indices for an element in a list, using a custom equality test.
492elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat
511elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat
493elemIndicesBy p e = findIndices $ p e
512elemIndicesBy p e = findIndices $ p e
514+||| Find all indices for an element in a list, using the default equality test for the type of list elements.
495elemIndices : Eq a => a -> List a -> List Nat
515elemIndices : Eq a => a -> List a -> List Nat
496elemIndices = elemIndicesBy (==)
516elemIndices = elemIndicesBy (==)
@@ -682,7 +702,12 @@ replaceOn a b l = map (\c => if c == a then b else c) l
682-- Predicates
702-- Predicates
683--------------------------------------------------------------------------------
703--------------------------------------------------------------------------------
705+||| Check whether a list is a prefix of another according to a user-supplied equality test.
707+||| @ eq the equality comparison
708+||| @ left the potential prefix
709+||| @ right the list that may have `left` as its prefix
685−isPrefixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
710+isPrefixOfBy : (eq : a -> a -> Bool) -> (left, right : List a) -> Bool
686isPrefixOfBy p [] right = True
711isPrefixOfBy p [] right = True
687isPrefixOfBy p left [] = False
712isPrefixOfBy p left [] = False
688isPrefixOfBy p (x::xs) (y::ys) =
713isPrefixOfBy p (x::xs) (y::ys) =
@@ -777,6 +802,7 @@ listToMaybe (x::xs) = Just x
778--------------------------------------------------------------------------------
803--------------------------------------------------------------------------------
805+||| Keep the `Just` elements in a list, discarding the `Nothing` elements.
780catMaybes : List (Maybe a) -> List a
806catMaybes : List (Maybe a) -> List a
781catMaybes [] = []
807catMaybes [] = []
782catMaybes (x::xs) =
808catMaybes (x::xs) =
@@ -850,6 +876,7 @@ hasAnyByNilFalse p (x::xs) =
850hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
876hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
851hasAnyNilFalse l = rewrite (hasAnyByNilFalse (==) l) in Refl
877hasAnyNilFalse l = rewrite (hasAnyByNilFalse (==) l) in Refl
879+||| Implement foldl using foldr, for a later equality proof.
853foldlAsFoldr : (b -> a -> b) -> b -> List a -> b
880foldlAsFoldr : (b -> a -> b) -> b -> List a -> b
854foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z
881foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z