diff options
| -rw-r--r-- | ox-arrays.cabal | 1 | ||||
| -rw-r--r-- | src/Data/Array/Mixed/Permutation.hs | 3 | ||||
| -rw-r--r-- | test/Gen.hs | 19 | ||||
| -rw-r--r-- | test/Main.hs | 5 | ||||
| -rw-r--r-- | test/Tests/Permutation.hs | 39 |
5 files changed, 54 insertions, 13 deletions
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 () + ] |