12||| Vectors: Generic lists with explicit length in the type
14data Vect : Nat -> Type -> Type where
17 ||| A non-empty vector of length `S k`, consisting of a head element and
18 ||| the rest of the list, of length `k`.
19 (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
21-- Hints for interactive editing
24--------------------------------------------------------------------------------
26--------------------------------------------------------------------------------
28||| Calculate the length of a `Vect`.
30||| **Note**: this is only useful if you don't already statically know the length
31||| and you want to avoid matching the implicit argument for erasure reasons.
32||| @ n the length (provably equal to the return value)
34length : (xs : Vect n a) -> Nat
36length (x::xs) = 1 + length xs
38||| Show that the length function on vectors in fact calculates the length
39private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n
40lengthCorrect Z [] = Refl
41lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
43--------------------------------------------------------------------------------
44-- Indexing into vectors
45--------------------------------------------------------------------------------
47||| All but the first element of the vector
48tail : Vect (S n) a -> Vect n a
51||| Only the first element of the vector
52head : Vect (S n) a -> a
55||| The last element of the vector
56last : Vect (S n) a -> a
58last (x::y::ys) = last $ y::ys
60||| All but the last element of the vector
61init : Vect (S n) a -> Vect n a
63init (x::y::ys) = x :: init (y::ys)
65||| Extract a particular element from a vector
66index : Fin n -> Vect n a -> a
68index (FS k) (x::xs) = index k xs
71||| Insert an element at a particular index
72insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a
73insertAt FZ y xs = y :: xs
74insertAt (FS k) y (x::xs) = x :: insertAt k y xs
75insertAt (FS k) y [] = absurd k
77||| Construct a new vector consisting of all but the indicated element
78deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
79deleteAt FZ (x::xs) = xs
80deleteAt {n = S m} (FS k) (x::xs) = x :: deleteAt k xs
81deleteAt {n = Z} (FS k) (x::xs) = absurd k
82deleteAt _ [] impossible
84||| Replace an element at a particlar index with another
85replaceAt : Fin n -> t -> Vect n t -> Vect n t
86replaceAt FZ y (x::xs) = y :: xs
87replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
89||| Replace the element at a particular index with the result of applying a function to it
90||| @ i the index to replace at
91||| @ f the update function
92||| @ xs the vector to replace in
93updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t
94updateAt FZ f (x::xs) = f x :: xs
95updateAt (FS k) f (x::xs) = x :: updateAt k f xs
97--------------------------------------------------------------------------------
99--------------------------------------------------------------------------------
101||| Get the first n elements of a Vect
102||| @ n the number of elements to take
103take : (n : Nat) -> Vect (n + m) a -> Vect n a
105take (S k) (x :: xs) = x :: take k xs
107||| Remove the first n elements of a Vect
108||| @ n the number of elements to remove
109drop : (n : Nat) -> Vect (n + m) a -> Vect m a
111drop (S k) (x :: xs) = drop k xs
113||| Take the longest prefix of a Vect such that all elements satisfy some
114||| Boolean predicate.
117takeWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)
118takeWhile p [] = (_ ** [])
120 let (len ** ys) = takeWhile p xs
126||| Remove the longest prefix of a Vect such that all removed elements satisfy some
127||| Boolean predicate.
130dropWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)
131dropWhile p [] = (_ ** [])
138--------------------------------------------------------------------------------
140--------------------------------------------------------------------------------
142||| Reverse the order of the elements of a vector
143reverse : Vect n a -> Vect n a
145 where go : Vect n a -> Vect m a -> Vect (n+m) a
146 go {n} acc [] = rewrite plusZeroRightNeutral n in acc
147 go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
150||| Alternate an element between the other elements of a vector
151||| @ sep the element to intersperse
152||| @ xs the vector to separate with `sep`
153intersperse : (sep : a) -> (xs : Vect n a) -> Vect (n + pred n) a
154intersperse sep [] = []
155intersperse sep (x::xs) = x :: intersperse' sep xs
157 intersperse' : a -> Vect n a -> Vect (n + n) a
158 intersperse' sep [] = []
159 intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n
160 in sep :: x :: intersperse' sep xs
162--------------------------------------------------------------------------------
163-- Conversion from list (toList is provided by Foldable)
164--------------------------------------------------------------------------------
167fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a
169fromList' {n} ys (x::xs) =
170 rewrite (plusSuccRightSucc (length xs) n) ==>
171 Vect (plus (length xs) (S n)) a in
174||| Convert a list to a vector.
176||| The length of the list should be statically known.
177fromList : (l : List a) -> Vect (length l) a
179 rewrite (sym $ plusZeroRightNeutral (length l)) in
180 reverse $ fromList' [] l
182--------------------------------------------------------------------------------
183-- Building (bigger) vectors
184--------------------------------------------------------------------------------
186||| Append two vectors
187(++) : Vect m a -> Vect n a -> Vect (m + n) a
189(++) (x::xs) ys = x :: xs ++ ys
191||| Repeate some value n times
192||| @ n the number of times to repeat it
193||| @ x the value to repeat
194replicate : (n : Nat) -> (x : a) -> Vect n a
196replicate (S k) x = x :: replicate k x
198--------------------------------------------------------------------------------
200--------------------------------------------------------------------------------
202||| Combine two equal-length vectors pairwise with some function
203zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
205zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
207||| Combine three equal-length vectors into a vector with some function
208zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d
209zipWith3 f [] [] [] = []
210zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
212||| Combine two equal-length vectors pairwise
213zip : Vect n a -> Vect n b -> Vect n (a, b)
214zip = zipWith (\x,y => (x,y))
216||| Combine three equal-length vectors elementwise into a vector of tuples
217zip3 : Vect n a -> Vect n b -> Vect n c -> Vect n (a, b, c)
218zip3 = zipWith3 (\x,y,z => (x,y,z))
220||| Convert a vector of pairs to a pair of vectors
221unzip : Vect n (a, b) -> (Vect n a, Vect n b)
223unzip ((l, r)::xs) with (unzip xs)
224 | (lefts, rights) = (l::lefts, r::rights)
226||| Convert a vector of three-tuples to a triplet of vectors
227unzip3 : Vect n (a, b, c) -> (Vect n a, Vect n b, Vect n c)
228unzip3 [] = ([], [], [])
229unzip3 ((l,c,r)::xs) with (unzip3 xs)
230 | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)
232--------------------------------------------------------------------------------
234--------------------------------------------------------------------------------
236instance (Eq a) => Eq (Vect n a) where
238 (==) (x::xs) (y::ys) =
245--------------------------------------------------------------------------------
247--------------------------------------------------------------------------------
249instance Ord a => Ord (Vect n a) where
251 compare (x::xs) (y::ys) =
258--------------------------------------------------------------------------------
260--------------------------------------------------------------------------------
262instance Functor (Vect n) where
264 map f (x::xs) = f x :: map f xs
267||| Map a partial function across a vector, returning those elements for which
268||| the function had a value.
270||| The first projection of the resulting pair (ie the length) will always be
271||| at most the length of the input vector. This is not, however, guaranteed
274||| @ f the partial function (expressed by returning `Maybe`)
275||| @ xs the vector to check for results
276mapMaybe : (f : a -> Maybe b) -> (xs : Vect n a) -> (m : Nat ** Vect m b)
277mapMaybe f [] = (_ ** [])
279 let (len ** ys) = mapMaybe f xs
281 Just y => (S len ** y :: ys)
282 Nothing => ( len ** ys)
285--------------------------------------------------------------------------------
287--------------------------------------------------------------------------------
289total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
290foldrImpl f e go [] = go e
291foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
293instance Foldable (Vect n) where
294 foldr f e xs = foldrImpl f e id xs
296--------------------------------------------------------------------------------
298--------------------------------------------------------------------------------
300||| Flatten a vector of equal-length vectors
301concat : Vect m (Vect n a) -> Vect (m * n) a
303concat (v::vs) = v ++ concat vs
305||| Foldr without seeding the accumulator
306foldr1 : (t -> t -> t) -> Vect (S n) t -> t
307foldr1 f (x::xs) = foldr f x xs
309||| Foldl without seeding the accumulator
310foldl1 : (t -> t -> t) -> Vect (S n) t -> t
311foldl1 f (x::xs) = foldl f x xs
312--------------------------------------------------------------------------------
314--------------------------------------------------------------------------------
316scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b
318scanl f q (x::xs) = q :: scanl f (f q x) xs
320--------------------------------------------------------------------------------
322--------------------------------------------------------------------------------
324||| Search for an item using a user-provided test
325||| @ p the equality test
326||| @ e the item to search for
327||| @ xs the vector to search in
328elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool
330elemBy p e (x::xs) with (p e x)
332 | False = elemBy p e xs
334||| Use the default Boolean equality on elements to search for an item
335||| @ x what to search for
336||| @ xs where to search
337elem : Eq a => (x : a) -> (xs : Vect n a) -> Bool
340||| Find the association of some key with a user-provided comparison
341||| @ p the comparison operator for keys (True if they match)
342||| @ e the key to look for
343lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b
344lookupBy p e [] = Nothing
345lookupBy p e ((l, r)::xs) with (p e l)
347 | False = lookupBy p e xs
349||| Find the assocation of some key using the default Boolean equality test
350lookup : Eq a => a -> Vect n (a, b) -> Maybe b
351lookup = lookupBy (==)
353||| Check if any element of xs is found in elems by a user-provided comparison
354||| @ p the comparison operator
355||| @ elems the vector to search
356||| @ xs what to search for
357hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool
358hasAnyBy p elems [] = False
359hasAnyBy p elems (x::xs) with (elemBy p x elems)
361 | False = hasAnyBy p elems xs
363||| Check if any element of xs is found in elems using the default Boolean equality test
364hasAny : Eq a => Vect m a -> Vect n a -> Bool
365hasAny = hasAnyBy (==)
367--------------------------------------------------------------------------------
368-- Searching with a predicate
369--------------------------------------------------------------------------------
371||| Find the first element of the vector that satisfies some test
372||| @ p the test to satisfy
373find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a
375find p (x::xs) with (p x)
379||| Find the index of the first element of the vector that satisfies some test
380findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)
381findIndex p [] = Nothing
382findIndex p (x :: xs) with (p x)
384 | False = map FS (findIndex p xs)
386||| Find the indices of all elements that satisfy some test
387total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
388findIndices = findIndices' 0
390 total findIndices' : Nat -> (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
391 findIndices' cnt p [] = (_ ** [])
392 findIndices' cnt p (x::xs) with (findIndices' (S cnt) p xs)
399elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)
400elemIndexBy p e = findIndex $ p e
402elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
403elemIndex = elemIndexBy (==)
405total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)
406elemIndicesBy p e = findIndices $ p e
408total elemIndices : Eq a => a -> Vect m a -> (p ** Vect p Nat)
409elemIndices = elemIndicesBy (==)
411--------------------------------------------------------------------------------
413--------------------------------------------------------------------------------
415||| Find all elements of a vector that satisfy some test
416total filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
417filter p [] = ( _ ** [] )
418filter p (x::xs) with (filter p xs)
425||| Make the elements of some vector unique by some test
426nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
429 nubBy' : Vect m a -> (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
430 nubBy' acc p [] = (_ ** [])
431 nubBy' acc p (x::xs) with (elemBy p x acc)
432 | True = nubBy' acc p xs
433 | False with (nubBy' (x::acc) p xs)
434 | (_ ** tail) = (_ ** x::tail)
436||| Make the elements of some vector unique by the default Boolean equality
437nub : Eq a => Vect n a -> (p ** Vect p a)
440deleteBy : (a -> a -> Bool) -> a -> Vect n a -> (p ** Vect p a)
441deleteBy _ _ [] = (_ ** [])
442deleteBy eq x (y::ys) =
443 let (len ** zs) = deleteBy eq x ys
444 in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
446delete : (Eq a) => a -> Vect n a -> (p ** Vect p a)
447delete = deleteBy (==)
449--------------------------------------------------------------------------------
450-- Splitting and breaking lists
451--------------------------------------------------------------------------------
453||| A tuple where the first element is a Vect of the n first elements and
454||| the second element is a Vect of the remaining elements of the original Vect
455||| It is equivalent to (take n xs, drop n xs)
456||| @ n the index to split at
457||| @ xs the Vect to split in two
458splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
459splitAt n xs = (take n xs, drop n xs)
461partition : (a -> Bool) -> Vect n a -> ((p ** Vect p a), (q ** Vect q a))
462partition p [] = ((_ ** []), (_ ** []))
464 let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in
466 ((S leftLen ** x::lefts), (rightLen ** rights))
468 ((leftLen ** lefts), (S rightLen ** x::rights))
470--------------------------------------------------------------------------------
472--------------------------------------------------------------------------------
474isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
475isPrefixOfBy p [] right = True
476isPrefixOfBy p left [] = False
477isPrefixOfBy p (x::xs) (y::ys) with (p x y)
478 | True = isPrefixOfBy p xs ys
481isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool
482isPrefixOf = isPrefixOfBy (==)
484isSuffixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
485isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
487isSuffixOf : Eq a => Vect m a -> Vect n a -> Bool
488isSuffixOf = isSuffixOfBy (==)
490--------------------------------------------------------------------------------
492--------------------------------------------------------------------------------
494total maybeToVect : Maybe a -> (p ** Vect p a)
495maybeToVect Nothing = (_ ** [])
496maybeToVect (Just j) = (_ ** [j])
498total vectToMaybe : Vect n a -> Maybe a
499vectToMaybe [] = Nothing
500vectToMaybe (x::xs) = Just x
502--------------------------------------------------------------------------------
504--------------------------------------------------------------------------------
506catMaybes : Vect n (Maybe a) -> (p ** Vect p a)
507catMaybes [] = (_ ** [])
508catMaybes (Nothing::xs) = catMaybes xs
509catMaybes ((Just j)::xs) with (catMaybes xs)
510 | (_ ** tail) = (_ ** j::tail)
512diag : Vect n (Vect n a) -> Vect n a
514diag ((x::xs)::xss) = x :: diag (map tail xss)
516range : Vect n (Fin n)
518range {n=S _} = FZ :: map FS range
520||| Transpose a Vect of Vects, turning rows into columns and vice versa.
522||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
523transpose : Vect m (Vect n a) -> Vect n (Vect m a)
524transpose [] = replicate _ []
525transpose (x :: xs) = zipWith (::) x (transpose xs)
527--------------------------------------------------------------------------------
528-- Applicative/Monad/Traversable
529--------------------------------------------------------------------------------
531instance Applicative (Vect k) where
534 fs <*> vs = zipWith apply fs vs
536||| This monad is different from the List monad, (>>=)
537||| uses the diagonal.
538instance Monad (Vect n) where
539 m >>= f = diag (map f m)
541instance Traversable (Vect n) where
542 traverse f [] = pure Vect.Nil
543 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
545--------------------------------------------------------------------------------
547--------------------------------------------------------------------------------
549instance Show a => Show (Vect n a) where
552--------------------------------------------------------------------------------
554--------------------------------------------------------------------------------
556vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)
557vectConsCong x xs xs Refl = Refl
559vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
560vectNilRightNeutral [] = Refl
561vectNilRightNeutral (x :: xs) =
562 vectConsCong _ _ _ (vectNilRightNeutral xs)
564vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z
565vectAppendAssociative [] y z = Refl
566vectAppendAssociative (x :: xs) ys zs =
567 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
571--------------------------------------------------------------------------------
573--------------------------------------------------------------------------------
576vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
577vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
580vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
581vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
583instance DecEq a => DecEq (Vect n a) where
584 decEq [] [] = Yes Refl
585 decEq (x :: xs) (y :: ys) with (decEq x y)
586 decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
587 decEq (x :: xs) (x :: xs) | Yes Refl | Yes Refl = Yes Refl
588 decEq (x :: xs) (x :: ys) | Yes Refl | No neq = No (neq . vectInjective2)
589 decEq (x :: xs) (y :: ys) | No neq = No (neq . vectInjective1)
591{- The following definition is elaborated in a wrong case-tree. Examination pending.
592instance DecEq a => DecEq (Vect n a) where
593 decEq [] [] = Yes Refl
594 decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)
595 decEq (x :: xs) (x :: xs) | (Yes Refl, Yes Refl) = Yes Refl
596 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
597 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
600-- For the primitives, we have to cheat because we don't have access to their
601-- internal implementations.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list