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

---
 test/Tests/Permutation.hs | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 test/Tests/Permutation.hs

(limited to 'test/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