module Data.Vect import Data.Listimport Data.Natimport public Data.Fin import Decidable.Equality public exportdata Vect : (len : Nat) -> (elem : Type) -> Type where  ||| Empty vector  Nil  : Vect Z elem  ||| A non-empty vector of length `S len`, consisting of a head element and  ||| the rest of the list, of length `len`.  (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem -- Hints for interactive editing%name Vect xs,ys,zs,ws public exportlength : (xs : Vect len elem) -> Natlength [] = 0length (x::xs) = 1 + length xs ||| Show that the length function on vectors in fact calculates the lengthprivatelengthCorrect : (len : Nat) -> (xs : Vect len elem) -> length xs = lenlengthCorrect Z     []        = RefllengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl ---------------------------------------------------------------------------------- Indexing into vectors-------------------------------------------------------------------------------- ||| All but the first element of the vector|||||| ```idris example||| tail [1,2,3,4]||| ```public exporttail : Vect (S len) elem -> Vect len elemtail (x::xs) = xs ||| Only the first element of the vector|||||| ```idris example||| head [1,2,3,4]||| ```public exporthead : Vect (S len) elem -> elemhead (x::xs) = x ||| The last element of the vector|||||| ```idris example||| last [1,2,3,4]||| ```public exportlast : Vect (S len) elem -> elemlast (x::[])    = xlast (x::y::ys) = last $ y::ys ||| All but the last element of the vector|||||| ```idris example||| init [1,2,3,4]||| ```public exportinit : Vect (S len) elem -> Vect len eleminit (x::[])    = []init (x::y::ys) = x :: init (y::ys) ||| Extract a particular element from a vector|||||| ```idris example||| index 1 [1,2,3,4]||| ```public exportindex : Fin len -> Vect len elem -> elemindex FZ     (x::xs) = xindex (FS k) (x::xs) = index k xs ||| Insert an element at a particular index|||||| ```idris example||| insertAt 1 8 [1,2,3,4]||| ```public exportinsertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) eleminsertAt FZ     y xs      = y :: xsinsertAt (FS k) y (x::xs) = x :: insertAt k y xsinsertAt (FS k) y []      = absurd k ||| Construct a new vector consisting of all but the indicated element|||||| ```idris example||| deleteAt 1 [1,2,3,4]||| ```public exportdeleteAt : {len : _} -> Fin (S len) -> Vect (S len) elem -> Vect len elemdeleteAt             FZ     (x::xs) = xsdeleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xsdeleteAt {len = Z}   (FS k) (x::xs) impossibledeleteAt             _      []      impossible ||| Replace an element at a particlar index with another|||||| ```idris example||| replaceAt 1 8 [1,2,3,4]||| ```public exportreplaceAt : Fin len -> elem -> Vect len elem -> Vect len elemreplaceAt FZ     y (x::xs) = y :: xsreplaceAt (FS k) y (x::xs) = x :: replaceAt k y xs ||| Replace the element at a particular index with the result of applying a function to it||| @ i the index to replace at||| @ f the update function||| @ xs the vector to replace in|||||| ```idris example||| updateAt 1 (+10) [1,2,3,4]||| ```public exportupdateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elemupdateAt FZ     f (x::xs) = f x :: xsupdateAt (FS k) f (x::xs) = x :: updateAt k f xs  ||| Append two vectors|||||| ```idris example||| [1,2,3,4] ++ [5,6]||| ```public export(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem(++) []      ys = ys(++) (x::xs) ys = x :: xs ++ ys ||| Repeate some value some number of times.|||||| @ len the number of times to repeat it||| @ x the value to repeat|||||| ```idris example||| replicate 4 1||| ```public exportreplicate : (len : Nat) -> (x : elem) -> Vect len elemreplicate Z     x = []replicate (S k) x = x :: replicate k x ||| Merge two ordered vectors|||||| ```idris example||| mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])||| ```exportmergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elemmergeBy order [] [] = []mergeBy order [] (x :: xs) = x :: xsmergeBy {n = S k} order (x :: xs) [] = rewrite plusZeroRightNeutral (S k) in                                               x :: xsmergeBy {n = S k} {m = S k'} order (x :: xs) (y :: ys)     = case order x y of            LT => x :: mergeBy order xs (y :: ys)            _  => rewrite sym (plusSuccRightSucc k k') in                             y :: mergeBy order (x :: xs) ys exportmerge : Ord elem => Vect n elem -> Vect m elem -> Vect (n + m) elemmerge = mergeBy compare ---------------------------------------------------------------------------------- Transformations-------------------------------------------------------------------------------- ||| Reverse the order of the elements of a vector|||||| ```idris example||| reverse [1,2,3,4]||| ```public exportreverse : Vect len elem -> Vect len elemreverse xs = go [] xs  where go : Vect n elem -> Vect m elem -> Vect (n+m) elem        go {n}         acc []        = rewrite plusZeroRightNeutral n in acc        go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m                                       in go (x::acc) xs ||| Alternate an element between the other elements of a vector||| @ sep the element to intersperse||| @ xs the vector to separate with `sep`|||||| ```idris example||| intersperse 0 [1,2,3,4]||| ```exportintersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elemintersperse sep []      = []intersperse sep (x::xs) = x :: intersperse' sep xs  where    intersperse' : elem -> Vect n elem -> Vect (n + n) elem    intersperse'         sep []      = []    intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n                                       in sep :: x :: intersperse' sep xs ---------------------------------------------------------------------------------- Conversion from list (toList is provided by Foldable)-------------------------------------------------------------------------------- public exportfromList' : Vect len elem -> (l : List elem) -> Vect (length l + len) elemfromList' ys [] = ysfromList' {len} ys (x::xs) =  rewrite (plusSuccRightSucc (length xs) len) in  fromList' (x::ys) xs ||| Convert a list to a vector.|||||| The length of the list should be statically known.|||||| ```idris example||| fromList [1,2,3,4]||| ```public exportfromList : (l : List elem) -> Vect (length l) elemfromList l =  rewrite (sym $ plusZeroRightNeutral (length l)) in  reverse $ fromList' [] l ---------------------------------------------------------------------------------- Zips and unzips-------------------------------------------------------------------------------- ||| Combine two equal-length vectors pairwise with some function.|||||| @ f the function to combine elements with||| @ xs the first vector of elements||| @ ys the second vector of elements|||||| ```idris example||| zipWith (+) (fromList [1,2,3,4]) (fromList [5,6,7,8])||| ```public exportzipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n czipWith f []      []      = []zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys ||| Combine three equal-length vectors into a vector with some function|||||| ```idris example||| zipWith3 (\x,y,z => x+y+z) (fromList [1,2,3,4]) (fromList [5,6,7,8]) (fromList [1,1,1,1])||| ```public exportzipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n dzipWith3 f []      []      []      = []zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs ||| Combine two equal-length vectors pairwise|||||| ```idris example||| zip (fromList [1,2,3,4]) (fromList [1,2,3,4])||| ```public exportzip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)zip = zipWith (\x,y => (x,y)) ||| Combine three equal-length vectors elementwise into a vector of tuples|||||| ```idris example||| zip3 (fromList [1,2,3,4]) (fromList [1,2,3,4]) (fromList [1,2,3,4])||| ```public exportzip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)zip3 = zipWith3 (\x,y,z => (x,y,z)) ||| Convert a vector of pairs to a pair of vectors|||||| ```idris example||| unzip (fromList [(1,2), (1,2)])||| ```public exportunzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)unzip []           = ([], [])unzip ((l, r)::xs) with (unzip xs)  unzip ((l, r)::xs) | (lefts, rights) = (l::lefts, r::rights) ||| Convert a vector of three-tuples to a triplet of vectors|||||| ```idris example||| unzip3 (fromList [(1,2,3), (1,2,3)])||| ```public exportunzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)unzip3 []            = ([], [], [])unzip3 ((l,c,r)::xs) with (unzip3 xs)  unzip3 ((l,c,r)::xs) | (lefts, centers, rights)      = (l::lefts, c::centers, r::rights) ---------------------------------------------------------------------------------- Equality-------------------------------------------------------------------------------- public exportimplementation (Eq elem) => Eq (Vect len elem) where  (==) []      []      = True  (==) (x::xs) (y::ys) = x == y && xs == ys  ---------------------------------------------------------------------------------- Order-------------------------------------------------------------------------------- public exportimplementation Ord elem => Ord (Vect len elem) where  compare []      []      = EQ  compare (x::xs) (y::ys)      = case compare x y of             EQ => compare xs ys             x => x ---------------------------------------------------------------------------------- Maps-------------------------------------------------------------------------------- public exportimplementation Functor (Vect n) where  map f []        = []  map f (x::xs) = f x :: map f xs ||| Map a partial function across a vector, returning those elements for which||| the function had a value.|||||| The first projection of the resulting pair (ie the length) will always be||| at most the length of the input vector. This is not, however, guaranteed||| by the type.|||||| @ f the partial function (expressed by returning `Maybe`)||| @ xs the vector to check for results|||||| ```idris example||| mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])||| ```exportmapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)mapMaybe f []      = (_ ** [])mapMaybe f (x::xs) =  let (len ** ys) = mapMaybe f xs  in case f x of       Just y  => (S len ** y :: ys)       Nothing => (  len **      ys) ---------------------------------------------------------------------------------- Folds-------------------------------------------------------------------------------- public exportfoldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> accfoldrImpl f e go [] = go efoldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs public exportimplementation Foldable (Vect n) where  foldr f e xs = foldrImpl f e id xs ---------------------------------------------------------------------------------- Special folds-------------------------------------------------------------------------------- ||| Flatten a vector of equal-length vectors|||||| ```idris example||| concat [[1,2,3], [4,5,6]]||| ```public exportconcat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elemconcat []      = []concat (v::vs) = v ++ Vect.concat vs ||| Foldr without seeding the accumulator|||||| ```idris example||| foldr1 (-) (fromList [1,2,3])||| ```public exportfoldr1 : (t -> t -> t) -> Vect (S n) t -> tfoldr1 f [x]        = xfoldr1 f (x::y::xs) = f x (foldr1 f (y::xs)) ||| Foldl without seeding the accumulator|||||| ```idris example||| foldl1 (-) (fromList [1,2,3])||| ```public exportfoldl1 : (t -> t -> t) -> Vect (S n) t -> tfoldl1 f (x::xs) = foldl f x xs---------------------------------------------------------------------------------- Scans-------------------------------------------------------------------------------- ||| The scanl function is similar to foldl, but returns all the intermediate||| accumulator states in the form of a vector.|||||| ```idris example||| scanl (-) 0 (fromList [1,2,3])||| ```public exportscanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) resscanl f q []      = [q]scanl f q (x::xs) = q :: scanl f (f q x) xs ||| The scanl1 function is a variant of scanl that doesn't require an explicit||| starting value.||| It assumes the first element of the vector to be the starting value and then||| starts the fold with the element following it.|||||| ```idris example||| scanl1 (-) (fromList [1,2,3])||| ```public exportscanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elemscanl1 f [] = []scanl1 f (x::xs) = scanl f x xs ---------------------------------------------------------------------------------- Membership tests-------------------------------------------------------------------------------- ||| Search for an item using a user-provided test||| @ p the equality test||| @ e the item to search for||| @ xs the vector to search in|||||| ```idris example||| elemBy (==) 2 [1,2,3,4]||| ```public exportelemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> BoolelemBy p e []      = FalseelemBy p e (x::xs) = p e x || elemBy p e xs ||| Use the default Boolean equality on elements to search for an item||| @ x what to search for||| @ xs where to search|||||| ```idris example||| elem 3 [1,2,3,4]||| ```public exportelem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Boolelem = elemBy (==) ||| Find the association of some key with a user-provided comparison||| @ p the comparison operator for keys (True if they match)||| @ e the key to look for|||||| ```idris example||| lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]||| ```public exportlookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe vallookupBy p e []           = NothinglookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs ||| Find the assocation of some key using the default Boolean equality test|||||| ```idris example||| lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]||| ```public exportlookup : Eq key => key -> Vect n (key, val) -> Maybe vallookup = lookupBy (==) ||| Check if any element of xs is found in elems by a user-provided comparison||| @ p the comparison operator||| @ elems the vector to search||| @ xs what to search for|||||| ```idris example||| hasAnyBy (==) [2,5] [1,2,3,4]||| ```public exporthasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> BoolhasAnyBy p elems []      = FalsehasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs ||| Check if any element of xs is found in elems using the default Boolean equality test|||||| ```idris example||| hasAny [2,5] [1,2,3,4]||| ```public exporthasAny : Eq elem => Vect m elem -> Vect len elem -> BoolhasAny = hasAnyBy (==) ---------------------------------------------------------------------------------- Searching with a predicate--------------------------------------------------------------------------------

Lines 1–500 of 899. Load more