blob: 1e7ad135ab20c366d0780b16997c59f7b2b89b16 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
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 ()
]
|
