@@ -5,110 +5,384 @@ import builtins
6%access public
6%access public
8infixr 7 ::
15infixr 7 ::
10−data List a = Nil | (::) a (List a)
17+data List a
21+--------------------------------------------------------------------------------
23+--------------------------------------------------------------------------------
25+isNil : List a -> Bool
29+isCons : List a -> Bool
33+--------------------------------------------------------------------------------
34+-- Indexing into lists
35+--------------------------------------------------------------------------------
12−rev : List a -> List a
37+head : (l : List a) -> (isCons l = True) -> a
13−rev xs = revAcc [] xs where
38+head (x::xs) p = x
14− revAcc : List a -> List a -> List a
16− revAcc acc (x :: xs) = revAcc (x :: acc) xs
18−app : List a -> List a -> List a
40+head' : (l : List a) -> Maybe a
19−app [] xs = xs
41+head' [] = Nothing
20−app (x :: xs) ys = x :: app xs ys
42+head' (x::xs) = Just x
22−head : List a -> Maybe a
44+tail : (l : List a) -> (isCons l = True) -> List a
23−head [] = Nothing
45+tail (x::xs) p = xs
24−head (x :: xs) = Just x
26−tail : List a -> List a
47+tail' : (l : List a) -> Maybe (List a)
27−tail [] = []
48+tail' [] = Nothing
28−tail (x :: xs) = xs
49+tail' (x::xs) = Just xs
30−length : List a -> Int
51+last : (l : List a) -> (isCons l = True) -> a
31−length [] = 0
52+last (x::xs) p =
32−length (x :: xs) = 1 + length xs
53+ case xs of
55+ y::ys => last (y::ys) ?lastProof
34−take : Int -> List a -> List a
57+last' : (l : List a) -> Maybe a
35−take 0 xs = []
58+last' [] = Nothing
36−take n [] = []
59+last' (x::xs) =
37−take n (x :: xs) = x :: take (n-1) xs
60+ case xs of
39−drop : Int -> List a -> List a
64+init : (l : List a) -> (isCons l = True) -> List a
40−drop 0 xs = xs
65+init (x::xs) p =
41−drop n [] = []
67+ [] => []
42−drop n (x :: xs) = drop (n-1) xs
68+ y::ys => x :: init (y::ys) ?initProof
44−map : (a -> b) -> List a -> List b
70+init' : (l : List a) -> Maybe (List a)
45−map f [] = []
71+init' [] = Nothing
46−map f (x :: xs) = f x :: map f xs
72+init' (x::xs) =
76+ -- XXX: Problem with typechecking a "do" block here
77+ case init' $ y::ys of
79+ Just j => Just $ x :: j
81+--------------------------------------------------------------------------------
83+--------------------------------------------------------------------------------
85+take : Nat -> List a -> List a
88+take (S n) (x::xs) = x :: take n xs
48−concatMap : (a -> List b) -> List a -> List b
90+drop : Nat -> List a -> List a
49−concatMap f [] = []
91+drop Z xs = xs
50−concatMap f (x :: xs) = app (f x) (concatMap f xs)
92+drop (S n) [] = []
93+drop (S n) (x::xs) = drop n xs
95+--------------------------------------------------------------------------------
97+--------------------------------------------------------------------------------
99+list : a -> (a -> List a -> a) -> List a -> a
100+list nil cons [] = nil
101+list nil cons (x::xs) = cons x xs
103+length : List a -> Nat
105+length (x::xs) = 1 + length xs
107+--------------------------------------------------------------------------------
108+-- Building bigger lists
109+--------------------------------------------------------------------------------
111+(++) : List a -> List a -> List a
112+(++) [] right = right
113+(++) (x::xs) right = x :: (xs ++ right)
115+--------------------------------------------------------------------------------
117+--------------------------------------------------------------------------------
119+map : (a -> b) -> List a -> List b
121+map f (x::xs) = f x :: map f xs
52mapMaybe : (a -> Maybe b) -> List a -> List b
123mapMaybe : (a -> Maybe b) -> List a -> List b
53−mapMaybe f [] = []
124+mapMaybe f [] = []
54−mapMaybe f (x :: xs) = case f x of
125+mapMaybe f (x::xs) =
55− Nothing => mapMaybe f xs
127+ Nothing => mapMaybe f xs
56− Just v => v :: mapMaybe f xs
128+ Just j => j :: mapMaybe f xs
130+--------------------------------------------------------------------------------
132+--------------------------------------------------------------------------------
58foldl : (a -> b -> a) -> a -> List b -> a
134foldl : (a -> b -> a) -> a -> List b -> a
59−foldl f a [] = a
135+foldl f e [] = e
60−foldl f a (x :: xs) = foldl f (f a x) xs
136+foldl f e (x::xs) = foldl f (f e x) xs
62foldr : (a -> b -> b) -> b -> List a -> b
138foldr : (a -> b -> b) -> b -> List a -> b
63−foldr f b [] = b
139+foldr f e [] = e
64−foldr f b (x :: xs) = f x (foldr f b xs)
140+foldr f e (x::xs) = f x (foldr f e xs)
142+--------------------------------------------------------------------------------
144+--------------------------------------------------------------------------------
146+concat : List (List a) -> List a
147+concat = foldr (++) []
149+concatMap : (a -> List b) -> List a -> List b
151+concatMap f (x::xs) = f x ++ concatMap f xs
66−filter : (y -> Bool) -> List y -> List y
153+and : List Bool -> Bool
67−filter pred [] = []
154+and = foldr (&&) True
68−filter pred (x :: xs) = if (pred x) then (x :: filter pred xs)
155+
156+or : List Bool -> Bool
157+or = foldr (||) False
159+any : (a -> Bool) -> List a -> Bool
162+all : (a -> Bool) -> List a -> Bool
165+--------------------------------------------------------------------------------
167+--------------------------------------------------------------------------------
169+reverse : List a -> List a
170+reverse = reverse' []
172+ reverse' : List a -> List a -> List a
173+ reverse' acc [] = acc
174+ reverse' acc (x::xs) = reverse' (x::acc) xs
176+intersperse : a -> List a -> List a
177+intersperse sep [] = []
178+intersperse sep (x::xs) = x :: intersperse' sep xs
180+ intersperse' : a -> List a -> List a
181+ intersperse' sep [] = []
182+ intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
184+intercalate : List a -> List (List a) -> List a
185+intercalate sep l = concat $ intersperse sep l
187+--------------------------------------------------------------------------------
189+--------------------------------------------------------------------------------
191+elemBy : (a -> a -> Bool) -> a -> List a -> Bool
192+elemBy p e [] = False
69− else (filter pred xs)
196+ else
71elem : Eq a => a -> List a -> Bool
199elem : Eq a => a -> List a -> Bool
72−elem x [] = False
200+elem = elemBy (==)
73−elem x (y :: ys) = if (x == y) then True else (elem x ys)
75−lookup : Eq k => k -> List (k, v) -> Maybe v
202+lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
76−lookup k [] = Nothing
203+lookupBy p e [] = Nothing
77−lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs)
204+lookupBy p e (x::xs) =
79−sort : Ord a => List a -> List a
211+lookup : Eq a => a -> List (a, b) -> Maybe b
80−sort [] = []
212+lookup = lookupBy (==)
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)
88− split : List a -> (List a, List a)
214+hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
89− split xs = splitrec xs xs id
215+hasAnyBy p elems [] = False
216+hasAnyBy p elems (x::xs) =
217+ if elemBy p x elems then
222+hasAny : Eq a => List a -> List a -> Bool
223+hasAny = hasAnyBy (==)
225+--------------------------------------------------------------------------------
226+-- Searching with a predicate
227+--------------------------------------------------------------------------------
229+find : (a -> Bool) -> List a -> Maybe a
237+findIndex : (a -> Bool) -> List a -> Maybe Nat
238+findIndex = findIndex' 0
240+ findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat
241+ findIndex' cnt p [] = Nothing
242+ findIndex' cnt p (x::xs) =
246+ findIndex' (S cnt) p xs
248+findIndices : (a -> Bool) -> List a -> List Nat
249+findIndices = findIndices' 0
251+ findIndices' : Nat -> (a -> Bool) -> List a -> List Nat
252+ findIndices' cnt p [] = []
253+ findIndices' cnt p (x::xs) =
255+ cnt :: findIndices' (S cnt) p xs
257+ findIndices' (S cnt) p xs
259+elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat
260+elemIndexBy p e = findIndex $ p e
262+elemIndex : Eq a => a -> List a -> Maybe Nat
263+elemIndex = elemIndexBy (==)
265+elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat
266+elemIndicesBy p e = findIndices $ p e
91− merge : Ord a => List a -> List a -> List a
268+elemIndices : Eq a => a -> List a -> List Nat
92− merge xs [] = xs
269+elemIndices = elemIndicesBy (==)
94− merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))
271+--------------------------------------------------------------------------------
273+--------------------------------------------------------------------------------
275+filter : (a -> Bool) -> List a -> List a
283+nubBy : (a -> a -> Bool) -> List a -> List a
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
95− else (y :: merge (x :: xs) ys)
291+ else
292+ x :: nubBy' (x::acc) p xs
294+nub : Eq a => List a -> List a
297+--------------------------------------------------------------------------------
298+-- Splitting and breaking lists
299+--------------------------------------------------------------------------------
97span : (a -> Bool) -> List a -> (List a, List a)
301span : (a -> Bool) -> List a -> (List a, List a)
98−span p [] = ([], [])
302+span p [] = ([], [])
99−span p (x :: xs) with (p x)
303+span p (x::xs) =
100− | True with (span p xs)
304+ if p x then
305+ let (ys, zs) = span p xs in
101− | (ys, zs) = (x :: ys, zs)
306+ (x::ys, zs)
102− | False = ([], x :: xs)
308+ ([], x::xs)
104break : (a -> Bool) -> List a -> (List a, List a)
310break : (a -> Bool) -> List a -> (List a, List a)
105break p = span (not . p)
311break p = span (not . p)
107split : (a -> Bool) -> List a -> List (List a)
313split : (a -> Bool) -> List a -> List (List a)
108split p [] = []
314split p [] = []
109−split p xs = case break p xs of
316+ case break p xs of
110− (chunk, []) => [chunk]
317+ (chunk, []) => [chunk]
111− (chunk, (c :: rest)) => chunk :: split p rest
318+ (chunk, (c :: rest)) => chunk :: split p rest
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
329+--------------------------------------------------------------------------------
331+--------------------------------------------------------------------------------
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) =
338+ isPrefixOfBy p xs ys
342+isPrefixOf : Eq a => List a -> List a -> Bool
343+isPrefixOf = isPrefixOfBy (==)
345+isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
346+isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
348+isSuffixOf : Eq a => List a -> List a -> Bool
349+isSuffixOf = isSuffixOfBy (==)
351+--------------------------------------------------------------------------------
353+--------------------------------------------------------------------------------
355+sorted : Ord a => List a -> Bool
360+ (y::ys) => x <= y && sorted (y::ys)
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) =
367+ LT => x :: mergeBy order xs (y::ys)
368+ _ => y :: mergeBy order (x::xs) ys
370+merge : Ord a => List a -> List a -> List a
371+merge = mergeBy compare
373+sort : Ord a => List a -> List a
377+ let (x, y) = split xs in
378+ merge (sort x) (sort y)
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)
384+ split : List a -> (List a, List a)
385+ split xs = splitRec xs xs id
113--------------------------------------------------------------------------------
387--------------------------------------------------------------------------------
114-- Conversions
388-- Conversions
@@ -133,3 +407,121 @@ catMaybes (x::xs) =
133 Nothing => catMaybes xs
407 Nothing => catMaybes xs
134 Just j => j :: catMaybes xs
408 Just j => j :: catMaybes xs
410+--------------------------------------------------------------------------------
412+--------------------------------------------------------------------------------
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
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
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
435+appendNilRightNeutral : (l : List a) ->
437+appendNilRightNeutral [] = refl
438+appendNilRightNeutral (x::xs) =
439+ let inductiveHypothesis = appendNilRightNeutral xs in
440+ ?appendNilRightNeutralStepCase
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
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
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
463+hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
464+hasAnyNilFalse l = ?hasAnyNilFalseBody
466+--------------------------------------------------------------------------------
468+--------------------------------------------------------------------------------
470+MoreList.lengthAppendStepCase = proof {
472+ rewrite inductiveHypothesis;
476+MoreList.hasAnyNilFalseBody = proof {
478+ rewrite (hasAnyByNilFalse (==) l);
482+MoreList.hasAnyByNilFalseStepCase = proof {
484+ rewrite inductiveHypothesis;
488+MoreList.initProof = proof {
493+MoreList.lastProof = proof {
498+MoreList.appendNilRightNeutralStepCase = proof {
500+ rewrite inductiveHypothesis;
504+MoreList.appendAssociativeStepCase = proof {
506+ rewrite inductiveHypothesis;
510+MoreList.mapFusionStepCase = proof {
512+ rewrite inductiveHypothesis;
516+MoreList.mapDistributesOverAppendStepCase = proof {
518+ rewrite inductiveHypothesis;
522+MoreList.mapPreservesLengthStepCase = proof {
524+ rewrite inductiveHypothesis;