Reorganize functions

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
+
+