finite-typelits 0.1.4.2 → 0.1.5.0
raw patch · 4 files changed
+616/−29 lines, 4 filesdep +QuickCheckdep +finite-typelitsdep ~basePVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies added: QuickCheck, finite-typelits
Dependency ranges changed: base
API changes (from Hackage documentation)
- Data.Finite: natToFinite :: (KnownNat n, KnownNat m, n + 1 <= m) => proxy n -> Finite m
+ Data.Finite: natToFinite :: (KnownNat n, KnownNat m, (n + 1) <= m) => proxy n -> Finite m
- Data.Finite: weakenN :: (n <= m) => Finite n -> Finite m
+ Data.Finite: weakenN :: n <= m => Finite n -> Finite m
- Data.Finite.Internal: Finite :: Integer -> Finite
+ Data.Finite.Internal: Finite :: Integer -> Finite (n :: Nat)
Files
- finite-typelits.cabal +15/−4
- src/Data/Finite.hs +26/−12
- src/Data/Finite/Internal.hs +27/−13
- test/Main.hs +548/−0
finite-typelits.cabal view
@@ -1,6 +1,6 @@ name: finite-typelits-version: 0.1.4.2-synopsis: A type inhabited by finitely many values, indexed by type-level naturals.+version: 0.1.5.0+synopsis: A type inhabited by finitely many values, indexed by type-level naturals description: A type inhabited by finitely many values, indexed by type-level naturals. homepage: https://github.com/mniip/finite-typelits license: BSD3@@ -12,8 +12,19 @@ cabal-version: >=1.10 library- exposed-modules: Data.Finite, Data.Finite.Internal- build-depends: base == 4.*+ exposed-modules: Data.Finite+ , Data.Finite.Internal+ build-depends: base >= 4.7 && <= 4.17 , deepseq >= 1.4 hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -Wall++test-Suite finite-typelits-tests+ type: exitcode-stdio-1.0+ main-is: test/Main.hs+ build-depends: finite-typelits+ , base >= 4.9 && <= 4.17+ , deepseq >= 1.4+ , QuickCheck default-language: Haskell2010
src/Data/Finite.hs view
@@ -1,13 +1,16 @@ -------------------------------------------------------------------------------- -- | -- Module : Data.Finite--- Copyright : (C) 2015 mniip+-- Copyright : (C) 2015-2022 mniip -- License : BSD3 -- Maintainer : mniip <mniip@mniip.com> -- Stability : experimental -- Portability : portable ---------------------------------------------------------------------------------{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies, FlexibleContexts #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} module Data.Finite ( Finite,@@ -32,7 +35,8 @@ import Data.Finite.Internal --- | Convert an 'Integer' into a 'Finite', returning 'Nothing' if the input is out of bounds.+-- | Convert an 'Integer' into a 'Finite', returning 'Nothing' if the input is+-- out of bounds. packFinite :: KnownNat n => Integer -> Maybe (Finite n) packFinite x = result where@@ -87,7 +91,8 @@ weaken :: Finite n -> Finite (n + 1) weaken (Finite x) = Finite x --- | Remove one inhabitant from the end. Returns 'Nothing' if the input was the removed inhabitant.+-- | Remove one inhabitant from the end. Returns 'Nothing' if the input was the+-- removed inhabitant. strengthen :: KnownNat n => Finite (n + 1) -> Maybe (Finite n) strengthen (Finite x) = result where@@ -99,7 +104,8 @@ shift :: Finite n -> Finite (n + 1) shift (Finite x) = Finite (x + 1) --- | Remove one inhabitant from the beginning, shifting everything down by one. Returns 'Nothing' if the input was the removed inhabitant.+-- | Remove one inhabitant from the beginning, shifting everything down by one.+-- Returns 'Nothing' if the input was the removed inhabitant. unshift :: Finite (n + 1) -> Maybe (Finite n) unshift (Finite x) = if x < 1 then Nothing@@ -109,7 +115,8 @@ weakenN :: (n <= m) => Finite n -> Finite m weakenN (Finite x) = Finite x --- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input was one of the removed inhabitants.+-- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input+-- was one of the removed inhabitants. strengthenN :: (KnownNat n, n <= m) => Finite m -> Maybe (Finite n) strengthenN (Finite x) = result where@@ -117,13 +124,16 @@ then Just $ Finite x else Nothing --- | Add multiple inhabitant in the beginning, shifting everything up by the amount of inhabitants added.+-- | Add multiple inhabitant in the beginning, shifting everything up by the+-- amount of inhabitants added. shiftN :: (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m shiftN fx@(Finite x) = result where result = Finite $ x + natVal result - natVal fx --- | Remove multiple inhabitants from the beginning, shifting everything down by the amount of inhabitants removed. Returns 'Nothing' if the input was one of the removed inhabitants.+-- | Remove multiple inhabitants from the beginning, shifting everything down by+-- the amount of inhabitants removed. Returns 'Nothing' if the input was one of+-- the removed inhabitants. unshiftN :: (KnownNat n, KnownNat m, n <= m) => Finite m -> Maybe (Finite n) unshiftN fx@(Finite x) = result where@@ -135,7 +145,7 @@ weakenProxy _ (Finite x) = Finite x strengthenProxy :: KnownNat n => proxy k -> Finite (n + k) -> Maybe (Finite n)-strengthenProxy p (Finite x) = result+strengthenProxy _ (Finite x) = result where result = if x < natVal (fromJust result) then Just $ Finite x@@ -153,7 +163,8 @@ add :: Finite n -> Finite m -> Finite (n + m) add (Finite x) (Finite y) = Finite $ x + y --- | Subtract two 'Finite's. Returns 'Left' for negative results, and 'Right' for positive results. Note that this function never returns @'Left' 0@.+-- | Subtract two 'Finite's. Returns 'Left' for negative results, and 'Right'+-- for positive results. Note that this function never returns @'Left' 0@. sub :: Finite n -> Finite m -> Either (Finite m) (Finite n) sub (Finite x) (Finite y) = if x >= y then Right $ Finite $ x - y@@ -171,7 +182,8 @@ combineSum (Left (Finite x)) = Finite x combineSum efx@(Right (Finite x)) = Finite $ x + natVal (getLeftType efx) --- | 'fst'-biased (fst is the inner, and snd is the outer iteratee) product of finite sets.+-- | 'fst'-biased (fst is the inner, and snd is the outer iteratee) product of+-- finite sets. combineProduct :: KnownNat n => (Finite n, Finite m) -> Finite (n GHC.TypeLits.* m) combineProduct (fx@(Finite x), Finite y) = Finite $ x + y * natVal fx @@ -189,6 +201,8 @@ where result = (Finite $ x `mod` natVal (fst result), Finite $ x `div` natVal (fst result)) --- | Verifies that a given 'Finite' is valid. Should always return 'True' unles you bring the @Data.Finite.Internal.Finite@ constructor into the scope, or use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks+-- | Verifies that a given 'Finite' is valid. Should always return 'True' unless+-- you bring the @Data.Finite.Internal.Finite@ constructor into the scope, or+-- use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks. isValidFinite :: KnownNat n => Finite n -> Bool isValidFinite fx@(Finite x) = x < natVal fx && x >= 0
src/Data/Finite/Internal.hs view
@@ -1,13 +1,15 @@ -------------------------------------------------------------------------------- -- | -- Module : Data.Finite.Internal--- Copyright : (C) 2015 mniip+-- Copyright : (C) 2015-2022 mniip -- License : BSD3 -- Maintainer : mniip <mniip@mniip.com> -- Stability : experimental -- Portability : portable ---------------------------------------------------------------------------------{-# LANGUAGE KindSignatures, DataKinds, DeriveGeneric #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE KindSignatures #-} module Data.Finite.Internal ( Finite(Finite),@@ -16,23 +18,25 @@ ) where -import GHC.Read-import GHC.TypeLits-import GHC.Generics import Control.DeepSeq import Control.Monad import Data.Ratio-import Text.Read.Lex+import GHC.Generics+import GHC.Read+import GHC.TypeLits import Text.ParserCombinators.ReadPrec+import Text.Read.Lex --- | Finite number type. @'Finite' n@ is inhabited by exactly @n@ values. Invariants:+-- | Finite number type. @'Finite' n@ is inhabited by exactly @n@ values+-- the range @[0, n)@ including @0@ but excluding @n@. Invariants: -- -- prop> getFinite x < natVal x -- prop> getFinite x >= 0 newtype Finite (n :: Nat) = Finite Integer deriving (Eq, Ord, Generic) --- | Convert an 'Integer' into a 'Finite', throwing an error if the input is out of bounds.+-- | Convert an 'Integer' into a 'Finite', throwing an error if the input is out+-- of bounds. finite :: KnownNat n => Integer -> Finite n finite x = result where@@ -58,29 +62,38 @@ else error "minBound: Finite 0 is uninhabited" instance KnownNat n => Enum (Finite n) where+ succ fx@(Finite x) = if x == natVal fx - 1+ then error "succ: bad argument"+ else Finite $ succ x+ pred (Finite x) = if x == 0+ then error "pred: bad argument"+ else Finite $ pred x fromEnum = fromEnum . getFinite toEnum = finite . toEnum enumFrom x = enumFromTo x maxBound+ enumFromTo (Finite x) (Finite y) = Finite `fmap` enumFromTo x y enumFromThen x y = enumFromThenTo x y (if x >= y then minBound else maxBound)+ enumFromThenTo (Finite x) (Finite y) (Finite z) = Finite `fmap` enumFromThenTo x y z instance Show (Finite n) where showsPrec d (Finite x) = showParen (d > 9) $ showString "finite " . showsPrec 10 x instance KnownNat n => Read (Finite n) where- readPrec = parens $ Text.ParserCombinators.ReadPrec.prec 10 $ do + readPrec = parens $ Text.ParserCombinators.ReadPrec.prec 10 $ do expectP (Ident "finite") x <- readPrec let result = finite x- guard (x >= 0 && x < natVal result) + guard (x >= 0 && x < natVal result) return result --- | Modular arithmetic. Only the 'fromInteger' function is supposed to be useful.+-- | 'Prelude.+', 'Prelude.-', and 'Prelude.*' implement arithmetic modulo @n@.+-- The 'fromInteger' function raises an error for inputs outside of bounds. instance KnownNat n => Num (Finite n) where fx@(Finite x) + Finite y = Finite $ (x + y) `mod` natVal fx fx@(Finite x) - Finite y = Finite $ (x - y) `mod` natVal fx fx@(Finite x) * Finite y = Finite $ (x * y) `mod` natVal fx abs fx = fx- signum _ = fromInteger 1+ signum (Finite x) = fromInteger $ if x == 0 then 0 else 1 fromInteger x = result where result = if x < natVal result && x >= 0@@ -90,7 +103,8 @@ instance KnownNat n => Real (Finite n) where toRational (Finite x) = x % 1 --- | __Not__ modular arithmetic.+-- | 'quot' and 'rem' are the same as 'div' and 'mod' and they implement regular+-- division of numbers in the range @[0, n)@, __not__ modular arithmetic. instance KnownNat n => Integral (Finite n) where quotRem (Finite x) (Finite y) = (Finite $ x `quot` y, Finite $ x `rem` y) toInteger (Finite x) = x
+ test/Main.hs view
@@ -0,0 +1,548 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+module Main where++import Control.Exception+import Control.DeepSeq+import Data.List+import Data.Maybe+import Data.Proxy+import Data.Type.Equality+import GHC.TypeLits+import System.Exit+import Test.QuickCheck+import Unsafe.Coerce++import Data.Finite+import Data.Finite.Internal++instance KnownNat n => Arbitrary (Finite n) where+ arbitrary+ | natVal @n Proxy == 0 = discard+ | otherwise = oneof+ [ pure (Finite 0)+ , pure (Finite $ natVal @n Proxy - 1)+ , Finite . (`mod` natVal @n Proxy) <$> arbitrary+ ]+ shrink (Finite x) = mapMaybe packFinite $ shrink x++withNat' :: forall prop. Testable prop => Gen Integer -> (Integer -> [Integer]) -> (forall n. KnownNat n => (forall i. Num i => i) -> Proxy n -> prop) -> Property+withNat' gen shr prop = forAllShrinkBlind gen shr $ \n -> case someNatVal n of+ Nothing -> counterexample "withNat" False+ Just (SomeNat p) -> counterexample ("@" ++ show n) $ prop (fromInteger (natVal p)) p++withNat :: forall prop. Testable prop => (forall n. KnownNat n => (forall i. Num i => i) -> Proxy n -> prop) -> Property+withNat = withNat' (getNonNegative <$> arbitrary) (map getNonNegative . shrink . NonNegative)++withNatPos :: forall prop. Testable prop => (forall n. KnownNat n => (forall i. Num i => i) -> Proxy n -> prop) -> Property+withNatPos = withNat' (getPositive <$> arbitrary) (map getPositive . shrink . Positive)++unsafeWithKnownNat :: forall n prop. Testable prop => Integer -> (KnownNat n => prop) -> Property+unsafeWithKnownNat n prop = case someNatVal n of+ Nothing -> counterexample "unsafeWithKnownNat: someNatVal" False+ Just (SomeNat (_ :: Proxy n')) -> case unsafeCoerce Refl :: n :~: n' of+ Refl -> property prop++newtype IneqCond (n :: Nat) (m :: Nat) = IneqCond ((n <= m) => Property)+unsafeWithInequality :: forall (n :: Nat) (m :: Nat) prop. Testable prop => ((n <= m) => prop) -> Property+unsafeWithInequality prop =+ case unsafeCoerce (IneqCond @n @m $ property prop) :: IneqCond 0 1 of+ IneqCond prop' -> prop'++prop_isvalid_under = withNat $ \_ (_ :: Proxy n) x ->+ x < 0 ==> expectFailure $ isValidFinite @n (Finite x)+prop_isvalid_over = withNat $ \n (_ :: Proxy n) x ->+ x >= n ==> expectFailure $ isValidFinite @n (Finite x)++prop_valid_finite = withNat $ \_ (_ :: Proxy n) x -> ioProperty $+ evaluate (isValidFinite $ finite @n x)+ `catch` \(_ :: ErrorCall) -> pure True+prop_getFinite_finite = withNat $ \_ (_ :: Proxy n) x -> ioProperty $+ evaluate (getFinite (finite @n x) == x)+ `catch` \(_ :: ErrorCall) -> pure True+prop_finite_getFinite = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x ->+ finite (getFinite @n x) === x++prop_valid_maxBound = withNat $ \n (_ :: Proxy n) ->+ n > 0 ==> isValidFinite (maxBound @(Finite n))+prop_maxBound_max = withNat $ \n (_ :: Proxy n) ->+ property $ \x ->+ n > 0 ==> maxBound @(Finite n) >= x++prop_valid_minBound = withNat $ \n (_ :: Proxy n) ->+ n > 0 ==> isValidFinite (minBound @(Finite n))+prop_minBound_min = withNat $ \n (_ :: Proxy n) ->+ property $ \x ->+ n > 0 ==> minBound @(Finite n) <= x++prop_valid_toEnum = withNat $ \_ (_ :: Proxy n) x -> ioProperty $+ evaluate (isValidFinite $ toEnum @(Finite n) x)+ `catch` \(_ :: ErrorCall) -> pure True+prop_fromEnum_toEnum = withNat $ \_ (_ :: Proxy n) x -> ioProperty $+ evaluate (fromEnum (toEnum @(Finite n) x) == x)+ `catch` \(_ :: ErrorCall) -> pure True+prop_toEnum_fromEnum = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x ->+ toEnum @(Finite n) (fromEnum x) == x++prop_valid_enumFrom = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x ->+ all isValidFinite $ enumFrom @(Finite n) x+prop_getFinite_enumFrom = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x ->+ map getFinite (enumFrom @(Finite n) x)+ === takeWhile (isJust . packFinite @n) (enumFrom (getFinite x))++prop_valid_enumFromTo = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ all isValidFinite $ enumFromTo @(Finite n) x y+prop_getFinite_enumFromTo = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ map getFinite (enumFromTo @(Finite n) x y)+ === enumFromTo (getFinite x) (getFinite y)++prop_valid_enumFromThen = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ x /= y ==> all isValidFinite $ enumFromThen @(Finite n) x y+prop_getFinite_enumFromThen = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ x /= y ==> map getFinite (enumFromThen @(Finite n) x y)+ === takeWhile (isJust . packFinite @n) (enumFromThen (getFinite x) (getFinite y))++prop_valid_enumFromThenTo = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y z ->+ x /= y ==> all isValidFinite $ enumFromThenTo @(Finite n) x y z+prop_getFinite_enumFromThenTo = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y z ->+ x /= y ==> map getFinite (enumFromThenTo @(Finite n) x y z)+ === enumFromThenTo (getFinite x) (getFinite y) (getFinite z)++prop_nonint_succ = withNat' genBig shrinkBig $ \_ (_ :: Proxy n) ->+ forAllShrink genBig shrinkBig $ \x ->+ case packFinite @n $ succ x of+ Nothing -> discard+ Just y -> y === succ (finite x)+ where+ big = toInteger (maxBound :: Int)+ genBig = (big +) . getNonNegative <$> arbitrary+ shrinkBig = map ((big +) . getNonNegative) . shrink . NonNegative . subtract big++prop_valid_read = withNatPos $ \_ (_ :: Proxy n) ->+ withNatPos $ \_ (_ :: Proxy m) ->+ property $ \x -> ioProperty $+ evaluate (isValidFinite $ read @(Finite n) (show @(Finite m) x))+ `catch` \(_ :: ErrorCall) -> pure True+prop_read_show = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x ->+ read (show @(Finite n) x) === x++prop_valid_plus = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ isValidFinite @n $ x + y+prop_getFinite_plus = withNatPos $ \n (_ :: Proxy n) ->+ property $ \x y ->+ (getFinite @n (x + y) - (getFinite x + getFinite y)) `mod` n === 0++prop_valid_minus = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ isValidFinite @n $ x - y+prop_getFinite_minus = withNatPos $ \n (_ :: Proxy n) ->+ property $ \x y ->+ (getFinite @n (x - y) - (getFinite x - getFinite y)) `mod` n === 0++prop_valid_times = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ isValidFinite @n $ x * y+prop_getFinite_times = withNatPos $ \n (_ :: Proxy n) ->+ property $ \x y ->+ (getFinite @n (x * y) - (getFinite x * getFinite y)) `mod` n === 0++prop_valid_negate = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x ->+ isValidFinite @n $ -x+prop_getFinite_negate = withNatPos $ \n (_ :: Proxy n) ->+ property $ \x ->+ (getFinite @n (-x) - (- getFinite x)) `mod` n === 0++prop_valid_abs = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x ->+ isValidFinite @n $ abs x+prop_getFinite_abs = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x ->+ getFinite @n (abs x) === abs (getFinite x)++prop_valid_signum = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x -> ioProperty $+ evaluate (isValidFinite @n $ signum x)+ `catch` \(_ :: ErrorCall) -> pure True++prop_getFinite_signum = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x -> ioProperty $+ evaluate (getFinite @n (signum x) == signum (getFinite x))+ `catch` \(_ :: ErrorCall) -> pure True++prop_valid_fromInteger = withNatPos $ \_ (_ :: Proxy n) x -> ioProperty $+ evaluate (isValidFinite $ fromInteger @(Finite n) x)+ `catch` \(_ :: ErrorCall) -> pure True+prop_toInteger_fromInteger = withNat $ \_ (_ :: Proxy n) x -> ioProperty $+ evaluate (toInteger (fromInteger @(Finite n) x) == x)+ `catch` \(_ :: ErrorCall) -> pure True+prop_fromInteger_toInteger = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x ->+ fromInteger (toInteger @(Finite n) x) === x++prop_valid_quot = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ y /= 0 ==> isValidFinite @n $ x `quot` y+prop_getFinite_quot = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ y /= 0 ==> getFinite @n (x `quot` y) === getFinite x `quot` getFinite y++prop_valid_rem = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ y /= 0 ==> isValidFinite @n $ x `rem` y+prop_getFinite_rem = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ y /= 0 ==> getFinite @n (x `rem` y) === getFinite x `rem` getFinite y++prop_valid_div = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ y /= 0 ==> isValidFinite @n $ x `div` y+prop_getFinite_div = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ y /= 0 ==> getFinite @n (x `div` y) === getFinite x `div` getFinite y++prop_valid_mod = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ y /= 0 ==> isValidFinite @n $ x `mod` y+prop_getFinite_mod = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x y ->+ y /= 0 ==> getFinite @n (x `mod` y) === getFinite x `mod` getFinite y++prop_force = withNat $ \_ (_ :: Proxy n) ->+ expectFailure $ rnf @(Finite n) (error "Expected exception") `seq` True++prop_valid_packFinite = withNat $ \_ (_ :: Proxy n) x ->+ maybe True isValidFinite $ packFinite @n x+prop_getFinite_packFinite = withNat $ \_ (_ :: Proxy n) x ->+ maybe (property True) ((x ===) . getFinite) $ packFinite @n x+prop_finite_packFinite = withNat $ \_ (_ :: Proxy n) x -> ioProperty $+ case packFinite @n x of+ Nothing -> (evaluate (finite @n x) >> pure False)+ `catch` \(_ :: ErrorCall) -> pure True+ Just y -> evaluate (y == finite x)++prop_valid_finites = withNat $ \_ (_ :: Proxy n) ->+ all isValidFinite $ finites @n+prop_finites_minMax = withNatPos $ \_ (_ :: Proxy n) ->+ minBound `elem` finites @n .&&. maxBound `elem` finites @n+prop_finites_ordered = withNat $ \_ (_ :: Proxy n) ->+ finites @n === sort finites+prop_finites_all = withNat $ \_ (_ :: Proxy n) ->+ property $ \x ->+ x {- could be discard -} `seq` x `elem` finites @n++prop_valid_modulo = withNatPos $ \_ (_ :: Proxy n) x ->+ isValidFinite $ modulo @n x+prop_getFinite_modulo = withNatPos $ \n (_ :: Proxy n) x ->+ (getFinite (modulo @n x) - x) `mod` n === 0+++prop_getFinite_equals = withNatPos $ \_ (_ :: Proxy n) ->+ withNatPos $ \_ (_ :: Proxy m) ->+ property $ \x y ->+ (x `equals` y) === (getFinite @n x == getFinite @m y)++prop_getFinite_cmp = withNatPos $ \_ (_ :: Proxy n) ->+ withNatPos $ \_ (_ :: Proxy m) ->+ property $ \x y ->+ (x `cmp` y) === (getFinite @n x `compare` getFinite @m y)++prop_valid_natToFinite = withNat $ \n (_ :: Proxy n) ->+ withNatPos $ \m (_ :: Proxy m) ->+ n + 1 <= m ==> unsafeWithInequality @(n + 1) @m @Bool $+ isValidFinite $ natToFinite @n @m Proxy+prop_getFinite_natToFinite = withNat $ \n (_ :: Proxy n) ->+ withNatPos $ \m (_ :: Proxy m) ->+ n + 1 <= m ==> unsafeWithInequality @(n + 1) @m @Property $+ getFinite (natToFinite @n @m Proxy) === natVal @n Proxy++prop_valid_weaken = withNatPos $ \n (_ :: Proxy n) ->+ unsafeWithKnownNat @(n + 1) (n + 1) $+ property $ \x ->+ isValidFinite $ weaken @n x+prop_finites_weaken = withNat $ \n (_ :: Proxy n) ->+ unsafeWithKnownNat @(n + 1) (n + 1) $+ map (weaken @n) finites === init finites++prop_valid_strengthen = withNat $ \n (_ :: Proxy n) ->+ unsafeWithKnownNat @(n + 1) (n + 1) $+ property $ \x ->+ maybe True isValidFinite $ strengthen @n x+prop_finites_strengthen = withNat $ \n (_ :: Proxy n) ->+ unsafeWithKnownNat @(n + 1) (n + 1) $+ map (strengthen @n) finites === map Just finites ++ [Nothing]++prop_valid_shift = withNatPos $ \n (_ :: Proxy n) ->+ unsafeWithKnownNat @(n + 1) (n + 1) $+ property $ \x ->+ isValidFinite $ shift @n x+prop_finites_shift = withNat $ \n (_ :: Proxy n) ->+ unsafeWithKnownNat @(n + 1) (n + 1) $+ map (shift @n) finites === tail finites++prop_valid_unshift = withNat $ \n (_ :: Proxy n) ->+ unsafeWithKnownNat @(n + 1) (n + 1) $+ property $ \x ->+ maybe True isValidFinite $ unshift @n x+prop_finites_unshift = withNat $ \n (_ :: Proxy n) ->+ unsafeWithKnownNat @(n + 1) (n + 1) $+ map (unshift @n) finites === [Nothing] ++ map Just finites++prop_valid_weakenN = withNatPos $ \n (_ :: Proxy n) ->+ withNatPos $ \m (_ :: Proxy m) ->+ n <= m ==> unsafeWithInequality @n @m @Property $+ property $ \x ->+ isValidFinite $ weakenN @n @m x+prop_finites_weakenN = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ n <= m ==> unsafeWithInequality @n @m @Property $+ map (weakenN @n @m) finites === take n finites++prop_valid_strengthenN = withNat $ \n (_ :: Proxy n) ->+ withNatPos $ \m (_ :: Proxy m) ->+ n <= m ==> unsafeWithInequality @n @m @Property $+ property $ \x ->+ maybe True isValidFinite $ strengthenN @n @m x+prop_finites_strengthenN = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ n <= m ==> unsafeWithInequality @m @n @Property $+ map (strengthenN @m @n) finites === take n (map Just finites) ++ replicate (n - m) Nothing++prop_valid_shiftN = withNatPos $ \n (_ :: Proxy n) ->+ withNatPos $ \m (_ :: Proxy m) ->+ n <= m ==> unsafeWithInequality @n @m @Property $+ property $ \x ->+ isValidFinite $ shiftN @n @m x+prop_finites_shiftN = withNat $ \n (_ :: Proxy n) ->+ withNatPos $ \m (_ :: Proxy m) ->+ n <= m ==> unsafeWithInequality @n @m @Property $+ map (shiftN @n @m) finites === drop (m - n) finites++prop_valid_unshiftN = withNatPos $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ n <= m ==> unsafeWithInequality @n @m @Property $+ property $ \x ->+ maybe True isValidFinite $ unshiftN @n @m x+prop_finites_unshiftN = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ m <= n ==> unsafeWithInequality @m @n @Property $+ map (unshiftN @m @n) finites === replicate (n - m) Nothing ++ drop (m - n) (map Just finites)++prop_valid_weakenProxy = withNatPos $ \n (_ :: Proxy n) ->+ withNat $ \k (_ :: Proxy k) ->+ unsafeWithKnownNat @(n + k) (n + k) $+ property $ \x ->+ isValidFinite $ weakenProxy @Proxy @k @n Proxy x+prop_finites_weakenProxy = withNat $ \n (_ :: Proxy n) ->+ withNat $ \k (_ :: Proxy k) ->+ unsafeWithKnownNat @(n + k) (n + k) $+ map (weakenProxy @Proxy @k @n Proxy) finites === take n finites++prop_valid_strengthenProxy = withNat $ \n (_ :: Proxy n) ->+ withNat $ \k (_ :: Proxy k) ->+ unsafeWithKnownNat @(n + k) (n + k) $+ property $ \x ->+ maybe True isValidFinite $ strengthenProxy @n @Proxy @k Proxy x+prop_finites_strengthenProxy = withNat $ \n (_ :: Proxy n) ->+ withNat $ \k (_ :: Proxy k) ->+ unsafeWithKnownNat @(n + k) (n + k) $+ map (strengthenProxy @n @Proxy @k Proxy) finites === take n (map Just finites) ++ replicate k Nothing++prop_valid_shiftProxy = withNatPos $ \n (_ :: Proxy n) ->+ withNat $ \k (_ :: Proxy k) ->+ unsafeWithKnownNat @(n + k) (n + k) $+ property $ \x ->+ isValidFinite $ shiftProxy @k @Proxy @n Proxy x+prop_finites_shiftProxy = withNat $ \n (_ :: Proxy n) ->+ withNat $ \k (_ :: Proxy k) ->+ unsafeWithKnownNat @(n + k) (n + k) $+ map (shiftProxy @k @Proxy @n Proxy) finites === drop k finites++prop_valid_unshiftProxy = withNat $ \n (_ :: Proxy n) ->+ withNat $ \k (_ :: Proxy k) ->+ unsafeWithKnownNat @(n + k) (n + k) $+ property $ \x ->+ maybe True isValidFinite $ unshiftProxy @k @Proxy @n Proxy x+prop_finites_unshiftProxy = withNat $ \n (_ :: Proxy n) ->+ withNat $ \k (_ :: Proxy k) ->+ unsafeWithKnownNat @(n + k) (n + k) $+ map (unshiftProxy @k @Proxy @n Proxy) finites === replicate k Nothing ++ map Just finites++prop_strengthen_weaken = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x ->+ strengthen @n (weaken x) === Just x+prop_weaken_strengthen = withNat $ \n (_ :: Proxy n) ->+ unsafeWithKnownNat @(n + 1) (n + 1) $+ property $ \x ->+ maybe True (== x) (weaken @n <$> strengthen x)++prop_unshift_shift = withNatPos $ \_ (_ :: Proxy n) ->+ property $ \x ->+ unshift @n (shift x) === Just x+prop_shift_unshift = withNat $ \n (_ :: Proxy n) ->+ unsafeWithKnownNat @(n + 1) (n + 1) $+ property $ \x ->+ maybe True (== x) (shift @n <$> unshift x)++prop_strengthenN_weakenN = withNatPos $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ m <= n ==> unsafeWithInequality @m @n @Property $+ property $ \x ->+ strengthenN @m @n (weakenN x) === Just x+prop_weakenN_strengthenN = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ n <= m ==> unsafeWithInequality @n @m @Property $+ property $ \x ->+ maybe True (== x) (weakenN @n @m <$> strengthenN x)++prop_unshiftN_shiftN = withNatPos $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ m <= n ==> unsafeWithInequality @m @n @Property $+ property $ \x ->+ unshiftN @m @n (shiftN x) === Just x+prop_shiftN_unshiftN = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ n <= m ==> unsafeWithInequality @n @m @Property $+ property $ \x ->+ maybe True (== x) (shiftN @n @m <$> unshiftN x)++prop_strengthenProxy_weakenProxy = withNatPos $ \_ (_ :: Proxy n) ->+ withNat $ \_ (_ :: Proxy k) ->+ property $ \x ->+ strengthenProxy @n @Proxy @k Proxy (weakenProxy Proxy x) === Just x+prop_weakenProxy_strengthenProxy = withNat $ \n (_ :: Proxy n) ->+ withNat $ \k (_ :: Proxy k) ->+ unsafeWithKnownNat @(n + k) (n + k) $+ property $ \x ->+ maybe True (== x) (weakenProxy @Proxy @k @n Proxy <$> strengthenProxy Proxy x)++prop_unshiftProxy_shiftProxy = withNatPos $ \_ (_ :: Proxy n) ->+ withNat $ \_ (_ :: Proxy k) ->+ property $ \x ->+ unshiftProxy @k @Proxy @n Proxy (shiftProxy Proxy x) === Just x+prop_shiftProxy_unshiftProxy = withNat $ \n (_ :: Proxy n) ->+ withNat $ \k (_ :: Proxy k) ->+ unsafeWithKnownNat @(n + k) (n + k) $+ property $ \x ->+ maybe True (== x) (shiftProxy @k @Proxy @n Proxy <$> unshiftProxy Proxy x)++prop_valid_add = withNatPos $ \n (_ :: Proxy n) ->+ withNatPos $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n + m) (n + m) $+ property $ \x y ->+ isValidFinite $ add @n @m x y+prop_getFinite_add = withNatPos $ \_ (_ :: Proxy n) ->+ withNatPos $ \_ (_ :: Proxy m) ->+ property $ \x y ->+ getFinite (add @n @m x y) === getFinite x + getFinite y++prop_valid_sub = withNatPos $ \_ (_ :: Proxy n) ->+ withNatPos $ \_ (_ :: Proxy m) ->+ property $ \x y ->+ either isValidFinite isValidFinite $ sub @n @m x y+prop_getFinite_sub = withNatPos $ \_ (_ :: Proxy n) ->+ withNatPos $ \_ (_ :: Proxy m) ->+ property $ \x y ->+ either (negate . getFinite) getFinite (sub @n @m x y) === getFinite x - getFinite y+prop_sub_Left_0 = withNatPos $ \_ (_ :: Proxy n) ->+ withNatPos $ \_ (_ :: Proxy m) ->+ property $ \x y ->+ sub @n @m x y =/= Left 0++prop_valid_multiply = withNatPos $ \n (_ :: Proxy n) ->+ withNatPos $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $+ property $ \x y ->+ isValidFinite $ multiply @n @m x y+prop_getFinite_multiply = withNatPos $ \_ (_ :: Proxy n) ->+ withNatPos $ \_ (_ :: Proxy m) ->+ property $ \x y ->+ getFinite (multiply @n @m x y) === getFinite x * getFinite y++prop_valid_combineSum = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n + m) (n + m) $+ property $ \x ->+ isValidFinite $ combineSum @n @m x+prop_finites_combineSum = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n + m) (n + m) $+ map (combineSum @n @m) (map Left finites ++ map Right finites) === finites++prop_valid_combineProduct = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $+ property $ \x ->+ isValidFinite (combineProduct @n @m x)+prop_finites_combineProduct = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $+ map (combineProduct @n @m) [(x, y) | y <- finites, x <- finites] === finites++prop_valid_separateSum = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n + m) (n + m) $+ property $ \x ->+ either isValidFinite isValidFinite $ separateSum @n @m x+prop_finites_separateSum = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n + m) (n + m) $+ map (separateSum @n @m) finites === map Left finites ++ map Right finites++prop_valid_separateProduct = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $+ property $ \x ->+ x {- could be discard -} `seq` isValidFinite (fst $ separateProduct @n @m x)+ .&&. isValidFinite (snd $ separateProduct @n @m x)+prop_finites_separateProduct = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $+ map (separateProduct @n @m) finites === [(x, y) | y <- finites, x <- finites]++prop_combineSum_separateSum = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n + m) (n + m) $+ property $ \x ->+ combineSum @n @m (separateSum x) === x+prop_separateSum_combineSum = withNat $ \_ (_ :: Proxy n) ->+ withNat $ \_ (_ :: Proxy m) ->+ property $ \x ->+ separateSum @n @m (combineSum x) === x++prop_combineProduct_separateProduct = withNat $ \n (_ :: Proxy n) ->+ withNat $ \m (_ :: Proxy m) ->+ unsafeWithKnownNat @(n GHC.TypeLits.* m) (n * m) $+ property $ \x ->+ x {- could be discard -} `seq` combineProduct @n @m (separateProduct x) === x+prop_separateProduct_combineProduct = withNat $ \_ (_ :: Proxy n) ->+ withNat $ \_ (_ :: Proxy m) ->+ property $ \x ->+ force x {- could be discard -} `seq` separateProduct @n @m (combineProduct x) === x++return []+main = $quickCheckAll >>= \case+ True -> pure ()+ False -> exitFailure