Merge pull request #367 from tweag/tbagrel1/inspection-testing-make-elim

Add inspection tests to `Replicator.elim` and `V.{make,elim}`

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,

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

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) =

src/Data/V/Linear.hs

@@ -35,6 +35,7 @@
 -- rather than linear types).
 module Data.V.Linear
   ( V,
+    empty,
     consume,
     map,
     pure,

src/Data/V/Linear/Internal.hs

@@ -22,6 +22,7 @@
 
 module Data.V.Linear.Internal
   ( V (..),
+    empty,
     consume,
     map,
     pure,
@@ -63,8 +64,13 @@ 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 (\_ -> ())
+{-# 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
@@ -80,13 +86,15 @@ 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)
 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@.
@@ -156,7 +164,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

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

test/Test/Data/Replicator.hs

@@ -0,0 +1,31 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# 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 f r = Replicator.elim f r
+
+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

test/Test/Data/V.hs

@@ -0,0 +1,42 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_GHC -O -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 f v = V.elim f v
+
+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