diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs index 859e4ca..4a9fdde 100644 --- a/src/Data/Vec.hs +++ b/src/Data/Vec.hs @@ -17,7 +17,7 @@ -- new dependantly typed language features in haskell module Data.Vec where -import Relation.Equality (gcastWith) +import Relation.Equality (gcastWith, cong, sym) import Data.Nat import Data.Bool import Data.Char (Char) @@ -84,19 +84,12 @@ fromList = f sing (⧺) Nil ys = ys --- | Given a nonempty 'Vec' returns the first element --- and the rest of the vector in a tuple. --- > uncons x ≡ (head x, tail x) -uncons ∷ Vec a (S n) → (a, Vec a n) -uncons (x :- xs) = (x, xs) - - --- | Returns the 'head' (ie the first element) of a nonempty 'Vec'. +-- | Extracts the 'head' (ie the first element) of a nonempty 'Vec'. head ∷ Vec a (S n) → a head (x :- _) = x --- | Returns the last element of a nonempty 'Vec'. +-- | Extracts the last element of a nonempty 'Vec'. last ∷ Vec a (S n) → a last (x :- Nil) = x last (x :- y :- ys) = last (y :- ys) @@ -115,8 +108,12 @@ init (x :- Nil) = Nil init (x :- y :- ys) = x :- init (y :- ys) +-- | Given a nonempty 'Vec' returns the first element +-- and the rest of the vector in a tuple. +-- > uncons x ≡ (head x, tail x) +uncons ∷ Vec a (S n) → (a, Vec a n) +uncons (x :- xs) = (x, xs) --- * Length information -- | Test whether a 'Vec' has zero length. null ∷ Vec a n → 𝔹 @@ -136,7 +133,7 @@ sLength (x :- xs) = SS (sLength xs) --- * Transforming and reducing a 'Vec' +-- * Transformations -- | Applies a function on every element of a 'Vec'. map ∷ (a → b) → Vec a n → Vec b n @@ -144,6 +141,23 @@ map _ Nil = Nil map f (x :- xs) = f x :- map f xs +-- | Reverse the order of the elements of a 'Vec' +-- > reverse ∘ reverse = id +reverse ∷ Vec a n → Vec a n +reverse Nil = Nil +reverse (y :- ys) = gcastWith proof (reverse ys ⧺ (y :- Nil)) + where proof = succ_plus (sLength ys) + + +-- | 'intersperse' @s@ takes a 'Vec' and produces one where +-- @s@ is interspersed (ie inserted between) every two elements +-- of the vector +intersperse ∷ a → Vec a n → Vec a (n :+ Pred n) +intersperse _ Nil = Nil +intersperse _ (x :- Nil) = x :- Nil +intersperse s (x :- xs) = x :- s :- intersperse s xs + + -- | 'foldl' applied to a binary operator, a starting value -- and a 'Vec' reduces the vector to a single value obtained -- by sequentially applying the operation from the left to the right. @@ -172,14 +186,6 @@ foldr₁ f (x :- Nil) = x foldr₁ f (x :- y :- ys) = f x (foldr₁ f (y :- ys)) --- | Reverse the order of the element of a 'Vec' --- > reverse ∘ reverse = id -reverse ∷ Vec a n → Vec a n -reverse Nil = Nil -reverse (y :- ys) = gcastWith proof (reverse ys ⧺ (y :- Nil)) - where proof = succ_plus (sLength ys) - - -- | Applied to a singleton natural @n@ and a value produces -- a vector obtained by duplicating the value @n@ times replicate ∷ Sℕ n → a → Vec a n @@ -199,3 +205,5 @@ take (SS n) (x :- xs) = x :- take n xs drop ∷ Sℕ n → Vec a m → Vec a (m :- n) drop SZ x = x drop (SS n) (x :- xs) = drop n xs + +