@@ -1,121 +1,383 @@
11module prelude.list
22
3−import prelude.maybe
43import builtins
54
5+import prelude.maybe
6+import prelude.nat
7+
68%access public
79
810infixr 7 ::
911
10−data List a = Nil | (::) a (List a)
12+data List a
13+ = Nil
14+ | (::) a (List a)
1115
12−rev : List a -> List a
13−rev xs = revAcc [] xs where
14− revAcc : List a -> List a -> List a
15− revAcc acc [] = acc
16− revAcc acc (x :: xs) = revAcc (x :: acc) xs
16+--------------------------------------------------------------------------------
17+-- Syntactic tests
18+--------------------------------------------------------------------------------
1719
18−app : List a -> List a -> List a
19−app [] xs = xs
20−app (x :: xs) ys = x :: app xs ys
20+isNil : List a -> Bool
21+isNil [] = True
22+isNil (x::xs) = False
2123
22−head : List a -> Maybe a
23−head [] = Nothing
24−head (x :: xs) = Just x
24+isCons : List a -> Bool
25+isCons [] = False
26+isCons (x::xs) = True
2527
26−tail : List a -> List a
27−tail [] = []
28−tail (x :: xs) = xs
28+--------------------------------------------------------------------------------
29+-- Indexing into lists
30+--------------------------------------------------------------------------------
2931
30−length : List a -> Int
31−length [] = 0
32−length (x :: xs) = 1 + length xs
32+head : (l : List a) -> (isCons l = True) -> a
33+head (x::xs) p = x
34+
35+head' : (l : List a) -> Maybe a
36+head' [] = Nothing
37+head' (x::xs) = Just x
38+
39+tail : (l : List a) -> (isCons l = True) -> List a
40+tail (x::xs) p = xs
41+
42+tail' : (l : List a) -> Maybe (List a)
43+tail' [] = Nothing
44+tail' (x::xs) = Just xs
45+
46+last : (l : List a) -> (isCons l = True) -> a
47+last (x::xs) p =
48+ case xs of
49+ [] => x
50+ y::ys => last (y::ys) ?lastProof
51+
52+last' : (l : List a) -> Maybe a
53+last' [] = Nothing
54+last' (x::xs) =
55+ case xs of
56+ [] => Just x
57+ y::ys => last' xs
58+
59+init : (l : List a) -> (isCons l = True) -> List a
60+init (x::xs) p =
61+ case xs of
62+ [] => []
63+ y::ys => x :: init (y::ys) ?initProof
64+
65+init' : (l : List a) -> Maybe (List a)
66+init' [] = Nothing
67+init' (x::xs) =
68+ case xs of
69+ [] => Just []
70+ y::ys =>
71+ -- XXX: Problem with typechecking a "do" block here
72+ case init' $ y::ys of
73+ Nothing => Nothing
74+ Just j => Just $ x :: j
3375
34−take : Int -> List a -> List a
35−take 0 xs = []
36−take n [] = []
37−take n (x :: xs) = x :: take (n-1) xs
76+--------------------------------------------------------------------------------
77+-- Sublists
78+--------------------------------------------------------------------------------
3879
39−drop : Int -> List a -> List a
40−drop 0 xs = xs
41−drop n [] = []
42−drop n (x :: xs) = drop (n-1) xs
80+take : Nat -> List a -> List a
81+take Z xs = []
82+take (S n) [] = []
83+take (S n) (x::xs) = x :: take n xs
4384
44−map : (a -> b) -> List a -> List b
45−map f [] = []
46−map f (x :: xs) = f x :: map f xs
85+drop : Nat -> List a -> List a
86+drop Z xs = xs
87+drop (S n) [] = []
88+drop (S n) (x::xs) = drop n xs
4789
48−concatMap : (a -> List b) -> List a -> List b
49−concatMap f [] = []
50−concatMap f (x :: xs) = app (f x) (concatMap f xs)
90+--------------------------------------------------------------------------------
91+-- Misc.
92+--------------------------------------------------------------------------------
93+
94+list : a -> (a -> List a -> a) -> List a -> a
95+list nil cons [] = nil
96+list nil cons (x::xs) = cons x xs
97+
98+length : List a -> Nat
99+length [] = 0
100+length (x::xs) = 1 + length xs
101+
102+--------------------------------------------------------------------------------
103+-- Building bigger lists
104+--------------------------------------------------------------------------------
105+
106+(++) : List a -> List a -> List a
107+(++) [] right = right
108+(++) (x::xs) right = x :: (xs ++ right)
109+
110+--------------------------------------------------------------------------------
111+-- Maps
112+--------------------------------------------------------------------------------
113+
114+map : (a -> b) -> List a -> List b
115+map f [] = []
116+map f (x::xs) = f x :: map f xs
51117
52118mapMaybe : (a -> Maybe b) -> List a -> List b
53−mapMaybe f [] = []
54−mapMaybe f (x :: xs) = case f x of
55− Nothing => mapMaybe f xs
56− Just v => v :: mapMaybe f xs
119+mapMaybe f [] = []
120+mapMaybe f (x::xs) =
121+ case f x of
122+ Nothing => mapMaybe f xs
123+ Just j => j :: mapMaybe f xs
124+
125+--------------------------------------------------------------------------------
126+-- Folds
127+--------------------------------------------------------------------------------
57128
58129foldl : (a -> b -> a) -> a -> List b -> a
59−foldl f a [] = a
60−foldl f a (x :: xs) = foldl f (f a x) xs
130+foldl f e [] = e
131+foldl f e (x::xs) = foldl f (f e x) xs
61132
62133foldr : (a -> b -> b) -> b -> List a -> b
63−foldr f b [] = b
64−foldr f b (x :: xs) = f x (foldr f b xs)
134+foldr f e [] = e
135+foldr f e (x::xs) = f x (foldr f e xs)
136+
137+--------------------------------------------------------------------------------
138+-- Special folds
139+--------------------------------------------------------------------------------
140+
141+concat : List (List a) -> List a
142+concat = foldr (++) []
143+
144+concatMap : (a -> List b) -> List a -> List b
145+concatMap f [] = []
146+concatMap f (x::xs) = f x ++ concatMap f xs
65147
66−filter : (y -> Bool) -> List y -> List y
67−filter pred [] = []
68−filter pred (x :: xs) = if (pred x) then (x :: filter pred xs)
69− else (filter pred xs)
148+and : List Bool -> Bool
149+and = foldr (&&) True
150+
151+or : List Bool -> Bool
152+or = foldr (||) False
153+
154+any : (a -> Bool) -> List a -> Bool
155+any p = or . map p
156+
157+all : (a -> Bool) -> List a -> Bool
158+all p = and . map p
159+
160+--------------------------------------------------------------------------------
161+-- Transformations
162+--------------------------------------------------------------------------------
163+
164+reverse : List a -> List a
165+reverse = reverse' []
166+ where
167+ reverse' : List a -> List a -> List a
168+ reverse' acc [] = acc
169+ reverse' acc (x::xs) = reverse' (x::acc) xs
170+
171+intersperse : a -> List a -> List a
172+intersperse sep [] = []
173+intersperse sep (x::xs) = x :: intersperse' sep xs
174+ where
175+ intersperse' : a -> List a -> List a
176+ intersperse' sep [] = []
177+ intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
178+
179+intercalate : List a -> List (List a) -> List a
180+intercalate sep l = concat $ intersperse sep l
181+
182+--------------------------------------------------------------------------------
183+-- Membership tests
184+--------------------------------------------------------------------------------
185+
186+elemBy : (a -> a -> Bool) -> a -> List a -> Bool
187+elemBy p e [] = False
188+elemBy p e (x::xs) =
189+ if p e x then
190+ True
191+ else
192+ elemBy p e xs
70193
71194elem : Eq a => a -> List a -> Bool
72−elem x [] = False
73−elem x (y :: ys) = if (x == y) then True else (elem x ys)
195+elem = elemBy (==)
196+
197+lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
198+lookupBy p e [] = Nothing
199+lookupBy p e (x::xs) =
200+ let (l, r) = x in
201+ if p e l then
202+ Just r
203+ else
204+ lookupBy p e xs
205+
206+lookup : Eq a => a -> List (a, b) -> Maybe b
207+lookup = lookupBy (==)
208+
209+hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
210+hasAnyBy p elems [] = False
211+hasAnyBy p elems (x::xs) =
212+ if elemBy p x elems then
213+ True
214+ else
215+ hasAnyBy p elems xs
216+
217+hasAny : Eq a => List a -> List a -> Bool
218+hasAny = hasAnyBy (==)
74219
75−lookup : Eq k => k -> List (k, v) -> Maybe v
76−lookup k [] = Nothing
77−lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs)
220+--------------------------------------------------------------------------------
221+-- Searching with a predicate
222+--------------------------------------------------------------------------------
78223
79−sort : Ord a => List a -> List a
80−sort [] = []
81−sort [x] = [x]
82−sort xs = let (x, y) = split xs in
83− merge (sort x) (sort y) where
84− splitrec : List a -> List a -> (List a -> List a) -> (List a, List a)
85− splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y))
86− splitrec _ ys zs = (zs [], ys)
224+find : (a -> Bool) -> List a -> Maybe a
225+find p [] = Nothing
226+find p (x::xs) =
227+ if p x then
228+ Just x
229+ else
230+ find p xs
231+
232+findIndex : (a -> Bool) -> List a -> Maybe Nat
233+findIndex = findIndex' 0
234+ where
235+ findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat
236+ findIndex' cnt p [] = Nothing
237+ findIndex' cnt p (x::xs) =
238+ if p x then
239+ Just cnt
240+ else
241+ findIndex' (S cnt) p xs
242+
243+findIndices : (a -> Bool) -> List a -> List Nat
244+findIndices = findIndices' 0
245+ where
246+ findIndices' : Nat -> (a -> Bool) -> List a -> List Nat
247+ findIndices' cnt p [] = []
248+ findIndices' cnt p (x::xs) =
249+ if p x then
250+ cnt :: findIndices' (S cnt) p xs
251+ else
252+ findIndices' (S cnt) p xs
253+
254+elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat
255+elemIndexBy p e = findIndex $ p e
256+
257+elemIndex : Eq a => a -> List a -> Maybe Nat
258+elemIndex = elemIndexBy (==)
259+
260+elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat
261+elemIndicesBy p e = findIndices $ p e
262+
263+elemIndices : Eq a => a -> List a -> List Nat
264+elemIndices = elemIndicesBy (==)
87265
88− split : List a -> (List a, List a)
89− split xs = splitrec xs xs id
266+--------------------------------------------------------------------------------
267+-- Filters
268+--------------------------------------------------------------------------------
90269
91− merge : Ord a => List a -> List a -> List a
92− merge xs [] = xs
93− merge [] ys = ys
94− merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))
95− else (y :: merge (x :: xs) ys)
270+filter : (a -> Bool) -> List a -> List a
271+filter p [] = []
272+filter p (x::xs) =
273+ if p x then
274+ x :: filter p xs
275+ else
276+ filter p xs
277+
278+nubBy : (a -> a -> Bool) -> List a -> List a
279+nubBy = nubBy' []
280+ where
281+ nubBy' : List a -> (a -> a -> Bool) -> List a -> List a
282+ nubBy' acc p [] = []
283+ nubBy' acc p (x::xs) =
284+ if elemBy p x acc then
285+ nubBy' acc p xs
286+ else
287+ x :: nubBy' (x::acc) p xs
288+
289+nub : Eq a => List a -> List a
290+nub = nubBy (==)
291+
292+--------------------------------------------------------------------------------
293+-- Splitting and breaking lists
294+--------------------------------------------------------------------------------
96295
97296span : (a -> Bool) -> List a -> (List a, List a)
98−span p [] = ([], [])
99−span p (x :: xs) with (p x)
100− | True with (span p xs)
101− | (ys, zs) = (x :: ys, zs)
102− | False = ([], x :: xs)
297+span p [] = ([], [])
298+span p (x::xs) =
299+ if p x then
300+ let (ys, zs) = span p xs in
301+ (x::ys, zs)
302+ else
303+ ([], x::xs)
103304
104305break : (a -> Bool) -> List a -> (List a, List a)
105306break p = span (not . p)
106−
307+
107308split : (a -> Bool) -> List a -> List (List a)
108309split p [] = []
109−split p xs = case break p xs of
110− (chunk, []) => [chunk]
111− (chunk, (c :: rest)) => chunk :: split p rest
310+split p xs =
311+ case break p xs of
312+ (chunk, []) => [chunk]
313+ (chunk, (c :: rest)) => chunk :: split p rest
314+
315+partition : (a -> Bool) -> List a -> (List a, List a)
316+partition p [] = ([], [])
317+partition p (x::xs) =
318+ let (lefts, rights) = partition p xs in
319+ if p x then
320+ (x::lefts, rights)
321+ else
322+ (lefts, x::rights)
112323
113−any : (a -> Bool) -> List a -> Bool
114−any predicate [] = False
115−any predicate (a::rest) =
116− if predicate a
117− then True
118− else any predicate rest
324+--------------------------------------------------------------------------------
325+-- Predicates
326+--------------------------------------------------------------------------------
327+
328+isPrefixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
329+isPrefixOfBy p [] right = True
330+isPrefixOfBy p left [] = False
331+isPrefixOfBy p (x::xs) (y::ys) =
332+ if p x y then
333+ isPrefixOfBy p xs ys
334+ else
335+ False
336+
337+isPrefixOf : Eq a => List a -> List a -> Bool
338+isPrefixOf = isPrefixOfBy (==)
339+
340+isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
341+isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
342+
343+isSuffixOf : Eq a => List a -> List a -> Bool
344+isSuffixOf = isSuffixOfBy (==)
345+
346+--------------------------------------------------------------------------------
347+-- Sorting
348+--------------------------------------------------------------------------------
349+
350+sorted : Ord a => List a -> Bool
351+sorted [] = True
352+sorted (x::xs) =
353+ case xs of
354+ Nil => True
355+ (y::ys) => x <= y && sorted (y::ys)
356+
357+mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
358+mergeBy order [] right = right
359+mergeBy order left [] = left
360+mergeBy order (x::xs) (y::ys) =
361+ case order x y of
362+ LT => x :: mergeBy order xs (y::ys)
363+ _ => y :: mergeBy order (x::xs) ys
364+
365+merge : Ord a => List a -> List a -> List a
366+merge = mergeBy compare
367+
368+sort : Ord a => List a -> List a
369+sort [] = []
370+sort [x] = [x]
371+sort xs =
372+ let (x, y) = split xs in
373+ merge (sort x) (sort y)
374+ where
375+ splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)
376+ splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))
377+ splitRec _ ys zs = (zs [], ys)
378+
379+ split : List a -> (List a, List a)
380+ split xs = splitRec xs xs id
119381
120382--------------------------------------------------------------------------------
121383-- Conversions
@@ -161,3 +423,122 @@ instance Ord a => Ord (List a) where
161423 if a /= b
162424 then compare a b
163425 else compare restA restB
426+
427+--------------------------------------------------------------------------------
428+-- Properties
429+--------------------------------------------------------------------------------
430+
431+mapPreservesLength : (f : a -> b) -> (l : List a) ->
432+ length (map f l) = length l
433+mapPreservesLength f [] = refl
434+mapPreservesLength f (x::xs) =
435+ let inductiveHypothesis = mapPreservesLength f xs in
436+ ?mapPreservesLengthStepCase
437+
438+mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->
439+ map f (l ++ r) = map f l ++ map f r
440+mapDistributesOverAppend f [] r = refl
441+mapDistributesOverAppend f (x::xs) r =
442+ let inductiveHypothesis = mapDistributesOverAppend f xs r in
443+ ?mapDistributesOverAppendStepCase
444+
445+mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
446+ map f (map g l) = map (f . g) l
447+mapFusion f g [] = refl
448+mapFusion f g (x::xs) =
449+ let inductiveHypothesis = mapFusion f g xs in
450+ ?mapFusionStepCase
451+
452+appendNilRightNeutral : (l : List a) ->
453+ l ++ [] = l
454+appendNilRightNeutral [] = refl
455+appendNilRightNeutral (x::xs) =
456+ let inductiveHypothesis = appendNilRightNeutral xs in
457+ ?appendNilRightNeutralStepCase
458+
459+appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
460+ (l ++ c) ++ r = l ++ (c ++ r)
461+appendAssociative [] c r = refl
462+appendAssociative (x::xs) c r =
463+ let inductiveHypothesis = appendAssociative xs c r in
464+ ?appendAssociativeStepCase
465+
466+hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
467+ hasAnyBy p [] l = False
468+hasAnyByNilFalse p [] = refl
469+hasAnyByNilFalse p (x::xs) =
470+ let inductiveHypothesis = hasAnyByNilFalse p xs in
471+ ?hasAnyByNilFalseStepCase
472+
473+lengthAppend : (left : List a) -> (right : List a) ->
474+ length (left ++ right) = length left + length right
475+lengthAppend [] right = refl
476+lengthAppend (x::xs) right =
477+ let inductiveHypothesis = lengthAppend xs right in
478+ ?lengthAppendStepCase
479+
480+hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
481+hasAnyNilFalse l = ?hasAnyNilFalseBody
482+
483+--------------------------------------------------------------------------------
484+-- Proofs
485+--------------------------------------------------------------------------------
486+
487+lengthAppendStepCase = proof {
488+ intros;
489+ rewrite inductiveHypothesis;
490+ trivial;
491+}
492+
493+hasAnyNilFalseBody = proof {
494+ intros;
495+ rewrite (hasAnyByNilFalse (==) l);
496+ trivial;
497+}
498+
499+hasAnyByNilFalseStepCase = proof {
500+ intros;
501+ rewrite inductiveHypothesis;
502+ trivial;
503+}
504+
505+initProof = proof {
506+ intros;
507+ trivial;
508+}
509+
510+lastProof = proof {
511+ intros;
512+ trivial;
513+}
514+
515+appendNilRightNeutralStepCase = proof {
516+ intros;
517+ rewrite inductiveHypothesis;
518+ trivial;
519+}
520+
521+appendAssociativeStepCase = proof {
522+ intros;
523+ rewrite inductiveHypothesis;
524+ trivial;
525+}
526+
527+mapFusionStepCase = proof {
528+ intros;
529+ rewrite inductiveHypothesis;
530+ trivial;
531+}
532+
533+mapDistributesOverAppendStepCase = proof {
534+ intros;
535+ rewrite inductiveHypothesis;
536+ trivial;
537+}
538+
539+mapPreservesLengthStepCase = proof {
540+ intros;
541+ rewrite inductiveHypothesis;
542+ trivial;
543+}
544+