From e290bf09b9a7bd2b009fbfb7ee61f6209e98546d Mon Sep 17 00:00:00 2001
From: Thomas BAGREL <tomsb07@gmail.com>
Date: Mon, 7 Feb 2022 18:00:10 +0100
Subject: [PATCH 1/2] Add inspection tests

Tests are now split into "Functional" and "Inspection" groups
---
 linear-base.cabal             |  4 ++++
 src/Data/V/Linear.hs          |  1 +
 src/Data/V/Linear/Internal.hs |  7 +++++-
 test/Main.hs                  | 22 +++++++++++++-----
 test/Test/Data/Replicator.hs  | 33 +++++++++++++++++++++++++++
 test/Test/Data/V.hs           | 42 +++++++++++++++++++++++++++++++++++
 6 files changed, 102 insertions(+), 7 deletions(-)
 create mode 100644 test/Test/Data/Replicator.hs
 create mode 100644 test/Test/Data/V.hs

diff --git a/linear-base.cabal b/linear-base.cabal
index 542f3df0..1a2dc88a 100644
--- a/linear-base.cabal
+++ b/linear-base.cabal
@@ -130,10 +130,14 @@ test-suite test
         Test.Data.Mutable.HashMap
         Test.Data.Mutable.Set
         Test.Data.Polarized
+        Test.Data.V
+        Test.Data.Replicator
 
     default-language: Haskell2010
     ghc-options:      -threaded -rtsopts -with-rtsopts=-N
     build-depends:
+        inspection-testing,
+        tasty-inspection-testing,
         base,
         linear-base,
         containers,
