@@ -14,9 +14,12 @@ import Prelude.Nat
1414
1515infixr 7 ::,++
1616
17−%elim data List a
18− = Nil
19− | (::) a (List a)
17+||| Linked lists
18+%elim data List a =
19+ ||| The empty list
20+ Nil |
21+ ||| Cons cell
22+ (::) a (List a)
2023
2124-- Name hints for interactive editing
2225%name List xs, ys, zs, ws
@@ -25,10 +28,12 @@ infixr 7 ::,++
2528-- Syntactic tests
2629--------------------------------------------------------------------------------
2730
31+||| Returns `True` iff the argument is empty
2832isNil : List a -> Bool
2933isNil [] = True
3034isNil (x::xs) = False
3135
36+||| Returns `True` iff the argument is not empty
3237isCons : List a -> Bool
3338isCons [] = False
3439isCons (x::xs) = True
@@ -37,6 +42,9 @@ isCons (x::xs) = True
3742-- Length
3843--------------------------------------------------------------------------------
3944
45+||| Compute the length of a list.
46+|||
47+||| Runs in linear time
4048length : List a -> Nat
4149length [] = 0
4250length (x::xs) = 1 + length xs
@@ -45,49 +53,74 @@ length (x::xs) = 1 + length xs
4553-- Indexing into lists
4654--------------------------------------------------------------------------------
4755
48−index : (n : Nat) -> (l : List a) -> (lt n (length l) = True) -> a
56+||| Find a particular element of a list.
57+|||
58+||| @ ok a proof that the index is within bounds
59+index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a
4960index Z (x::xs) p = x
5061index (S n) (x::xs) p = index n xs ?indexTailProof
5162index _ [] refl impossible
5263
64+||| Attempt to find a particular element of a list.
65+|||
66+||| If the provided index is out of bounds, return Nothing.
5367index' : (n : Nat) -> (l : List a) -> Maybe a
5468index' Z (x::xs) = Just x
5569index' (S n) (x::xs) = index' n xs
5670index' _ [] = Nothing
5771
58−head : (l : List a) -> (isCons l = True) -> a
72+||| Get the first element of a non-empty list
73+||| @ ok proof that the list is non-empty
74+head : (l : List a) -> (ok : isCons l = True) -> a
5975head [] refl impossible
6076head (x::xs) p = x
6177
78+||| Attempt to get the first element of a list. If the list is empty, return
79+||| `Nothing`.
6280head' : (l : List a) -> Maybe a
6381head' [] = Nothing
6482head' (x::xs) = Just x
6583
66−tail : (l : List a) -> (isCons l = True) -> List a
84+||| Get the tail of a non-empty list.
85+||| @ ok proof that the list is non-empty
86+tail : (l : List a) -> (ok : isCons l = True) -> List a
6787tail [] refl impossible
6888tail (x::xs) p = xs
6989
90+||| Attempt to get the tail of a list.
91+|||
92+||| If the list is empty, return `Nothing`.
7093tail' : (l : List a) -> Maybe (List a)
7194tail' [] = Nothing
7295tail' (x::xs) = Just xs
7396
74−last : (l : List a) -> (isCons l = True) -> a
97+||| Retrieve the last element of a non-empty list.
98+||| @ ok proof that the list is non-empty
99+last : (l : List a) -> (ok : isCons l = True) -> a
75100last [] refl impossible
76101last [x] p = x
77102last (x::y::ys) p = last (y::ys) refl
78103
104+||| Attempt to retrieve the last element of a non-empty list.
105+|||
106+||| If the list is empty, return `Nothing`.
79107last' : (l : List a) -> Maybe a
80108last' [] = Nothing
81−last' (x::xs) =
109+last' (x::xs) =
82110 case xs of
83111 [] => Just x
84112 y :: ys => last' xs
85113
86−init : (l : List a) -> (isCons l = True) -> List a
114+||| Return all but the last element of a non-empty list.
115+||| @ ok proof that the list is non-empty
116+init : (l : List a) -> (ok : isCons l = True) -> List a
87117init [] refl impossible
88118init [x] p = []
89119init (x::y::ys) p = x :: init (y::ys) refl
90120
121+||| Attempt to Return all but the last element of a list.
122+|||
123+||| If the list is empty, return `Nothing`.
91124init' : (l : List a) -> Maybe (List a)
92125init' [] = Nothing
93126init' (x::xs) =
@@ -103,21 +136,39 @@ init' (x::xs) =
103136-- Sublists
104137--------------------------------------------------------------------------------
105138
106−take : Nat -> List a -> List a
139+||| Take the first `n` elements of `xs`
140+|||
141+||| If there are not enough elements, return the whole list.
142+||| @ n how many elements to take
143+||| @ xs the list to take them from
144+take : (n : Nat) -> (xs : List a) -> List a
107145take Z xs = []
108146take (S n) [] = []
109147take (S n) (x::xs) = x :: take n xs
110148
111−drop : Nat -> List a -> List a
149+||| Drop the first `n` elements of `xs`
150+|||
151+||| If there are not enough elements, return the empty list.
152+||| @ n how many elements to drop
153+||| @ xs the list to drop them from
154+drop : (n : Nat) -> (xs : List a) -> List a
112155drop Z xs = xs
113156drop (S n) [] = []
114157drop (S n) (x::xs) = drop n xs
115158
116−takeWhile : (a -> Bool) -> List a -> List a
159+||| Take the longest prefix of a list such that all elements satsify some
160+||| Boolean predicate.
161+|||
162+||| @ p the predicate
163+takeWhile : (p : a -> Bool) -> List a -> List a
117164takeWhile p [] = []
118165takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
119166
120−dropWhile : (a -> Bool) -> List a -> List a
167+||| Remove the longest prefix of a list such that all removed elements satsify some
168+||| Boolean predicate.
169+|||
170+||| @ p the predicate
171+dropWhile : (p : a -> Bool) -> List a -> List a
121172dropWhile p [] = []
122173dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
123174
@@ -125,7 +176,12 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
125176-- Misc.
126177--------------------------------------------------------------------------------
127178
128−list : a -> (a -> List a -> a) -> List a -> a
179+||| Simply-typed recursion operator for lists.
180+|||
181+||| @ nil what to return at the end of the list
182+||| @ cons what to do at each step of recursion
183+||| @ xs the list to recurse over
184+list : (nil : a) -> (cons : a -> List a -> a) -> (xs : List a) -> a
129185list nil cons [] = nil
130186list nil cons (x::xs) = cons x xs
131187
@@ -133,16 +189,23 @@ list nil cons (x::xs) = cons x xs
133189-- Building (bigger) lists
134190--------------------------------------------------------------------------------
135191
192+||| Append two lists
136193(++) : List a -> List a -> List a
137−(++) [] right = right
194+(++) [] right = right
138195(++) (x::xs) right = x :: (xs ++ right)
139196
197+||| Create an infinite sequence of some item.
198+|||
199+||| Consider using a `Stream` instead.
140200partial
141201repeat : a -> List a
142202repeat x = x :: lazy (repeat x)
143203
144−replicate : Nat -> a -> List a
145−replicate Z x = []
204+||| Construct a list with `n` copies of `x`
205+||| @ n how many copies
206+||| @ x the element to replicate
207+replicate : (n : Nat) -> (x : a) -> List a
208+replicate Z x = []
146209replicate (S n) x = x :: replicate n x
147210
148211--------------------------------------------------------------------------------
@@ -187,15 +250,27 @@ instance Functor List where
187250-- Zips and unzips
188251--------------------------------------------------------------------------------
189252
253+||| Combine two lists of the same length elementwise using some function.
254+||| @ f the function to combine elements with
255+||| @ l the first list
256+||| @ r the second list
257+||| @ ok a proof that the lengths of the inputs are equal
190258zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
191− (length l = length r) -> List c
259+ (ok : length l = length r) -> List c
192260zipWith f [] (y::ys) refl impossible
193261zipWith f (x::xs) [] refl impossible
194262zipWith f [] [] p = []
195263zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
196264
265+||| Combine three lists of the same length elementwise using some function.
266+||| @ f the function to combine elements with
267+||| @ x the first list
268+||| @ y the second list
269+||| @ z the third list
270+||| @ ok a proof that the lengths of the first two inputs are equal
271+||| @ ok' a proof that the lengths of the second and third inputs are equal
197272zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
198− (z : List c) -> (length x = length y) -> (length y = length z) -> List d
273+ (z : List c) -> (ok : length x = length y) -> (ok' : length y = length z) -> List d
199274zipWith3 f _ [] (z::zs) p refl impossible
200275zipWith3 f _ (y::ys) [] p refl impossible
201276zipWith3 f [] (y::ys) _ refl q impossible
@@ -204,18 +279,22 @@ zipWith3 f [] [] [] p q = []
204279zipWith3 f (x::xs) (y::ys) (z::zs) p q =
205280 f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
206281
282+||| Combine two lists elementwise into pairs
207283zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
208284zip = zipWith (\x => \y => (x, y))
209285
286+||| Combine three lists elementwise into tuples
210287zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
211288 (length y = length z) -> List (a, b, c)
212289zip3 = zipWith3 (\x => \y => \z => (x, y, z))
213290
291+||| Split a list of pairs into two lists
214292unzip : List (a, b) -> (List a, List b)
215293unzip [] = ([], [])
216294unzip ((l, r)::xs) with (unzip xs)
217295 | (lefts, rights) = (l::lefts, r::rights)
218296
297+||| Split a list of triples into three lists
219298unzip3 : List (a, b, c) -> (List a, List b, List c)
220299unzip3 [] = ([], [], [])
221300unzip3 ((l, c, r)::xs) with (unzip3 xs)
@@ -225,6 +304,8 @@ unzip3 ((l, c, r)::xs) with (unzip3 xs)
225304-- Maps
226305--------------------------------------------------------------------------------
227306
307+||| Apply a partial function to the elements of a list, keeping the ones at which
308+||| it is defined.
228309mapMaybe : (a -> Maybe b) -> List a -> List b
229310mapMaybe f [] = []
230311mapMaybe f (x::xs) =
@@ -236,6 +317,7 @@ mapMaybe f (x::xs) =
236317-- Folds
237318--------------------------------------------------------------------------------
238319
320+||| A tail recursive right fold on Lists.
239321total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> List t -> acc
240322foldrImpl f e go [] = go e
241323foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
@@ -247,6 +329,7 @@ instance Foldable List where
247329-- Special folds
248330--------------------------------------------------------------------------------
249331
332+||| Convert any Foldable structure to a list.
250333toList : Foldable t => t a -> List a
251334toList = foldr (::) []
252335
@@ -254,6 +337,7 @@ toList = foldr (::) []
254337-- Transformations
255338--------------------------------------------------------------------------------
256339
340+||| Return the elements of a list in reverse order.
257341reverse : List a -> List a
258342reverse = reverse' []
259343 where
@@ -261,6 +345,7 @@ reverse = reverse' []
261345 reverse' acc [] = acc
262346 reverse' acc (x::xs) = reverse' (x::acc) xs
263347
348+||| Insert some separator between the elements of a list.
264349intersperse : a -> List a -> List a
265350intersperse sep [] = []
266351intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -274,13 +359,13 @@ intercalate sep l = concat $ intersperse sep l
274359
275360||| Transposes rows and columns of a list of lists.
276361|||
277−||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
362+||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
278363|||
279364||| This also works for non square scenarios, thus
280365||| involution does not always hold:
281366|||
282−||| > transpose [[], [1, 2]] = [[1], [2]]
283−||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]
367+||| > transpose [[], [1, 2]] = [[1], [2]]
368+||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]
284369|||
285370||| TODO: Solution which satisfies the totality checker?
286371%assert_total
@@ -293,6 +378,7 @@ transpose ((x::xs) :: xss) = (x :: (mapMaybe head' xss)) :: (transpose (xs :: (m
293378-- Membership tests
294379--------------------------------------------------------------------------------
295380
381+||| Check if something is a member of a list using a custom comparison.
296382elemBy : (a -> a -> Bool) -> a -> List a -> Bool
297383elemBy p e [] = False
298384elemBy p e (x::xs) =
@@ -301,9 +387,11 @@ elemBy p e (x::xs) =
301387 else
302388 elemBy p e xs
303389
390+||| Check if something is a member of a list using the default Boolean equality.
304391elem : Eq a => a -> List a -> Bool
305392elem = elemBy (==)
306393
394+||| Find associated information in a list using a custom comparison.
307395lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
308396lookupBy p e [] = Nothing
309397lookupBy p e (x::xs) =
@@ -313,9 +401,12 @@ lookupBy p e (x::xs) =
313401 else
314402 lookupBy p e xs
315403
404+||| Find associated information in a list using Boolean equality.
316405lookup : Eq a => a -> List (a, b) -> Maybe b
317406lookup = lookupBy (==)
318407
408+||| Check if any elements of the first list are found in the second, using
409+||| a custom comparison.
319410hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
320411hasAnyBy p elems [] = False
321412hasAnyBy p elems (x::xs) =
@@ -324,6 +415,8 @@ hasAnyBy p elems (x::xs) =
324415 else
325416 hasAnyBy p elems xs
326417
418+||| Check if any elements of the first list are found in the second, using
419+||| Boolean equality.
327420hasAny : Eq a => List a -> List a -> Bool
328421hasAny = hasAnyBy (==)
329422
@@ -331,6 +424,7 @@ hasAny = hasAnyBy (==)
331424-- Searching with a predicate
332425--------------------------------------------------------------------------------
333426
427+||| Find the first element of a list that satisfies a predicate, or `Nothing` if none do.
334428find : (a -> Bool) -> List a -> Maybe a
335429find p [] = Nothing
336430find p (x::xs) =
@@ -339,6 +433,8 @@ find p (x::xs) =
339433 else
340434 find p xs
341435
436+||| Find the index of the first element of a list that satisfies a predicate, or
437+||| `Nothing` if none do.
342438findIndex : (a -> Bool) -> List a -> Maybe Nat
343439findIndex = findIndex' Z
344440 where
@@ -350,6 +446,7 @@ findIndex = findIndex' Z
350446 else
351447 findIndex' (S cnt) p xs
352448
449+||| Find the indices of all elements that satisfy some predicate.
353450findIndices : (a -> Bool) -> List a -> List Nat
354451findIndices = findIndices' Z
355452 where
@@ -403,6 +500,8 @@ nub = nubBy (==)
403500-- Splitting and breaking lists
404501--------------------------------------------------------------------------------
405502
503+||| Given a list and a predicate, returns a pair consisting of the longest
504+||| prefix of the list that satisfies a predicate and the rest of the list.
406505span : (a -> Bool) -> List a -> (List a, List a)
407506span p [] = ([], [])
408507span p (x::xs) =
@@ -501,6 +600,7 @@ sort xs = let (x, y) = split xs in
501600-- Conversions
502601--------------------------------------------------------------------------------
503602
603+||| Either return the head of a list, or `Nothing` if it is empty.
504604listToMaybe : List a -> Maybe a
505605listToMaybe [] = Nothing
506606listToMaybe (x::xs) = Just x
@@ -520,7 +620,7 @@ catMaybes (x::xs) =
520620-- Properties
521621--------------------------------------------------------------------------------
522622
523−-- append
623+||| The empty list is a right identity for append.
524624appendNilRightNeutral : (l : List a) ->
525625 l ++ [] = l
526626appendNilRightNeutral [] = refl
@@ -528,6 +628,7 @@ appendNilRightNeutral (x::xs) =
528628 let inductiveHypothesis = appendNilRightNeutral xs in
529629 ?appendNilRightNeutralStepCase
530630
631+||| Appending lists is associative.
531632appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
532633 l ++ (c ++ r) = (l ++ c) ++ r
533634appendAssociative [] c r = refl
@@ -535,7 +636,8 @@ appendAssociative (x::xs) c r =
535636 let inductiveHypothesis = appendAssociative xs c r in
536637 ?appendAssociativeStepCase
537638
538−-- length
639+||| The length of two lists that are appended is the sum of the lengths
640+||| of the input lists.
539641lengthAppend : (left : List a) -> (right : List a) ->
540642 length (left ++ right) = length left + length right
541643lengthAppend [] right = refl
@@ -543,7 +645,7 @@ lengthAppend (x::xs) right =
543645 let inductiveHypothesis = lengthAppend xs right in
544646 ?lengthAppendStepCase
545647
546−-- map
648+||| Mapping a function over a list doesn't change its length.
547649mapPreservesLength : (f : a -> b) -> (l : List a) ->
548650 length (map f l) = length l
549651mapPreservesLength f [] = refl
@@ -551,6 +653,8 @@ mapPreservesLength f (x::xs) =
551653 let inductiveHypothesis = mapPreservesLength f xs in
552654 ?mapPreservesLengthStepCase
553655
656+||| Mapping a function over two lists and appending them is equivalent
657+||| to appending them and then mapping the function.
554658mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->
555659 map f (l ++ r) = map f l ++ map f r
556660mapDistributesOverAppend f [] r = refl
@@ -558,6 +662,7 @@ mapDistributesOverAppend f (x::xs) r =
558662 let inductiveHypothesis = mapDistributesOverAppend f xs r in
559663 ?mapDistributesOverAppendStepCase
560664
665+||| Mapping two functions is the same as mapping their composition.
561666mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
562667 map f (map g l) = map (f . g) l
563668mapFusion f g [] = refl
@@ -565,7 +670,7 @@ mapFusion f g (x::xs) =
565670 let inductiveHypothesis = mapFusion f g xs in
566671 ?mapFusionStepCase
567672
568−-- hasAny
673+||| No list contains an element of the empty list by any predicate.
569674hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
570675 hasAnyBy p [] l = False
571676hasAnyByNilFalse p [] = refl
@@ -573,6 +678,7 @@ hasAnyByNilFalse p (x::xs) =
573678 let inductiveHypothesis = hasAnyByNilFalse p xs in
574679 ?hasAnyByNilFalseStepCase
575680
681+||| No list contains an element of the empty list.
576682hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
577683hasAnyNilFalse l = ?hasAnyNilFalseBody
578684