From 39cc8556e36845f52583695ab713123396144ec1 Mon Sep 17 00:00:00 2001
From: Lucas Bollen <lucas@qbaylogic.com>
Date: Tue, 24 Sep 2024 11:36:08 +0200
Subject: [PATCH 1/4] Create `Protocols.Vec` with `vecCircuits`

---
 clash-protocols/clash-protocols.cabal     |  1 +
 clash-protocols/src/Protocols/DfConv.hs   |  5 +++--
 clash-protocols/src/Protocols/Internal.hs |  8 --------
 clash-protocols/src/Protocols/Vec.hs      | 18 ++++++++++++++++++
 4 files changed, 22 insertions(+), 10 deletions(-)
 create mode 100644 clash-protocols/src/Protocols/Vec.hs

diff --git a/clash-protocols/clash-protocols.cabal b/clash-protocols/clash-protocols.cabal
index 98d6cbb5..197732b4 100644
--- a/clash-protocols/clash-protocols.cabal
+++ b/clash-protocols/clash-protocols.cabal
@@ -151,6 +151,7 @@ library
     Protocols.Idle
     Protocols.Internal
     Protocols.Internal.TH
+    Protocols.Vec
     Protocols.Wishbone
     Protocols.Wishbone.Standard
     Protocols.Wishbone.Standard.Hedgehog
diff --git a/clash-protocols/src/Protocols/DfConv.hs b/clash-protocols/src/Protocols/DfConv.hs
index e6eccc95..02652a6c 100644
--- a/clash-protocols/src/Protocols/DfConv.hs
+++ b/clash-protocols/src/Protocols/DfConv.hs
@@ -115,6 +115,7 @@ import Protocols.Axi4.WriteResponse
 import Protocols.Df (Data (..), Df)
 import qualified Protocols.Df as Df
 import Protocols.Internal
+import qualified Protocols.Vec as Vec
 
 {- | Class for protocols that are "similar" to 'Df', i.e. they can be converted
 to and from a pair of 'Df' ports (one going 'Fwd', one going 'Bwd'), using
@@ -599,7 +600,7 @@ vecToDfConv ::
     (Vec n df)
 vecToDfConv proxy =
   mapCircuit (uncurry C.zip) unzip id id
-    $ vecCircuits
+    $ Vec.vecCircuits
     $ repeat
     $ toDfCircuit proxy
 
@@ -616,7 +617,7 @@ vecFromDfConv ::
     )
 vecFromDfConv proxy =
   mapCircuit id id unzip (uncurry C.zip)
-    $ vecCircuits
+    $ Vec.vecCircuits
     $ repeat
     $ fromDfCircuit proxy
 
diff --git a/clash-protocols/src/Protocols/Internal.hs b/clash-protocols/src/Protocols/Internal.hs
index 33ce4f58..aa36ef07 100644
--- a/clash-protocols/src/Protocols/Internal.hs
+++ b/clash-protocols/src/Protocols/Internal.hs
@@ -539,14 +539,6 @@ mapCircuit ::
   Circuit a' b'
 mapCircuit ia oa ob ib (Circuit f) = Circuit ((oa *** ob) . f . (ia *** ib))
 
-{- | "Bundle" together a 'C.Vec' of 'Circuit's into a 'Circuit' with 'C.Vec' input and output.
-The 'Circuit's all run in parallel.
--}
-vecCircuits :: (C.KnownNat n) => C.Vec n (Circuit a b) -> Circuit (C.Vec n a) (C.Vec n b)
-vecCircuits fs = Circuit (\inps -> C.unzip $ f <$> fs <*> uncurry C.zip inps)
- where
-  f (Circuit ff) x = ff x
-
 {- | "Bundle" together a pair of 'Circuit's into a 'Circuit' with two inputs and outputs.
 The 'Circuit's run in parallel.
 -}
