From ee653f38221157a4fbc958dec193ca59b22c2a3b Mon Sep 17 00:00:00 2001
From: rnhmjoj <micheleguerinirocco@me.com>
Date: Tue, 15 Nov 2016 22:23:31 +0100
Subject: [PATCH] add concatMap

---
 src/Data/Vec.hs | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs
index 77257bf..177e7a2 100644
--- a/src/Data/Vec.hs
+++ b/src/Data/Vec.hs
@@ -155,8 +155,10 @@ reverse (y :- ys) = gcastWith proof (reverse ys ⧺ (y :- Nil))
 intersperse ∷ a → Vec a n → Vec a (n :+ Pred n)
 intersperse _ Nil        = Nil
 intersperse _ (x :- Nil) = x :- Nil
-intersperse s (x :- xs)  = gcastWith (double n) (x :- s :- intersperse s xs)
-  where n = sLength (x :- xs)
+intersperse s (x :- xs)  = gcastWith proof (x :- s :- intersperse s xs)
+  where
+    n     = sLength xs
+    proof = double (SS n)
 
 
 -- | 'intercalate' @xs xss@ is equivalent to
@@ -204,6 +206,12 @@ concat (xs :- xss) = gcastWith proof (xs ⧺ concat xss)
     proof = plus_commut n (m %:× n)
 
 
+-- | Map a function over all the elements of a vector and concatenate
+-- the resulting vectos.
+concatMap ∷ (a → Vec b n) → Vec a m → Vec b (m :× n)
+concatMap f = concat ∘ map f
+
+
 -- | 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