finite-typelits 0.1.6.0 → 0.2.0.0

raw patch · 6 files changed

+2079/−743 lines, 6 filesdep +taggeddep +template-haskelldep ~QuickCheckdep ~basedep ~deepseqPVP ok

version bump matches the API change (PVP)

Dependencies added: tagged, template-haskell

Dependency ranges changed: QuickCheck, base, deepseq

API changes (from Hackage documentation)

Files

• finite-typelits.cabal +11/−7
• src/Data/Finite.hs +119/−107
• src/Data/Finite/Integral.hs +353/−0
• src/Data/Finite/Internal.hs +21/−90
• src/Data/Finite/Internal/Integral.hs +460/−0
• test/Main.hs +1115/−539

@@ -1,5 +1,5 @@ name:                finite-typelits-version:             0.1.6.0+version:             0.2.0.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@@ -13,18 +13,22 @@  library   exposed-modules:     Data.Finite+                     , Data.Finite.Integral                      , Data.Finite.Internal-  build-depends:       base >= 4.7 && < 4.18-                     , deepseq >= 1.4+                     , Data.Finite.Internal.Integral+  build-depends:       base >= 4.7 && < 4.20+                     , deepseq >= 1.3 && < 1.6+                     , tagged >= 0.8 && < 0.9+                     , template-haskell >= 2.9 && < 2.22   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall -test-Suite finite-typelits-tests+test-suite finite-typelits-tests   type:                exitcode-stdio-1.0   main-is:             test/Main.hs   build-depends:       finite-typelits-                     , base >= 4.9 && < 4.18-                     , deepseq >= 1.4-                     , QuickCheck+                     , base >= 4.9 && < 4.20+                     , deepseq >= 1.3 && < 1.6+                     , QuickCheck >= 2.12 && < 2.15   default-language:    Haskell2010

