From 30d5f7a84c5bf516785a95de51cd0176367df450 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Mon, 3 Jun 2024 18:49:08 +0200
Subject: Test permInverse

---
 ox-arrays.cabal                     |  1 +
 src/Data/Array/Mixed/Permutation.hs |  3 +--
 test/Gen.hs                         | 19 +++++++++---------
 test/Main.hs                        |  5 ++++-
 test/Tests/Permutation.hs           | 39 +++++++++++++++++++++++++++++++++++++
 5 files changed, 54 insertions(+), 13 deletions(-)
 create mode 100644 test/Tests/Permutation.hs

diff --git a/ox-arrays.cabal b/ox-arrays.cabal
index 241f20e..99df88c 100644
--- a/ox-arrays.cabal
+++ b/ox-arrays.cabal
@@ -47,6 +47,7 @@ test-suite test
   other-modules:
     Gen
     Tests.C
+    Tests.Permutation
     Util
   build-depends:
     ox-arrays,
diff --git a/src/Data/Array/Mixed/Permutation.hs b/src/Data/Array/Mixed/Permutation.hs
index 7c77fc4..ca99b02 100644
--- a/src/Data/Array/Mixed/Permutation.hs
+++ b/src/Data/Array/Mixed/Permutation.hs
@@ -65,7 +65,7 @@ permToList' = map fromIntegral . permToList
 -- | When called as @permCheckPermutation p k@, if @p@ is a permutation of
 -- @[0 .. 'length' ('permToList' p) - 1]@, @Just k@ is returned. If it isn't,
 -- then @Nothing@ is returned.
-permCheckPermutation :: forall list r. Perm list -> (IsPermutation list => r) -> Maybe r
+permCheckPermutation :: forall r list. Perm list -> (IsPermutation list => r) -> Maybe r
 permCheckPermutation = \p k ->
   let n = permLengthSNat p
   in case (provePerm1 (Proxy @list) n p, provePerm2 (SNat @0) n p) of
@@ -210,7 +210,6 @@ shxPermutePrefix = coerce (listxPermutePrefix @(SMayNat Int SNat))
 
 -- * Operations on permutations
 
--- TODO: test this thing more properly
 permInverse :: Perm is
             -> (forall is'.
                      IsPermutation is'
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 ()
+  ]
-- 
cgit v1.2.3-70-g09d2