{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Main where
import Control.Exception
import Control.DeepSeq
import Control.Monad
import Data.Bifunctor
import Data.Int
import Data.List
import Data.Maybe
import Data.Proxy
import Data.Type.Equality
import Data.Typeable
import Data.Void
import Data.Word
import GHC.TypeLits
import System.Exit
import Test.QuickCheck hiding (Small)
import Unsafe.Coerce
import Numeric.Natural
import Debug.Trace
import Data.Finite.Integral
import Data.Finite.Internal.Integral
newtype SmallNonNeg a = SmallNonNeg { getSmallNonNeg :: a }
deriving (Show)
instance (Integral a, Arbitrary a) => Arbitrary (SmallNonNeg a) where
arbitrary = SmallNonNeg <$> arbitrarySizedNatural
shrink (SmallNonNeg x) = SmallNonNeg <$> shrink x
instance Arbitrary Natural where
arbitrary = fromInteger . getNonNegative <$> arbitrary
instance CoArbitrary Natural where
coarbitrary n = coarbitrary (toInteger n)
newtype Small a n = Small (Finite a n)
deriving (Show)
newtype Big a n = Big (Finite a n)
deriving (Show)
newtype Edgy a n = Edgy (Finite a n)
deriving (Show)
instance
(Arbitrary a, SaneIntegral a, KnownIntegral a n)
=> Arbitrary (Small a n) where
arbitrary
| intVal @n @a Proxy == 0 = discard
| otherwise = Small . Finite . (`mod` n)
. getSmallNonNeg <$> arbitrary
where n = intVal @n Proxy
shrink (Small (Finite x)) = Small <$> mapMaybe packFinite (shrink x)
instance
(Arbitrary a, SaneIntegral a, KnownIntegral a n)
=> Arbitrary (Big a n) where
arbitrary
| intVal @n @a Proxy == 0 = discard
| otherwise = Big . Finite . ((n - 1) -) . (`mod` n)
. getSmallNonNeg <$> arbitrary
where n = intVal @n Proxy
shrink (Big (Finite x)) = Big <$> mapMaybe packFinite (shrink x)
instance CoArbitrary a => CoArbitrary (Big a n) where
coarbitrary (Big (Finite x)) = coarbitrary x
instance
(Arbitrary a, SaneIntegral a, KnownIntegral a n)
=> Arbitrary (Edgy a n) where
arbitrary
| intVal @n @a Proxy == 0 = discard
| otherwise = Edgy . Finite <$> oneof
[ (`mod` n) . getSmallNonNeg <$> arbitrary
, ((n - 1) -) . (`mod` n) . getSmallNonNeg <$> arbitrary
]
where n = intVal @n Proxy
shrink (Edgy (Finite x)) = Edgy <$> mapMaybe packFinite (shrink x)
data SLimited a where
SLimited :: (Limited a n, KnownNat n) => Proxy n -> SLimited a
class MkSLimited (lim :: Maybe Nat) where
mkSLimited
:: forall a. (SaneIntegral a, Limit a ~ lim)
=> Integer -> Maybe (SLimited a)
instance KnownNat lim => MkSLimited ('Just lim) where
mkSLimited
:: forall a. (SaneIntegral a, Limit a ~ 'Just lim)
=> Integer -> Maybe (SLimited a)
mkSLimited n = case someNatVal n of
Just (SomeNat p)
| n <= natVal @lim Proxy
-> Just $ unsafeWithLimited (Proxy @a) p $ SLimited p
_ -> Nothing
instance MkSLimited 'Nothing where
mkSLimited n = case someNatVal n of
Just (SomeNat p) -> Just $ SLimited p
_ -> Nothing
genSmall, genOver7, genOver8, genOver15, genOver16, genOver31, genOver32,
genOver63, genOver64, genOverI, genOverW, genUnder7, genUnder8, genUnder15,
genUnder16, genUnder32, genUnder63, genUnder64, genUnderI, genUnderW
:: Gen Integer
genSmall = getNonNegative <$> arbitrary
genOver7 = (toInteger (maxBound @Int8) +) <$> genSmall
genOver8 = (toInteger (maxBound @Word8) +) <$> genSmall
genOver15 = (toInteger (maxBound @Int16) +) <$> genSmall
genOver16 = (toInteger (maxBound @Word16) +) <$> genSmall
genOver31 = (toInteger (maxBound @Int32) +) <$> genSmall
genOver32 = (toInteger (maxBound @Word32) +) <$> genSmall
genOver63 = (toInteger (maxBound @Int64) +) <$> genSmall
genOver64 = (toInteger (maxBound @Word64) +) <$> genSmall
genOverI = (toInteger (maxBound @Int) +) <$> genSmall
genOverW = (toInteger (maxBound @Word) +) <$> genSmall
genUnder7 = ((toInteger (maxBound @Int8) -) <$> genSmall) `suchThat` (>= 0)
genUnder8 = ((toInteger (maxBound @Word8) -) <$> genSmall) `suchThat` (>= 0)
genUnder15 = ((toInteger (maxBound @Int16) -) <$> genSmall) `suchThat` (>= 0)
genUnder16 = ((toInteger (maxBound @Word16) -) <$> genSmall) `suchThat` (>= 0)
genUnder31 = ((toInteger (maxBound @Int32) -) <$> genSmall) `suchThat` (>= 0)
genUnder32 = ((toInteger (maxBound @Word32) -) <$> genSmall) `suchThat` (>= 0)
genUnder63 = ((toInteger (maxBound @Int64) -) <$> genSmall) `suchThat` (>= 0)
genUnder64 = ((toInteger (maxBound @Word64) -) <$> genSmall) `suchThat` (>= 0)
genUnderI = ((toInteger (maxBound @Int) -) <$> genSmall) `suchThat` (>= 0)
genUnderW = ((toInteger (maxBound @Word) -) <$> genSmall) `suchThat` (>= 0)
shrinkSLimited
:: (SaneIntegral a, MkSLimited (Limit a), Arbitrary a)
=> SLimited a -> [SLimited a]
shrinkSLimited (SLimited p) = mapMaybe mkSLimited $ shrink $ natVal p
instance Arbitrary (SLimited Integer) where
arbitrary = oneof
[ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
, genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
, genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI
, genOverI, genUnderW, genOverW ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
instance Arbitrary (SLimited Natural) where
arbitrary = oneof
[ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
, genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
, genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI
, genOverI, genUnderW, genOverW ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
instance Arbitrary (SLimited Word) where
arbitrary = oneof
[ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
, genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
, genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI
, genOverI, genUnderW ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
instance Arbitrary (SLimited Int) where
arbitrary = oneof
[ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
, genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
, genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
instance Arbitrary (SLimited Word8) where
arbitrary = oneof
[ genSmall, genUnder7, genOver7, genUnder8 ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
instance Arbitrary (SLimited Int8) where
arbitrary = oneof
[ genSmall, genUnder7 ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
instance Arbitrary (SLimited Word16) where
arbitrary = oneof
[ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
, genOver15, genUnder16 ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
instance Arbitrary (SLimited Int16) where
arbitrary = oneof
[ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
instance Arbitrary (SLimited Word32) where
arbitrary = oneof
[ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
, genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
instance Arbitrary (SLimited Int32) where
arbitrary = oneof
[ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
, genOver15, genUnder16, genOver16, genUnder31 ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
instance Arbitrary (SLimited Word64) where
arbitrary = oneof
[ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
, genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
, genOver32, genUnder63, genOver63, genUnder64, genOverI, genUnderW
, genOverW ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
instance Arbitrary (SLimited Int64) where
arbitrary = oneof
[ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15
, genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32
, genOver32, genUnder63, genUnderI, genOverI, genUnderW, genOverW ]
`suchThatMap` mkSLimited
shrink = shrinkSLimited
newtype SmallLimited a = SmallLimited { getSmallLimited :: SLimited a }
instance (SaneIntegral a, MkSLimited (Limit a), Arbitrary (SLimited a))
=> Arbitrary (SmallLimited a) where
arbitrary = SmallLimited <$> genSmall `suchThatMap` mkSLimited
shrink = map SmallLimited . shrink . getSmallLimited
type Good a =
( Show a
, Read a
, NFData a
, Typeable a
, SaneIntegral a
, Arbitrary a
, Arbitrary (SLimited a)
, MkSLimited (Limit a)
, CoArbitrary a
)
data SType where
SType :: Good a => Proxy a -> SType
forType :: forall prop. Testable prop
=> (forall a. Good a => Proxy a -> prop)
-> Property
forType prop = forAllBlind gen $ \case
(name, SType p) -> counterexample @prop ("@" ++ name) $ prop p
where
gen = elements
[ ("Integer", SType @Integer Proxy)
, ("Natural", SType @Natural Proxy)
, ("Word", SType @Word Proxy)
, ("Int", SType @Int Proxy)
, ("Word8", SType @Word8 Proxy)
, ("Int8", SType @Int8 Proxy)
, ("Word16", SType @Word16 Proxy)
, ("Int16", SType @Int16 Proxy)
, ("Word32", SType @Word32 Proxy)
, ("Int32", SType @Int32 Proxy)
, ("Word64", SType @Word64 Proxy)
, ("Int64", SType @Int64 Proxy)
]
forLimit'
:: forall a. SaneIntegral a
=> Gen (SLimited a)
-> (SLimited a -> [SLimited a])
-> (forall n. (KnownIntegral a n, Limited a n)
=> (forall i. Num i => i) -> Proxy n -> Property)
-> Property
forLimit' gen shr prop = forAllShrinkBlind @Property gen shr $ \case
SLimited p -> counterexample ("@" ++ show (natVal p)) $
prop (fromInteger $ natVal p) p
forLimit
:: forall a. (SaneIntegral a, Arbitrary (SLimited a))
=> (forall n. (KnownIntegral a n, Limited a n)
=> (forall i. Num i => i) -> Proxy n -> Property)
-> Property
forLimit = forLimit' @a arbitrary shrink
forPositiveLimit
:: forall a. (SaneIntegral a, Arbitrary (SLimited a))
=> (forall n. (KnownIntegral a n, Limited a n)
=> (forall i. Num i => i) -> Proxy n -> Property)
-> Property
forPositiveLimit = forLimit' @a
(arbitrary `suchThat` isPositive)
(filter isPositive . shrink)
where
isPositive :: SLimited a -> Bool
isPositive (SLimited p) = natVal p > 0
forSmallLimit
:: forall a. (SaneIntegral a, Arbitrary (SmallLimited a))
=> (forall n. (KnownIntegral a n, Limited a n)
=> (forall i. Num i => i) -> Proxy n -> Property)
-> Property
forSmallLimit = forLimit' @a
(getSmallLimited <$> arbitrary)
(map getSmallLimited . shrink . SmallLimited)
unsafeWithKnownIntegral
:: forall n a. (SaneIntegral a, MkSLimited (Limit a), Typeable a)
=> Integer -> ((KnownNat n, Limited a n) => Property) -> Property
unsafeWithKnownIntegral n prop
| Just (SLimited (_ :: Proxy n')) <- mkSLimited @_ @a n
, Refl <- unsafeCoerce Refl :: n :~: n'
= prop
| otherwise = discard
newtype IneqCond (n :: Nat) (m :: Nat) = IneqCond ((n <= m) => Property)
unsafeWithInequality
:: forall (n :: Nat) (m :: Nat). ((n <= m) => Property) -> Property
unsafeWithInequality prop =
case unsafeCoerce (IneqCond @n @m $ property prop) :: IneqCond 0 1 of
IneqCond prop' -> prop'
prop_isvalid_under = forType $ \(_ :: Proxy a) ->
forLimit @a $ \_ (_ :: Proxy n) ->
property $ \x ->
x < 0 ==> not $ isValidFinite @n @a (Finite x)
prop_isvalid_over = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
property $ \x ->
not (x >= n) .||. not (isValidFinite @n @a (Finite x))
prop_valid_finite = forType $ \(_ :: Proxy a) ->
forLimit @a $ \_ (_ :: Proxy n) ->
property $ \x -> ioProperty $
evaluate (isValidFinite $ finite @n @a x)
`catch` \(_ :: ErrorCall) -> pure True
prop_getFinite_finite = forType $ \(_ :: Proxy a) ->
forLimit @a $ \_ (_ :: Proxy n) ->
property $ \x -> ioProperty $
evaluate (getFinite (finite @n @a x) == x)
`catch` \(_ :: ErrorCall) -> pure True
prop_finite_getFinite = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
finite (getFinite x) === x
prop_valid_maxBound = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
n > 0 ==> isValidFinite (maxBound @(Finite a n))
prop_maxBound_max = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
n > 0 ==> maxBound >= x
prop_valid_minBound = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
n > 0 ==> isValidFinite (minBound @(Finite a n))
prop_minBound_min = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
n > 0 ==> minBound <= x
prop_valid_toEnum = forType $ \(_ :: Proxy a) ->
forLimit @a $ \_ (_ :: Proxy n) ->
property $ \x -> ioProperty $
evaluate (isValidFinite $ toEnum @(Finite a n) x)
`catch` \(_ :: ErrorCall) -> pure True
prop_fromEnum_toEnum = forType $ \(_ :: Proxy a) ->
forLimit @a $ \_ (_ :: Proxy n) ->
property $ \x -> ioProperty $
evaluate (fromEnum (toEnum @(Finite a n) x) == x)
`catch` \(_ :: ErrorCall) -> pure True
prop_toEnum_fromEnum = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
n <= toInteger (maxBound @Int) ==> toEnum (fromEnum x) == x
prop_valid_enumFrom = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Big x :: Big a n) ->
all isValidFinite [x..]
prop_getFinite_enumFrom = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
property $ \(Big x :: Big a n) ->
map getFinite [x..]
=== takeWhile (isJust . packFinite @n @a) [getFinite x..]
prop_valid_enumFromTo = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Big x :: Big a n) (Big y) ->
all isValidFinite [x..y]
prop_valid_enumFromTo' = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Small x :: Small a n) (Small y) ->
all isValidFinite [x..y]
prop_getFinite_enumFromTo = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Big x :: Big a n) (Big y) ->
map getFinite [x..y] === [getFinite x..getFinite y]
prop_getFinite_enumFromTo' = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Small x :: Small a n) (Small y) ->
map getFinite [x..y] === [getFinite x..getFinite y]
prop_valid_enumFromThen = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Big x :: Big a n) (Big y) ->
x < y ==> all isValidFinite [x,y..]
prop_valid_enumFromThen' = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Small x :: Small a n) (Small y) ->
x > y ==> all isValidFinite [x,y..]
prop_getFinite_enumFromThen = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Big x :: Big a n) (Big y) ->
x < y ==> map getFinite [x,y..]
=== takeWhile (isJust . packFinite @n @a) [getFinite x,getFinite y..]
prop_getFinite_enumFromThen' = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Small x :: Small a n) (Small y) ->
x > y ==> map getFinite [x,y..]
=== takeWhile (isJust . packFinite @n @a) [getFinite x,getFinite y..]
prop_valid_enumFromThenTo = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Small x :: Small a n) (Small y) (Small z) ->
x /= y ==> all isValidFinite [x,y..z]
prop_getFinite_enumFromThenTo = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Small x :: Small a n) (Small y) (Small z) ->
x /= y ==> map getFinite [x,y..z] === [getFinite x,getFinite y..getFinite z]
prop_nonint_succ = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Big x :: Big a n) ->
case packFinite @n @a $ succ $ getFinite x of
Nothing -> discard
Just y -> y === succ x
prop_valid_read = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
forPositiveLimit @a $ \_ (_ :: Proxy m) ->
property $ \(Edgy x :: Edgy a n) -> ioProperty $
evaluate (isValidFinite $ read @(Finite a m) (show x))
`catch` \(_ :: ErrorCall) -> pure True
prop_read_show = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
read (show x) === x
prop_valid_plus = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
isValidFinite $ x + y
prop_getFinite_plus = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
(getFinite x + getFinite y - getFinite (x + y)) `mod` n === 0
prop_valid_minus = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
isValidFinite $ x - y
prop_getFinite_minus = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
(getFinite x + n - getFinite y - getFinite (x - y)) `mod` n === 0
prop_valid_times = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
isValidFinite $ x * y
prop_getFinite_times = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
(toInteger (getFinite x) * toInteger (getFinite y)
- toInteger (getFinite $ x * y)) `mod` n === 0
prop_valid_negate = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
isValidFinite $ -x
prop_getFinite_negate = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
(n - getFinite x - getFinite (-x)) `mod` n === 0
prop_valid_abs = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
isValidFinite $ abs x
prop_getFinite_abs = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
getFinite (abs x) === abs (getFinite x)
prop_valid_signum = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
isValidFinite $ signum x
prop_getFinite_signum = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
getFinite (signum x) === signum (getFinite x)
prop_valid_fromInteger = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \x -> ioProperty $
evaluate (isValidFinite $ fromInteger @(Finite a n) x)
`catch` \(_ :: ErrorCall) -> pure True
prop_toInteger_fromInteger = forType $ \(_ :: Proxy a) ->
forLimit @a $ \_ (_ :: Proxy n) ->
property $ \x -> ioProperty $
evaluate (toInteger (fromInteger @(Finite a n) x) == x)
`catch` \(_ :: ErrorCall) -> pure True
prop_fromInteger_toInteger = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
fromInteger (toInteger x) === x
prop_valid_quot = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
y /= 0 ==> isValidFinite $ x `quot` y
prop_getFinite_quot = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
y /= 0 ==> getFinite (x `quot` y) === getFinite x `quot` getFinite y
prop_valid_rem = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
y /= 0 ==> isValidFinite $ x `rem` y
prop_getFinite_rem = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
y /= 0 ==> getFinite (x `rem` y) === getFinite x `rem` getFinite y
prop_valid_div = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
y /= 0 ==> isValidFinite $ x `div` y
prop_getFinite_div = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
y /= 0 ==> getFinite (x `div` y) === getFinite x `div` getFinite y
prop_valid_mod = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
y /= 0 ==> isValidFinite $ x `mod` y
prop_getFinite_mod = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) (Edgy y) ->
y /= 0 ==> getFinite (x `mod` y) === getFinite x `mod` getFinite y
prop_force = forType $ \(_ :: Proxy a) ->
forLimit @a $ \_ (_ :: Proxy n) ->
ioProperty $
evaluate (rnf @(Finite a n) (error "Expected exception") `seq` False)
`catch` (\(_ :: ErrorCall) -> pure True)
prop_valid_packFinite = forType $ \(_ :: Proxy a) ->
forLimit @a $ \_ (_ :: Proxy n) ->
property $ \x ->
maybe True isValidFinite $ packFinite @n @a x
prop_getFinite_packFinite = forType $ \(_ :: Proxy a) ->
forLimit @a $ \_ (_ :: Proxy n) ->
property $ \x ->
maybe (property True) ((x ===) . getFinite) $ packFinite @n @a x
prop_finite_packFinite = forType $ \(_ :: Proxy a) ->
forLimit @a $ \_ (_ :: Proxy n) ->
property $ \x -> ioProperty $
case packFinite @n @a x of
Nothing -> (evaluate (finite @n @a x) >> pure False)
`catch` \(_ :: ErrorCall) -> pure True
Just y -> evaluate (y == finite x)
prop_valid_finites = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \_ (_ :: Proxy n) ->
property $
all isValidFinite $ finites @n @a
prop_finites_minMax = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
n > 0 ==> minBound `elem` finites @n @a .&&. maxBound `elem` finites @n @a
prop_finites_ordered = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \_ (_ :: Proxy n) ->
finites @n @a === sort finites
prop_finites_all = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \_ (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
x -- could be discard
`seq` x `elem` finites @n @a
prop_valid_modulo = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
property $ \x ->
isValidFinite $ modulo @n @a x
prop_getFinite_modulo = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
property $ \x ->
(toInteger x - toInteger (getFinite $ modulo @n @a x)) `mod` n === 0
prop_getFinite_equals = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
forPositiveLimit @a $ \_ (_ :: Proxy m) ->
property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
(x `equals` y) === (getFinite x == getFinite y)
prop_getFinite_cmp = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
forPositiveLimit @a $ \_ (_ :: Proxy m) ->
property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
(x `cmp` y) === (getFinite x `compare` getFinite y)
prop_valid_natToFinite = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forPositiveLimit @a $ \m (_ :: Proxy m) ->
n + 1 <= m ==> unsafeWithInequality @(n + 1) @m $
property $
isValidFinite $ natToFinite @n @m @a Proxy
prop_getFinite_natToFinite = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forPositiveLimit @a $ \m (_ :: Proxy m) ->
n + 1 <= m ==> unsafeWithInequality @(n + 1) @m $
getFinite (natToFinite @n @m @a Proxy) === n
prop_valid_weaken = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
property $ \(Edgy x :: Edgy a n) ->
isValidFinite $ weaken x
prop_finites_weaken = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
map (weaken @n @a) finites === init finites
prop_valid_strengthen = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
property $ \(Edgy x :: Edgy a (n + 1)) ->
maybe True isValidFinite $ strengthen x
prop_finites_strengthen = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
map (strengthen @n @a) finites === map Just finites ++ [Nothing]
prop_valid_shift = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
property $ \(Edgy x :: Edgy a n) ->
isValidFinite $ shift x
prop_finites_shift = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
map (shift @n @a) finites === drop 1 finites
prop_valid_unshift = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
property $ \(Edgy x :: Edgy a (n + 1)) ->
maybe True isValidFinite $ unshift x
prop_finites_unshift = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
map (unshift @n @a) finites === [Nothing] ++ map Just finites
prop_valid_weakenN = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forPositiveLimit @a $ \m (_ :: Proxy m) ->
n <= m ==> unsafeWithInequality @n @m $
property $ \(Edgy x :: Edgy a n) ->
isValidFinite $ weakenN @n @m @a x
prop_finites_weakenN = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
n <= m ==> unsafeWithInequality @n @m $
map (weakenN @n @m @a) finites === take n finites
prop_valid_strengthenN = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
forLimit @a $ \_ (_ :: Proxy m) ->
property $ \(Edgy x :: Edgy a n) ->
maybe True isValidFinite $ strengthenN @n @m x
prop_finites_strengthenN = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
map (strengthenN @n @m @a) finites
=== take n (map Just finites) ++ replicate (n - m) Nothing
prop_valid_shiftN = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forPositiveLimit @a $ \m (_ :: Proxy m) ->
n <= m ==> unsafeWithInequality @n @m $
property $ \(Edgy x :: Edgy a n) ->
isValidFinite $ shiftN @n @m @a x
prop_finites_shiftN = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
n <= m ==> unsafeWithInequality @n @m $
map (shiftN @n @m @a) finites === drop (m - n) finites
prop_valid_unshiftN = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
forLimit @a $ \_ (_ :: Proxy m) ->
property $ \(Edgy x :: Edgy a n) ->
maybe True isValidFinite $ unshiftN @n @m x
prop_finites_unshiftN = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
map (unshiftN @n @m @a) finites
=== replicate (n - m) Nothing ++ drop (m - n) (map Just finites)
prop_valid_weakenProxy = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \k (_ :: Proxy k) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
property $ \(Edgy x :: Edgy a n) ->
isValidFinite $ weakenProxy @n @k Proxy x
prop_finites_weakenProxy = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \k (_ :: Proxy k) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
map (weakenProxy @n @k @a Proxy) finites === take n finites
prop_valid_strengthenProxy = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \k (_ :: Proxy k) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
property $ \(Edgy x :: Edgy a (n + k)) ->
maybe True isValidFinite $ strengthenProxy @n @k Proxy x
prop_finites_strengthenProxy = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \k (_ :: Proxy k) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
map (strengthenProxy @n @k @a Proxy) finites
=== take n (map Just finites) ++ replicate k Nothing
prop_valid_shiftProxy = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \k (_ :: Proxy k) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
property $ \(Edgy x :: Edgy a n) ->
isValidFinite $ shiftProxy @n @k Proxy x
prop_finites_shiftProxy = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \k (_ :: Proxy k) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
map (shiftProxy @n @k @a Proxy) finites === drop k finites
prop_valid_unshiftProxy = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \k (_ :: Proxy k) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
property $ \(Edgy x :: Edgy a (n + k)) ->
maybe True isValidFinite $ unshiftProxy @n @k Proxy x
prop_finites_unshiftProxy = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \k (_ :: Proxy k) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
map (unshiftProxy @n @k @a Proxy) finites
=== replicate k Nothing ++ map Just finites
prop_strengthen_weaken = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
strengthen (weaken x) === Just x
prop_weaken_strengthen = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
property $ \(Edgy x :: Edgy a (n + 1)) ->
maybe True (== x) (weaken <$> strengthen x)
prop_unshift_shift = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
property $ \(Edgy x :: Edgy a n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
unshift (shift x) === Just x
prop_shift_unshift = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @(n + 1) @a (n + 1) $
property $ \(Edgy x :: Edgy a (n + 1)) ->
maybe True (== x) (shift <$> unshift x)
prop_strengthenN_weakenN = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forPositiveLimit @a $ \m (_ :: Proxy m) ->
n <= m ==> unsafeWithInequality @n @m $
property $ \(Edgy x :: Edgy a n) ->
strengthenN (weakenN @n @m x) === Just x
prop_weakenN_strengthenN = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \m (_ :: Proxy m) ->
m <= n ==> unsafeWithInequality @m @n $
property $ \(Edgy x :: Edgy a n) ->
maybe True (== x) (weakenN <$> strengthenN @n @m x)
prop_unshiftN_shiftN = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forPositiveLimit @a $ \m (_ :: Proxy m) ->
n <= m ==> unsafeWithInequality @n @m $
property $ \(Edgy x :: Edgy a n) ->
unshiftN (shiftN @n @m x) === Just x
prop_shiftN_unshiftN = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \m (_ :: Proxy m) ->
m <= n ==> unsafeWithInequality @m @n $
property $ \(Edgy x :: Edgy a n) ->
maybe True (== x) (shiftN <$> unshiftN @n @m x)
prop_strengthenProxy_weakenProxy = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \k (_ :: Proxy k) ->
property $ \(Edgy x :: Edgy a n) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
strengthenProxy Proxy (weakenProxy @n @k Proxy x) === Just x
prop_weakenProxy_strengthenProxy = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \k (_ :: Proxy k) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
property $ \(Edgy x :: Edgy a (n + k)) ->
maybe True (== x) (weakenProxy Proxy <$> strengthenProxy @n @k Proxy x)
prop_unshiftProxy_shiftProxy = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \k (_ :: Proxy k) ->
property $ \(Edgy x :: Edgy a n) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
unshiftProxy Proxy (shiftProxy @n @k Proxy x) === Just x
prop_shiftProxy_unshiftProxy = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \k (_ :: Proxy k) ->
unsafeWithKnownIntegral @(n + k) @a (n + k) $
property $ \(Edgy x :: Edgy a (n + k)) ->
maybe True (== x) (shiftProxy Proxy <$> unshiftProxy @n @k Proxy x)
prop_valid_add = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forPositiveLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n + m) @a (n + m) $
property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
isValidFinite $ add x y
prop_getFinite_add = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forPositiveLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n + m) @a (n + m) $
property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
getFinite (add x y) === getFinite x + getFinite y
prop_valid_sub = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
forPositiveLimit @a $ \_ (_ :: Proxy m) ->
property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
either isValidFinite isValidFinite $ sub x y
prop_getFinite_sub = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
forPositiveLimit @a $ \_ (_ :: Proxy m) ->
property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
either (negate . toInteger . getFinite) (toInteger . getFinite) (sub x y)
=== toInteger (getFinite x) - toInteger (getFinite y)
prop_sub_Left_0 = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \_ (_ :: Proxy n) ->
forPositiveLimit @a $ \_ (_ :: Proxy m) ->
property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
sub x y =/= Left 0
prop_valid_multiply = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forPositiveLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
isValidFinite $ multiply x y
prop_getFinite_multiply = forType $ \(_ :: Proxy a) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
forPositiveLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) ->
getFinite (multiply x y) === getFinite x * getFinite y
prop_valid_combineSum = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n + m) @a (n + m) $
property $ \e ->
isValidFinite $ combineSum
$ bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) e
prop_finites_combineSum = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n + m) @a (n + m) $
map (combineSum @n @m @a) (map Left finites ++ map Right finites)
=== finites
prop_valid_combineZero = forType $ \(_ :: Proxy a) ->
unsafeWithKnownIntegral @0 @a 0 $
ioProperty $ evaluate (isValidFinite $ combineZero @a $ error "test")
`catch` \(ErrorCall msg) -> pure (msg == "test")
prop_finites_combineZero = forType $ \(_ :: Proxy a) ->
unsafeWithKnownIntegral @0 @a 0 $
map (combineZero @a) [] === finites
prop_valid_combineProduct = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
property $ \p ->
isValidFinite $ combineProduct
$ bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) p
prop_finites_combineProduct = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
map (combineProduct @n @m @a) [(x, y) | y <- finites, x <- finites]
=== finites
prop_valid_combineOne = forType $ \(_ :: Proxy a) ->
unsafeWithKnownIntegral @1 @a 1 $
property $ isValidFinite $ combineOne @a ()
prop_finites_combineOne = forType $ \(_ :: Proxy a) ->
unsafeWithKnownIntegral @1 @a 1 $
property $ [combineOne @a ()] === finites
prop_valid_combineExponential = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
property $ \(Blind (f :: Big a n -> Big a m)) ->
isValidFinite $ combineExponential (\x -> case f (Big x) of Big y -> y)
prop_finites_combineExponential = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
if m ^ n > 2000000 then property () else
m ^ n <= 10000 ==>
unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
property $
[ combineExponential ((xs !!) . fromIntegral . getFinite @n @a)
| xs <- reverse <$> replicateM n (finites @m)
] === finites
prop_valid_separateSum = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n + m) @a (n + m) $
property $ \(Edgy x :: Edgy a (n + m)) ->
either isValidFinite isValidFinite $ separateSum @n @m x
prop_finites_separateSum = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n + m) @a (n + m) $
map (separateSum @n @m @a) finites === map Left finites ++ map Right finites
prop_seq_separateZero = forType $ \(_ :: Proxy a) ->
unsafeWithKnownIntegral @0 @a 0 $
ioProperty $ evaluate (absurd $ separateZero @a $ error "test")
`catch` \(ErrorCall msg) -> pure (msg == "test")
prop_finites_separateZero = forType $ \(_ :: Proxy a) ->
unsafeWithKnownIntegral @0 @a 0 $
map (separateZero @a) finites === []
prop_valid_separateProduct = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
property $ \(Edgy x :: Edgy a (n GHC.TypeLits.* m)) ->
x -- could be discard
`seq` isValidFinite (fst $ separateProduct @n @m x)
.&&. isValidFinite (snd $ separateProduct @n @m x)
prop_finites_separateProduct = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
map (separateProduct @n @m @a) finites
=== [(x, y) | y <- finites, x <- finites]
prop_finites_separateOne = forType $ \(_ :: Proxy a) ->
unsafeWithKnownIntegral @1 @a 1 $
map (separateOne @a) finites === [()]
prop_valid_separateExponential = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
property $ \(Big f :: Big a (m ^ n)) (Big x :: Big a n) ->
f `seq` x -- could be discard
`seq` isValidFinite (separateExponential @n @m @a f x)
prop_finites_separateExponential = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
if m ^ n > 2000000 then property () else
m ^ n <= 10000 ==>
unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
map (<$> finites) (map (separateExponential @n @m @a) finites)
=== [reverse xs | xs <- replicateM n finites]
prop_combineSum_separateSum = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n + m) @a (n + m) $
property $ \(Edgy x :: Edgy a (n + m)) ->
combineSum (separateSum @n @m x) === x
prop_separateSum_combineSum = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n + m) @a (n + m) $
property $ \e ->
let x = bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) e in
separateSum (combineSum x) === x
prop_combineProduct_separateProduct = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
property $ \(Edgy x :: Edgy a (n GHC.TypeLits.* m)) ->
x -- could be discard
`seq` combineProduct (separateProduct @n @m x) === x
prop_separateProduct_combineProduct = forType $ \(_ :: Proxy a) ->
forLimit @a $ \n (_ :: Proxy n) ->
forLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $
property $ \p ->
let x = bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) p in
force x -- could be discard
`seq` separateProduct (combineProduct x) === x
prop_combineOne_separateOne = forType $ \(_ :: Proxy a) ->
unsafeWithKnownIntegral @1 @a 1 $
property $ \(Big x :: Big a 1) ->
combineOne (separateOne @a x) === x
prop_separateOne_combineOne = forType $ \(_ :: Proxy a) ->
unsafeWithKnownIntegral @1 @a 1 $
property $ \x ->
separateOne (combineOne @a x) === x
prop_separateExponential_combineExponential = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
property $ \(Blind (f :: Big a n -> Big a m)) ->
let f' x = case f (Big x) of Big y -> y in
force (f' <$> listToMaybe finites) -- could be discard
`seq` (separateExponential @n @m @a (combineExponential f') <$> finites)
=== (f' <$> finites)
prop_combineExponential_separateExponential = forType $ \(_ :: Proxy a) ->
forSmallLimit @a $ \n (_ :: Proxy n) ->
forSmallLimit @a $ \m (_ :: Proxy m) ->
unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $
property $ \(Big f :: Big a (m ^ n)) ->
f `seq` -- could be discard
combineExponential (separateExponential @n @m @a f) === f
prop_valid_castFinite = forType $ \(_ :: Proxy b) ->
forType $ \(_ :: Proxy a) ->
forPositiveLimit @b $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @n @a n $
property $ \(Edgy x :: Edgy a n) ->
isValidFinite $ castFinite @b x
prop_sym_castFinite = forType $ \(_ :: Proxy a) ->
forType $ \(_ :: Proxy b) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @n @b n $
property $ \(Edgy x :: Edgy b n) ->
castFinite @b (castFinite @a x) === x
prop_trans_castFinite = forType $ \(_ :: Proxy a) ->
forType $ \(_ :: Proxy b) ->
forType $ \(_ :: Proxy c) ->
forPositiveLimit @a $ \n (_ :: Proxy n) ->
unsafeWithKnownIntegral @n @b n $
unsafeWithKnownIntegral @n @c n $
property $ \(Edgy x :: Edgy a n) ->
castFinite @c (castFinite @b x) === castFinite @c x
return []
main = $quickCheckAll >>= \case
True -> pure ()
False -> exitFailure