git.iko.soy/Idris-dev
on master help sign in
Merge pull request #11 from dpmulligan/master
c887611Edwin Brady
lib/prelude/vect.idr+255−32
compare with master
unifiedsplit
@@ -1,56 +1,279 @@
1module prelude.vect
1module prelude.vect
2
2
3−import prelude.nat
4import prelude.fin
3import prelude.fin
4+import prelude.list
5+import prelude.nat
5
6
6%access public
7%access public
7
8
8infixr 10 ::
9infixr 10 ::
9
10
10data Vect : Set -> Nat -> Set where
11data Vect : Set -> Nat -> Set where
11− Nil : Vect a 0
12+ Nil : Vect a O
12− (::) : a -> Vect a k -> Vect a (1 + k)
13+ (::) : a -> Vect a n -> Vect a (S n)
14+
15+--------------------------------------------------------------------------------
16+-- Indexing into vectors
17+--------------------------------------------------------------------------------
13
18
14tail : Vect a (S n) -> Vect a n
19tail : Vect a (S n) -> Vect a n
15−tail (x :: xs) = xs
20+tail (x::xs) = xs
16−
21+
22+head : Vect a (S n) -> a
23+head (x::xs) = x
24+
25+last : Vect a (S n) -> a
26+last (x::[]) = x
27+last (x::y::ys) = last $ y::ys
28+
29+init : Vect a (S n) -> Vect a n
30+init (x::[]) = []
31+init (x::y::ys) = x :: init (y::ys)
32+
17−lookup : Fin n -> Vect a n -> a
33+index : Fin n -> Vect a n -> a
18−lookup fO (x :: xs) = x
34+index fO (x::xs) = x
19−lookup (fS k) (x :: xs) = lookup k xs
35+index (fS k) (x::xs) = index k xs
20−lookup fO [] impossible
36+index fO [] impossible
21−lookup (fS _) [] impossible
37+index (fS _) [] impossible
22−
38+
39+--------------------------------------------------------------------------------
40+-- Conversions to and from list
41+--------------------------------------------------------------------------------
42+
43+total toList : Vect a n -> List a
44+toList [] = []
45+toList (x::xs) = x :: toList xs
46+
47+total fromList : (l : List a) -> Vect a (length l)
48+fromList [] = []
49+fromList (x::xs) = x :: fromList xs
50+
51+--------------------------------------------------------------------------------
52+-- Building bigger vectors
53+--------------------------------------------------------------------------------
54+
23−(++) : Vect a n -> Vect a m -> Vect a (n + m)
55+(++) : Vect a m -> Vect a n -> Vect a (m + n)
24−(++) [] ys = ys
56+(++) [] ys = ys
25−(++) (x :: xs) ys = x :: xs ++ ys
57+(++) (x::xs) ys = x :: xs ++ ys
26−
58+
59+--------------------------------------------------------------------------------
60+-- Maps
61+--------------------------------------------------------------------------------
62+
63+total map : (a -> b) -> Vect a n -> Vect b n
64+map f [] = []
65+map f (x::xs) = f x :: map f xs
66+
67+--------------------------------------------------------------------------------
68+-- Folds
69+--------------------------------------------------------------------------------
70+
71+total foldl : (a -> b -> a) -> a -> Vect b m -> a
72+foldl f e [] = e
73+foldl f e (x::xs) = foldl f (f e x) xs
74+
75+total foldr : (a -> b -> b) -> b -> Vect a m -> b
76+foldr f e [] = e
77+foldr f e (x::xs) = f x (foldr f e xs)
78+
79+--------------------------------------------------------------------------------
80+-- Special folds
81+--------------------------------------------------------------------------------
82+
83+total and : Vect Bool m -> Bool
84+and = foldr (&&) True
85+
86+total or : Vect Bool m -> Bool
87+or = foldr (||) False
88+
89+total any : (a -> Bool) -> Vect a m -> Bool
90+any p = or . map p
91+
92+total all : (a -> Bool) -> Vect a m -> Bool
93+all p = and . map p
94+
95+--------------------------------------------------------------------------------
96+-- Transformations
97+--------------------------------------------------------------------------------
98+
99+total reverse : Vect a n -> Vect a n
100+reverse = reverse' []
101+ where
102+ total reverse' : Vect a m -> Vect a n -> Vect a (m + n)
103+ reverse' acc [] ?= acc
104+ reverse' acc (x::xs) ?= reverse' (x::acc) xs
105+
106+total intersperse' : a -> Vect a m -> (p ** Vect a p)
107+intersperse' sep [] = (_ ** [])
108+intersperse' sep (y::ys) with (intersperse' sep ys)
109+ | (_ ** tail) = (_ ** sep::y::tail)
110+
111+total intersperse : a -> Vect a m -> (p ** Vect a p)
112+intersperse sep [] = (_ ** [])
113+intersperse sep (x::xs) with (intersperse' sep xs)
114+ | (_ ** tail) = (_ ** x::tail)
115+
116+--------------------------------------------------------------------------------
117+-- Membership tests
118+--------------------------------------------------------------------------------
119+
120+elemBy : (a -> a -> Bool) -> a -> Vect a n -> Bool
121+elemBy p e [] = False
122+elemBy p e (x::xs) with (p e x)
123+ | True = True
124+ | False = elemBy p e xs
125+
126+elem : Eq a => a -> Vect a n -> Bool
127+elem = elemBy (==)
128+
129+lookupBy : (a -> a -> Bool) -> a -> Vect (a, b) n -> Maybe b
130+lookupBy p e [] = Nothing
131+lookupBy p e ((l, r)::xs) with (p e l)
132+ | True = Just r
133+ | False = lookupBy p e xs
134+
135+lookup : Eq a => a -> Vect (a, b) n -> Maybe b
136+lookup = lookupBy (==)
137+
138+hasAnyBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool
139+hasAnyBy p elems [] = False
140+hasAnyBy p elems (x::xs) with (elemBy p x elems)
141+ | True = True
142+ | False = hasAnyBy p elems xs
143+
144+hasAny : Eq a => Vect a m -> Vect a n -> Bool
145+hasAny = hasAnyBy (==)
146+
147+--------------------------------------------------------------------------------
148+-- Searching with a predicate
149+--------------------------------------------------------------------------------
150+
151+find : (a -> Bool) -> Vect a n -> Maybe a
152+find p [] = Nothing
153+find p (x::xs) with (p x)
154+ | True = Just x
155+ | False = find p xs
156+
157+findIndex : (a -> Bool) -> Vect a n -> Maybe Nat
158+findIndex = findIndex' 0
159+ where
160+ findIndex' : Nat -> (a -> Bool) -> Vect a n -> Maybe Nat
161+ findIndex' cnt p [] = Nothing
162+ findIndex' cnt p (x::xs) with (p x)
163+ | True = Just cnt
164+ | False = findIndex' (S cnt) p xs
165+
166+total findIndices : (a -> Bool) -> Vect a m -> (p ** Vect Nat p)
167+findIndices = findIndices' 0
168+ where
169+ total findIndices' : Nat -> (a -> Bool) -> Vect a m -> (p ** Vect Nat p)
170+ findIndices' cnt p [] = (_ ** [])
171+ findIndices' cnt p (x::xs) with (findIndices' (S cnt) p xs)
172+ | (_ ** tail) =
173+ if p x then
174+ (_ ** cnt::tail)
175+ else
176+ (_ ** tail)
177+
178+elemIndexBy : (a -> a -> Bool) -> a -> Vect a m -> Maybe Nat
179+elemIndexBy p e = findIndex $ p e
180+
181+elemIndex : Eq a => a -> Vect a m -> Maybe Nat
182+elemIndex = elemIndexBy (==)
183+
184+total elemIndicesBy : (a -> a -> Bool) -> a -> Vect a m -> (p ** Vect Nat p)
185+elemIndicesBy p e = findIndices $ p e
186+
187+total elemIndices : Eq a => a -> Vect a m -> (p ** Vect Nat p)
188+elemIndices = elemIndicesBy (==)
189+
190+--------------------------------------------------------------------------------
191+-- Filters
192+--------------------------------------------------------------------------------
193+
27−filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
194+total filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
28filter p [] = ( _ ** [] )
195filter p [] = ( _ ** [] )
29−filter p (x :: xs)
196+filter p (x::xs) with (filter p xs)
30− = let (_ ** xs') = filter p xs in
197+ | (_ ** tail) =
31− if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
198+ if p x then
199+ (_ ** x::tail)
200+ else
201+ (_ ** tail)
202+
203+nubBy : (a -> a -> Bool) -> Vect a n -> (p ** Vect a p)
204+nubBy = nubBy' []
205+ where
206+ nubBy' : Vect a m -> (a -> a -> Bool) -> Vect a n -> (p ** Vect a p)
207+ nubBy' acc p [] = (_ ** [])
208+ nubBy' acc p (x::xs) with (elemBy p x acc)
209+ | True = nubBy' acc p xs
210+ | False with (nubBy' (x::acc) p xs)
211+ | (_ ** tail) = (_ ** x::tail)
212+
213+nub : Eq a => Vect a n -> (p ** Vect a p)
214+nub = nubBy (==)
215+
216+--------------------------------------------------------------------------------
217+-- Splitting and breaking lists
218+--------------------------------------------------------------------------------
219+
220+-- XXX: todo
221+
222+--------------------------------------------------------------------------------
223+-- Predicates
224+--------------------------------------------------------------------------------
225+
226+isPrefixOfBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool
227+isPrefixOfBy p [] right = True
228+isPrefixOfBy p left [] = False
229+isPrefixOfBy p (x::xs) (y::ys) with (p x y)
230+ | True = isPrefixOfBy p xs ys
231+ | False = False
232+
233+isPrefixOf : Eq a => Vect a m -> Vect a n -> Bool
234+isPrefixOf = isPrefixOfBy (==)
235+
236+isSuffixOfBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool
237+isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
238+
239+isSuffixOf : Eq a => Vect a m -> Vect a n -> Bool
240+isSuffixOf = isSuffixOfBy (==)
241+
242+--------------------------------------------------------------------------------
243+-- Conversions
244+--------------------------------------------------------------------------------
245+
246+total maybeToVect : Maybe a -> (p ** Vect a p)
247+maybeToVect Nothing = (_ ** [])
248+maybeToVect (Just j) = (_ ** [j])
249+
250+total vectToMaybe : Vect a n -> Maybe a
251+vectToMaybe [] = Nothing
252+vectToMaybe (x::xs) = Just x
32
253
33−map : (a -> b) -> Vect a n -> Vect b n
254+--------------------------------------------------------------------------------
34−map f [] = []
255+-- Misc
35−map f (x :: xs) = f x :: map f xs
256+--------------------------------------------------------------------------------
36
257
37−reverse : Vect a n -> Vect a n
258+catMaybes : Vect (Maybe a) n -> (p ** Vect a p)
38−reverse xs = revAcc [] xs where
259+catMaybes [] = (_ ** [])
39− revAcc : Vect a n -> Vect a m -> Vect a (n + m)
260+catMaybes (Nothing::xs) = catMaybes xs
40− revAcc acc [] ?= acc
261+catMaybes ((Just j)::xs) with (catMaybes xs)
41− revAcc acc (x :: xs) ?= revAcc (x :: acc) xs
262+ | (_ ** tail) = (_ ** j::tail)
42
263
264+--------------------------------------------------------------------------------
43−---------- Proofs ----------
265+-- Proofs
266+--------------------------------------------------------------------------------
44
267
45−revAcc_lemma_2 = proof {
268+prelude.vect.reverse'_lemma_2 = proof {
46 intros;
269 intros;
47− rewrite plusSuccRightSucc n k;
270+ rewrite (plusSuccRightSucc m n1);
48 exact value;
271 exact value;
49}
272}
50
273
51−revAcc_lemma_1 = proof {
274+prelude.vect.reverse'_lemma_1 = proof {
52 intros;
275 intros;
53− rewrite sym (plusZeroRightNeutral n);
276+ rewrite sym (plusZeroRightNeutral m);
54 exact value;
277 exact value;
55}
278}
56
279