Test permInverse

3 files changed, 52 insertions, 11 deletions

diff --git a/test/Gen.hs b/test/Gen.hs
index bd641af..19c50c8 100644
--- a/test/Gen.hs
+++ b/test/Gen.hs
@@ -35,7 +35,8 @@ import Util
 
 genRank :: Monad m => (forall n. SNat n -> PropertyT m ()) -> PropertyT m ()
 genRank k = do
-  rank <- forAll $ Gen.int (Range.linear 0 8)
+  rank <- forAll $ Gen.frequency [(1, return 0)
+                                 ,(49, Gen.int (Range.linear 1 8))]
   TN.withSomeSNat (fromIntegral rank) k
 
 genLowBiased :: RealFloat a => (a, a) -> Gen a
@@ -87,16 +88,14 @@ genStorables rng f = do
   let readW64 i = sum (zipWith (*) (iterate (*256) 1) [fromIntegral (bs `BS.index` (8 * i + j)) | j <- [0..7]])
   return $ VS.generate n (f . readW64)
 
-genStaticShX :: Monad m => (forall sh. StaticShX sh -> PropertyT m ()) -> PropertyT m ()
-genStaticShX = \k -> genRank (\sn -> go sn k)
+genStaticShX :: Monad m => SNat n -> (forall sh. Rank sh ~ n => StaticShX sh -> PropertyT m ()) -> PropertyT m ()
+genStaticShX = \n k -> case n of
+  SZ -> k ZKX
+  SS n' ->
+    genItem $ \item ->
+    genStaticShX n' $ \ssh ->
+      k (item :!% ssh)
   where
-    go :: Monad m => SNat n -> (forall sh. StaticShX sh -> PropertyT m ()) -> PropertyT m ()
-    go SZ k = k ZKX
-    go (SS n) k =
-      genItem $ \item ->
-      go n $ \ssh ->
-        k (item :!% ssh)
-
     genItem :: Monad m => (forall n. SMayNat () SNat n -> PropertyT m ()) -> PropertyT m ()
     genItem k = do
       b <- forAll Gen.bool
diff --git a/test/Main.hs b/test/Main.hs
index d3b97ab..575bb15 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -4,9 +4,12 @@ module Main where
 import Test.Tasty
 
 import Tests.C qualified
+import Tests.Permutation qualified
 
 
 main :: IO ()
 main = defaultMain $
   testGroup "Tests"
-    [Tests.C.tests]
+    [Tests.C.tests
+    ,Tests.Permutation.tests
+    ]
diff --git a/test/Tests/Permutation.hs b/test/Tests/Permutation.hs
new file mode 100644
index 0000000..1e7ad13
--- /dev/null
+++ b/test/Tests/Permutation.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+-- {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+-- {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
+module Tests.Permutation where
+
+import Data.Type.Equality
+
+import Data.Array.Mixed.Permutation
+
+import Hedgehog
+import Hedgehog.Gen qualified as Gen
+import Hedgehog.Range qualified as Range
+import Test.Tasty
+import Test.Tasty.Hedgehog
+
+-- import Debug.Trace
+
+import Gen
+
+
+tests :: TestTree
+tests = testGroup "Permutation"
+  [testProperty "permCheckPermutation" $ property $ do
+    n <- forAll $ Gen.int (Range.linear 0 10)
+    list <- forAll $ genPermR n
+    let r = permFromList list $ \perm ->
+              permCheckPermutation perm ()
+    case r of
+      Just () -> return ()
+      Nothing -> failure
+  ,testProperty "permInverse" $ property $
+    genRank $ \n ->
+    genPerm n $ \perm ->
+    genStaticShX n $ \ssh ->
+    permInverse perm $ \_invperm proof ->
+      case proof ssh of
+        Refl -> return ()
+  ]