@@ -5,110 +5,384 @@ import builtins
55
66%access public
77
8+import builtins
9+
10+import prelude.maybe
11+import prelude.nat
12+
13+%access public
14+
815infixr 7 ::
916
10−data List a = Nil | (::) a (List a)
17+data List a
18+ = Nil
19+ | (::) a (List a)
20+
21+--------------------------------------------------------------------------------
22+-- Syntactic tests
23+--------------------------------------------------------------------------------
24+
25+isNil : List a -> Bool
26+isNil [] = True
27+isNil (x::xs) = False
28+
29+isCons : List a -> Bool
30+isCons [] = False
31+isCons (x::xs) = True
32+
33+--------------------------------------------------------------------------------
34+-- Indexing into lists
35+--------------------------------------------------------------------------------
1136
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
37+head : (l : List a) -> (isCons l = True) -> a
38+head (x::xs) p = x
1739
18−app : List a -> List a -> List a
19−app [] xs = xs
20−app (x :: xs) ys = x :: app xs ys
40+head' : (l : List a) -> Maybe a
41+head' [] = Nothing
42+head' (x::xs) = Just x
2143
22−head : List a -> Maybe a
23−head [] = Nothing
24−head (x :: xs) = Just x
44+tail : (l : List a) -> (isCons l = True) -> List a
45+tail (x::xs) p = xs
2546
26−tail : List a -> List a
27−tail [] = []
28−tail (x :: xs) = xs
47+tail' : (l : List a) -> Maybe (List a)
48+tail' [] = Nothing
49+tail' (x::xs) = Just xs
2950
30−length : List a -> Int
31−length [] = 0
32−length (x :: xs) = 1 + length xs
51+last : (l : List a) -> (isCons l = True) -> a
52+last (x::xs) p =
53+ case xs of
54+ [] => x
55+ y::ys => last (y::ys) ?lastProof
3356
34−take : Int -> List a -> List a
35−take 0 xs = []
36−take n [] = []
37−take n (x :: xs) = x :: take (n-1) xs
57+last' : (l : List a) -> Maybe a
58+last' [] = Nothing
59+last' (x::xs) =
60+ case xs of
61+ [] => Just x
62+ y::ys => last' xs
3863
39−drop : Int -> List a -> List a
40−drop 0 xs = xs
41−drop n [] = []
42−drop n (x :: xs) = drop (n-1) xs
64+init : (l : List a) -> (isCons l = True) -> List a
65+init (x::xs) p =
66+ case xs of
67+ [] => []
68+ y::ys => x :: init (y::ys) ?initProof
4369
44−map : (a -> b) -> List a -> List b
45−map f [] = []
46−map f (x :: xs) = f x :: map f xs
70+init' : (l : List a) -> Maybe (List a)
71+init' [] = Nothing
72+init' (x::xs) =
73+ case xs of
74+ [] => Just []
75+ y::ys =>
76+ -- XXX: Problem with typechecking a "do" block here
77+ case init' $ y::ys of
78+ Nothing => Nothing
79+ Just j => Just $ x :: j
4780
48−concatMap : (a -> List b) -> List a -> List b
49−concatMap f [] = []
50−concatMap f (x :: xs) = app (f x) (concatMap f xs)
81+--------------------------------------------------------------------------------
82+-- Sublists
83+--------------------------------------------------------------------------------
84+
85+take : Nat -> List a -> List a
86+take Z xs = []
87+take (S n) [] = []
88+take (S n) (x::xs) = x :: take n xs
89+
90+drop : Nat -> List a -> List a
91+drop Z xs = xs
92+drop (S n) [] = []
93+drop (S n) (x::xs) = drop n xs
94+
95+--------------------------------------------------------------------------------
96+-- Misc.
97+--------------------------------------------------------------------------------
98+
99+list : a -> (a -> List a -> a) -> List a -> a
100+list nil cons [] = nil
101+list nil cons (x::xs) = cons x xs
102+
103+length : List a -> Nat
104+length [] = 0
105+length (x::xs) = 1 + length xs
106+
107+--------------------------------------------------------------------------------
108+-- Building bigger lists
109+--------------------------------------------------------------------------------
110+
111+(++) : List a -> List a -> List a
112+(++) [] right = right
113+(++) (x::xs) right = x :: (xs ++ right)
114+
115+--------------------------------------------------------------------------------
116+-- Maps
117+--------------------------------------------------------------------------------
118+
119+map : (a -> b) -> List a -> List b
120+map f [] = []
121+map f (x::xs) = f x :: map f xs
51122
52123mapMaybe : (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
124+mapMaybe f [] = []
125+mapMaybe f (x::xs) =
126+ case f x of
127+ Nothing => mapMaybe f xs
128+ Just j => j :: mapMaybe f xs
129+
130+--------------------------------------------------------------------------------
131+-- Folds
132+--------------------------------------------------------------------------------
57133
58134foldl : (a -> b -> a) -> a -> List b -> a
59−foldl f a [] = a
60−foldl f a (x :: xs) = foldl f (f a x) xs
135+foldl f e [] = e
136+foldl f e (x::xs) = foldl f (f e x) xs
61137
62138foldr : (a -> b -> b) -> b -> List a -> b
63−foldr f b [] = b
64−foldr f b (x :: xs) = f x (foldr f b xs)
139+foldr f e [] = e
140+foldr f e (x::xs) = f x (foldr f e xs)
141+
142+--------------------------------------------------------------------------------
143+-- Special folds
144+--------------------------------------------------------------------------------
145+
146+concat : List (List a) -> List a
147+concat = foldr (++) []
148+
149+concatMap : (a -> List b) -> List a -> List b
150+concatMap f [] = []
151+concatMap f (x::xs) = f x ++ concatMap f xs
65152
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)
153+and : List Bool -> Bool
154+and = foldr (&&) True
155+
156+or : List Bool -> Bool
157+or = foldr (||) False
158+
159+any : (a -> Bool) -> List a -> Bool
160+any p = or . map p
161+
162+all : (a -> Bool) -> List a -> Bool
163+all p = and . map p
164+
165+--------------------------------------------------------------------------------
166+-- Transformations
167+--------------------------------------------------------------------------------
168+
169+reverse : List a -> List a
170+reverse = reverse' []
171+ where
172+ reverse' : List a -> List a -> List a
173+ reverse' acc [] = acc
174+ reverse' acc (x::xs) = reverse' (x::acc) xs
175+
176+intersperse : a -> List a -> List a
177+intersperse sep [] = []
178+intersperse sep (x::xs) = x :: intersperse' sep xs
179+ where
180+ intersperse' : a -> List a -> List a
181+ intersperse' sep [] = []
182+ intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
183+
184+intercalate : List a -> List (List a) -> List a
185+intercalate sep l = concat $ intersperse sep l
186+
187+--------------------------------------------------------------------------------
188+-- Membership tests
189+--------------------------------------------------------------------------------
190+
191+elemBy : (a -> a -> Bool) -> a -> List a -> Bool
192+elemBy p e [] = False
193+elemBy p e (x::xs) =
194+ if p e x then
195+ True
196+ else
197+ elemBy p e xs
70198
71199elem : Eq a => a -> List a -> Bool
72−elem x [] = False
73−elem x (y :: ys) = if (x == y) then True else (elem x ys)
200+elem = elemBy (==)
74201
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)
202+lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
203+lookupBy p e [] = Nothing
204+lookupBy p e (x::xs) =
205+ let (l, r) = x in
206+ if p e l then
207+ Just r
208+ else
209+ lookupBy p e xs
78210
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)
211+lookup : Eq a => a -> List (a, b) -> Maybe b
212+lookup = lookupBy (==)
87213
88− split : List a -> (List a, List a)
89− split xs = splitrec xs xs id
214+hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
215+hasAnyBy p elems [] = False
216+hasAnyBy p elems (x::xs) =
217+ if elemBy p x elems then
218+ True
219+ else
220+ hasAnyBy p elems xs
221+
222+hasAny : Eq a => List a -> List a -> Bool
223+hasAny = hasAnyBy (==)
224+
225+--------------------------------------------------------------------------------
226+-- Searching with a predicate
227+--------------------------------------------------------------------------------
228+
229+find : (a -> Bool) -> List a -> Maybe a
230+find p [] = Nothing
231+find p (x::xs) =
232+ if p x then
233+ Just x
234+ else
235+ find p xs
236+
237+findIndex : (a -> Bool) -> List a -> Maybe Nat
238+findIndex = findIndex' 0
239+ where
240+ findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat
241+ findIndex' cnt p [] = Nothing
242+ findIndex' cnt p (x::xs) =
243+ if p x then
244+ Just cnt
245+ else
246+ findIndex' (S cnt) p xs
247+
248+findIndices : (a -> Bool) -> List a -> List Nat
249+findIndices = findIndices' 0
250+ where
251+ findIndices' : Nat -> (a -> Bool) -> List a -> List Nat
252+ findIndices' cnt p [] = []
253+ findIndices' cnt p (x::xs) =
254+ if p x then
255+ cnt :: findIndices' (S cnt) p xs
256+ else
257+ findIndices' (S cnt) p xs
258+
259+elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat
260+elemIndexBy p e = findIndex $ p e
261+
262+elemIndex : Eq a => a -> List a -> Maybe Nat
263+elemIndex = elemIndexBy (==)
264+
265+elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat
266+elemIndicesBy p e = findIndices $ p e
90267
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)
268+elemIndices : Eq a => a -> List a -> List Nat
269+elemIndices = elemIndicesBy (==)
270+
271+--------------------------------------------------------------------------------
272+-- Filters
273+--------------------------------------------------------------------------------
274+
275+filter : (a -> Bool) -> List a -> List a
276+filter p [] = []
277+filter p (x::xs) =
278+ if p x then
279+ x :: filter p xs
280+ else
281+ filter p xs
282+
283+nubBy : (a -> a -> Bool) -> List a -> List a
284+nubBy = nubBy' []
285+ where
286+ nubBy' : List a -> (a -> a -> Bool) -> List a -> List a
287+ nubBy' acc p [] = []
288+ nubBy' acc p (x::xs) =
289+ if elemBy p x acc then
290+ nubBy' acc p xs
291+ else
292+ x :: nubBy' (x::acc) p xs
293+
294+nub : Eq a => List a -> List a
295+nub = nubBy (==)
296+
297+--------------------------------------------------------------------------------
298+-- Splitting and breaking lists
299+--------------------------------------------------------------------------------
96300
97301span : (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)
302+span p [] = ([], [])
303+span p (x::xs) =
304+ if p x then
305+ let (ys, zs) = span p xs in
306+ (x::ys, zs)
307+ else
308+ ([], x::xs)
103309
104310break : (a -> Bool) -> List a -> (List a, List a)
105311break p = span (not . p)
106−
312+
107313split : (a -> Bool) -> List a -> List (List a)
108314split p [] = []
109−split p xs = case break p xs of
110− (chunk, []) => [chunk]
111− (chunk, (c :: rest)) => chunk :: split p rest
315+split p xs =
316+ case break p xs of
317+ (chunk, []) => [chunk]
318+ (chunk, (c :: rest)) => chunk :: split p rest
319+
320+partition : (a -> Bool) -> List a -> (List a, List a)
321+partition p [] = ([], [])
322+partition p (x::xs) =
323+ let (lefts, rights) = partition p xs in
324+ if p x then
325+ (x::lefts, rights)
326+ else
327+ (lefts, x::rights)
328+
329+--------------------------------------------------------------------------------
330+-- Predicates
331+--------------------------------------------------------------------------------
332+
333+isPrefixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
334+isPrefixOfBy p [] right = True
335+isPrefixOfBy p left [] = False
336+isPrefixOfBy p (x::xs) (y::ys) =
337+ if p x y then
338+ isPrefixOfBy p xs ys
339+ else
340+ False
341+
342+isPrefixOf : Eq a => List a -> List a -> Bool
343+isPrefixOf = isPrefixOfBy (==)
344+
345+isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
346+isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
347+
348+isSuffixOf : Eq a => List a -> List a -> Bool
349+isSuffixOf = isSuffixOfBy (==)
350+
351+--------------------------------------------------------------------------------
352+-- Sorting
353+--------------------------------------------------------------------------------
354+
355+sorted : Ord a => List a -> Bool
356+sorted [] = True
357+sorted (x::xs) =
358+ case xs of
359+ Nil => True
360+ (y::ys) => x <= y && sorted (y::ys)
361+
362+mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
363+mergeBy order [] right = right
364+mergeBy order left [] = left
365+mergeBy order (x::xs) (y::ys) =
366+ case order x y of
367+ LT => x :: mergeBy order xs (y::ys)
368+ _ => y :: mergeBy order (x::xs) ys
369+
370+merge : Ord a => List a -> List a -> List a
371+merge = mergeBy compare
372+
373+sort : Ord a => List a -> List a
374+sort [] = []
375+sort [x] = [x]
376+sort xs =
377+ let (x, y) = split xs in
378+ merge (sort x) (sort y)
379+ where
380+ splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)
381+ splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))
382+ splitRec _ ys zs = (zs [], ys)
383+
384+ split : List a -> (List a, List a)
385+ split xs = splitRec xs xs id
112386
113387--------------------------------------------------------------------------------
114388-- Conversions
@@ -133,3 +407,121 @@ catMaybes (x::xs) =
133407 Nothing => catMaybes xs
134408 Just j => j :: catMaybes xs
135409
410+--------------------------------------------------------------------------------
411+-- Properties
412+--------------------------------------------------------------------------------
413+
414+mapPreservesLength : (f : a -> b) -> (l : List a) ->
415+ length (map f l) = length l
416+mapPreservesLength f [] = refl
417+mapPreservesLength f (x::xs) =
418+ let inductiveHypothesis = mapPreservesLength f xs in
419+ ?mapPreservesLengthStepCase
420+
421+mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->
422+ map f (l ++ r) = map f l ++ map f r
423+mapDistributesOverAppend f [] r = refl
424+mapDistributesOverAppend f (x::xs) r =
425+ let inductiveHypothesis = mapDistributesOverAppend f xs r in
426+ ?mapDistributesOverAppendStepCase
427+
428+mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
429+ map f (map g l) = map (f . g) l
430+mapFusion f g [] = refl
431+mapFusion f g (x::xs) =
432+ let inductiveHypothesis = mapFusion f g xs in
433+ ?mapFusionStepCase
434+
435+appendNilRightNeutral : (l : List a) ->
436+ l ++ [] = l
437+appendNilRightNeutral [] = refl
438+appendNilRightNeutral (x::xs) =
439+ let inductiveHypothesis = appendNilRightNeutral xs in
440+ ?appendNilRightNeutralStepCase
441+
442+appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
443+ (l ++ c) ++ r = l ++ (c ++ r)
444+appendAssociative [] c r = refl
445+appendAssociative (x::xs) c r =
446+ let inductiveHypothesis = appendAssociative xs c r in
447+ ?appendAssociativeStepCase
448+
449+hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
450+ hasAnyBy p [] l = False
451+hasAnyByNilFalse p [] = refl
452+hasAnyByNilFalse p (x::xs) =
453+ let inductiveHypothesis = hasAnyByNilFalse p xs in
454+ ?hasAnyByNilFalseStepCase
455+
456+lengthAppend : (left : List a) -> (right : List a) ->
457+ length (left ++ right) = length left + length right
458+lengthAppend [] right = refl
459+lengthAppend (x::xs) right =
460+ let inductiveHypothesis = lengthAppend xs right in
461+ ?lengthAppendStepCase
462+
463+hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
464+hasAnyNilFalse l = ?hasAnyNilFalseBody
465+
466+--------------------------------------------------------------------------------
467+-- Proofs
468+--------------------------------------------------------------------------------
469+
470+MoreList.lengthAppendStepCase = proof {
471+ intros;
472+ rewrite inductiveHypothesis;
473+ trivial;
474+}
475+
476+MoreList.hasAnyNilFalseBody = proof {
477+ intros;
478+ rewrite (hasAnyByNilFalse (==) l);
479+ trivial;
480+}
481+
482+MoreList.hasAnyByNilFalseStepCase = proof {
483+ intros;
484+ rewrite inductiveHypothesis;
485+ trivial;
486+}
487+
488+MoreList.initProof = proof {
489+ intros;
490+ trivial;
491+}
492+
493+MoreList.lastProof = proof {
494+ intros;
495+ trivial;
496+}
497+
498+MoreList.appendNilRightNeutralStepCase = proof {
499+ intros;
500+ rewrite inductiveHypothesis;
501+ trivial;
502+}
503+
504+MoreList.appendAssociativeStepCase = proof {
505+ intros;
506+ rewrite inductiveHypothesis;
507+ trivial;
508+}
509+
510+MoreList.mapFusionStepCase = proof {
511+ intros;
512+ rewrite inductiveHypothesis;
513+ trivial;
514+}
515+
516+MoreList.mapDistributesOverAppendStepCase = proof {
517+ intros;
518+ rewrite inductiveHypothesis;
519+ trivial;
520+}
521+
522+MoreList.mapPreservesLengthStepCase = proof {
523+ intros;
524+ rewrite inductiveHypothesis;
525+ trivial;
526+}
527+