diff --git a/clash-protocols/src/Protocols/Vec.hs b/clash-protocols/src/Protocols/Vec.hs
new file mode 100644
index 00000000..0b8afb36
--- /dev/null
+++ b/clash-protocols/src/Protocols/Vec.hs
@@ -0,0 +1,18 @@
+module Protocols.Vec where
+
+-- base
+import Prelude hiding (const, map)
+
+-- clash-prelude
+import qualified Clash.Prelude as C
+
+-- clash-protocols-base
+import Protocols.Plugin
+
+{- | "Bundle" together a 'C.Vec' of 'Circuit's into a 'Circuit' with 'C.Vec' input and output.
+The 'Circuit's all run in parallel.
+-}
+vecCircuits :: (C.KnownNat n) => C.Vec n (Circuit a b) -> Circuit (C.Vec n a) (C.Vec n b)
+vecCircuits fs = Circuit (\inps -> C.unzip $ f <$> fs <*> uncurry C.zip inps)
+ where
+  f (Circuit ff) = ff

From d59432f2539e71c9b1c60ff635696bbefb191dcb Mon Sep 17 00:00:00 2001
From: Lucas Bollen <lucas@qbaylogic.com>
Date: Tue, 24 Sep 2024 11:40:49 +0200
Subject: [PATCH 2/4] Add clarification to `vecCircuits` that the inverse can
 not exist

---
 clash-protocols/src/Protocols/Vec.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/clash-protocols/src/Protocols/Vec.hs b/clash-protocols/src/Protocols/Vec.hs
index 0b8afb36..a743ac1d 100644
--- a/clash-protocols/src/Protocols/Vec.hs
+++ b/clash-protocols/src/Protocols/Vec.hs
@@ -11,6 +11,9 @@ import Protocols.Plugin
 
 {- | "Bundle" together a 'C.Vec' of 'Circuit's into a 'Circuit' with 'C.Vec' input and output.
 The 'Circuit's all run in parallel.
+
+The inverse of 'vecCircuits' can not exist, as we can not guarantee that that the @n@th
+manager interface only depends on the @n@th subordinate interface.
 -}
 vecCircuits :: (C.KnownNat n) => C.Vec n (Circuit a b) -> Circuit (C.Vec n a) (C.Vec n b)
 vecCircuits fs = Circuit (\inps -> C.unzip $ f <$> fs <*> uncurry C.zip inps)

From 87c4073f8fb9af98786c6c56483f040be3cceeb2 Mon Sep 17 00:00:00 2001
From: Lucas Bollen <lucas@qbaylogic.com>
Date: Tue, 24 Sep 2024 14:07:39 +0200
Subject: [PATCH 3/4] More utility functions for `Vec`s of  `Circuits`

append
append3
split
split3
zip
zip3
unzip
unzip3
concat
unconcat
---
 clash-protocols/src/Protocols/Vec.hs | 118 ++++++++++++++++++++++++++-
 1 file changed, 115 insertions(+), 3 deletions(-)

diff --git a/clash-protocols/src/Protocols/Vec.hs b/clash-protocols/src/Protocols/Vec.hs
index a743ac1d..0d46cf7a 100644
--- a/clash-protocols/src/Protocols/Vec.hs
+++ b/clash-protocols/src/Protocols/Vec.hs
@@ -1,15 +1,32 @@
-module Protocols.Vec where
+-- | Utility functions for working with `Vec`s of `Circuit`s.
+module Protocols.Vec (
+  vecCircuits,
+  append,
+  append3,
+  split,
+  split3,
+  zip,
+  zip3,
+  unzip,
+  unzip3,
+  concat,
+  unconcat,
+) where
 
 -- base
-import Prelude hiding (const, map)
+import Data.Tuple
+import Prelude ()
 
 -- clash-prelude
+import Clash.Prelude hiding (concat, split, unconcat, unzip, unzip3, zip, zip3)
 import qualified Clash.Prelude as C
 
 -- clash-protocols-base
 import Protocols.Plugin
 
