diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-06-03 18:49:08 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-06-03 19:24:48 +0200 |
| commit | 30d5f7a84c5bf516785a95de51cd0176367df450 (patch) | |
| tree | 0543c7761fc216b911a2e9077c5ef2e4ace224ce /test/Gen.hs | |
| parent | cc193feee38429e1a853cc23365b95e96b206672 (diff) | |
Test permInverse
Diffstat (limited to 'test/Gen.hs')
| -rw-r--r-- | test/Gen.hs | 19 |
1 files changed, 9 insertions, 10 deletions
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 |