@@ -1,121 +1,383 @@
1module prelude.list
1module prelude.list
4import builtins
3import builtins
6%access public
8%access public
8infixr 7 ::
10infixr 7 ::
10−data List a = Nil | (::) a (List a)
12+data List a
12−rev : List a -> List a
16+--------------------------------------------------------------------------------
13−rev xs = revAcc [] xs where
17+-- Syntactic tests
14− revAcc : List a -> List a -> List a
18+--------------------------------------------------------------------------------
16− revAcc acc (x :: xs) = revAcc (x :: acc) xs
18−app : List a -> List a -> List a
20+isNil : List a -> Bool
19−app [] xs = xs
21+isNil [] = True
20−app (x :: xs) ys = x :: app xs ys
22+isNil (x::xs) = False
22−head : List a -> Maybe a
24+isCons : List a -> Bool
23−head [] = Nothing
25+isCons [] = False
24−head (x :: xs) = Just x
26+isCons (x::xs) = True
26−tail : List a -> List a
28+--------------------------------------------------------------------------------
27−tail [] = []
29+-- Indexing into lists
28−tail (x :: xs) = xs
30+--------------------------------------------------------------------------------
30−length : List a -> Int
32+head : (l : List a) -> (isCons l = True) -> a
31−length [] = 0
33+head (x::xs) p = x
32−length (x :: xs) = 1 + length xs
34+
35+head' : (l : List a) -> Maybe a
37+head' (x::xs) = Just x
39+tail : (l : List a) -> (isCons l = True) -> List a
42+tail' : (l : List a) -> Maybe (List a)
44+tail' (x::xs) = Just xs
46+last : (l : List a) -> (isCons l = True) -> a
50+ y::ys => last (y::ys) ?lastProof
52+last' : (l : List a) -> Maybe a
59+init : (l : List a) -> (isCons l = True) -> List a
63+ y::ys => x :: init (y::ys) ?initProof
65+init' : (l : List a) -> Maybe (List a)
71+ -- XXX: Problem with typechecking a "do" block here
72+ case init' $ y::ys of
74+ Just j => Just $ x :: j
34−take : Int -> List a -> List a
76+--------------------------------------------------------------------------------
35−take 0 xs = []
77+-- Sublists
36−take n [] = []
78+--------------------------------------------------------------------------------
37−take n (x :: xs) = x :: take (n-1) xs
39−drop : Int -> List a -> List a
80+take : Nat -> List a -> List a
40−drop 0 xs = xs
81+take Z xs = []
41−drop n [] = []
82+take (S n) [] = []
42−drop n (x :: xs) = drop (n-1) xs
83+take (S n) (x::xs) = x :: take n xs
44−map : (a -> b) -> List a -> List b
85+drop : Nat -> List a -> List a
45−map f [] = []
86+drop Z xs = xs
46−map f (x :: xs) = f x :: map f xs
87+drop (S n) [] = []
88+drop (S n) (x::xs) = drop n xs
90+--------------------------------------------------------------------------------
92+--------------------------------------------------------------------------------
94+list : a -> (a -> List a -> a) -> List a -> a
95+list nil cons [] = nil
96+list nil cons (x::xs) = cons x xs
98+length : List a -> Nat
100+length (x::xs) = 1 + length xs
102+--------------------------------------------------------------------------------
103+-- Building bigger lists
104+--------------------------------------------------------------------------------
106+(++) : List a -> List a -> List a
107+(++) [] right = right
108+(++) (x::xs) right = x :: (xs ++ right)
110+--------------------------------------------------------------------------------
112+--------------------------------------------------------------------------------
48−concatMap : (a -> List b) -> List a -> List b
114+map : (a -> b) -> List a -> List b
49−concatMap f [] = []
115+map f [] = []
50−concatMap f (x :: xs) = app (f x) (concatMap f xs)
116+map f (x::xs) = f x :: map f xs
52mapMaybe : (a -> Maybe b) -> List a -> List b
118mapMaybe : (a -> Maybe b) -> List a -> List b
53−mapMaybe f [] = []
119+mapMaybe f [] = []
54−mapMaybe f (x :: xs) = case f x of
120+mapMaybe f (x::xs) =
55− Nothing => mapMaybe f xs
122+ Nothing => mapMaybe f xs
56− Just v => v :: mapMaybe f xs
123+ Just j => j :: mapMaybe f xs
125+--------------------------------------------------------------------------------
127+--------------------------------------------------------------------------------
58foldl : (a -> b -> a) -> a -> List b -> a
129foldl : (a -> b -> a) -> a -> List b -> a
59−foldl f a [] = a
130+foldl f e [] = e
60−foldl f a (x :: xs) = foldl f (f a x) xs
131+foldl f e (x::xs) = foldl f (f e x) xs
62foldr : (a -> b -> b) -> b -> List a -> b
133foldr : (a -> b -> b) -> b -> List a -> b
63−foldr f b [] = b
134+foldr f e [] = e
64−foldr f b (x :: xs) = f x (foldr f b xs)
135+foldr f e (x::xs) = f x (foldr f e xs)
137+--------------------------------------------------------------------------------
139+--------------------------------------------------------------------------------
141+concat : List (List a) -> List a
142+concat = foldr (++) []
144+concatMap : (a -> List b) -> List a -> List b
146+concatMap f (x::xs) = f x ++ concatMap f xs
66−filter : (y -> Bool) -> List y -> List y
148+and : List Bool -> Bool
67−filter pred [] = []
149+and = foldr (&&) True
68−filter pred (x :: xs) = if (pred x) then (x :: filter pred xs)
150+
151+or : List Bool -> Bool
152+or = foldr (||) False
154+any : (a -> Bool) -> List a -> Bool
157+all : (a -> Bool) -> List a -> Bool
160+--------------------------------------------------------------------------------
162+--------------------------------------------------------------------------------
164+reverse : List a -> List a
165+reverse = reverse' []
167+ reverse' : List a -> List a -> List a
168+ reverse' acc [] = acc
169+ reverse' acc (x::xs) = reverse' (x::acc) xs
171+intersperse : a -> List a -> List a
172+intersperse sep [] = []
173+intersperse sep (x::xs) = x :: intersperse' sep xs
175+ intersperse' : a -> List a -> List a
176+ intersperse' sep [] = []
177+ intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
179+intercalate : List a -> List (List a) -> List a
180+intercalate sep l = concat $ intersperse sep l
182+--------------------------------------------------------------------------------
184+--------------------------------------------------------------------------------
186+elemBy : (a -> a -> Bool) -> a -> List a -> Bool
187+elemBy p e [] = False
69− else (filter pred xs)
191+ else
71elem : Eq a => a -> List a -> Bool
194elem : Eq a => a -> List a -> Bool
72−elem x [] = False
195+elem = elemBy (==)
73−elem x (y :: ys) = if (x == y) then True else (elem x ys)
196+
197+lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
198+lookupBy p e [] = Nothing
199+lookupBy p e (x::xs) =
206+lookup : Eq a => a -> List (a, b) -> Maybe b
207+lookup = lookupBy (==)
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
217+hasAny : Eq a => List a -> List a -> Bool
218+hasAny = hasAnyBy (==)
75−lookup : Eq k => k -> List (k, v) -> Maybe v
220+--------------------------------------------------------------------------------
76−lookup k [] = Nothing
221+-- Searching with a predicate
77−lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs)
222+--------------------------------------------------------------------------------
79−sort : Ord a => List a -> List a
224+find : (a -> Bool) -> List a -> Maybe a
80−sort [] = []
225+find p [] = Nothing
81−sort [x] = [x]
226+find p (x::xs) =
82−sort xs = let (x, y) = split xs in
227+ if p x then
83− merge (sort x) (sort y) where
228+ Just x
84− splitrec : List a -> List a -> (List a -> List a) -> (List a, List a)
229+ else
85− splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y))
230+ find p xs
86− splitrec _ ys zs = (zs [], ys)
231+
232+findIndex : (a -> Bool) -> List a -> Maybe Nat
233+findIndex = findIndex' 0
235+ findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat
236+ findIndex' cnt p [] = Nothing
237+ findIndex' cnt p (x::xs) =
241+ findIndex' (S cnt) p xs
243+findIndices : (a -> Bool) -> List a -> List Nat
244+findIndices = findIndices' 0
246+ findIndices' : Nat -> (a -> Bool) -> List a -> List Nat
247+ findIndices' cnt p [] = []
248+ findIndices' cnt p (x::xs) =
250+ cnt :: findIndices' (S cnt) p xs
252+ findIndices' (S cnt) p xs
254+elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat
255+elemIndexBy p e = findIndex $ p e
257+elemIndex : Eq a => a -> List a -> Maybe Nat
258+elemIndex = elemIndexBy (==)
260+elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat
261+elemIndicesBy p e = findIndices $ p e
263+elemIndices : Eq a => a -> List a -> List Nat
264+elemIndices = elemIndicesBy (==)
88− split : List a -> (List a, List a)
266+--------------------------------------------------------------------------------
89− split xs = splitrec xs xs id
267+-- Filters
268+--------------------------------------------------------------------------------
270+filter : (a -> Bool) -> List a -> List a
278+nubBy : (a -> a -> Bool) -> List a -> List a
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
287+ x :: nubBy' (x::acc) p xs
91− merge : Ord a => List a -> List a -> List a
289+nub : Eq a => List a -> List a
92− merge xs [] = xs
290+nub = nubBy (==)
94− merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))
292+--------------------------------------------------------------------------------
95− else (y :: merge (x :: xs) ys)
293+-- Splitting and breaking lists
294+--------------------------------------------------------------------------------
97span : (a -> Bool) -> List a -> (List a, List a)
296span : (a -> Bool) -> List a -> (List a, List a)
98−span p [] = ([], [])
297+span p [] = ([], [])
99−span p (x :: xs) with (p x)
298+span p (x::xs) =
100− | True with (span p xs)
299+ if p x then
300+ let (ys, zs) = span p xs in
101− | (ys, zs) = (x :: ys, zs)
301+ (x::ys, zs)
102− | False = ([], x :: xs)
303+ ([], x::xs)
104break : (a -> Bool) -> List a -> (List a, List a)
305break : (a -> Bool) -> List a -> (List a, List a)
105break p = span (not . p)
306break p = span (not . p)
107split : (a -> Bool) -> List a -> List (List a)
308split : (a -> Bool) -> List a -> List (List a)
108split p [] = []
309split p [] = []
109−split p xs = case break p xs of
311+ case break p xs of
110− (chunk, []) => [chunk]
312+ (chunk, []) => [chunk]
111− (chunk, (c :: rest)) => chunk :: split p rest
313+ (chunk, (c :: rest)) => chunk :: split p rest
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
324+--------------------------------------------------------------------------------
326+--------------------------------------------------------------------------------
113−any : (a -> Bool) -> List a -> Bool
328+isPrefixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
114−any predicate [] = False
329+isPrefixOfBy p [] right = True
115−any predicate (a::rest) =
330+isPrefixOfBy p left [] = False
116− if predicate a
331+isPrefixOfBy p (x::xs) (y::ys) =
117− then True
332+ if p x y then
118− else any predicate rest
333+ isPrefixOfBy p xs ys
337+isPrefixOf : Eq a => List a -> List a -> Bool
338+isPrefixOf = isPrefixOfBy (==)
340+isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
341+isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
343+isSuffixOf : Eq a => List a -> List a -> Bool
344+isSuffixOf = isSuffixOfBy (==)
346+--------------------------------------------------------------------------------
348+--------------------------------------------------------------------------------
350+sorted : Ord a => List a -> Bool
355+ (y::ys) => x <= y && sorted (y::ys)
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) =
362+ LT => x :: mergeBy order xs (y::ys)
363+ _ => y :: mergeBy order (x::xs) ys
365+merge : Ord a => List a -> List a -> List a
366+merge = mergeBy compare
368+sort : Ord a => List a -> List a
372+ let (x, y) = split xs in
373+ merge (sort x) (sort y)
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)
379+ split : List a -> (List a, List a)
380+ split xs = splitRec xs xs id
120--------------------------------------------------------------------------------
382--------------------------------------------------------------------------------
121-- Conversions
383-- Conversions
@@ -161,3 +423,122 @@ instance Ord a => Ord (List a) where
161 if a /= b
423 if a /= b
162 then compare a b
424 then compare a b
163 else compare restA restB
425 else compare restA restB
427+--------------------------------------------------------------------------------
429+--------------------------------------------------------------------------------
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
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
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
452+appendNilRightNeutral : (l : List a) ->
454+appendNilRightNeutral [] = refl
455+appendNilRightNeutral (x::xs) =
456+ let inductiveHypothesis = appendNilRightNeutral xs in
457+ ?appendNilRightNeutralStepCase
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
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
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
480+hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
481+hasAnyNilFalse l = ?hasAnyNilFalseBody
483+--------------------------------------------------------------------------------
485+--------------------------------------------------------------------------------
487+lengthAppendStepCase = proof {
489+ rewrite inductiveHypothesis;
493+hasAnyNilFalseBody = proof {
495+ rewrite (hasAnyByNilFalse (==) l);
499+hasAnyByNilFalseStepCase = proof {
501+ rewrite inductiveHypothesis;
515+appendNilRightNeutralStepCase = proof {
517+ rewrite inductiveHypothesis;
521+appendAssociativeStepCase = proof {
523+ rewrite inductiveHypothesis;
527+mapFusionStepCase = proof {
529+ rewrite inductiveHypothesis;
533+mapDistributesOverAppendStepCase = proof {
535+ rewrite inductiveHypothesis;
539+mapPreservesLengthStepCase = proof {
541+ rewrite inductiveHypothesis;