@@ -8,7 +8,9 @@ -- Portability :  portable -------------------------------------------------------------------------------- {-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Data.Finite@@ -24,185 +26,195 @@         weakenN, strengthenN, shiftN, unshiftN,         weakenProxy, strengthenProxy, shiftProxy, unshiftProxy,         add, sub, multiply,-        combineSum, combineProduct,-        separateSum, separateProduct,+        combineSum, combineZero, combineProduct, combineOne, combineExponential,+        separateSum, separateZero, separateProduct, separateOne,+        separateExponential,         isValidFinite     )     where -import Data.Maybe import GHC.TypeLits+import Data.Void +import qualified Data.Finite.Integral as I import Data.Finite.Internal  -- | 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-        result = if x < natVal (fromJust result) && x >= 0-            then Just $ Finite x-            else Nothing+packFinite :: forall n. KnownNat n => Integer -> Maybe (Finite n)+packFinite = I.packFinite  -- | Same as 'packFinite' but with a proxy argument to avoid type signatures.-packFiniteProxy :: KnownNat n => proxy n -> Integer -> Maybe (Finite n)-packFiniteProxy _ = packFinite+packFiniteProxy+    :: forall n proxy. KnownNat n+    => proxy n -> Integer -> Maybe (Finite n)+packFiniteProxy = I.packFiniteProxy  -- | Same as 'finite' but with a proxy argument to avoid type signatures.-finiteProxy :: KnownNat n => proxy n -> Integer -> Finite n-finiteProxy _ = finite+finiteProxy :: forall n proxy. KnownNat n => proxy n -> Integer -> Finite n+finiteProxy = I.finiteProxy  -- | Generate a list of length @n@ of all elements of @'Finite' n@.-finites :: KnownNat n => [Finite n]-finites = results-  where-    results = Finite `fmap` [0 .. (natVal (head results) - 1)]+finites :: forall n. KnownNat n => [Finite n]+finites = I.finites  -- | Same as 'finites' but with a proxy argument to avoid type signatures.-finitesProxy :: KnownNat n => proxy n -> [Finite n]-finitesProxy _ = finites+finitesProxy :: forall n proxy. KnownNat n => proxy n -> [Finite n]+finitesProxy = I.finitesProxy  -- | Produce the 'Finite' that is congruent to the given integer modulo @n@.-modulo :: KnownNat n => Integer -> Finite n-modulo x = result-    where-        result = if natVal result == 0-            then error "modulo: division by zero"-            else Finite (x `mod` natVal result)+modulo :: forall n. KnownNat n => Integer -> Finite n+modulo = I.modulo  -- | Same as 'modulo' but with a proxy argument to avoid type signatures.-moduloProxy :: KnownNat n => proxy n -> Integer -> Finite n-moduloProxy _ = modulo+moduloProxy :: forall n proxy. KnownNat n => proxy n -> Integer -> Finite n+moduloProxy = I.moduloProxy  -- | Test two different types of finite numbers for equality.-equals :: Finite n -> Finite m -> Bool-equals (Finite x) (Finite y) = x == y+equals :: forall n m. Finite n -> Finite m -> Bool+equals = I.equals infix 4 `equals`  -- | Compare two different types of finite numbers.-cmp :: Finite n -> Finite m -> Ordering-cmp (Finite x) (Finite y) = x `compare` y+cmp :: forall n m. Finite n -> Finite m -> Ordering+cmp = I.cmp  -- | Convert a type-level literal into a 'Finite'.-natToFinite :: (KnownNat n, KnownNat m, n + 1 <= m) => proxy n -> Finite m-natToFinite p = Finite $ natVal p+natToFinite+    :: forall n m proxy. (KnownNat n, KnownNat m, n + 1 <= m)+    => proxy n -> Finite m+natToFinite = I.natToFinite  -- | Add one inhabitant in the end.-weaken :: Finite n -> Finite (n + 1)-weaken (Finite x) = Finite x+weaken :: forall n. Finite n -> Finite (n + 1)+weaken = I.weaken  -- | 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-        result = if x < natVal (fromJust result)-            then Just $ Finite x-            else Nothing+strengthen :: forall n. KnownNat n => Finite (n + 1) -> Maybe (Finite n)+strengthen = I.strengthen  -- | Add one inhabitant in the beginning, shifting everything up by one.-shift :: Finite n -> Finite (n + 1)-shift (Finite x) = Finite (x + 1)+shift :: forall n. Finite n -> Finite (n + 1)+shift = I.shift  -- | 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-    else Just $ Finite $ x - 1+unshift :: forall n. Finite (n + 1) -> Maybe (Finite n)+unshift = I.unshift  -- | Add multiple inhabitants in the end.-weakenN :: (n <= m) => Finite n -> Finite m-weakenN (Finite x) = Finite x+weakenN :: forall n m. (n <= m) => Finite n -> Finite m+weakenN = I.weakenN  -- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input -- was one of the removed inhabitants.-strengthenN :: KnownNat n => Finite m -> Maybe (Finite n)-strengthenN (Finite x) = result-    where-        result = if x < natVal (fromJust result)-            then Just $ Finite x-            else Nothing+strengthenN :: forall n m. KnownNat m => Finite n -> Maybe (Finite m)+strengthenN = I.strengthenN  -- | Add multiple inhabitants 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+shiftN :: forall n m. (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m+shiftN = I.shiftN  -- | 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) => Finite m -> Maybe (Finite n)-unshiftN fx@(Finite x) = result-    where-        result = if x < natVal fx - natVal (fromJust result)-            then Nothing-            else Just $ Finite $ x - natVal fx + natVal (fromJust result)+unshiftN :: forall n m. (KnownNat n, KnownNat m) => Finite n -> Maybe (Finite m)+unshiftN = I.unshiftN -weakenProxy :: proxy k -> Finite n -> Finite (n + k)-weakenProxy _ (Finite x) = Finite x+weakenProxy :: forall n k proxy. proxy k -> Finite n -> Finite (n + k)+weakenProxy = I.weakenProxy -strengthenProxy :: KnownNat n => proxy k -> Finite (n + k) -> Maybe (Finite n)-strengthenProxy _ (Finite x) = result-    where-        result = if x < natVal (fromJust result)-            then Just $ Finite x-            else Nothing+strengthenProxy+    :: forall n k proxy. KnownNat n+    => proxy k -> Finite (n + k) -> Maybe (Finite n)+strengthenProxy = I.strengthenProxy -shiftProxy :: KnownNat k => proxy k -> Finite n -> Finite (n + k)-shiftProxy p (Finite x) = Finite $ x + natVal p+shiftProxy+    :: forall n k proxy. KnownNat k+    => proxy k -> Finite n -> Finite (n + k)+shiftProxy = I.shiftProxy -unshiftProxy :: KnownNat k => proxy k -> Finite (n + k) -> Maybe (Finite n)-unshiftProxy p (Finite x) = if x < natVal p-    then Nothing-    else Just $ Finite $ x - natVal p+unshiftProxy+    :: forall n k proxy. KnownNat k+    => proxy k -> Finite (n + k) -> Maybe (Finite n)+unshiftProxy = I.unshiftProxy  -- | Add two 'Finite's.-add :: Finite n -> Finite m -> Finite (n + m)-add (Finite x) (Finite y) = Finite $ x + y+add :: forall n m. Finite n -> Finite m -> Finite (n + m)+add = I.add  -- | 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-    else Left $ Finite $ y - x+sub :: forall n m. Finite n -> Finite m -> Either (Finite m) (Finite n)+sub = I.sub  -- | Multiply two 'Finite's.-multiply :: Finite n -> Finite m -> Finite (n GHC.TypeLits.* m)-multiply (Finite x) (Finite y) = Finite $ x * y--getLeftType :: Either a b -> a-getLeftType = error "getLeftType"+multiply :: forall n m. Finite n -> Finite m -> Finite (n GHC.TypeLits.* m)+multiply = I.multiply  -- | 'Left'-biased (left values come first) disjoint union of finite sets.-combineSum :: KnownNat n => Either (Finite n) (Finite m) -> Finite (n + m)-combineSum (Left (Finite x)) = Finite x-combineSum efx@(Right (Finite x)) = Finite $ x + natVal (getLeftType efx)+combineSum+    :: forall n m. KnownNat n+    => Either (Finite n) (Finite m) -> Finite (n + m)+combineSum = I.combineSum +-- | Witness that 'combineSum' preserves units: @0@ is the unit of+-- 'GHC.TypeLits.+', and 'Void' is the unit of 'Either'.+combineZero :: Void -> Finite 0+combineZero = I.combineZero+ -- | '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+combineProduct+    :: forall n m. KnownNat n+    => (Finite n, Finite m) -> Finite (n GHC.TypeLits.* m)+combineProduct = I.combineProduct +-- | Witness that 'combineProduct' preserves units: @1@ is the unit of+-- 'GHC.TypeLits.*', and '()' is the unit of '(,)'.+combineOne :: () -> Finite 1+combineOne = I.combineOne++-- | Product of @n@ copies of a finite set of size @m@, biased towards the lower+-- values of the argument (colex order).+combineExponential+    :: forall n m. (KnownNat m, KnownNat n)+    => (Finite n -> Finite m) -> Finite (m ^ n)+combineExponential = I.combineExponential+ -- | Take a 'Left'-biased disjoint union apart.-separateSum :: KnownNat n => Finite (n + m) -> Either (Finite n) (Finite m)-separateSum (Finite x) = result-    where-        result = if x >= natVal (getLeftType result)-            then Right $ Finite $ x - natVal (getLeftType result)-            else Left $ Finite x+separateSum+    :: forall n m. KnownNat n+    => Finite (n + m) -> Either (Finite n) (Finite m)+separateSum = I.separateSum +-- | Witness that 'separateSum' preserves units: @0@ is the unit of+-- 'GHC.TypeLits.+', and 'Void' is the unit of 'Either'.+--+-- Also witness that a @'Finite' 0@ is uninhabited.+separateZero :: Finite 0 -> Void+separateZero = I.separateZero+ -- | Take a 'fst'-biased product apart.-separateProduct :: KnownNat n => Finite (n GHC.TypeLits.* m) -> (Finite n, Finite m)-separateProduct (Finite x) = result-    where-        result = (Finite $ x `mod` natVal (fst result), Finite $ x `div` natVal (fst result))+separateProduct+    :: forall n m. KnownNat n+    => Finite (n GHC.TypeLits.* m) -> (Finite n, Finite m)+separateProduct = I.separateProduct +separateOne :: Finite 1 -> ()+separateOne = I.separateOne++-- | Take a product of @n@ copies of a finite set of size @m@ apart, biased+-- towards the lower values of the argument (colex order).+separateExponential+    :: forall n m. KnownNat m+    => Finite (m ^ n) -> Finite n -> Finite m+separateExponential = I.separateExponential+ -- | 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+isValidFinite :: forall n. KnownNat n => Finite n -> Bool+isValidFinite = I.isValidFinite

