@@ -15,9 +15,12 @@ import Prelude.Nat
1515infix 5 \\
1616infixr 7 ::,++
1717
18−%elim data List a
19− = Nil
20− | (::) a (List a)
18+||| Linked lists
19+%elim data List a =
20+ ||| The empty list
21+ Nil |
22+ ||| Cons cell
23+ (::) a (List a)
2124
2225-- Name hints for interactive editing
2326%name List xs, ys, zs, ws
@@ -26,10 +29,12 @@ infixr 7 ::,++
2629-- Syntactic tests
2730--------------------------------------------------------------------------------
2831
32+||| Returns `True` iff the argument is empty
2933isNil : List a -> Bool
3034isNil [] = True
3135isNil (x::xs) = False
3236
37+||| Returns `True` iff the argument is not empty
3338isCons : List a -> Bool
3439isCons [] = False
3540isCons (x::xs) = True
@@ -38,6 +43,9 @@ isCons (x::xs) = True
3843-- Length
3944--------------------------------------------------------------------------------
4045
46+||| Compute the length of a list.
47+|||
48+||| Runs in linear time
4149length : List a -> Nat
4250length [] = 0
4351length (x::xs) = 1 + length xs
@@ -46,49 +54,74 @@ length (x::xs) = 1 + length xs
4654-- Indexing into lists
4755--------------------------------------------------------------------------------
4856
49−index : (n : Nat) -> (l : List a) -> (lt n (length l) = True) -> a
57+||| Find a particular element of a list.
58+|||
59+||| @ ok a proof that the index is within bounds
60+index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a
5061index Z (x::xs) p = x
5162index (S n) (x::xs) p = index n xs ?indexTailProof
5263index _ [] refl impossible
5364
65+||| Attempt to find a particular element of a list.
66+|||
67+||| If the provided index is out of bounds, return Nothing.
5468index' : (n : Nat) -> (l : List a) -> Maybe a
5569index' Z (x::xs) = Just x
5670index' (S n) (x::xs) = index' n xs
5771index' _ [] = Nothing
5872
59−head : (l : List a) -> (isCons l = True) -> a
73+||| Get the first element of a non-empty list
74+||| @ ok proof that the list is non-empty
75+head : (l : List a) -> (ok : isCons l = True) -> a
6076head [] refl impossible
6177head (x::xs) p = x
6278
79+||| Attempt to get the first element of a list. If the list is empty, return
80+||| `Nothing`.
6381head' : (l : List a) -> Maybe a
6482head' [] = Nothing
6583head' (x::xs) = Just x
6684
67−tail : (l : List a) -> (isCons l = True) -> List a
85+||| Get the tail of a non-empty list.
86+||| @ ok proof that the list is non-empty
87+tail : (l : List a) -> (ok : isCons l = True) -> List a
6888tail [] refl impossible
6989tail (x::xs) p = xs
7090
91+||| Attempt to get the tail of a list.
92+|||
93+||| If the list is empty, return `Nothing`.
7194tail' : (l : List a) -> Maybe (List a)
7295tail' [] = Nothing
7396tail' (x::xs) = Just xs
7497
75−last : (l : List a) -> (isCons l = True) -> a
98+||| Retrieve the last element of a non-empty list.
99+||| @ ok proof that the list is non-empty
100+last : (l : List a) -> (ok : isCons l = True) -> a
76101last [] refl impossible
77102last [x] p = x
78103last (x::y::ys) p = last (y::ys) refl
79104
105+||| Attempt to retrieve the last element of a non-empty list.
106+|||
107+||| If the list is empty, return `Nothing`.
80108last' : (l : List a) -> Maybe a
81109last' [] = Nothing
82−last' (x::xs) =
110+last' (x::xs) =
83111 case xs of
84112 [] => Just x
85113 y :: ys => last' xs
86114
87−init : (l : List a) -> (isCons l = True) -> List a
115+||| Return all but the last element of a non-empty list.
116+||| @ ok proof that the list is non-empty
117+init : (l : List a) -> (ok : isCons l = True) -> List a
88118init [] refl impossible
89119init [x] p = []
90120init (x::y::ys) p = x :: init (y::ys) refl
91121
122+||| Attempt to Return all but the last element of a list.
123+|||
124+||| If the list is empty, return `Nothing`.
92125init' : (l : List a) -> Maybe (List a)
93126init' [] = Nothing
94127init' (x::xs) =
@@ -104,21 +137,39 @@ init' (x::xs) =
104137-- Sublists
105138--------------------------------------------------------------------------------
106139
107−take : Nat -> List a -> List a
140+||| Take the first `n` elements of `xs`
141+|||
142+||| If there are not enough elements, return the whole list.
143+||| @ n how many elements to take
144+||| @ xs the list to take them from
145+take : (n : Nat) -> (xs : List a) -> List a
108146take Z xs = []
109147take (S n) [] = []
110148take (S n) (x::xs) = x :: take n xs
111149
112−drop : Nat -> List a -> List a
150+||| Drop the first `n` elements of `xs`
151+|||
152+||| If there are not enough elements, return the empty list.
153+||| @ n how many elements to drop
154+||| @ xs the list to drop them from
155+drop : (n : Nat) -> (xs : List a) -> List a
113156drop Z xs = xs
114157drop (S n) [] = []
115158drop (S n) (x::xs) = drop n xs
116159
117−takeWhile : (a -> Bool) -> List a -> List a
160+||| Take the longest prefix of a list such that all elements satsify some
161+||| Boolean predicate.
162+|||
163+||| @ p the predicate
164+takeWhile : (p : a -> Bool) -> List a -> List a
118165takeWhile p [] = []
119166takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
120167
121−dropWhile : (a -> Bool) -> List a -> List a
168+||| Remove the longest prefix of a list such that all removed elements satsify some
169+||| Boolean predicate.
170+|||
171+||| @ p the predicate
172+dropWhile : (p : a -> Bool) -> List a -> List a
122173dropWhile p [] = []
123174dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
124175
@@ -126,7 +177,12 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
126177-- Misc.
127178--------------------------------------------------------------------------------
128179
129−list : a -> (a -> List a -> a) -> List a -> a
180+||| Simply-typed recursion operator for lists.
181+|||
182+||| @ nil what to return at the end of the list
183+||| @ cons what to do at each step of recursion
184+||| @ xs the list to recurse over
185+list : (nil : a) -> (cons : a -> List a -> a) -> (xs : List a) -> a
130186list nil cons [] = nil
131187list nil cons (x::xs) = cons x xs
132188
@@ -134,16 +190,23 @@ list nil cons (x::xs) = cons x xs
134190-- Building (bigger) lists
135191--------------------------------------------------------------------------------
136192
193+||| Append two lists
137194(++) : List a -> List a -> List a
138−(++) [] right = right
195+(++) [] right = right
139196(++) (x::xs) right = x :: (xs ++ right)
140197
198+||| Create an infinite sequence of some item.
199+|||
200+||| Consider using a `Stream` instead.
141201partial
142202repeat : a -> List a
143203repeat x = x :: lazy (repeat x)
144204
145−replicate : Nat -> a -> List a
146−replicate Z x = []
205+||| Construct a list with `n` copies of `x`
206+||| @ n how many copies
207+||| @ x the element to replicate
208+replicate : (n : Nat) -> (x : a) -> List a
209+replicate Z x = []
147210replicate (S n) x = x :: replicate n x
148211
149212--------------------------------------------------------------------------------
@@ -188,15 +251,27 @@ instance Functor List where
188251-- Zips and unzips
189252--------------------------------------------------------------------------------
190253
254+||| Combine two lists of the same length elementwise using some function.
255+||| @ f the function to combine elements with
256+||| @ l the first list
257+||| @ r the second list
258+||| @ ok a proof that the lengths of the inputs are equal
191259zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
192− (length l = length r) -> List c
260+ (ok : length l = length r) -> List c
193261zipWith f [] (y::ys) refl impossible
194262zipWith f (x::xs) [] refl impossible
195263zipWith f [] [] p = []
196264zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
197265
266+||| Combine three lists of the same length elementwise using some function.
267+||| @ f the function to combine elements with
268+||| @ x the first list
269+||| @ y the second list
270+||| @ z the third list
271+||| @ ok a proof that the lengths of the first two inputs are equal
272+||| @ ok' a proof that the lengths of the second and third inputs are equal
198273zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
199− (z : List c) -> (length x = length y) -> (length y = length z) -> List d
274+ (z : List c) -> (ok : length x = length y) -> (ok' : length y = length z) -> List d
200275zipWith3 f _ [] (z::zs) p refl impossible
201276zipWith3 f _ (y::ys) [] p refl impossible
202277zipWith3 f [] (y::ys) _ refl q impossible
@@ -205,18 +280,22 @@ zipWith3 f [] [] [] p q = []
205280zipWith3 f (x::xs) (y::ys) (z::zs) p q =
206281 f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
207282
283+||| Combine two lists elementwise into pairs
208284zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
209285zip = zipWith (\x => \y => (x, y))
210286
287+||| Combine three lists elementwise into tuples
211288zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
212289 (length y = length z) -> List (a, b, c)
213290zip3 = zipWith3 (\x => \y => \z => (x, y, z))
214291
292+||| Split a list of pairs into two lists
215293unzip : List (a, b) -> (List a, List b)
216294unzip [] = ([], [])
217295unzip ((l, r)::xs) with (unzip xs)
218296 | (lefts, rights) = (l::lefts, r::rights)
219297
298+||| Split a list of triples into three lists
220299unzip3 : List (a, b, c) -> (List a, List b, List c)
221300unzip3 [] = ([], [], [])
222301unzip3 ((l, c, r)::xs) with (unzip3 xs)
@@ -226,6 +305,8 @@ unzip3 ((l, c, r)::xs) with (unzip3 xs)
226305-- Maps
227306--------------------------------------------------------------------------------
228307
308+||| Apply a partial function to the elements of a list, keeping the ones at which
309+||| it is defined.
229310mapMaybe : (a -> Maybe b) -> List a -> List b
230311mapMaybe f [] = []
231312mapMaybe f (x::xs) =
@@ -237,6 +318,7 @@ mapMaybe f (x::xs) =
237318-- Folds
238319--------------------------------------------------------------------------------
239320
321+||| A tail recursive right fold on Lists.
240322total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> List t -> acc
241323foldrImpl f e go [] = go e
242324foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
@@ -248,6 +330,7 @@ instance Foldable List where
248330-- Special folds
249331--------------------------------------------------------------------------------
250332
333+||| Convert any Foldable structure to a list.
251334toList : Foldable t => t a -> List a
252335toList = foldr (::) []
253336
@@ -255,6 +338,7 @@ toList = foldr (::) []
255338-- Transformations
256339--------------------------------------------------------------------------------
257340
341+||| Return the elements of a list in reverse order.
258342reverse : List a -> List a
259343reverse = reverse' []
260344 where
@@ -262,6 +346,7 @@ reverse = reverse' []
262346 reverse' acc [] = acc
263347 reverse' acc (x::xs) = reverse' (x::acc) xs
264348
349+||| Insert some separator between the elements of a list.
265350intersperse : a -> List a -> List a
266351intersperse sep [] = []
267352intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -275,13 +360,13 @@ intercalate sep l = concat $ intersperse sep l
275360
276361||| Transposes rows and columns of a list of lists.
277362|||
278−||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
363+||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
279364|||
280365||| This also works for non square scenarios, thus
281366||| involution does not always hold:
282367|||
283−||| > transpose [[], [1, 2]] = [[1], [2]]
284−||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]
368+||| > transpose [[], [1, 2]] = [[1], [2]]
369+||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]
285370|||
286371||| TODO: Solution which satisfies the totality checker?
287372%assert_total
@@ -294,6 +379,7 @@ transpose ((x::xs) :: xss) = (x :: (mapMaybe head' xss)) :: (transpose (xs :: (m
294379-- Membership tests
295380--------------------------------------------------------------------------------
296381
382+||| Check if something is a member of a list using a custom comparison.
297383elemBy : (a -> a -> Bool) -> a -> List a -> Bool
298384elemBy p e [] = False
299385elemBy p e (x::xs) =
@@ -302,9 +388,11 @@ elemBy p e (x::xs) =
302388 else
303389 elemBy p e xs
304390
391+||| Check if something is a member of a list using the default Boolean equality.
305392elem : Eq a => a -> List a -> Bool
306393elem = elemBy (==)
307394
395+||| Find associated information in a list using a custom comparison.
308396lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
309397lookupBy p e [] = Nothing
310398lookupBy p e (x::xs) =
@@ -314,9 +402,12 @@ lookupBy p e (x::xs) =
314402 else
315403 lookupBy p e xs
316404
405+||| Find associated information in a list using Boolean equality.
317406lookup : Eq a => a -> List (a, b) -> Maybe b
318407lookup = lookupBy (==)
319408
409+||| Check if any elements of the first list are found in the second, using
410+||| a custom comparison.
320411hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
321412hasAnyBy p elems [] = False
322413hasAnyBy p elems (x::xs) =
@@ -325,6 +416,8 @@ hasAnyBy p elems (x::xs) =
325416 else
326417 hasAnyBy p elems xs
327418
419+||| Check if any elements of the first list are found in the second, using
420+||| Boolean equality.
328421hasAny : Eq a => List a -> List a -> Bool
329422hasAny = hasAnyBy (==)
330423
@@ -332,6 +425,7 @@ hasAny = hasAnyBy (==)
332425-- Searching with a predicate
333426--------------------------------------------------------------------------------
334427
428+||| Find the first element of a list that satisfies a predicate, or `Nothing` if none do.
335429find : (a -> Bool) -> List a -> Maybe a
336430find p [] = Nothing
337431find p (x::xs) =
@@ -340,6 +434,8 @@ find p (x::xs) =
340434 else
341435 find p xs
342436
437+||| Find the index of the first element of a list that satisfies a predicate, or
438+||| `Nothing` if none do.
343439findIndex : (a -> Bool) -> List a -> Maybe Nat
344440findIndex = findIndex' Z
345441 where
@@ -351,6 +447,7 @@ findIndex = findIndex' Z
351447 else
352448 findIndex' (S cnt) p xs
353449
450+||| Find the indices of all elements that satisfy some predicate.
354451findIndices : (a -> Bool) -> List a -> List Nat
355452findIndices = findIndices' Z
356453 where
@@ -420,6 +517,8 @@ union = unionBy (==)
420517-- Splitting and breaking lists
421518--------------------------------------------------------------------------------
422519
520+||| Given a list and a predicate, returns a pair consisting of the longest
521+||| prefix of the list that satisfies a predicate and the rest of the list.
423522span : (a -> Bool) -> List a -> (List a, List a)
424523span p [] = ([], [])
425524span p (x::xs) =
@@ -528,6 +627,7 @@ sort xs = let (x, y) = split xs in
528627-- Conversions
529628--------------------------------------------------------------------------------
530629
630+||| Either return the head of a list, or `Nothing` if it is empty.
531631listToMaybe : List a -> Maybe a
532632listToMaybe [] = Nothing
533633listToMaybe (x::xs) = Just x
@@ -547,7 +647,7 @@ catMaybes (x::xs) =
547647-- Properties
548648--------------------------------------------------------------------------------
549649
550−-- append
650+||| The empty list is a right identity for append.
551651appendNilRightNeutral : (l : List a) ->
552652 l ++ [] = l
553653appendNilRightNeutral [] = refl
@@ -555,6 +655,7 @@ appendNilRightNeutral (x::xs) =
555655 let inductiveHypothesis = appendNilRightNeutral xs in
556656 ?appendNilRightNeutralStepCase
557657
658+||| Appending lists is associative.
558659appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
559660 l ++ (c ++ r) = (l ++ c) ++ r
560661appendAssociative [] c r = refl
@@ -562,7 +663,8 @@ appendAssociative (x::xs) c r =
562663 let inductiveHypothesis = appendAssociative xs c r in
563664 ?appendAssociativeStepCase
564665
565−-- length
666+||| The length of two lists that are appended is the sum of the lengths
667+||| of the input lists.
566668lengthAppend : (left : List a) -> (right : List a) ->
567669 length (left ++ right) = length left + length right
568670lengthAppend [] right = refl
@@ -570,7 +672,7 @@ lengthAppend (x::xs) right =
570672 let inductiveHypothesis = lengthAppend xs right in
571673 ?lengthAppendStepCase
572674
573−-- map
675+||| Mapping a function over a list doesn't change its length.
574676mapPreservesLength : (f : a -> b) -> (l : List a) ->
575677 length (map f l) = length l
576678mapPreservesLength f [] = refl
@@ -578,6 +680,8 @@ mapPreservesLength f (x::xs) =
578680 let inductiveHypothesis = mapPreservesLength f xs in
579681 ?mapPreservesLengthStepCase
580682
683+||| Mapping a function over two lists and appending them is equivalent
684+||| to appending them and then mapping the function.
581685mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->
582686 map f (l ++ r) = map f l ++ map f r
583687mapDistributesOverAppend f [] r = refl
@@ -585,6 +689,7 @@ mapDistributesOverAppend f (x::xs) r =
585689 let inductiveHypothesis = mapDistributesOverAppend f xs r in
586690 ?mapDistributesOverAppendStepCase
587691
692+||| Mapping two functions is the same as mapping their composition.
588693mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
589694 map f (map g l) = map (f . g) l
590695mapFusion f g [] = refl
@@ -592,7 +697,7 @@ mapFusion f g (x::xs) =
592697 let inductiveHypothesis = mapFusion f g xs in
593698 ?mapFusionStepCase
594699
595−-- hasAny
700+||| No list contains an element of the empty list by any predicate.
596701hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
597702 hasAnyBy p [] l = False
598703hasAnyByNilFalse p [] = refl
@@ -600,6 +705,7 @@ hasAnyByNilFalse p (x::xs) =
600705 let inductiveHypothesis = hasAnyByNilFalse p xs in
601706 ?hasAnyByNilFalseStepCase
602707
708+||| No list contains an element of the empty list.
603709hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
604710hasAnyNilFalse l = ?hasAnyNilFalseBody
605711