diff --git a/src/Data/V/Linear.hs b/src/Data/V/Linear.hs
index e0bf5dbf..7664e353 100644
--- a/src/Data/V/Linear.hs
+++ b/src/Data/V/Linear.hs
@@ -35,6 +35,7 @@
 -- rather than linear types).
 module Data.V.Linear
   ( V,
+    empty,
     consume,
     map,
     pure,
diff --git a/src/Data/V/Linear/Internal.hs b/src/Data/V/Linear/Internal.hs
index 38385c60..ccf67535 100644
--- a/src/Data/V/Linear/Internal.hs
+++ b/src/Data/V/Linear/Internal.hs
@@ -22,6 +22,7 @@
 
 module Data.V.Linear.Internal
   ( V (..),
+    empty,
     consume,
     map,
     pure,
@@ -63,6 +64,10 @@ newtype V (n :: Nat) (a :: Type) = V (Vector a)
 -- probably have to write my own fusion anyway. Therefore, starting from
 -- Vectors at the moment.
 
+-- | Returns an empty 'V'.
+empty :: forall a. V 0 a
+empty = V Vector.empty
+
 consume :: V 0 a %1 -> ()
 consume = Unsafe.toLinear (\_ -> ())
 
@@ -156,7 +161,7 @@ class (m ~ Arity (V n a) f) => Make m n a f | f -> m n a where
   make' :: (V m a %1 -> V n a) %1 -> f
 
 instance Make 0 n a (V n a) where
-  make' produceFrom = produceFrom (V Vector.empty)
+  make' produceFrom = produceFrom empty
   {-# INLINE make' #-}
 
 instance (m ~ Arity (V n a) (a %1 -> f), Make (m - 1) n a f) => Make m n a (a %1 -> f) where
diff --git a/test/Main.hs b/test/Main.hs
index 75b15fec..46490701 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -9,6 +9,8 @@ import Test.Data.Mutable.HashMap (mutHMTests)
 import Test.Data.Mutable.Set (mutSetTests)
 import Test.Data.Mutable.Vector (mutVecTests)
 import Test.Data.Polarized (polarizedArrayTests)
+import Test.Data.Replicator (replicatorInspectionTests)
+import Test.Data.V (vInspectionTests)
 import Test.Tasty
 
 main :: IO ()
@@ -18,10 +20,18 @@ allTests :: TestTree
 allTests =
   testGroup
     "All tests"
-    [ mutArrTests,
-      mutVecTests,
-      mutHMTests,
-      mutSetTests,
-      destArrayTests,
-      polarizedArrayTests
+    [ testGroup
+        "Functional tests"
+        [ mutArrTests,
+          mutVecTests,
+          mutHMTests,
+          mutSetTests,
+          destArrayTests,
+          polarizedArrayTests
+        ],
+      testGroup
+        "Inspection tests"
+        [ vInspectionTests,
+          replicatorInspectionTests
+        ]
     ]
diff --git a/test/Test/Data/Replicator.hs b/test/Test/Data/Replicator.hs
new file mode 100644
index 00000000..5c99343e
--- /dev/null
+++ b/test/Test/Data/Replicator.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_GHC -O -dno-suppress-type-signatures -fplugin=Test.Tasty.Inspection.Plugin #-}
+
+module Test.Data.Replicator (replicatorInspectionTests) where
+
+import Data.Replicator.Linear (Replicator)
+import qualified Data.Replicator.Linear as Replicator
+import Prelude.Linear
+import Test.Tasty
+import Test.Tasty.Inspection
+
+replicatorInspectionTests :: TestTree
+replicatorInspectionTests =
+  testGroup
+    "Inspection testing of elim for Replicator"
+    [$(inspectTest $ 'elim3 === 'manualElim3)]
+
+elim3 :: (a %1 -> a %1 -> a %1 -> [a]) %1 -> Replicator a %1 -> [a]
+elim3 = Replicator.elim
+
+manualElim3 :: (a %1 -> a %1 -> a %1 -> [a]) %1 -> Replicator a %1 -> [a]
+manualElim3 f r =
+  Replicator.next r & \case
+    (x, r') ->
+      Replicator.next r' & \case
+        (y, r'') ->
+          Replicator.extract r'' & \case
+            z -> f x y z
diff --git a/test/Test/Data/V.hs b/test/Test/Data/V.hs
new file mode 100644
index 00000000..de3e8180
--- /dev/null
+++ b/test/Test/Data/V.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_GHC -O -dsuppress-all -dno-suppress-type-signatures -fplugin=Test.Tasty.Inspection.Plugin #-}
+
+module Test.Data.V (vInspectionTests) where
+
+import Data.V.Linear (V)
+import qualified Data.V.Linear as V
+import Prelude.Linear
+import Test.Tasty
+import Test.Tasty.Inspection
+
+vInspectionTests :: TestTree
+vInspectionTests =
+  testGroup
+    "Inspection testing of elim and make for V"
+    [ $(inspectTest $ 'make3 === 'manualMake3),
+      $(inspectTest $ 'elim3 === 'manualElim3)
+    ]
+
+make3 :: a %1 -> a %1 -> a %1 -> V 3 a
+make3 = V.make
+
+manualMake3 :: a %1 -> a %1 -> a %1 -> V 3 a
+manualMake3 x y z = V.cons x . V.cons y . V.cons z $ V.empty
+
+elim3 :: (a %1 -> a %1 -> a %1 -> [a]) %1 -> V 3 a %1 -> [a]
+elim3 = V.elim
+
+manualElim3 :: (a %1 -> a %1 -> a %1 -> [a]) %1 -> V 3 a %1 -> [a]
+manualElim3 f v =
+  V.uncons v & \case
+    (x, v') ->
+      V.uncons v' & \case
+        (y, v'') ->
+          V.uncons v'' & \case
+            (z, v''') ->
+              V.consume v''' & \case
+                () -> f x y z

From 83b91845383536f7f4a1c7f5dd556212b5f59eb8 Mon Sep 17 00:00:00 2001
From: Thomas BAGREL <tomsb07@gmail.com>
Date: Wed, 9 Feb 2022 11:20:50 +0100
Subject: [PATCH 2/2] Mark {consume,next,next#,extract,uncons,uncons#} as
 INLINABLE

---
 src/Data/Replicator/Linear/Internal.hs                   | 4 ++++
 src/Data/Replicator/Linear/Internal/ReplicationStream.hs | 1 +
 src/Data/V/Linear/Internal.hs                            | 3 +++
 test/Test/Data/Replicator.hs                             | 4 +---
 test/Test/Data/V.hs                                      | 6 +++---
 5 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/Data/Replicator/Linear/Internal.hs b/src/Data/Replicator/Linear/Internal.hs
index 24781db4..0e52cc25 100644
--- a/src/Data/Replicator/Linear/Internal.hs
+++ b/src/Data/Replicator/Linear/Internal.hs
@@ -49,6 +49,7 @@ data Replicator a where
 consume :: Replicator a %1 -> ()
 consume (Moved _) = ()
 consume (Streamed stream) = ReplicationStream.consume stream
+{-# INLINEABLE consume #-}
 
 duplicate :: Replicator a %1 -> Replicator (Replicator a)
 duplicate = \case
@@ -78,6 +79,7 @@ next (Moved x) = (x, Moved x)
 next (Streamed (ReplicationStream s give dups consumes)) =
   dups s & \case
     (s1, s2) -> (give s1, Streamed (ReplicationStream s2 give dups consumes))
+{-# INLINEABLE next #-}
 
 -- | Extracts the next item from the \"infinite stream\" @'Replicator' a@.
 -- Same function as 'next', but returning an unboxed tuple.
@@ -86,6 +88,7 @@ next# (Moved x) = (# x, Moved x #)
 next# (Streamed (ReplicationStream s give dups consumes)) =
   dups s & \case
     (s1, s2) -> (# give s1, Streamed (ReplicationStream s2 give dups consumes) #)
+{-# INLINEABLE next# #-}
 
 -- | @'take' n as@ is a list of size @n@, containing @n@ replicas from @as@.
 take :: Prelude.Int -> Replicator a %1 -> [a]
@@ -102,6 +105,7 @@ take n r =
 extract :: Replicator a %1 -> a
 extract (Moved x) = x
 extract (Streamed (ReplicationStream s give _ _)) = give s
+{-# INLINEABLE extract #-}
 
 -- | Comonadic 'extend' function.
 --
diff --git a/src/Data/Replicator/Linear/Internal/ReplicationStream.hs b/src/Data/Replicator/Linear/Internal/ReplicationStream.hs
index 3020d02b..475366d9 100644
--- a/src/Data/Replicator/Linear/Internal/ReplicationStream.hs
+++ b/src/Data/Replicator/Linear/Internal/ReplicationStream.hs
@@ -37,6 +37,7 @@ data ReplicationStream a where
 
 consume :: ReplicationStream a %1 -> ()
 consume (ReplicationStream s _ _ consumes) = consumes s
+{-# INLINEABLE consume #-}
 
 duplicate :: ReplicationStream a %1 -> ReplicationStream (ReplicationStream a)
 duplicate (ReplicationStream s give dups consumes) =
diff --git a/src/Data/V/Linear/Internal.hs b/src/Data/V/Linear/Internal.hs
index ccf67535..1b0348a7 100644
--- a/src/Data/V/Linear/Internal.hs
+++ b/src/Data/V/Linear/Internal.hs
@@ -70,6 +70,7 @@ empty = V Vector.empty
 
 consume :: V 0 a %1 -> ()
 consume = Unsafe.toLinear (\_ -> ())
+{-# INLINEABLE consume #-}
 
 map :: (a %1 -> b) -> V n a %1 -> V n b
 map f (V xs) = V $ Unsafe.toLinear (Vector.map (\x -> f x)) xs
@@ -85,6 +86,7 @@ uncons# = Unsafe.toLinear uncons'#
   where
     uncons'# :: 1 <= n => V n a -> (# a, V (n - 1) a #)
     uncons'# (V xs) = (# Vector.head xs, V (Vector.tail xs) #)
+{-# INLINEABLE uncons# #-}
 
 -- | Splits the head and tail of the 'V', returning a boxed tuple.
 uncons :: 1 <= n => V n a %1 -> (a, V (n - 1) a)
@@ -92,6 +94,7 @@ uncons = Unsafe.toLinear uncons'
   where
     uncons' :: 1 <= n => V n a -> (a, V (n - 1) a)
     uncons' (V xs) = (Vector.head xs, V (Vector.tail xs))
+{-# INLINEABLE uncons #-}
 
 -- | @'Elim' n a b f@ asserts that @f@ is a function taking @n@ linear arguments
 -- of type @a@ and then returning a value of type @b@.
diff --git a/test/Test/Data/Replicator.hs b/test/Test/Data/Replicator.hs
index 5c99343e..53db227f 100644
--- a/test/Test/Data/Replicator.hs
+++ b/test/Test/Data/Replicator.hs
@@ -1,8 +1,6 @@
-{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE LinearTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# OPTIONS_GHC -O -dno-suppress-type-signatures -fplugin=Test.Tasty.Inspection.Plugin #-}
 
@@ -21,7 +19,7 @@ replicatorInspectionTests =
     [$(inspectTest $ 'elim3 === 'manualElim3)]
 
 elim3 :: (a %1 -> a %1 -> a %1 -> [a]) %1 -> Replicator a %1 -> [a]
-elim3 = Replicator.elim
+elim3 f r = Replicator.elim f r
 
 manualElim3 :: (a %1 -> a %1 -> a %1 -> [a]) %1 -> Replicator a %1 -> [a]
 manualElim3 f r =
diff --git a/test/Test/Data/V.hs b/test/Test/Data/V.hs
index de3e8180..3cb5fc82 100644
--- a/test/Test/Data/V.hs
+++ b/test/Test/Data/V.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE LinearTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE NoImplicitPrelude #-}
-{-# OPTIONS_GHC -O -dsuppress-all -dno-suppress-type-signatures -fplugin=Test.Tasty.Inspection.Plugin #-}
+{-# OPTIONS_GHC -O -dno-suppress-type-signatures -fplugin=Test.Tasty.Inspection.Plugin #-}
 
 module Test.Data.V (vInspectionTests) where
 
@@ -18,7 +18,7 @@ vInspectionTests =
   testGroup
     "Inspection testing of elim and make for V"
     [ $(inspectTest $ 'make3 === 'manualMake3),
-      $(inspectTest $ 'elim3 === 'manualElim3)
+      $(inspectTest $ 'elim3 ==- 'manualElim3)
     ]
 
 make3 :: a %1 -> a %1 -> a %1 -> V 3 a
@@ -28,7 +28,7 @@ manualMake3 :: a %1 -> a %1 -> a %1 -> V 3 a
 manualMake3 x y z = V.cons x . V.cons y . V.cons z $ V.empty
 
 elim3 :: (a %1 -> a %1 -> a %1 -> [a]) %1 -> V 3 a %1 -> [a]
-elim3 = V.elim
+elim3 f v = V.elim f v
 
 manualElim3 :: (a %1 -> a %1 -> a %1 -> [a]) %1 -> V 3 a %1 -> [a]
 manualElim3 f v =