git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/libs/base/Data/Vect.idr
670 lines 26 kB history raw
1module Data.Vect
3import public Data.Fin
4import Language.Reflection
6%access public export
7%default total
9infixr 7 ::
11||| Vectors: Generic lists with explicit length in the type
12||| @ len the length of the list
13||| @ elem the type of elements
14%elim
15data Vect : (len : Nat) -> (elem : Type) -> Type where
16 ||| Empty vector
17 Nil : Vect Z elem
18 ||| A non-empty vector of length `S len`, consisting of a head element and
19 ||| the rest of the list, of length `len`.
20 (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
22-- Hints for interactive editing
23%name Vect xs,ys,zs,ws
25--------------------------------------------------------------------------------
26-- Length
27--------------------------------------------------------------------------------
29||| Calculate the length of a `Vect`.
30|||
31||| **Note**: this is only useful if you don't already statically know the length
32||| and you want to avoid matching the implicit argument for erasure reasons.
33||| @ len the length (provably equal to the return value)
34||| @ xs the vector
35length : (xs : Vect len elem) -> Nat
36length [] = 0
37length (x::xs) = 1 + length xs
39||| Show that the length function on vectors in fact calculates the length
40private lengthCorrect : (len : Nat) -> (xs : Vect len elem) -> length xs = len
41lengthCorrect Z [] = Refl
42lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
44--------------------------------------------------------------------------------
45-- Indexing into vectors
46--------------------------------------------------------------------------------
48||| All but the first element of the vector
49tail : Vect (S len) elem -> Vect len elem
50tail (x::xs) = xs
52||| Only the first element of the vector
53head : Vect (S len) elem -> elem
54head (x::xs) = x
56||| The last element of the vector
57last : Vect (S len) elem -> elem
58last (x::[]) = x
59last (x::y::ys) = last $ y::ys
61||| All but the last element of the vector
62init : Vect (S len) elem -> Vect len elem
63init (x::[]) = []
64init (x::y::ys) = x :: init (y::ys)
66||| Extract a particular element from a vector
67index : Fin len -> Vect len elem -> elem
68index FZ (x::xs) = x
69index (FS k) (x::xs) = index k xs
72||| Insert an element at a particular index
73insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
74insertAt FZ y xs = y :: xs
75insertAt (FS k) y (x::xs) = x :: insertAt k y xs
76insertAt (FS k) y [] = absurd k
78||| Construct a new vector consisting of all but the indicated element
79deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
80deleteAt FZ (x::xs) = xs
81deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
82deleteAt {len = Z} (FS k) (x::xs) = absurd k
83deleteAt _ [] impossible
85||| Replace an element at a particlar index with another
86replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
87replaceAt FZ y (x::xs) = y :: xs
88replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
90||| Replace the element at a particular index with the result of applying a function to it
91||| @ i the index to replace at
92||| @ f the update function
93||| @ xs the vector to replace in
94updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem
95updateAt FZ f (x::xs) = f x :: xs
96updateAt (FS k) f (x::xs) = x :: updateAt k f xs
98--------------------------------------------------------------------------------
99-- Subvectors
100--------------------------------------------------------------------------------
102||| Get the first n elements of a Vect
103||| @ n the number of elements to take
104take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
105take Z xs = []
106take (S k) (x :: xs) = x :: take k xs
108||| Remove the first n elements of a Vect
109||| @ n the number of elements to remove
110drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
111drop Z xs = xs
112drop (S k) (x :: xs) = drop k xs
114||| Take the longest prefix of a Vect such that all elements satisfy some
115||| Boolean predicate.
116|||
117||| @ p the predicate
118takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
119takeWhile p [] = (_ ** [])
120takeWhile p (x::xs) =
121 let (len ** ys) = takeWhile p xs
122 in if p x then
123 (S len ** x :: ys)
124 else
125 (_ ** [])
127||| Remove the longest prefix of a Vect such that all removed elements satisfy some
128||| Boolean predicate.
129|||
130||| @ p the predicate
131dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
132dropWhile p [] = (_ ** [])
133dropWhile p (x::xs) =
134 if p x then
135 dropWhile p xs
136 else
137 (_ ** x::xs)
139--------------------------------------------------------------------------------
140-- Transformations
141--------------------------------------------------------------------------------
143||| Reverse the order of the elements of a vector
144reverse : Vect len elem -> Vect len elem
145reverse xs = go [] xs
146 where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
147 go {n} acc [] = rewrite plusZeroRightNeutral n in acc
148 go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
149 in go (x::acc) xs
151||| Alternate an element between the other elements of a vector
152||| @ sep the element to intersperse
153||| @ xs the vector to separate with `sep`
154intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
155intersperse sep [] = []
156intersperse sep (x::xs) = x :: intersperse' sep xs
157 where
158 intersperse' : elem -> Vect n elem -> Vect (n + n) elem
159 intersperse' sep [] = []
160 intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n
161 in sep :: x :: intersperse' sep xs
163--------------------------------------------------------------------------------
164-- Conversion from list (toList is provided by Foldable)
165--------------------------------------------------------------------------------
168fromList' : Vect len elem -> (l : List elem) -> Vect (length l + len) elem
169fromList' ys [] = ys
170fromList' {len} ys (x::xs) =
171 rewrite (plusSuccRightSucc (length xs) len) ==>
172 Vect (plus (length xs) (S len)) elem in
173 fromList' (x::ys) xs
175||| Convert a list to a vector.
176|||
177||| The length of the list should be statically known.
178fromList : (l : List elem) -> Vect (length l) elem
179fromList l =
180 rewrite (sym $ plusZeroRightNeutral (length l)) in
181 reverse $ fromList' [] l
183--------------------------------------------------------------------------------
184-- Building (bigger) vectors
185--------------------------------------------------------------------------------
187||| Append two vectors
188(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
189(++) [] ys = ys
190(++) (x::xs) ys = x :: xs ++ ys
192||| Repeate some value some number of times.
193|||
194||| @ len the number of times to repeat it
195||| @ x the value to repeat
196replicate : (len : Nat) -> (x : elem) -> Vect len elem
197replicate Z x = []
198replicate (S k) x = x :: replicate k x
200||| Merge two ordered vectors
201mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem
202mergeBy order [] [] = []
203mergeBy order [] (x :: xs) = x :: xs
204mergeBy {n = S k} order (x :: xs) [] = rewrite plusZeroRightNeutral (S k) in
205 x :: xs
206mergeBy {n = S k} {m = S k'} order (x :: xs) (y :: ys)
207 = case order x y of
208 LT => x :: mergeBy order xs (y :: ys)
209 _ => rewrite sym (plusSuccRightSucc k k') in
210 y :: mergeBy order (x :: xs) ys
212merge : Ord elem => Vect n elem -> Vect m elem -> Vect (n + m) elem
213merge = mergeBy compare
215--------------------------------------------------------------------------------
216-- Zips and unzips
217--------------------------------------------------------------------------------
219||| Combine two equal-length vectors pairwise with some function.
220|||
221||| @ f the function to combine elements with
222||| @ xs the first vector of elements
223||| @ ys the second vector of elements
224zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
225zipWith f [] [] = []
226zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
228||| Combine three equal-length vectors into a vector with some function
229zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d
230zipWith3 f [] [] [] = []
231zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
233||| Combine two equal-length vectors pairwise
234zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
235zip = zipWith (\x,y => (x,y))
237||| Combine three equal-length vectors elementwise into a vector of tuples
238zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)
239zip3 = zipWith3 (\x,y,z => (x,y,z))
241||| Convert a vector of pairs to a pair of vectors
242unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
243unzip [] = ([], [])
244unzip ((l, r)::xs) with (unzip xs)
245 | (lefts, rights) = (l::lefts, r::rights)
247||| Convert a vector of three-tuples to a triplet of vectors
248unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
249unzip3 [] = ([], [], [])
250unzip3 ((l,c,r)::xs) with (unzip3 xs)
251 | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)
253--------------------------------------------------------------------------------
254-- Equality
255--------------------------------------------------------------------------------
257implementation (Eq elem) => Eq (Vect len elem) where
258 (==) [] [] = True
259 (==) (x::xs) (y::ys) = x == y && xs == ys
262--------------------------------------------------------------------------------
263-- Order
264--------------------------------------------------------------------------------
266implementation Ord elem => Ord (Vect len elem) where
267 compare [] [] = EQ
268 compare (x::xs) (y::ys) = compare x y `thenCompare` compare xs ys
271--------------------------------------------------------------------------------
272-- Maps
273--------------------------------------------------------------------------------
275implementation Functor (Vect n) where
276 map f [] = []
277 map f (x::xs) = f x :: map f xs
280||| Map a partial function across a vector, returning those elements for which
281||| the function had a value.
282|||
283||| The first projection of the resulting pair (ie the length) will always be
284||| at most the length of the input vector. This is not, however, guaranteed
285||| by the type.
286|||
287||| @ f the partial function (expressed by returning `Maybe`)
288||| @ xs the vector to check for results
289mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
290mapMaybe f [] = (_ ** [])
291mapMaybe f (x::xs) =
292 let (len ** ys) = mapMaybe f xs
293 in case f x of
294 Just y => (S len ** y :: ys)
295 Nothing => ( len ** ys)
298--------------------------------------------------------------------------------
299-- Folds
300--------------------------------------------------------------------------------
302foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
303foldrImpl f e go [] = go e
304foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
306implementation Foldable (Vect n) where
307 foldr f e xs = foldrImpl f e id xs
309--------------------------------------------------------------------------------
310-- Special folds
311--------------------------------------------------------------------------------
313||| Flatten a vector of equal-length vectors
314concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
315concat [] = []
316concat (v::vs) = v ++ concat vs
318||| Foldr without seeding the accumulator
319foldr1 : (t -> t -> t) -> Vect (S n) t -> t
320foldr1 f (x::xs) = foldr f x xs
322||| Foldl without seeding the accumulator
323foldl1 : (t -> t -> t) -> Vect (S n) t -> t
324foldl1 f (x::xs) = foldl f x xs
325--------------------------------------------------------------------------------
326-- Scans
327--------------------------------------------------------------------------------
329scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
330scanl f q [] = [q]
331scanl f q (x::xs) = q :: scanl f (f q x) xs
333--------------------------------------------------------------------------------
334-- Membership tests
335--------------------------------------------------------------------------------
337||| Search for an item using a user-provided test
338||| @ p the equality test
339||| @ e the item to search for
340||| @ xs the vector to search in
341elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
342elemBy p e [] = False
343elemBy p e (x::xs) = p e x || elemBy p e xs
345||| Use the default Boolean equality on elements to search for an item
346||| @ x what to search for
347||| @ xs where to search
348elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
349elem = elemBy (==)
351||| Find the association of some key with a user-provided comparison
352||| @ p the comparison operator for keys (True if they match)
353||| @ e the key to look for
354lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
355lookupBy p e [] = Nothing
356lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
358||| Find the assocation of some key using the default Boolean equality test
359lookup : Eq key => key -> Vect n (key, val) -> Maybe val
360lookup = lookupBy (==)
362||| Check if any element of xs is found in elems by a user-provided comparison
363||| @ p the comparison operator
364||| @ elems the vector to search
365||| @ xs what to search for
366hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
367hasAnyBy p elems [] = False
368hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
370||| Check if any element of xs is found in elems using the default Boolean equality test
371hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
372hasAny = hasAnyBy (==)
374--------------------------------------------------------------------------------
375-- Searching with a predicate
376--------------------------------------------------------------------------------
378||| Find the first element of the vector that satisfies some test
379||| @ p the test to satisfy
380find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
381find p [] = Nothing
382find p (x::xs) = if p x then Just x else find p xs
384||| Find the index of the first element of the vector that satisfies some test
385findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
386findIndex p [] = Nothing
387findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
389||| Find the indices of all elements that satisfy some test
390findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
391findIndices p [] = []
392findIndices p (x :: xs) = let is = map FS $ findIndices p xs
393 in if p x then 0 :: is else is
395elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
396elemIndexBy p e = findIndex $ p e
398elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
399elemIndex = elemIndexBy (==)
401elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
402elemIndicesBy p e = findIndices $ p e
404elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
405elemIndices = elemIndicesBy (==)
407--------------------------------------------------------------------------------
408-- Filters
409--------------------------------------------------------------------------------
411||| Find all elements of a vector that satisfy some test
412filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
413filter p [] = ( _ ** [] )
414filter p (x::xs) =
415 let (_ ** tail) = filter p xs
416 in if p x then
417 (_ ** x::tail)
418 else
419 (_ ** tail)
421||| Make the elements of some vector unique by some test
422nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
423nubBy = nubBy' []
424 where
425 nubBy' : Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
426 nubBy' acc p [] = (_ ** [])
427 nubBy' acc p (x::xs) with (elemBy p x acc)
428 | True = nubBy' acc p xs
429 | False with (nubBy' (x::acc) p xs)
430 | (_ ** tail) = (_ ** x::tail)
432||| Make the elements of some vector unique by the default Boolean equality
433nub : Eq elem => Vect len elem -> (p ** Vect p elem)
434nub = nubBy (==)
436deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
437deleteBy _ _ [] = (_ ** [])
438deleteBy eq x (y::ys) =
439 let (len ** zs) = deleteBy eq x ys
440 in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
442delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
443delete = deleteBy (==)
445--------------------------------------------------------------------------------
446-- Splitting and breaking lists
447--------------------------------------------------------------------------------
449||| A tuple where the first element is a Vect of the n first elements and
450||| the second element is a Vect of the remaining elements of the original Vect
451||| It is equivalent to (take n xs, drop n xs)
452||| @ n the index to split at
453||| @ xs the Vect to split in two
454splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
455splitAt n xs = (take n xs, drop n xs)
457partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
458partition p [] = ((_ ** []), (_ ** []))
459partition p (x::xs) =
460 let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in
461 if p x then
462 ((S leftLen ** x::lefts), (rightLen ** rights))
463 else
464 ((leftLen ** lefts), (S rightLen ** x::rights))
466--------------------------------------------------------------------------------
467-- Predicates
468--------------------------------------------------------------------------------
470isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
471isPrefixOfBy p [] right = True
472isPrefixOfBy p left [] = False
473isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
475isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
476isPrefixOf = isPrefixOfBy (==)
478isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
479isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
481isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
482isSuffixOf = isSuffixOfBy (==)
484--------------------------------------------------------------------------------
485-- Conversions
486--------------------------------------------------------------------------------
488maybeToVect : Maybe elem -> (p ** Vect p elem)
489maybeToVect Nothing = (_ ** [])
490maybeToVect (Just j) = (_ ** [j])
492vectToMaybe : Vect len elem -> Maybe elem
493vectToMaybe [] = Nothing
494vectToMaybe (x::xs) = Just x
496--------------------------------------------------------------------------------
497-- Misc
498--------------------------------------------------------------------------------
500catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
501catMaybes [] = (_ ** [])
502catMaybes (Nothing::xs) = catMaybes xs
503catMaybes ((Just j)::xs) =
504 let (_ ** tail) = catMaybes xs
505 in (_ ** j::tail)
507diag : Vect len (Vect len elem) -> Vect len elem
508diag [] = []
509diag ((x::xs)::xss) = x :: diag (map tail xss)
511range : {len : Nat} -> Vect len (Fin len)
512range {len=Z} = []
513range {len=S _} = FZ :: map FS range
515||| Transpose a Vect of Vects, turning rows into columns and vice versa.
516|||
517||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
518transpose : {n : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
519transpose [] = replicate _ []
520transpose (x :: xs) = zipWith (::) x (transpose xs)
522--------------------------------------------------------------------------------
523-- Applicative/Monad/Traversable
524--------------------------------------------------------------------------------
526implementation Applicative (Vect k) where
527 pure = replicate _
529 fs <*> vs = zipWith apply fs vs
531||| This monad is different from the List monad, (>>=)
532||| uses the diagonal.
533implementation Monad (Vect len) where
534 m >>= f = diag (map f m)
536implementation Traversable (Vect n) where
537 traverse f [] = pure Vect.Nil
538 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
540--------------------------------------------------------------------------------
541-- Show
542--------------------------------------------------------------------------------
544implementation Show elem => Show (Vect len elem) where
545 show = show . toList
547--------------------------------------------------------------------------------
548-- Properties
549--------------------------------------------------------------------------------
551vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
552vectConsCong x xs xs Refl = Refl
554vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
555vectNilRightNeutral [] = Refl
556vectNilRightNeutral (x :: xs) =
557 vectConsCong _ _ _ (vectNilRightNeutral xs)
559vectAppendAssociative : (xs : Vect xLen elem) ->
560 (ys : Vect yLen elem) ->
561 (zs : Vect zLen elem) ->
562 xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
563vectAppendAssociative [] y z = Refl
564vectAppendAssociative (x :: xs) ys zs =
565 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
567--------------------------------------------------------------------------------
568-- DecEq
569--------------------------------------------------------------------------------
571vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
572vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
574vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
575vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
577implementation DecEq a => DecEq (Vect n a) where
578 decEq [] [] = Yes Refl
579 decEq (x :: xs) (y :: ys) with (decEq x y)
580 decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
581 decEq (x :: xs) (x :: xs) | Yes Refl | Yes Refl = Yes Refl
582 decEq (x :: xs) (x :: ys) | Yes Refl | No neq = No (neq . vectInjective2)
583 decEq (x :: xs) (y :: ys) | No neq = No (neq . vectInjective1)
585{- The following definition is elaborated in a wrong case-tree. Examination pending.
586implementation DecEq a => DecEq (Vect n a) where
587 decEq [] [] = Yes Refl
588 decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)
589 decEq (x :: xs) (x :: xs) | (Yes Refl, Yes Refl) = Yes Refl
590 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
591 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
592-}
594--------------------------------------------------------------------------------
595-- Elem
596--------------------------------------------------------------------------------
598||| A proof that some element is found in a vector
599data Elem : a -> Vect k a -> Type where
600 Here : Elem x (x::xs)
601 There : (later : Elem x xs) -> Elem x (y::xs)
603||| Nothing can be in an empty Vect
604noEmptyElem : {x : a} -> Elem x [] -> Void
605noEmptyElem Here impossible
607Uninhabited (Elem x []) where
608 uninhabited = noEmptyElem
610||| An item not in the head and not in the tail is not in the Vect at all
611neitherHereNorThere : {x, y : a} -> {xs : Vect n a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
612neitherHereNorThere xneqy xninxs Here = xneqy Refl
613neitherHereNorThere xneqy xninxs (There xinxs) = xninxs xinxs
615||| A decision procedure for Elem
616isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)
617isElem x [] = No noEmptyElem
618isElem x (y :: xs) with (decEq x y)
619 isElem x (x :: xs) | (Yes Refl) = Yes Here
620 isElem x (y :: xs) | (No xneqy) with (isElem x xs)
621 isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
622 isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)
624replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)
625replaceElem (x::xs) Here y = (y :: xs ** Here)
626replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)
627 | (ys ** yinys) = (x :: ys ** There yinys)
629replaceByElem : (xs : Vect k t) -> Elem x xs -> t -> Vect k t
630replaceByElem (x::xs) Here y = y :: xs
631replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y
633mapElem : {xs : Vect k t} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)
634mapElem Here = Here
635mapElem (There e) = There (mapElem e)
637||| Remove the element at the given position.
638|||
639||| @xs The vector to be removed from
640||| @p A proof that the element to be removed is in the vector
641dropElem : (xs : Vect (S k) t) -> (p : Elem x xs) -> Vect k t
642dropElem (x :: ys) Here = ys
643dropElem {k = (S k)} (x :: ys) (There later) = x :: dropElem ys later
645-- Some convenience functions for testing lengths
647||| If the given Vect is the required length, return a Vect with that
648||| length in its type, otherwise return Nothing
649||| @len the required length
650||| @xs the vector with the desired length
651-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we
652-- only know we don't know how to make a Vect n a, not that one can't exist.
653exactLength : {m : Nat} -> -- expected at run-time
654 (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
655exactLength {m} len xs with (decEq m len)
656 exactLength {m = m} m xs | (Yes Refl) = Just xs
657 exactLength {m = m} len xs | (No contra) = Nothing
659||| If the given Vect is at least the required length, return a Vect with
660||| at least that length in its type, otherwise return Nothing
661||| @len the required length
662||| @xs the vector with the desired length
663overLength : {m : Nat} -> -- expected at run-time
664 (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)
665overLength {m} n xs with (cmp m n)
666 overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing
667 overLength {m = m} m xs | CmpEQ
668 = Just (0 ** xs)
669 overLength {m = plus n (S x)} n xs | (CmpGT x)
670 = Just (S x ** rewrite plusCommutative (S x) n in xs)