@@ -0,0 +1,353 @@+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Finite.Integral+-- Copyright   :  (C) 2015-2022 mniip+-- License     :  BSD3+-- Maintainer  :  mniip <mniip@mniip.com>+-- Stability   :  experimental+-- Portability :  portable+--------------------------------------------------------------------------------+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+module Data.Finite.Integral+    (+        SaneIntegral, Limited, KnownIntegral, intVal,+        withIntegral,+        Finite,+        packFinite, packFiniteProxy,+        finite, finiteProxy,+        getFinite, finites, finitesProxy,+        modulo, moduloProxy,+        equals, cmp,+        natToFinite,+        weaken, strengthen, shift, unshift,+        weakenN, strengthenN, shiftN, unshiftN,+        weakenProxy, strengthenProxy, shiftProxy, unshiftProxy,+        add, sub, multiply,+        combineSum, combineZero, combineProduct, combineOne, combineExponential,+        separateSum, separateZero, separateProduct, separateOne,+        separateExponential,+        isValidFinite+    )+    where++import Data.Coerce+import Data.List+import Data.Proxy+import Data.Void+import GHC.TypeLits++import Data.Finite.Internal.Integral++-- | Convert an @a@ into a @'Finite' a@, returning 'Nothing' if the input is+-- out of bounds.+packFinite+    :: forall n a. (SaneIntegral a, KnownIntegral a n)+    => a -> Maybe (Finite a n)+packFinite x+    | x < n && x >= 0 = Just $ Finite x+    | otherwise = Nothing+    where n = intVal (Proxy :: Proxy n)+{-# INLINABLE packFinite #-}++-- | Same as 'packFinite' but with a proxy argument to avoid type signatures.+packFiniteProxy+    :: forall n a proxy. (SaneIntegral a, KnownIntegral a n)+    => proxy n -> a -> Maybe (Finite a n)+packFiniteProxy _ = packFinite+{-# INLINABLE packFiniteProxy #-}++-- | Same as 'finite' but with a proxy argument to avoid type signatures.+finiteProxy+    :: forall n a proxy. (SaneIntegral a, KnownIntegral a n)+    => proxy n -> a -> Finite a n+finiteProxy _ = finite+{-# INLINABLE finiteProxy #-}++-- | Generate an ascending list of length @n@ of all elements of @'Finite' a n@.+finites :: forall n a. (SaneIntegral a, KnownIntegral a n) => [Finite a n]+finites = Finite `fmap` takeWhile (< n) [0..]+    -- [0 .. n - 1] does not work if n is 0 of an unsigned type+    where n = intVal (Proxy :: Proxy n)+{-# INLINABLE finites #-}++-- | Same as 'finites' but with a proxy argument to avoid type signatures.+finitesProxy+    :: forall n a proxy. (SaneIntegral a, KnownIntegral a n)+    => proxy n -> [Finite a n]+finitesProxy _ = finites+{-# INLINABLE finitesProxy #-}++-- | Produce the 'Finite' that is congruent to the given integer modulo @n@.+modulo :: forall n a. (SaneIntegral a, KnownIntegral a n) => a -> Finite a n+modulo x+    | n == 0 = error "modulo: division by zero"+    | otherwise = Finite $ x `mod` n+    where n = intVal (Proxy :: Proxy n)+{-# INLINABLE modulo #-}++-- | Same as 'modulo' but with a proxy argument to avoid type signatures.+moduloProxy+    :: forall n a proxy. (SaneIntegral a, KnownIntegral a n)+    => proxy n -> a -> Finite a n+moduloProxy _ = modulo+{-# INLINABLE moduloProxy #-}++-- | Test two different types of finite numbers for equality.+equals :: forall n m a. Eq a => Finite a n -> Finite a m -> Bool+equals = coerce ((==) :: a -> a -> Bool)+infix 4 `equals`+{-# INLINABLE equals #-}++-- | Compare two different types of finite numbers.+cmp :: forall n m a. Ord a => Finite a n -> Finite a m -> Ordering+cmp = coerce (compare :: a -> a -> Ordering)+{-# INLINABLE cmp #-}++-- | Convert a type-level literal into a 'Finite'.+natToFinite+    :: forall n m a proxy.+        (SaneIntegral a, KnownIntegral a n, Limited a m, n + 1 <= m)+    => proxy n -> Finite a m+natToFinite p = Finite $ intVal p+{-# INLINABLE natToFinite #-}++-- | Add one inhabitant in the end.+weaken :: forall n a. Limited a (n + 1) => Finite a n -> Finite a (n + 1)+weaken = coerce+{-# INLINABLE weaken #-}++-- | Remove one inhabitant from the end. Returns 'Nothing' if the input was the+-- removed inhabitant.+strengthen+    :: forall n a. (SaneIntegral a, KnownIntegral a n)+    => Finite a (n + 1) -> Maybe (Finite a n)+strengthen (Finite x)+    | x < n = Just $ Finite x+    | otherwise = Nothing+    where n = intVal (Proxy :: Proxy n)+{-# INLINABLE strengthen #-}++-- | Add one inhabitant in the beginning, shifting everything up by one.+shift+    :: forall n a. (SaneIntegral a, Limited a (n + 1))+    => Finite a n -> Finite a (n + 1)+shift (Finite x) = Finite $ x + 1+{-# INLINABLE shift #-}++-- | Remove one inhabitant from the beginning, shifting everything down by one.+-- Returns 'Nothing' if the input was the removed inhabitant.+unshift :: forall n a. SaneIntegral a => Finite a (n + 1) -> Maybe (Finite a n)+unshift (Finite x)+    | x < 1 = Nothing+    | otherwise = Just $ Finite $ x - 1+{-# INLINABLE unshift #-}++-- | Add multiple inhabitants in the end.+weakenN :: forall n m a. (n <= m, Limited a m) => Finite a n -> Finite a m+weakenN = coerce+{-# INLINABLE weakenN #-}++-- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input+-- was one of the removed inhabitants.+strengthenN+    :: forall n m a. (SaneIntegral a, KnownIntegral a m, Limited a m)+    => Finite a n -> Maybe (Finite a m)+strengthenN (Finite x)+    | x < m = Just $ Finite x+    | otherwise = Nothing+    where m = intVal (Proxy :: Proxy m)+{-# INLINABLE strengthenN #-}++-- | Add multiple inhabitants in the beginning, shifting everything up by the+-- amount of inhabitants added.+shiftN+    :: forall n m a.+        ( SaneIntegral a+        , KnownIntegral a n+        , KnownIntegral a m+        , n <= m+        )+    => Finite a n -> Finite a m+shiftN (Finite x) = Finite $ x + (m - n)+    where+        n = intVal (Proxy :: Proxy n)+        m = intVal (Proxy :: Proxy m)+{-# INLINABLE shiftN #-}++-- | 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+    :: forall n m a.+        (SaneIntegral a, KnownIntegral a n, KnownIntegral a m, Limited a m)+    => Finite a n -> Maybe (Finite a m)+unshiftN (Finite x)+    | m >= n = Just $ Finite $ x + (m - n)+    | x < n - m = Nothing+    | otherwise = Just $ Finite $ x - (n - m)+    where+        n = intVal (Proxy :: Proxy n)+        m = intVal (Proxy :: Proxy m)+{-# INLINABLE unshiftN #-}++weakenProxy+    :: forall n k a proxy. (Limited a (n + k))+    => proxy k -> Finite a n -> Finite a (n + k)+weakenProxy _ = coerce+{-# INLINABLE weakenProxy #-}++strengthenProxy+    :: forall n k a proxy. (SaneIntegral a, KnownIntegral a n)+    => proxy k -> Finite a (n + k) -> Maybe (Finite a n)+strengthenProxy _ (Finite x)+    | x < n = Just $ Finite x+    | otherwise = Nothing+    where n = intVal (Proxy :: Proxy n)+{-# INLINABLE strengthenProxy #-}++shiftProxy+    :: forall n k a proxy.+        (SaneIntegral a, KnownIntegral a k, Limited a (n + k))+    => proxy k -> Finite a n -> Finite a (n + k)+shiftProxy _ (Finite x) = Finite $ x + k+    where k = intVal (Proxy :: Proxy k)+{-# INLINABLE shiftProxy #-}++unshiftProxy+    :: forall n k a proxy. (SaneIntegral a, KnownIntegral a k)+    => proxy k -> Finite a (n + k) -> Maybe (Finite a n)+unshiftProxy _ (Finite x)+    | x < k = Nothing+    | otherwise = Just $ Finite $ x - k+    where k = intVal (Proxy :: Proxy k)+{-# INLINABLE unshiftProxy #-}++-- | Add two 'Finite's.+add+    :: forall n m a. (SaneIntegral a, Limited a (n + m))+    => Finite a n -> Finite a m -> Finite a (n + m)+add (Finite x) (Finite y) = Finite $ x + y+{-# INLINABLE add #-}++-- | Subtract two 'Finite's. Returns 'Left' for negative results, and 'Right'+-- for positive results. Note that this function never returns @'Left' 0@.+sub+    :: forall n m a. SaneIntegral a+    => Finite a n -> Finite a m -> Either (Finite a m) (Finite a n)+sub (Finite x) (Finite y)+    | x >= y = Right $ Finite $ x - y+    | otherwise = Left $ Finite $ y - x+{-# INLINABLE sub #-}++-- | Multiply two 'Finite's.+multiply+    :: forall n m a. (SaneIntegral a, Limited a (n GHC.TypeLits.* m))+    => Finite a n -> Finite a m -> Finite a (n GHC.TypeLits.* m)+multiply (Finite x) (Finite y) = Finite $ x * y+{-# INLINABLE multiply #-}++-- | 'Left'-biased (left values come first) disjoint union of finite sets.+combineSum+    :: forall n m a. (SaneIntegral a, KnownIntegral a n, Limited a (n + m))+    => Either (Finite a n) (Finite a m) -> Finite a (n + m)+combineSum (Left (Finite x)) = Finite x+combineSum (Right (Finite x)) = Finite $ x + n+    where n = intVal (Proxy :: Proxy n)+{-# INLINABLE combineSum #-}++-- | Witness that 'combineSum' preserves units: @0@ is the unit of+-- 'GHC.TypeLits.+', and 'Void' is the unit of 'Either'.+combineZero :: forall a. Void -> Finite a 0+combineZero = absurd+{-# INLINABLE combineZero #-}++-- | 'fst'-biased (fst is the inner, and snd is the outer iteratee) product of+-- finite sets.+combineProduct+    :: forall n m a.+        (SaneIntegral a, KnownIntegral a n, Limited a (n GHC.TypeLits.* m))+    => (Finite a n, Finite a m) -> Finite a (n GHC.TypeLits.* m)+combineProduct (Finite x, Finite y) = Finite $ x + y * n+    where n = intVal (Proxy :: Proxy n)+{-# INLINABLE combineProduct #-}++-- | Witness that 'combineProduct' preserves units: @1@ is the unit of+-- 'GHC.TypeLits.*', and '()' is the unit of '(,)'.+combineOne :: forall a. (SaneIntegral a, Limited a 1) => () -> Finite a 1+combineOne _ = Finite 0+{-# INLINABLE combineOne #-}++-- | Product of @n@ copies of a finite set of size @m@, biased towards the lower+-- values of the argument (colex order).+combineExponential+    :: forall n m a.+        (SaneIntegral a, KnownIntegral a m, KnownIntegral a n, Limited a (m ^ n))+    => (Finite a n -> Finite a m) -> Finite a (m ^ n)+combineExponential f+    = Finite $ fst $ foldl' next (0, 1) (finites :: [Finite a n])+    where+        next (acc, power) x = acc' `seq` (acc', m * power)+            where acc' = acc + getFinite (f x) * power+        m = intVal (Proxy :: Proxy m)+{-# INLINABLE combineExponential #-}++-- | Take a 'Left'-biased disjoint union apart.+separateSum+    :: forall n m a. (SaneIntegral a, KnownIntegral a n)+    => Finite a (n + m) -> Either (Finite a n) (Finite a m)+separateSum (Finite x)+    | x >= n = Right $ Finite $ x - n+    | otherwise = Left $ Finite x+    where n = intVal (Proxy :: Proxy n)+{-# INLINABLE separateSum #-}++-- | Witness that 'separateSum' preserves units: @0@ is the unit of+-- 'GHC.TypeLits.+', and 'Void' is the unit of 'Either'.+--+-- Also witness that a @'Finite' a 0@ is uninhabited.+separateZero :: forall a. SaneIntegral a => Finite a 0 -> Void+separateZero (Finite n) = n `seq` error+    ("separateZero: got Finite " ++ show (toInteger n))+{-# INLINABLE separateZero #-}++-- | Take a 'fst'-biased product apart.+separateProduct+    :: forall n m a. (SaneIntegral a, KnownIntegral a n)+    => Finite a (n GHC.TypeLits.* m) -> (Finite a n, Finite a m)+separateProduct (Finite x) = case divMod x n of+    (d, m) -> (Finite m, Finite d)+    where n = intVal (Proxy :: Proxy n)+{-# INLINABLE separateProduct #-}++separateOne :: forall a. Finite a 1 -> ()+separateOne _ = ()+{-# INLINABLE separateOne #-}++-- | Take a product of @n@ copies of a finite set of size @m@ apart, biased+-- towards the lower values of the argument (colex order).+separateExponential+    :: forall n m a. (SaneIntegral a, KnownIntegral a m)+    => Finite a (m ^ n) -> Finite a n -> Finite a m+separateExponential = go+    where+        go (Finite n) (Finite 0) = Finite $ n `mod` m+        go (Finite n) (Finite x) = n' `seq` go (Finite n') (Finite $ x - 1)+            where n' = n `div` m+        m = intVal (Proxy :: Proxy m)+{-# INLINABLE separateExponential #-}++-- | 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+    :: forall n a. (Ord a, Num a, KnownIntegral a n)+    => Finite a n -> Bool+isValidFinite (Finite x) = x < n && x >= 0+    where n = intVal (Proxy :: Proxy n)+{-# INLINABLE isValidFinite #-}

@@ -1,112 +1,43 @@ -------------------------------------------------------------------------------- -- |--- Module      :  Data.Finite.Internal--- Copyright   :  (C) 2015-2022 mniip+-- Module      :  Data.Finite+-- Copyright   :  (C) 2022-2023 mniip -- License     :  BSD3 -- Maintainer  :  mniip <mniip@mniip.com> -- Stability   :  experimental -- Portability :  portable ---------------------------------------------------------------------------------{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE CPP #-} module Data.Finite.Internal     (-        Finite(Finite),-        finite,-        getFinite+        Finite, pattern Finite,+        finite, getFinite     )     where -import Control.DeepSeq-import Control.Monad-import Data.Ratio-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--- the range @[0, n)@ including @0@ but excluding @n@. Invariants:+import qualified Data.Finite.Internal.Integral as I++-- | Finite number type. The type @'Finite' n@ is inhabited by exactly @n@+-- values in 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)+type Finite = I.Finite Integer +#if __GLASGOW_HASKELL__ >= 710+pattern Finite :: forall n. Integer -> Finite n+#endif+pattern Finite x = I.Finite (x :: Integer)+ -- | 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-        result = if x < natVal result && x >= 0-            then Finite x-            else error $ "finite: Integer " ++ show x ++ " is not representable in Finite " ++ show (natVal result)+finite :: forall n. KnownNat n => Integer -> Finite n+finite = I.finite  -- | Convert a 'Finite' into the corresponding 'Integer'.-getFinite :: Finite n -> Integer-getFinite (Finite x) = x---- | Throws an error for @'Finite' 0@-instance KnownNat n => Bounded (Finite n) where-    maxBound = result-        where-            result = if natVal result > 0-                then Finite $ natVal result - 1-                else error "maxBound: Finite 0 is uninhabited"-    minBound = result-        where-            result = if natVal result > 0-                then Finite 0-                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-                 expectP (Ident "finite")-                 x <- readPrec-                 let result = finite x-                 guard (x >= 0 && x < natVal result)-                 return result---- | '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 (Finite x) = fromInteger $ if x == 0 then 0 else 1-    fromInteger x = result-        where-            result = if x < natVal result && x >= 0-                then Finite x-                else error $ "fromInteger: Integer " ++ show x ++ " is not representable in Finite " ++ show (natVal result)--instance KnownNat n => Real (Finite n) where-    toRational (Finite x) = x % 1---- | '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--instance NFData (Finite n)+getFinite :: forall n. Finite n -> Integer+getFinite = I.getFinite

@@ -0,0 +1,460 @@+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Finite.Internal.Integral+-- Copyright   :  (C) 2015-2024 mniip+-- License     :  BSD3+-- Maintainer  :  mniip <mniip@mniip.com>+-- Stability   :  experimental+-- Portability :  portable+--------------------------------------------------------------------------------+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UndecidableInstances #-}+#if __GLASGOW_HASKELL__ >= 800+{-# LANGUAGE UndecidableSuperClasses #-}+#endif+module Data.Finite.Internal.Integral+    (+        SaneIntegral(..), Limited, KnownIntegral, intVal,+        withIntegral, withLimited,+        Finite(Finite), finite, getFinite+    )+    where++#if MIN_VERSION_base(4,8,0)+import Numeric.Natural+#endif+import Control.DeepSeq+import Control.Monad+import Data.Ix+import Data.Int+import Data.Proxy+import Data.Tagged+import Data.Type.Equality+import Data.Word+import GHC.Exts+import GHC.Read+import GHC.TypeLits+import Language.Haskell.TH.Lib+import Text.ParserCombinators.ReadPrec+import Text.Read.Lex+import Unsafe.Coerce++#include "MachDeps.h"++-- | A class of datatypes that faithfully represent a sub-range of 'Integer'+-- that includes @0@. A valid instance must obey the following laws:+--+-- 'fromInteger' must be a retract of 'toInteger':+--+-- prop> fromInteger (toInteger a) == a+--+-- Restricted to the range @[0, 'Limit']@ (with 'Nothing' understood as positive+-- infinity), 'fromInteger' must be an inverse of 'toInteger':+--+-- prop> limited i ==> toInteger (fromInteger i) == i+-- where:+--+-- > limited i = case limit of+-- >     Just l -> 0 <= i && i <= l+-- >     Nothing -> 0 <= i+--+-- __WARNING__: violating the above constraint in particular breaks type safety.+--+-- The implementations of 'Ord', 'Enum', 'Num', 'Integral' must be compatible+-- with that of 'Integer', whenever all arguments and results fall within+-- @[0, 'Limit']@, for example:+--+-- prop> limited i && limited j && limited k && (i * j == k) ==> (fromInteger i * fromInteger j == fromInteger k)+--+-- Methods 'modAdd', 'modSub', and 'modMul' implement modular addition,+-- multiplication, and subtraction. The default implementation is via 'Integer',+-- but a faster implementation can be provided instead. If provided, the+-- implementation must be correct for moduli in range @[1, 'Limit']@.+--+-- __WARNING:__ a naive implementaton is prone to arithmetic overflow and may+-- produce invalid results for moduli close to 'Limit'.+class Integral a => SaneIntegral a where+    type Limit a :: Maybe Nat+    -- | Given @n > 0@, @0 <= a < n@, and @0 <= b < n@, @'modAdd' n a b@+    -- computes @(a 'Prelude.+' b) \` 'mod' \` n@.+    modAdd :: a -> a -> a -> a+    modAdd n a b = fromInteger+        (modAdd (toInteger n) (toInteger a) (toInteger b) :: Integer)+    -- | Given @n > 0@, @0 <= a < n@, and @0 <= b < n@, @'modSub' n a b@+    -- computes @(a 'Prelude.-' b) \` 'mod' \` n@.+    modSub :: a -> a -> a -> a+    modSub n a b = fromInteger+        (modSub (toInteger n) (toInteger a) (toInteger b) :: Integer)+    -- | Given @n > 0@, @0 <= a < n@, and @0 <= b < n@, @'modMul' n a b@+    -- computes @(a 'Prelude.*' b) \` 'mod' \` n@.+    modMul :: a -> a -> a -> a+    modMul n a b = fromInteger+        (modMul (toInteger n) (toInteger a) (toInteger b) :: Integer)++instance SaneIntegral Integer where+    type Limit Integer = 'Nothing+    modAdd n a b = case a + b of+        r | r >= n -> r - n+        r -> r+    modSub n a b = if a >= b then a - b else n - b + a+    modMul n a b = (a * b) `mod` n++#if MIN_VERSION_base(4,8,0)+instance SaneIntegral Natural where+    type Limit Natural = 'Nothing+    modAdd n a b = case a + b of+        r | r >= n -> r - n+        r -> r+    modSub n a b = if a >= b then a - b else n - b + a+    modMul n a b = (a * b) `mod` n+#endif++instance SaneIntegral Word where+    type Limit Word = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Word))++    modAdd (W# n) (W# a) (W# b) = W# (case plusWord2# a b of+        (# 0##, r #) | isTrue# (ltWord# r n) -> r+        (# _, r #) -> minusWord# r n)++    modSub (W# n) (W# a) (W# b) = W# (if isTrue# (leWord# b a)+        then minusWord# a b+        else plusWord# (minusWord# n b) a)++    modMul (W# n) (W# a) (W# b) = W# (case n of+        0## -> error "modMul: division by zero"+        _ -> case timesWord2# a b of+            (# h, l #) -> case quotRemWord2# h l n of+                (# _, r #) -> r)++modAddViaWord :: (Num a, Integral a) => a -> a -> a -> a+modAddViaWord n a b = fromIntegral+    (modAdd (fromIntegral n) (fromIntegral a) (fromIntegral b) :: Word)++modSubViaWord :: (Num a, Integral a) => a -> a -> a -> a+modSubViaWord n a b = fromIntegral+    (modSub (fromIntegral n) (fromIntegral a) (fromIntegral b) :: Word)++modMulViaWord :: (Num a, Integral a) => a -> a -> a -> a+modMulViaWord n a b = fromIntegral+    (modMul (fromIntegral n) (fromIntegral a) (fromIntegral b) :: Word)++instance SaneIntegral Int where+    type Limit Int = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Int))+    modAdd = modAddViaWord+    modSub = modSubViaWord+    modMul = modMulViaWord++instance SaneIntegral Word8 where+    type Limit Word8+        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Word8))+    modAdd = modAddViaWord+    modSub = modSubViaWord+    modMul = modMulViaWord++instance SaneIntegral Int8 where+    type Limit Int8+        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Int8))+    modAdd = modAddViaWord+    modSub = modSubViaWord+    modMul = modMulViaWord++instance SaneIntegral Word16 where+    type Limit Word16+        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Word16))+    modAdd = modAddViaWord+    modSub = modSubViaWord+    modMul = modMulViaWord++instance SaneIntegral Int16 where+    type Limit Int16+        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Int16))+    modAdd = modAddViaWord+    modSub = modSubViaWord+    modMul = modMulViaWord++instance SaneIntegral Word32 where+    type Limit Word32+        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Word32))+#if WORD_SIZE_IN_BITS >= 32+    modAdd = modAddViaWord+    modSub = modSubViaWord+    modMul = modMulViaWord+#endif++instance SaneIntegral Int32 where+    type Limit Int32+        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Int32))+#if WORD_SIZE_IN_BITS >= 32+    modAdd = modAddViaWord+    modSub = modSubViaWord+    modMul = modMulViaWord+#endif++instance SaneIntegral Word64 where+    type Limit Word64+        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Word64))+#if WORD_SIZE_IN_BITS >= 64+    modAdd = modAddViaWord+    modSub = modSubViaWord+    modMul = modMulViaWord+#endif++instance SaneIntegral Int64 where+    type Limit Int64+        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Int64))+#if WORD_SIZE_IN_BITS >= 64+    modAdd = modAddViaWord+    modSub = modSubViaWord+    modMul = modMulViaWord+#endif++class LeqMaybe (n :: Nat) (c :: Maybe Nat)+instance LeqMaybe n 'Nothing+instance n <= m => LeqMaybe n ('Just m)++-- | Ensures that the value of @n@ is representable in type @a@ (which should be+-- a 'SaneIntegral').+type Limited a (n :: Nat) = LeqMaybe n (Limit a)++-- | This class asserts that the value of @n@ is known at runtime, and that it+-- is representable in type @a@ (which should be a 'SaneIntegral').+--+-- At runtime it acts like an implicit parameter of type @a@, much like+-- 'KnownNat' is an implicit parameter of type 'Integer'.+class KnownIntegral a (n :: Nat) where+    intVal_ :: Tagged n a++instance (SaneIntegral a, Limited a n, KnownNat n) => KnownIntegral a n where+    intVal_ = Tagged $ fromInteger $ natVal (Proxy :: Proxy n)++-- | Reflect a type-level number into a term.+intVal :: forall n a proxy. KnownIntegral a n => proxy n -> a+intVal _ = unTagged (intVal_ :: Tagged n a)+{-# INLINABLE intVal #-}++-- | Recover a 'KnownNat' constraint from a 'KnownIntegral' constraint.+withIntegral+    :: forall a n r proxy1 proxy2. (SaneIntegral a, KnownIntegral a n)+    => proxy1 a -> proxy2 n -> (KnownNat n => r) -> r+withIntegral _ _ k = case someNatVal n of+    Nothing -> error $ "withIntegral: got KnowIntegral instance dictionary "+        ++ " for which toInteger returns " ++ show n+    Just (SomeNat (_ :: Proxy m)) -> case unsafeCoerce Refl :: n :~: m of+        Refl -> k+    where n = toInteger $ (intVal_  :: Tagged n a)+{-# INLINABLE withIntegral #-}++-- | Recover a 'Limited' constraint from a 'KnownIntegral' constraint.+withLimited+    :: forall a n r lim proxy1 proxy2. (Limit a ~ 'Just lim, KnownIntegral a n)+    => proxy1 a -> proxy2 n -> (Limited a n => r) -> r+withLimited _ _ k = case unsafeCoerce Refl :: (n <=? lim) :~: 'True of+    Refl -> k+{-# INLINABLE withLimited #-}++-- | Finite number type. The type @'Finite' a n@ is inhabited by exactly @n@+-- values from type @a@, in the range @[0, n)@ including @0@ but excluding @n@.+-- @a@ must be an instance of 'SaneIntegral' to use this type. Invariants:+--+-- prop> getFinite x < intVal x+-- prop> getFinite x >= 0+newtype Finite a (n :: Nat) = Finite a+    deriving (Eq, Ord, Ix)++type role Finite nominal nominal++-- | Convert an @a@ into a @'Finite' a@, throwing an error if the input is out+-- of bounds.+finite :: forall n a. (SaneIntegral a, KnownIntegral a n) => a -> Finite a n+finite x+    | x < n && x >= 0 = Finite x+    | otherwise = error $ "finite: Integral " ++ show (toInteger x)+        ++ " is not representable in Finite _ " ++ show (toInteger n)+    where n = intVal (Proxy :: Proxy n)+{-# INLINABLE finite #-}++-- | Convert a @'Finite' a@ into the corresponding @a@.+getFinite :: forall n a. Finite a n -> a+getFinite (Finite x) = x+{-# INLINABLE getFinite #-}++-- | Throws an error for @'Finite' _ 0@+instance (SaneIntegral a, KnownIntegral a n) => Bounded (Finite a n) where+    {-# SPECIALIZE instance KnownNat n => Bounded (Finite Integer n) #-}+#if MIN_VERSION_base(4,8,0)+    {-# SPECIALIZE instance KnownNat n => Bounded (Finite Natural n) #-}+#endif+    {-# SPECIALIZE instance KnownIntegral Word n => Bounded (Finite Word n) #-}+    {-# SPECIALIZE instance KnownIntegral Int n => Bounded (Finite Int n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Word8 n => Bounded (Finite Word8 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Int8 n => Bounded (Finite Int8 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Word16 n => Bounded (Finite Word16 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Int16 n => Bounded (Finite Int16 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Word32 n => Bounded (Finite Word32 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Int32 n => Bounded (Finite Int32 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Word64 n => Bounded (Finite Word64 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Int64 n => Bounded (Finite Int64 n) #-}+    maxBound+        | n > 0 = Finite $ n - 1+        | otherwise = error "maxBound: Finite _ 0 is uninhabited"+        where n = intVal (Proxy :: Proxy n) :: a+    minBound+        | n > 0 = Finite 0+        | otherwise = error "minBound: Finite _ 0 is uninhabited"+        where n = intVal (Proxy :: Proxy n) :: a++instance (SaneIntegral a, KnownIntegral a n) => Enum (Finite a n) where+    {-# SPECIALIZE instance KnownNat n => Enum (Finite Integer n) #-}+#if MIN_VERSION_base(4,8,0)+    {-# SPECIALIZE instance KnownNat n => Enum (Finite Natural n) #-}+#endif+    {-# SPECIALIZE instance KnownIntegral Word n => Enum (Finite Word n) #-}+    {-# SPECIALIZE instance KnownIntegral Int n => Enum (Finite Int n) #-}+    {-# SPECIALIZE instance KnownIntegral Word8 n => Enum (Finite Word8 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int8 n => Enum (Finite Int8 n) #-}+    {-# SPECIALIZE instance KnownIntegral Word16 n => Enum (Finite Word16 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int16 n => Enum (Finite Int16 n) #-}+    {-# SPECIALIZE instance KnownIntegral Word32 n => Enum (Finite Word32 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int32 n => Enum (Finite Int32 n) #-}+    {-# SPECIALIZE instance KnownIntegral Word64 n => Enum (Finite Word64 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int64 n => Enum (Finite Int64 n) #-}+    succ (Finite x)+        | x == n - 1 = error "succ: bad argument"+        | otherwise = Finite $ succ x+        where n = intVal (Proxy :: Proxy n)+    pred (Finite x)+        | x == 0 = error "pred: bad argument"+        | otherwise = Finite $ pred x+    fromEnum = fromEnum . getFinite+    toEnum x+        | toInteger x < toInteger n && x >= 0 = Finite $ fromIntegral x+        | otherwise = error $ "toEnum: Int " ++ show x+            ++ " is not representable in Finite _ " ++ show (toInteger n)+        where n = intVal (Proxy :: Proxy n) :: a+    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 a => Show (Finite a n) where+    showsPrec d (Finite x)+        = showParen (d > 9) $ showString "finite " . showsPrec 10 x++instance (Read a, SaneIntegral a, KnownIntegral a n) => Read (Finite a n) where+    readPrec = parens $ Text.ParserCombinators.ReadPrec.prec 10 $ do+        expectP (Ident "finite")+        x <- readPrec+        guard (x >= 0 && x < n)+        return $ Finite x+        where n = intVal (Proxy :: Proxy n)++-- | 'Prelude.+', 'Prelude.-', and 'Prelude.*' implement arithmetic modulo @n@.+-- The 'fromInteger' function raises an error for inputs outside of bounds.+instance (SaneIntegral a, KnownIntegral a n) => Num (Finite a n) where+    {-# SPECIALIZE instance KnownNat n => Num (Finite Integer n) #-}+#if MIN_VERSION_base(4,8,0)+    {-# SPECIALIZE instance KnownNat n => Num (Finite Natural n) #-}+#endif+    {-# SPECIALIZE instance KnownIntegral Word n => Num (Finite Word n) #-}+    {-# SPECIALIZE instance KnownIntegral Int n => Num (Finite Int n) #-}+    {-# SPECIALIZE instance KnownIntegral Word8 n => Num (Finite Word8 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int8 n => Num (Finite Int8 n) #-}+    {-# SPECIALIZE instance KnownIntegral Word16 n => Num (Finite Word16 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int16 n => Num (Finite Int16 n) #-}+    {-# SPECIALIZE instance KnownIntegral Word32 n => Num (Finite Word32 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int32 n => Num (Finite Int32 n) #-}+    {-# SPECIALIZE instance KnownIntegral Word64 n => Num (Finite Word64 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int64 n => Num (Finite Int64 n) #-}+    Finite x + Finite y = Finite $ modAdd n x y+        where n = intVal (Proxy :: Proxy n)+    Finite x - Finite y = Finite $ modSub n x y+        where n = intVal (Proxy :: Proxy n)+    Finite x * Finite y = Finite $ modMul n x y+        where n = intVal (Proxy :: Proxy n)+    abs fx = fx+    signum (Finite x) = Finite $ if x == 0 then 0 else 1+    fromInteger x+        | x < toInteger n && x >= 0 = Finite $ fromInteger x+        | otherwise = error $ "fromInteger: Integer " ++ show x+            ++ " is not representable in Finite _ " ++ show (toInteger n)+        where n = intVal (Proxy :: Proxy n) :: a++instance (SaneIntegral a, KnownIntegral a n) => Real (Finite a n) where+    {-# SPECIALIZE instance KnownNat n => Real (Finite Integer n) #-}+#if MIN_VERSION_base(4,8,0)+    {-# SPECIALIZE instance KnownNat n => Real (Finite Natural n) #-}+#endif+    {-# SPECIALIZE instance KnownIntegral Word n => Real (Finite Word n) #-}+    {-# SPECIALIZE instance KnownIntegral Int n => Real (Finite Int n) #-}+    {-# SPECIALIZE instance KnownIntegral Word8 n => Real (Finite Word8 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int8 n => Real (Finite Int8 n) #-}+    {-# SPECIALIZE instance KnownIntegral Word16 n => Real (Finite Word16 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int16 n => Real (Finite Int16 n) #-}+    {-# SPECIALIZE instance KnownIntegral Word32 n => Real (Finite Word32 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int32 n => Real (Finite Int32 n) #-}+    {-# SPECIALIZE instance KnownIntegral Word64 n => Real (Finite Word64 n) #-}+    {-# SPECIALIZE instance KnownIntegral Int64 n => Real (Finite Int64 n) #-}+    toRational (Finite x) = toRational x++-- | 'quot' and 'rem' are the same as 'div' and 'mod' and they implement regular+-- division of numbers in the range @[0, n)@, __not__ modular inverses.+instance (SaneIntegral a, KnownIntegral a n) => Integral (Finite a n) where+    {-# SPECIALIZE instance KnownNat n => Integral (Finite Integer n) #-}+#if MIN_VERSION_base(4,8,0)+    {-# SPECIALIZE instance KnownNat n => Integral (Finite Natural n) #-}+#endif+    {-# SPECIALIZE instance KnownIntegral Word n => Integral (Finite Word n) #-}+    {-# SPECIALIZE instance KnownIntegral Int n => Integral (Finite Int n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Word8 n => Integral (Finite Word8 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Int8 n => Integral (Finite Int8 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Word16 n => Integral (Finite Word16 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Int16 n => Integral (Finite Int16 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Word32 n => Integral (Finite Word32 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Int32 n => Integral (Finite Int32 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Word64 n => Integral (Finite Word64 n) #-}+    {-# SPECIALIZE instance+        KnownIntegral Int64 n => Integral (Finite Int64 n) #-}+    quot (Finite x) (Finite y) = Finite $ quot x y+    rem (Finite x) (Finite y) = Finite $ rem x y+    quotRem (Finite x) (Finite y) = case quotRem x y of+        (q, r) -> (Finite q, Finite r)+    div (Finite x) (Finite y) = Finite $ div x y+    mod (Finite x) (Finite y) = Finite $ mod x y+    divMod (Finite x) (Finite y) = case divMod x y of+        (q, r) -> (Finite q, Finite r)+    toInteger (Finite x) = toInteger x++instance NFData a => NFData (Finite a n) where+    rnf (Finite x) = rnf x

@@ -1,542 +1,1118 @@-{-# 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 $ \_ (_ :: Proxy n) ->-    withNatPos $ \_ (_ :: Proxy m) ->-        property $ \x ->-            maybe True isValidFinite $ strengthenN @n @m x-prop_finites_strengthenN = withNat $ \n (_ :: Proxy n) ->-    withNat $ \m (_ :: Proxy m) ->-        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 $ \_ (_ :: Proxy n) ->-    withNat $ \_ (_ :: Proxy m) ->-        property $ \x ->-            maybe True isValidFinite $ unshiftN @n @m x-prop_finites_unshiftN = withNat $ \n (_ :: Proxy n) ->-    withNat $ \m (_ :: Proxy m) ->-        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+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+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++mkLimited+    :: forall a lim. (Limit a ~ 'Just lim, KnownNat lim)+    => Integer -> Maybe (SLimited a)+mkLimited n = case someNatVal n of+    Just (SomeNat (p :: Proxy b))+        | n <= natVal @lim Proxy+        , Refl :: (b <=? lim) :~: 'True <- unsafeCoerce Refl+        -> Just $ SLimited p+    _ -> Nothing++mkUnlimited+    :: forall a. Limit a ~ 'Nothing+    => Integer -> Maybe (SLimited a)+mkUnlimited 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)++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` mkUnlimited+    shrink (SLimited p) = mapMaybe mkUnlimited $ shrink $ natVal p++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` mkUnlimited+    shrink (SLimited p) = mapMaybe mkUnlimited $ shrink $ natVal p++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` mkLimited+    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p++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` mkLimited+    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p++instance Arbitrary (SLimited Word8) where+    arbitrary = oneof+        [ genSmall, genUnder7, genOver7, genUnder8 ]+        `suchThatMap` mkLimited+    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p++instance Arbitrary (SLimited Int8) where+    arbitrary = oneof+        [ genSmall, genUnder7 ]+        `suchThatMap` mkLimited+    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p++instance Arbitrary (SLimited Word16) where+    arbitrary = oneof+        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15+        , genOver15, genUnder16 ]+        `suchThatMap` mkLimited+    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p++instance Arbitrary (SLimited Int16) where+    arbitrary = oneof+        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 ]+        `suchThatMap` mkLimited+    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p++instance Arbitrary (SLimited Word32) where+    arbitrary = oneof+        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15+        , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 ]+        `suchThatMap` mkLimited+    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p++instance Arbitrary (SLimited Int32) where+    arbitrary = oneof+        [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15+        , genOver15, genUnder16, genOver16, genUnder31 ]+        `suchThatMap` mkLimited+    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p++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` mkLimited+    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p++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` mkLimited+    shrink (SLimited p) = mapMaybe mkLimited $ shrink $ natVal p++newtype SmallLimited a = SmallLimited { getSmallLimited :: SLimited a }++instance Arbitrary (SmallLimited Integer) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkUnlimited+    shrink = map SmallLimited . shrink . getSmallLimited++instance Arbitrary (SmallLimited Natural) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkUnlimited+    shrink = map SmallLimited . shrink . getSmallLimited++instance Arbitrary (SmallLimited Word) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited+    shrink = map SmallLimited . shrink . getSmallLimited++instance Arbitrary (SmallLimited Int) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited+    shrink = map SmallLimited . shrink . getSmallLimited++instance Arbitrary (SmallLimited Word8) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited+    shrink = map SmallLimited . shrink . getSmallLimited++instance Arbitrary (SmallLimited Int8) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited+    shrink = map SmallLimited . shrink . getSmallLimited++instance Arbitrary (SmallLimited Word16) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited+    shrink = map SmallLimited . shrink . getSmallLimited++instance Arbitrary (SmallLimited Int16) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited+    shrink = map SmallLimited . shrink . getSmallLimited++instance Arbitrary (SmallLimited Word32) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited+    shrink = map SmallLimited . shrink . getSmallLimited++instance Arbitrary (SmallLimited Int32) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited+    shrink = map SmallLimited . shrink . getSmallLimited++instance Arbitrary (SmallLimited Word64) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited+    shrink = map SmallLimited . shrink . getSmallLimited++instance Arbitrary (SmallLimited Int64) where+    arbitrary = SmallLimited <$> genSmall `suchThatMap` mkLimited+    shrink = map SmallLimited . shrink . getSmallLimited++type Good a =+    ( Show a+    , Read a+    , NFData a+    , Typeable a+    , SaneIntegral a+    , Arbitrary a+    , Arbitrary (SLimited a)+    , Arbitrary (SmallLimited 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, Typeable a)+    => Integer -> ((KnownNat n, Limited a n) => Property) -> Property+unsafeWithKnownIntegral n prop+    | Just (Refl :: a :~: Integer) <- cast (Refl @a)+    , Just (SLimited (_ :: Proxy n')) <- mkUnlimited @a n+    , Refl <- unsafeCoerce Refl :: n :~: n'+    = prop+    | Just (Refl :: a :~: Natural) <- cast (Refl @a)+    , Just (SLimited (_ :: Proxy n')) <- mkUnlimited @a n+    , Refl <- unsafeCoerce Refl :: n :~: n'+    = prop+    | Just (Refl :: a :~: Word) <- cast (Refl @a)+    , Just (SLimited (_ :: Proxy n')) <- mkLimited @a n+    , Refl <- unsafeCoerce Refl :: n :~: n'+    = prop+    | Just (Refl :: a :~: Int) <- cast (Refl @a)+    , Just (SLimited (_ :: Proxy n')) <- mkLimited @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  return [] main = $quickCheckAll >>= \case