-{- | "Bundle" together a 'C.Vec' of 'Circuit's into a 'Circuit' with 'C.Vec' input and output.
+import Data.Bifunctor
+
+{- | "Bundle" together a 'Vec' of 'Circuit's into a 'Circuit' with 'Vec' input and output.
 The 'Circuit's all run in parallel.
 
 The inverse of 'vecCircuits' can not exist, as we can not guarantee that that the @n@th
@@ -19,3 +36,98 @@ vecCircuits :: (C.KnownNat n) => C.Vec n (Circuit a b) -> Circuit (C.Vec n a) (C
 vecCircuits fs = Circuit (\inps -> C.unzip $ f <$> fs <*> uncurry C.zip inps)
  where
   f (Circuit ff) = ff
+
+-- | Append two separate vectors of the same circuits into one vector of circuits
+append ::
+  (C.KnownNat n0) =>
+  Circuit (C.Vec n0 circuit, C.Vec n1 circuit) (C.Vec (n0 + n1) circuit)
+append = Circuit (swap . bimap (uncurry (++)) splitAtI)
+
+-- | Append three separate vectors of the same circuits into one vector of circuits
+append3 ::
+  (C.KnownNat n0, C.KnownNat n1, KnownNat n2) =>
+  Circuit
+    (C.Vec n0 circuit, C.Vec n1 circuit, C.Vec n2 circuit)
+    (C.Vec (n0 + n1 + n2) circuit)
+append3 = Circuit (swap . bimap (uncurry3 append3Vec) split3Vec)
+
+-- | Split a vector of circuits into two vectors of circuits.
+split ::
+  (C.KnownNat n0) =>
+  Circuit (C.Vec (n0 + n1) circuit) (C.Vec n0 circuit, C.Vec n1 circuit)
+split = Circuit go
+ where
+  go ~(splitAtI -> (fwd0, fwd1), (bwd0, bwd1)) = (bwd0 ++ bwd1, (fwd0, fwd1))
+
+-- | Split a vector of circuits into three vectors of circuits.
+split3 ::
+  (C.KnownNat n0, C.KnownNat n1, C.KnownNat n2) =>
+  Circuit
+    (C.Vec (n0 + n1 + n2) circuit)
+    (C.Vec n0 circuit, C.Vec n1 circuit, C.Vec n2 circuit)
+split3 = Circuit (swap . bimap split3Vec (uncurry3 append3Vec))
+
+{- | Transforms two vectors of circuits into a vector of tuples of circuits.
+Only works if the two vectors have the same length.
+-}
+zip ::
+  (C.KnownNat n) =>
+  Circuit (C.Vec n a, C.Vec n b) (C.Vec n (a, b))
+zip = Circuit (swap . bimap (uncurry C.zip) C.unzip)
+
+{- | Transforms three vectors of circuits into a vector of tuples of circuits.
+Only works if the three vectors have the same length.
+-}
+zip3 ::
+  (C.KnownNat n) =>
+  Circuit (C.Vec n a, C.Vec n b, C.Vec n c) (C.Vec n (a, b, c))
+zip3 = Circuit (swap . bimap (uncurry3 C.zip3) C.unzip3)
+
+-- | Unzip a vector of tuples of circuits into a tuple of vectors of circuits.
+unzip ::
+  (C.KnownNat n) =>
+  Circuit (C.Vec n (a, b)) (C.Vec n a, C.Vec n b)
+unzip = Circuit (swap . bimap C.unzip (uncurry C.zip))
+
+-- | Unzip a vector of 3-tuples of circuits into a 3-tuple of vectors of circuits.
+unzip3 ::
+  (C.KnownNat n) =>
+  Circuit (C.Vec n (a, b, c)) (C.Vec n a, C.Vec n b, C.Vec n c)
+unzip3 = Circuit (swap . bimap C.unzip3 (uncurry3 C.zip3))
+
+-- | transform a vector of vectors of circuits into a vector of circuits.
+concat ::
+  (C.KnownNat n0, C.KnownNat n1) =>
+  Circuit (C.Vec n0 (C.Vec n1 circuit)) (C.Vec (n0 * n1) circuit)
+concat = Circuit (swap . bimap C.concat (C.unconcat SNat))
+
+-- | transform a vector of circuits into a vector of vectors of circuits.
+unconcat ::
+  (C.KnownNat n, C.KnownNat m) =>
+  SNat m ->
+  Circuit (C.Vec (n * m) circuit) (C.Vec n (C.Vec m circuit))
+unconcat SNat = Circuit (swap . bimap (C.unconcat SNat) C.concat)
+
+-- Internal utilities
+
+-- | Uncurry a function with three arguments into a function that takes a 3-tuple as argument.
+uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
+uncurry3 f (a, b, c) = f a b c
+
+-- Append three vectors of `a` into one vector of `a`.
+append3Vec ::
+  (KnownNat n0, KnownNat n1, KnownNat n2) =>
+  C.Vec n0 a ->
+  C.Vec n1 a ->
+  C.Vec n2 a ->
+  C.Vec (n0 + n1 + n2) a
+append3Vec v0 v1 v2 = v0 ++ v1 ++ v2
+
+-- Split a C.Vector of 3-tuples into three vectors of the same length.
+split3Vec ::
+  (KnownNat n0, KnownNat n1, KnownNat n2) =>
+  C.Vec (n0 + n1 + n2) a ->
+  (C.Vec n0 a, C.Vec n1 a, C.Vec n2 a)
+split3Vec v = (v0, v1, v2)
+ where
+  (v0, splitAtI -> (v1, v2)) = splitAtI v

From 6109f0ac15f5ca7584edd09142e6fc69d1c81390 Mon Sep 17 00:00:00 2001
From: Lucas Bollen <lucas@qbaylogic.com>
Date: Wed, 20 Nov 2024 10:12:46 +0100
Subject: [PATCH 4/4] Add `Tests.Protocols.Vec`

---
 clash-protocols/clash-protocols.cabal        |   1 +
 clash-protocols/tests/Tests/Protocols.hs     |   2 +
 clash-protocols/tests/Tests/Protocols/Vec.hs | 191 +++++++++++++++++++
 3 files changed, 194 insertions(+)
 create mode 100644 clash-protocols/tests/Tests/Protocols/Vec.hs

diff --git a/clash-protocols/clash-protocols.cabal b/clash-protocols/clash-protocols.cabal
index 197732b4..00386f30 100644
--- a/clash-protocols/clash-protocols.cabal
+++ b/clash-protocols/clash-protocols.cabal
@@ -185,6 +185,7 @@ test-suite unittests
     Tests.Protocols.Avalon
     Tests.Protocols.Axi4
     Tests.Protocols.Plugin
+    Tests.Protocols.Vec
     Tests.Protocols.Wishbone
     Util
 
diff --git a/clash-protocols/tests/Tests/Protocols.hs b/clash-protocols/tests/Tests/Protocols.hs
index a09bc008..043732ec 100644
--- a/clash-protocols/tests/Tests/Protocols.hs
+++ b/clash-protocols/tests/Tests/Protocols.hs
@@ -5,6 +5,7 @@ import qualified Tests.Protocols.Avalon
 import qualified Tests.Protocols.Axi4
 import qualified Tests.Protocols.Df
 import qualified Tests.Protocols.DfConv
+import qualified Tests.Protocols.Vec
 import qualified Tests.Protocols.Wishbone
 
 tests :: TestTree
@@ -16,6 +17,7 @@ tests =
     , Tests.Protocols.Avalon.tests
     , Tests.Protocols.Axi4.tests
     , Tests.Protocols.Wishbone.tests
+    , Tests.Protocols.Vec.tests
     ]
 
 main :: IO ()
diff --git a/clash-protocols/tests/Tests/Protocols/Vec.hs b/clash-protocols/tests/Tests/Protocols/Vec.hs
new file mode 100644
index 00000000..936aef20
--- /dev/null
+++ b/clash-protocols/tests/Tests/Protocols/Vec.hs
@@ -0,0 +1,191 @@
+{-# LANGUAGE NumericUnderscores #-}
+
+module Tests.Protocols.Vec where
+
+-- base
+import Prelude
+
+-- clash-prelude
+import Clash.Prelude (System)
+import qualified Clash.Prelude as C
+
+-- hedgehog
+import Hedgehog
+
+-- tasty
+import Test.Tasty
+import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit))
+import Test.Tasty.Hedgehog.Extra (testProperty)
+import Test.Tasty.TH (testGroupGenerator)
+
+-- clash-protocols (me!)
+import Protocols
+import qualified Protocols.Vec as Vec
+
+import Clash.Hedgehog.Sized.Vector (genVec)
+import Protocols.Hedgehog
+
+-- tests
+import Tests.Protocols.Df (genData, genSmallInt, genVecData)
+
+prop_append :: Property
+prop_append =
+  idWithModel
+    @(C.Vec 2 (Df System Int), C.Vec 3 (Df System Int))
+    defExpectOptions
+    gen
+    model
+    dut
+ where
+  gen =
+    (,)
+      <$> genVecData genSmallInt
+      <*> genVecData genSmallInt
+  dut = Vec.append
+  model = uncurry (C.++)
+
+prop_append3 :: Property
+prop_append3 =
+  idWithModel
+    @(C.Vec 2 (Df System Int), C.Vec 3 (Df System Int), C.Vec 4 (Df System Int))
+    @(C.Vec 9 (Df System Int))
+    defExpectOptions
+    gen
+    model
+    dut
+ where
+  gen :: Gen (C.Vec 2 [Int], C.Vec 3 [Int], C.Vec 4 [Int])
+  gen =
+    (,,)
+      <$> genVecData genSmallInt
+      <*> genVecData genSmallInt
+      <*> genVecData genSmallInt
+  dut = Vec.append3
+  model (a, b, c) = (a C.++ b) C.++ c
+
+prop_split :: Property
+prop_split =
+  idWithModel
+    @(C.Vec 5 (Df System Int))
+    @(C.Vec 2 (Df System Int), C.Vec 3 (Df System Int))
+    defExpectOptions
+    gen
+    model
+    dut
+ where
+  gen = genVecData genSmallInt
+  dut = Vec.split
+  model = C.splitAtI
+
+prop_split3 :: Property
+prop_split3 =
+  idWithModel
+    @(C.Vec 9 (Df System Int))
+    @(C.Vec 2 (Df System Int), C.Vec 3 (Df System Int), C.Vec 4 (Df System Int))
+    defExpectOptions
+    gen
+    model
+    dut
+ where
+  gen = genVecData genSmallInt
+  dut = Vec.split3
+  model v = (v0, v1, v2)
+   where
+    (v0, C.splitAtI -> (v1, v2)) = C.splitAtI v
+
+prop_zip :: Property
+prop_zip =
+  idWithModel
+    @(C.Vec 2 (Df System Int), C.Vec 2 (Df System Int))
+    defExpectOptions
+    gen
+    model
+    dut
+ where
+  gen =
+    (,)
+      <$> genVecData genSmallInt
+      <*> genVecData genSmallInt
+  dut = Vec.zip
+  model (a, b) = C.zip a b
+
+prop_zip3 :: Property
+prop_zip3 =
+  idWithModel
+    @(C.Vec 2 (Df System Int), C.Vec 2 (Df System Int), C.Vec 2 (Df System Int))
+    defExpectOptions
+    gen
+    model
+    dut
+ where
+  gen =
+    (,,)
+      <$> genVecData genSmallInt
+      <*> genVecData genSmallInt
+      <*> genVecData genSmallInt
+  dut = Vec.zip3
+  model (a, b, c) = C.zip3 a b c
+
+prop_unzip :: Property
+prop_unzip =
+  idWithModel
+    @(C.Vec 2 (Df System Int, Df System Int))
+    defExpectOptions
+    gen
+    model
+    dut
+ where
+  gen = genVec ((,) <$> genData genSmallInt <*> genData genSmallInt)
+  dut = Vec.unzip
+  model = C.unzip
+
+prop_unzip3 :: Property
+prop_unzip3 =
+  idWithModel
+    @(C.Vec 2 (Df System Int, Df System Int, Df System Int))
+    defExpectOptions
+    gen
+    model
+    dut
+ where
+  gen = genVec ((,,) <$> genData genSmallInt <*> genData genSmallInt <*> genData genSmallInt)
+  dut = Vec.unzip3
+  model = C.unzip3
+
+prop_concat :: Property
+prop_concat =
+  idWithModel
+    @(C.Vec 2 (C.Vec 3 (Df System Int)))
+    defExpectOptions
+    gen
+    model
+    dut
+ where
+  gen = genVec (genVecData genSmallInt)
+  dut = Vec.concat
+  model = C.concat
+
+prop_unconcat :: Property
+prop_unconcat =
+  idWithModel
+    @(C.Vec 6 (Df System Int))
+    defExpectOptions
+    gen
+    model
+    dut
+ where
+  gen = genVecData genSmallInt
+  dut = Vec.unconcat C.d2
+  model = C.unconcat C.d2
+
+tests :: TestTree
+tests =
+  -- TODO: Move timeout option to hedgehog for better error messages.
+  -- TODO: Does not seem to work for combinatorial loops like @let x = x in x@??
+  localOption (mkTimeout 20_000_000 {- 20 seconds -}) $
+    localOption
+      (HedgehogTestLimit (Just 1000))
+      $(testGroupGenerator)
+
+main :: IO ()
+main = defaultMain tests