@@ -157,7 +157,7 @@ drop Z xs = xs
157157drop (S n) [] = []
158158drop (S n) (x::xs) = drop n xs
159159
160−||| Take the longest prefix of a list such that all elements satsify some
160+||| Take the longest prefix of a list such that all elements satisfy some
161161||| Boolean predicate.
162162|||
163163||| @ p the predicate
@@ -165,7 +165,7 @@ takeWhile : (p : a -> Bool) -> List a -> List a
165165takeWhile p [] = []
166166takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
167167
168−||| Remove the longest prefix of a list such that all removed elements satsify some
168+||| Remove the longest prefix of a list such that all removed elements satisfy some
169169||| Boolean predicate.
170170|||
171171||| @ p the predicate
@@ -340,6 +340,9 @@ reverse = reverse' []
340340 reverse' acc (x::xs) = reverse' (x::acc) xs
341341
342342||| Insert some separator between the elements of a list.
343+|||
344+||| > intersperse ',' (unpack "abcde") == unpack "a,b,c,d,e"
345+|||
343346intersperse : a -> List a -> List a
344347intersperse sep [] = []
345348intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -468,6 +471,10 @@ elemIndices = elemIndicesBy (==)
468471-- Filters
469472--------------------------------------------------------------------------------
470473
474+||| filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; e.g.,
475+|||
476+||| > filter (<3) [0..5] == [0,1,2]
477+|||
471478filter : (a -> Bool) -> List a -> List a
472479filter p [] = []
473480filter p (x::xs) =
@@ -476,6 +483,7 @@ filter p (x::xs) =
476483 else
477484 filter p xs
478485
486+||| The nubBy function behaves just like nub, except it uses a user-supplied equality predicate instead of the overloaded == function.
479487nubBy : (a -> a -> Bool) -> List a -> List a
480488nubBy = nubBy' []
481489 where
@@ -487,22 +495,40 @@ nubBy = nubBy' []
487495 else
488496 x :: nubBy' (x::acc) p xs
489497
498+||| 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.
499+|||
500+||| > nub (the (List _) [1,2,1,3]) == [1,2,3]
501+|||
490502nub : Eq a => List a -> List a
491503nub = nubBy (==)
492504
505+||| The deleteBy function behaves like delete, but takes a user-supplied equality predicate.
493506deleteBy : (a -> a -> Bool) -> a -> List a -> List a
494507deleteBy _ _ [] = []
495508deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys
496509
510+||| delete x removes the first occurrence of x from its list argument. For example,
511+|||
512+||| > delete 'a' (unpack "banana") == unpack "bnana"
513+|||
514+||| It is a special case of deleteBy, which allows the programmer to supply their own equality test.
497515delete : (Eq a) => a -> List a -> List a
498516delete = deleteBy (==)
499517
518+||| 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.,
519+|||
520+||| > (([1,2] ++ [2,3]) \\ [1,2]) == [2,3]
521+|||
500522(\\) : (Eq a) => List a -> List a -> List a
501523(\\) = foldl (flip delete)
502524
503525unionBy : (a -> a -> Bool) -> List a -> List a -> List a
504526unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
505527
528+||| The union function returns the list union of the two lists. For example,
529+|||
530+||| > union (unpack "dog") (unpack "cow") == unpack "dogcw"
531+|||
506532union : (Eq a) => List a -> List a -> List a
507533union = unionBy (==)
508534
@@ -512,6 +538,9 @@ union = unionBy (==)
512538
513539||| Given a list and a predicate, returns a pair consisting of the longest
514540||| prefix of the list that satisfies a predicate and the rest of the list.
541+|||
542+||| > span (<3) [1,2,3,2,1] == the ((List _, List _)) ([1, 2], [3, 2, 1])
543+|||
515544span : (a -> Bool) -> List a -> (List a, List a)
516545span p [] = ([], [])
517546span p (x::xs) =
@@ -521,9 +550,18 @@ span p (x::xs) =
521550 else
522551 ([], x::xs)
523552
553+||| Given a list and a predicate, returns a pair consisting of the longest
554+||| prefix of the list that does not satisfy a predicate and the rest of the list.
555+|||
556+||| > break (>=3) [1,2,3,2,1] == the ((List _, List _)) ([1, 2], [3, 2, 1])
557+|||
524558break : (a -> Bool) -> List a -> (List a, List a)
525559break p = span (not . p)
526560
561+||| Split on any elements that satisfy the given predicate.
562+|||
563+||| > split (<2) [2,0,3,1,4] == [[2], [3], [4]]
564+|||
527565split : (a -> Bool) -> List a -> List (List a)
528566split p xs =
529567 case break p xs of
@@ -538,6 +576,10 @@ split p xs =
538576splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
539577splitAt n xs = (take n xs, drop n xs)
540578
579+||| 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.,
580+|||
581+||| > partition (<3) [0..5] == (the (List Integer) [0,1,2], the (List Integer) [3,4,5])
582+|||
541583partition : (a -> Bool) -> List a -> (List a, List a)
542584partition p [] = ([], [])
543585partition p (x::xs) =
@@ -547,19 +589,35 @@ partition p (x::xs) =
547589 else
548590 (lefts, x::rights)
549591
592+||| The inits function returns all initial segments of the argument, shortest first. For example,
593+|||
594+||| > inits [1,2,3] == [[],[1],[1,2],[1,2,3]]
595+|||
550596inits : List a -> List (List a)
551597inits xs = [] :: case xs of
552598 [] => []
553599 x :: xs' => map (x ::) (inits xs')
554600
601+||| The tails function returns all final segments of the argument, longest first. For example,
602+|||
603+||| > tails [1,2,3] == [[1,2,3], [2,3], [3], []]
604+|||
555605tails : List a -> List (List a)
556606tails xs = xs :: case xs of
557607 [] => []
558608 _ :: xs' => tails xs'
559609
610+||| Split on the given element.
611+|||
612+||| > splitOn 0 [1,0,2,0,0,3] == [[1],[2],[],[3]]
613+|||
560614splitOn : Eq a => a -> List a -> List (List a)
561615splitOn a = split (== a)
562616
617+||| Replaces all occurences of the first argument with the second argument in a list.
618+|||
619+||| > replaceOn '-' ',' (unpack "1-2-3") == unpack "1,2,3"
620+|||
563621replaceOn : Eq a => a -> a -> List a -> List a
564622replaceOn a b l = map (\c => if c == a then b else c) l
565623
@@ -576,15 +634,22 @@ isPrefixOfBy p (x::xs) (y::ys) =
576634 else
577635 False
578636
637+||| The isPrefixOf function takes two lists and returns True iff the first list is a prefix of the second.
579638isPrefixOf : Eq a => List a -> List a -> Bool
580639isPrefixOf = isPrefixOfBy (==)
581640
582641isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
583642isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
584643
644+||| The isSuffixOf function takes two lists and returns True iff the first list is a suffix of the second.
585645isSuffixOf : Eq a => List a -> List a -> Bool
586646isSuffixOf = isSuffixOfBy (==)
587647
648+||| The isInfixOf function takes two lists and returns True iff the first list is contained, wholly and intact, anywhere within the second.
649+|||
650+||| > isInfixOf "Idris" "I really like Idris." == True
651+||| > isInfixOf "Ial" "I really like Idris." == False
652+|||
588653isInfixOf : Eq a => List a -> List a -> Bool
589654isInfixOf n h = any (isPrefixOf n) (tails h)
590655