From c205db3ff7f379963e306c84b68bb27ee44346b1 Mon Sep 17 00:00:00 2001
From: rnhmjoj <micheleguerinirocco@me.com>
Date: Tue, 15 Nov 2016 20:28:12 +0100
Subject: [PATCH] add intercalate and concat

---
 src/Data/Vec.hs | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs
index bd88233..77257bf 100644
--- a/src/Data/Vec.hs
+++ b/src/Data/Vec.hs
@@ -158,6 +158,14 @@ intersperse _ (x :- Nil) = x :- Nil
 intersperse s (x :- xs)  = gcastWith (double n) (x :- s :- intersperse s xs)
   where n = sLength (x :- xs)
 
+
+-- | 'intercalate' @xs xss@ is equivalent to
+-- @('concat' ('intersperse' xs xss))@. It inserts the vector @xs@
+-- in between the vectors in @xss@ and concatenates the result.
+intercalate ∷ Vec a n → Vec (Vec a n) m → Vec a ((m :+ Pred m) :× n)
+intercalate xs xss = concat (intersperse xs xss)
+
+
 -- | '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.
@@ -186,6 +194,16 @@ foldr₁ f (x :- Nil)     = x
 foldr₁ f (x :- y :- ys) = f x (foldr₁ f (y :- ys))
 
 
+-- | The concatenation of all the elements of a vector of vectors.
+concat ∷ Vec (Vec a n) m → Vec a (m :× n)
+concat Nil = Nil
+concat (xs :- xss) = gcastWith proof (xs ⧺ concat xss)
+  where
+    n = sLength xs
+    m = sLength xss
+    proof = plus_commut n (m %:× n)
+
+
 -- | 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