Test permInverse

1 files changed, 39 insertions, 0 deletions

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