@@ -18,19 +18,15 @@ data Vect : Set -> Nat -> Set where
1818
1919tail : Vect a (S n) -> Vect a n
2020tail (x::xs) = xs
21−tail [] impossible
2221
2322head : Vect a (S n) -> a
2423head (x::xs) = x
25−head [] impossible
2624
2725last : Vect a (S n) -> a
28−last [] impossible
2926last (x::[]) = x
3027last (x::y::ys) = last $ y::ys
3128
3229init : Vect a (S n) -> Vect a n
33−init [] impossible
3430init (x::[]) = []
3531init (x::y::ys) = x :: init (y::ys)
3632
@@ -44,11 +40,11 @@ index (fS _) [] impossible
4440-- Conversions to and from list
4541--------------------------------------------------------------------------------
4642
47−toList : Vect a n -> List a
43+total toList : Vect a n -> List a
4844toList [] = []
4945toList (x::xs) = x :: toList xs
5046
51−fromList : (l : List a) -> Vect a (length l)
47+total fromList : (l : List a) -> Vect a (length l)
5248fromList [] = []
5349fromList (x::xs) = x :: fromList xs
5450
@@ -61,36 +57,61 @@ fromList (x::xs) = x :: fromList xs
6157(++) (x::xs) ys = x :: xs ++ ys
6258
6359--------------------------------------------------------------------------------
64−-- Transformations
60+-- Maps
6561--------------------------------------------------------------------------------
6662
67−reverse : Vect a n -> Vect a n
68−reverse = reverse' []
69− where
70− reverse' : Vect a m -> Vect a n -> Vect a (m + n)
71− reverse' acc [] ?= acc
72− reverse' acc (x::xs) ?= reverse' (x::acc) xs
63+total map : (a -> b) -> Vect a n -> Vect b n
64+map f [] = []
65+map f (x::xs) = f x :: map f xs
7366
7467--------------------------------------------------------------------------------
75−-- Maps
68+-- Folds
7669--------------------------------------------------------------------------------
7770
78−map : (a -> b) -> Vect a n -> Vect b n
79−map f [] = []
80−map f (x::xs) = f x :: map f xs
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)
8178
8279--------------------------------------------------------------------------------
83−-- Filters
80+-- Special folds
8481--------------------------------------------------------------------------------
8582
86−filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
87−filter p [] = ( _ ** [] )
88−filter p (x::xs) with (filter p xs)
89− | (_ ** tail) =
90− if p x then
91− (_ ** x::tail)
92− else
93− (_ ** tail)
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)
94115
95116--------------------------------------------------------------------------------
96117-- Membership tests
@@ -123,6 +144,123 @@ hasAnyBy p elems (x::xs) with (elemBy p x elems)
123144hasAny : Eq a => Vect a m -> Vect a n -> Bool
124145hasAny = hasAnyBy (==)
125146
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+
194+total filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
195+filter p [] = ( _ ** [] )
196+filter p (x::xs) with (filter p xs)
197+ | (_ ** tail) =
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
253+
254+--------------------------------------------------------------------------------
255+-- Misc
256+--------------------------------------------------------------------------------
257+
258+catMaybes : Vect (Maybe a) n -> (p ** Vect a p)
259+catMaybes [] = (_ ** [])
260+catMaybes (Nothing::xs) = catMaybes xs
261+catMaybes ((Just j)::xs) with (catMaybes xs)
262+ | (_ ** tail) = (_ ** j::tail)
263+
126264--------------------------------------------------------------------------------
127265-- Proofs
128266--------------------------------------------------------------------------------