diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2015, mniip +Copyright (c) 2015-2022, mniip All rights reserved. diff --git a/finite-typelits.cabal b/finite-typelits.cabal --- a/finite-typelits.cabal +++ b/finite-typelits.cabal @@ -1,6 +1,6 @@ name: finite-typelits -version: 0.1.4.2 -synopsis: A type inhabited by finitely many values, indexed by type-level naturals. +version: 0.2.1.0 +synopsis: A type inhabited by finitely many values, indexed by type-level naturals description: A type inhabited by finitely many values, indexed by type-level naturals. homepage: https://github.com/mniip/finite-typelits license: BSD3 @@ -12,8 +12,23 @@ cabal-version: >=1.10 library - exposed-modules: Data.Finite, Data.Finite.Internal - build-depends: base == 4.* - , deepseq >= 1.4 + exposed-modules: Data.Finite + , Data.Finite.Integral + , Data.Finite.Internal + , Data.Finite.Internal.Integral + build-depends: base >= 4.7 && < 4.21 + , deepseq >= 1.3 && < 1.6 + , tagged >= 0.8 && < 0.9 + , template-haskell >= 2.9 && < 2.23 hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -Wall + +test-suite finite-typelits-tests + type: exitcode-stdio-1.0 + main-is: test/Main.hs + build-depends: finite-typelits + , base >= 4.9 && < 4.21 + , deepseq >= 1.3 && < 1.6 + , QuickCheck >= 2.12 && < 2.15 default-language: Haskell2010 diff --git a/src/Data/Finite.hs b/src/Data/Finite.hs --- a/src/Data/Finite.hs +++ b/src/Data/Finite.hs @@ -1,13 +1,18 @@ -------------------------------------------------------------------------------- -- | -- Module : Data.Finite --- Copyright : (C) 2015 mniip +-- Copyright : (C) 2015-2022 mniip -- License : BSD3 -- Maintainer : mniip -- Stability : experimental -- Portability : portable -------------------------------------------------------------------------------- -{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies, FlexibleContexts #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} module Data.Finite ( Finite, @@ -21,174 +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 +-- | Convert an 'Integer' into a 'Finite', returning 'Nothing' if the input is +-- out of bounds. +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 +-- | Remove one inhabitant from the end. Returns 'Nothing' if the input was the +-- removed inhabitant. +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 +-- | Remove one inhabitant from the beginning, shifting everything down by one. +-- Returns 'Nothing' if the input was the removed inhabitant. +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, n <= m) => Finite m -> Maybe (Finite n) -strengthenN (Finite x) = result - where - result = if x < natVal (fromJust result) - then Just $ Finite x - else Nothing +-- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input +-- was one of the removed inhabitants. +strengthenN :: forall n m. KnownNat m => Finite n -> Maybe (Finite m) +strengthenN = I.strengthenN --- | Add multiple inhabitant in the beginning, shifting everything up by the amount of inhabitants added. -shiftN :: (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m -shiftN fx@(Finite x) = result - where - result = Finite $ x + natVal result - natVal fx +-- | Add multiple inhabitants in the beginning, shifting everything up by the +-- amount of inhabitants added. +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, n <= 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) +-- | 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. (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 p (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 +-- | 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. 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 --- | '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 +-- | 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 + :: 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 --- | Verifies that a given 'Finite' is valid. Should always return 'True' unles you bring the @Data.Finite.Internal.Finite@ constructor into the scope, or use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks -isValidFinite :: KnownNat n => Finite n -> Bool -isValidFinite fx@(Finite x) = x < natVal fx && x >= 0 +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 :: forall n. KnownNat n => Finite n -> Bool +isValidFinite = I.isValidFinite diff --git a/src/Data/Finite/Integral.hs b/src/Data/Finite/Integral.hs new file mode 100644 --- /dev/null +++ b/src/Data/Finite/Integral.hs @@ -0,0 +1,364 @@ +-------------------------------------------------------------------------------- +-- | +-- Module : Data.Finite.Integral +-- Copyright : (C) 2015-2022 mniip +-- License : BSD3 +-- Maintainer : mniip +-- Stability : experimental +-- Portability : portable +-------------------------------------------------------------------------------- +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE CPP #-} +{-# 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, + castFinite, + isValidFinite + ) + where + +import Data.Coerce +#if __GLASGOW_HASKELL__ < 910 +import Data.List (foldl') +#endif +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 #-} + +-- | Convert a 'Finite' between different 'SaneIntegral' numeric types. +castFinite + :: forall b a n. (SaneIntegral a, SaneIntegral b, Limited b n) + => Finite a n -> Finite b n +castFinite (Finite x) = Finite $ fromIntegral x +{-# INLINABLE castFinite #-} + +-- | 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 #-} diff --git a/src/Data/Finite/Internal.hs b/src/Data/Finite/Internal.hs --- a/src/Data/Finite/Internal.hs +++ b/src/Data/Finite/Internal.hs @@ -1,98 +1,43 @@ -------------------------------------------------------------------------------- -- | --- Module : Data.Finite.Internal --- Copyright : (C) 2015 mniip +-- Module : Data.Finite +-- Copyright : (C) 2022-2023 mniip -- License : BSD3 -- Maintainer : mniip -- Stability : experimental -- Portability : portable -------------------------------------------------------------------------------- -{-# LANGUAGE KindSignatures, DataKinds, DeriveGeneric #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE CPP #-} module Data.Finite.Internal ( - Finite(Finite), - finite, - getFinite + Finite, pattern Finite, + finite, getFinite ) where -import GHC.Read import GHC.TypeLits -import GHC.Generics -import Control.DeepSeq -import Control.Monad -import Data.Ratio -import Text.Read.Lex -import Text.ParserCombinators.ReadPrec --- | Finite number type. @'Finite' n@ is inhabited by exactly @n@ values. 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) - --- | 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) - --- | 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 - fromEnum = fromEnum . getFinite - toEnum = finite . toEnum - enumFrom x = enumFromTo x maxBound - enumFromThen x y = enumFromThenTo x y (if x >= y then minBound else maxBound) - -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 - --- | Modular arithmetic. Only the 'fromInteger' function is supposed to be useful. -instance KnownNat n => Num (Finite n) where - fx@(Finite x) + Finite y = Finite $ (x + y) `mod` natVal fx - fx@(Finite x) - Finite y = Finite $ (x - y) `mod` natVal fx - fx@(Finite x) * Finite y = Finite $ (x * y) `mod` natVal fx - abs fx = fx - signum _ = fromInteger 1 - 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) +type Finite = I.Finite Integer -instance KnownNat n => Real (Finite n) where - toRational (Finite x) = x % 1 +#if __GLASGOW_HASKELL__ >= 710 +pattern Finite :: forall n. Integer -> Finite n +#endif +pattern Finite x = I.Finite (x :: Integer) --- | __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 +-- | Convert an 'Integer' into a 'Finite', throwing an error if the input is out +-- of bounds. +finite :: forall n. KnownNat n => Integer -> Finite n +finite = I.finite -instance NFData (Finite n) +-- | Convert a 'Finite' into the corresponding 'Integer'. +getFinite :: forall n. Finite n -> Integer +getFinite = I.getFinite diff --git a/src/Data/Finite/Internal/Integral.hs b/src/Data/Finite/Internal/Integral.hs new file mode 100644 --- /dev/null +++ b/src/Data/Finite/Internal/Integral.hs @@ -0,0 +1,474 @@ +-------------------------------------------------------------------------------- +-- | +-- Module : Data.Finite.Internal.Integral +-- Copyright : (C) 2015-2024 mniip +-- License : BSD3 +-- Maintainer : mniip +-- Stability : experimental +-- Portability : portable +-------------------------------------------------------------------------------- +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# 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) + + -- | Unsafely obtain evidence that @n <= Limit a@. When 'Limit' is 'Nothing' + -- there is no evidence to obtain, and @\\_ _ k -> k@ is a valid + -- implementation. When 'Limit' is a 'Just', the default implementation + -- should work. + unsafeWithLimited :: proxy1 a -> proxy2 n -> (Limited a n => r) -> r + default unsafeWithLimited + :: forall n r lim proxy1 proxy2. (Limit a ~ 'Just lim) + => proxy1 a -> proxy2 n -> (Limited a n => r) -> r + unsafeWithLimited _ _ k = case unsafeCoerce Refl :: (n <=? lim) :~: 'True of + Refl -> k + +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 + unsafeWithLimited _ _ k = k + +#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 + unsafeWithLimited _ _ k = k +#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 KnownIntegral 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 proxy1 proxy2. (SaneIntegral a, KnownIntegral a n) + => proxy1 a -> proxy2 n -> (Limited a n => r) -> r +withLimited = unsafeWithLimited + where _n = intVal_ :: Tagged n a +{-# 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 diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,1095 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module Main where + +import Control.Exception +import Control.DeepSeq +import Control.Monad +import Data.Bifunctor +import Data.Int +import Data.List +import Data.Maybe +import Data.Proxy +import Data.Type.Equality +import Data.Typeable +import Data.Void +import Data.Word +import GHC.TypeLits +import System.Exit +import Test.QuickCheck hiding (Small) +import Unsafe.Coerce +import Numeric.Natural + +import Debug.Trace + +import Data.Finite.Integral +import Data.Finite.Internal.Integral + +newtype SmallNonNeg a = SmallNonNeg { getSmallNonNeg :: a } + deriving (Show) + +instance (Integral a, Arbitrary a) => Arbitrary (SmallNonNeg a) where + arbitrary = SmallNonNeg <$> arbitrarySizedNatural + shrink (SmallNonNeg x) = SmallNonNeg <$> shrink x + +instance Arbitrary Natural where + arbitrary = fromInteger . getNonNegative <$> arbitrary + +instance CoArbitrary Natural where + coarbitrary n = coarbitrary (toInteger n) + +newtype Small a n = Small (Finite a n) + deriving (Show) + +newtype Big a n = Big (Finite a n) + deriving (Show) + +newtype Edgy a n = Edgy (Finite a n) + deriving (Show) + +instance + (Arbitrary a, SaneIntegral a, KnownIntegral a n) + => Arbitrary (Small a n) where + arbitrary + | intVal @n @a Proxy == 0 = discard + | otherwise = Small . Finite . (`mod` n) + . getSmallNonNeg <$> arbitrary + where n = intVal @n Proxy + shrink (Small (Finite x)) = Small <$> mapMaybe packFinite (shrink x) + +instance + (Arbitrary a, SaneIntegral a, KnownIntegral a n) + => Arbitrary (Big a n) where + arbitrary + | intVal @n @a Proxy == 0 = discard + | otherwise = Big . Finite . ((n - 1) -) . (`mod` n) + . getSmallNonNeg <$> arbitrary + where n = intVal @n Proxy + shrink (Big (Finite x)) = Big <$> mapMaybe packFinite (shrink x) + +instance CoArbitrary a => CoArbitrary (Big a n) where + coarbitrary (Big (Finite x)) = coarbitrary x + +instance + (Arbitrary a, SaneIntegral a, KnownIntegral a n) + => Arbitrary (Edgy a n) where + arbitrary + | intVal @n @a Proxy == 0 = discard + | otherwise = Edgy . Finite <$> oneof + [ (`mod` n) . getSmallNonNeg <$> arbitrary + , ((n - 1) -) . (`mod` n) . getSmallNonNeg <$> arbitrary + ] + where n = intVal @n Proxy + shrink (Edgy (Finite x)) = Edgy <$> mapMaybe packFinite (shrink x) + +data SLimited a where + SLimited :: (Limited a n, KnownNat n) => Proxy n -> SLimited a + +class MkSLimited (lim :: Maybe Nat) where + mkSLimited + :: forall a. (SaneIntegral a, Limit a ~ lim) + => Integer -> Maybe (SLimited a) + +instance KnownNat lim => MkSLimited ('Just lim) where + mkSLimited + :: forall a. (SaneIntegral a, Limit a ~ 'Just lim) + => Integer -> Maybe (SLimited a) + mkSLimited n = case someNatVal n of + Just (SomeNat p) + | n <= natVal @lim Proxy + -> Just $ unsafeWithLimited (Proxy @a) p $ SLimited p + _ -> Nothing + +instance MkSLimited 'Nothing where + mkSLimited n = case someNatVal n of + Just (SomeNat p) -> Just $ SLimited p + _ -> Nothing + +genSmall, genOver7, genOver8, genOver15, genOver16, genOver31, genOver32, + genOver63, genOver64, genOverI, genOverW, genUnder7, genUnder8, genUnder15, + genUnder16, genUnder32, genUnder63, genUnder64, genUnderI, genUnderW + :: Gen Integer +genSmall = getNonNegative <$> arbitrary +genOver7 = (toInteger (maxBound @Int8) +) <$> genSmall +genOver8 = (toInteger (maxBound @Word8) +) <$> genSmall +genOver15 = (toInteger (maxBound @Int16) +) <$> genSmall +genOver16 = (toInteger (maxBound @Word16) +) <$> genSmall +genOver31 = (toInteger (maxBound @Int32) +) <$> genSmall +genOver32 = (toInteger (maxBound @Word32) +) <$> genSmall +genOver63 = (toInteger (maxBound @Int64) +) <$> genSmall +genOver64 = (toInteger (maxBound @Word64) +) <$> genSmall +genOverI = (toInteger (maxBound @Int) +) <$> genSmall +genOverW = (toInteger (maxBound @Word) +) <$> genSmall +genUnder7 = ((toInteger (maxBound @Int8) -) <$> genSmall) `suchThat` (>= 0) +genUnder8 = ((toInteger (maxBound @Word8) -) <$> genSmall) `suchThat` (>= 0) +genUnder15 = ((toInteger (maxBound @Int16) -) <$> genSmall) `suchThat` (>= 0) +genUnder16 = ((toInteger (maxBound @Word16) -) <$> genSmall) `suchThat` (>= 0) +genUnder31 = ((toInteger (maxBound @Int32) -) <$> genSmall) `suchThat` (>= 0) +genUnder32 = ((toInteger (maxBound @Word32) -) <$> genSmall) `suchThat` (>= 0) +genUnder63 = ((toInteger (maxBound @Int64) -) <$> genSmall) `suchThat` (>= 0) +genUnder64 = ((toInteger (maxBound @Word64) -) <$> genSmall) `suchThat` (>= 0) +genUnderI = ((toInteger (maxBound @Int) -) <$> genSmall) `suchThat` (>= 0) +genUnderW = ((toInteger (maxBound @Word) -) <$> genSmall) `suchThat` (>= 0) + +shrinkSLimited + :: (SaneIntegral a, MkSLimited (Limit a), Arbitrary a) + => SLimited a -> [SLimited a] +shrinkSLimited (SLimited p) = mapMaybe mkSLimited $ shrink $ natVal p + +instance Arbitrary (SLimited Integer) where + arbitrary = oneof + [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 + , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 + , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI + , genOverI, genUnderW, genOverW ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +instance Arbitrary (SLimited Natural) where + arbitrary = oneof + [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 + , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 + , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI + , genOverI, genUnderW, genOverW ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +instance Arbitrary (SLimited Word) where + arbitrary = oneof + [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 + , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 + , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI + , genOverI, genUnderW ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +instance Arbitrary (SLimited Int) where + arbitrary = oneof + [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 + , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 + , genOver32, genUnder63, genOver63, genUnder64, genOver64, genUnderI ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +instance Arbitrary (SLimited Word8) where + arbitrary = oneof + [ genSmall, genUnder7, genOver7, genUnder8 ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +instance Arbitrary (SLimited Int8) where + arbitrary = oneof + [ genSmall, genUnder7 ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +instance Arbitrary (SLimited Word16) where + arbitrary = oneof + [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 + , genOver15, genUnder16 ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +instance Arbitrary (SLimited Int16) where + arbitrary = oneof + [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +instance Arbitrary (SLimited Word32) where + arbitrary = oneof + [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 + , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +instance Arbitrary (SLimited Int32) where + arbitrary = oneof + [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 + , genOver15, genUnder16, genOver16, genUnder31 ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +instance Arbitrary (SLimited Word64) where + arbitrary = oneof + [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 + , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 + , genOver32, genUnder63, genOver63, genUnder64, genOverI, genUnderW + , genOverW ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +instance Arbitrary (SLimited Int64) where + arbitrary = oneof + [ genSmall, genUnder7, genOver7, genUnder8, genOver8, genUnder15 + , genOver15, genUnder16, genOver16, genUnder31, genOver31, genUnder32 + , genOver32, genUnder63, genUnderI, genOverI, genUnderW, genOverW ] + `suchThatMap` mkSLimited + shrink = shrinkSLimited + +newtype SmallLimited a = SmallLimited { getSmallLimited :: SLimited a } + +instance (SaneIntegral a, MkSLimited (Limit a), Arbitrary (SLimited a)) + => Arbitrary (SmallLimited a) where + arbitrary = SmallLimited <$> genSmall `suchThatMap` mkSLimited + shrink = map SmallLimited . shrink . getSmallLimited + +type Good a = + ( Show a + , Read a + , NFData a + , Typeable a + , SaneIntegral a + , Arbitrary a + , Arbitrary (SLimited a) + , MkSLimited (Limit a) + , CoArbitrary a + ) + +data SType where + SType :: Good a => Proxy a -> SType + +forType :: forall prop. Testable prop + => (forall a. Good a => Proxy a -> prop) + -> Property +forType prop = forAllBlind gen $ \case + (name, SType p) -> counterexample @prop ("@" ++ name) $ prop p + where + gen = elements + [ ("Integer", SType @Integer Proxy) + , ("Natural", SType @Natural Proxy) + , ("Word", SType @Word Proxy) + , ("Int", SType @Int Proxy) + , ("Word8", SType @Word8 Proxy) + , ("Int8", SType @Int8 Proxy) + , ("Word16", SType @Word16 Proxy) + , ("Int16", SType @Int16 Proxy) + , ("Word32", SType @Word32 Proxy) + , ("Int32", SType @Int32 Proxy) + , ("Word64", SType @Word64 Proxy) + , ("Int64", SType @Int64 Proxy) + ] + +forLimit' + :: forall a. SaneIntegral a + => Gen (SLimited a) + -> (SLimited a -> [SLimited a]) + -> (forall n. (KnownIntegral a n, Limited a n) + => (forall i. Num i => i) -> Proxy n -> Property) + -> Property +forLimit' gen shr prop = forAllShrinkBlind @Property gen shr $ \case + SLimited p -> counterexample ("@" ++ show (natVal p)) $ + prop (fromInteger $ natVal p) p + +forLimit + :: forall a. (SaneIntegral a, Arbitrary (SLimited a)) + => (forall n. (KnownIntegral a n, Limited a n) + => (forall i. Num i => i) -> Proxy n -> Property) + -> Property +forLimit = forLimit' @a arbitrary shrink + + +forPositiveLimit + :: forall a. (SaneIntegral a, Arbitrary (SLimited a)) + => (forall n. (KnownIntegral a n, Limited a n) + => (forall i. Num i => i) -> Proxy n -> Property) + -> Property +forPositiveLimit = forLimit' @a + (arbitrary `suchThat` isPositive) + (filter isPositive . shrink) + where + isPositive :: SLimited a -> Bool + isPositive (SLimited p) = natVal p > 0 + +forSmallLimit + :: forall a. (SaneIntegral a, Arbitrary (SmallLimited a)) + => (forall n. (KnownIntegral a n, Limited a n) + => (forall i. Num i => i) -> Proxy n -> Property) + -> Property +forSmallLimit = forLimit' @a + (getSmallLimited <$> arbitrary) + (map getSmallLimited . shrink . SmallLimited) + +unsafeWithKnownIntegral + :: forall n a. (SaneIntegral a, MkSLimited (Limit a), Typeable a) + => Integer -> ((KnownNat n, Limited a n) => Property) -> Property +unsafeWithKnownIntegral n prop + | Just (SLimited (_ :: Proxy n')) <- mkSLimited @_ @a n + , Refl <- unsafeCoerce Refl :: n :~: n' + = prop + | otherwise = discard + +newtype IneqCond (n :: Nat) (m :: Nat) = IneqCond ((n <= m) => Property) +unsafeWithInequality + :: forall (n :: Nat) (m :: Nat). ((n <= m) => Property) -> Property +unsafeWithInequality prop = + case unsafeCoerce (IneqCond @n @m $ property prop) :: IneqCond 0 1 of + IneqCond prop' -> prop' + +prop_isvalid_under = forType $ \(_ :: Proxy a) -> + forLimit @a $ \_ (_ :: Proxy n) -> + property $ \x -> + x < 0 ==> not $ isValidFinite @n @a (Finite x) +prop_isvalid_over = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + property $ \x -> + not (x >= n) .||. not (isValidFinite @n @a (Finite x)) + +prop_valid_finite = forType $ \(_ :: Proxy a) -> + forLimit @a $ \_ (_ :: Proxy n) -> + property $ \x -> ioProperty $ + evaluate (isValidFinite $ finite @n @a x) + `catch` \(_ :: ErrorCall) -> pure True +prop_getFinite_finite = forType $ \(_ :: Proxy a) -> + forLimit @a $ \_ (_ :: Proxy n) -> + property $ \x -> ioProperty $ + evaluate (getFinite (finite @n @a x) == x) + `catch` \(_ :: ErrorCall) -> pure True +prop_finite_getFinite = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + finite (getFinite x) === x + +prop_valid_maxBound = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + n > 0 ==> isValidFinite (maxBound @(Finite a n)) +prop_maxBound_max = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + n > 0 ==> maxBound >= x + +prop_valid_minBound = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + n > 0 ==> isValidFinite (minBound @(Finite a n)) +prop_minBound_min = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + n > 0 ==> minBound <= x + +prop_valid_toEnum = forType $ \(_ :: Proxy a) -> + forLimit @a $ \_ (_ :: Proxy n) -> + property $ \x -> ioProperty $ + evaluate (isValidFinite $ toEnum @(Finite a n) x) + `catch` \(_ :: ErrorCall) -> pure True +prop_fromEnum_toEnum = forType $ \(_ :: Proxy a) -> + forLimit @a $ \_ (_ :: Proxy n) -> + property $ \x -> ioProperty $ + evaluate (fromEnum (toEnum @(Finite a n) x) == x) + `catch` \(_ :: ErrorCall) -> pure True +prop_toEnum_fromEnum = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + n <= toInteger (maxBound @Int) ==> toEnum (fromEnum x) == x + +prop_valid_enumFrom = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Big x :: Big a n) -> + all isValidFinite [x..] +prop_getFinite_enumFrom = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + property $ \(Big x :: Big a n) -> + map getFinite [x..] + === takeWhile (isJust . packFinite @n @a) [getFinite x..] + +prop_valid_enumFromTo = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Big x :: Big a n) (Big y) -> + all isValidFinite [x..y] +prop_valid_enumFromTo' = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Small x :: Small a n) (Small y) -> + all isValidFinite [x..y] +prop_getFinite_enumFromTo = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Big x :: Big a n) (Big y) -> + map getFinite [x..y] === [getFinite x..getFinite y] +prop_getFinite_enumFromTo' = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Small x :: Small a n) (Small y) -> + map getFinite [x..y] === [getFinite x..getFinite y] + +prop_valid_enumFromThen = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Big x :: Big a n) (Big y) -> + x < y ==> all isValidFinite [x,y..] +prop_valid_enumFromThen' = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Small x :: Small a n) (Small y) -> + x > y ==> all isValidFinite [x,y..] +prop_getFinite_enumFromThen = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Big x :: Big a n) (Big y) -> + x < y ==> map getFinite [x,y..] + === takeWhile (isJust . packFinite @n @a) [getFinite x,getFinite y..] +prop_getFinite_enumFromThen' = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Small x :: Small a n) (Small y) -> + x > y ==> map getFinite [x,y..] + === takeWhile (isJust . packFinite @n @a) [getFinite x,getFinite y..] + +prop_valid_enumFromThenTo = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Small x :: Small a n) (Small y) (Small z) -> + x /= y ==> all isValidFinite [x,y..z] +prop_getFinite_enumFromThenTo = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Small x :: Small a n) (Small y) (Small z) -> + x /= y ==> map getFinite [x,y..z] === [getFinite x,getFinite y..getFinite z] + +prop_nonint_succ = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Big x :: Big a n) -> + case packFinite @n @a $ succ $ getFinite x of + Nothing -> discard + Just y -> y === succ x + +prop_valid_read = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + forPositiveLimit @a $ \_ (_ :: Proxy m) -> + property $ \(Edgy x :: Edgy a n) -> ioProperty $ + evaluate (isValidFinite $ read @(Finite a m) (show x)) + `catch` \(_ :: ErrorCall) -> pure True +prop_read_show = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + read (show x) === x + +prop_valid_plus = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + isValidFinite $ x + y +prop_getFinite_plus = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + (getFinite x + getFinite y - getFinite (x + y)) `mod` n === 0 + +prop_valid_minus = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + isValidFinite $ x - y +prop_getFinite_minus = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + (getFinite x + n - getFinite y - getFinite (x - y)) `mod` n === 0 + +prop_valid_times = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + isValidFinite $ x * y +prop_getFinite_times = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + (toInteger (getFinite x) * toInteger (getFinite y) + - toInteger (getFinite $ x * y)) `mod` n === 0 + +prop_valid_negate = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + isValidFinite $ -x +prop_getFinite_negate = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + (n - getFinite x - getFinite (-x)) `mod` n === 0 + +prop_valid_abs = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + isValidFinite $ abs x +prop_getFinite_abs = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + getFinite (abs x) === abs (getFinite x) + +prop_valid_signum = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + isValidFinite $ signum x +prop_getFinite_signum = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + getFinite (signum x) === signum (getFinite x) + +prop_valid_fromInteger = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \x -> ioProperty $ + evaluate (isValidFinite $ fromInteger @(Finite a n) x) + `catch` \(_ :: ErrorCall) -> pure True +prop_toInteger_fromInteger = forType $ \(_ :: Proxy a) -> + forLimit @a $ \_ (_ :: Proxy n) -> + property $ \x -> ioProperty $ + evaluate (toInteger (fromInteger @(Finite a n) x) == x) + `catch` \(_ :: ErrorCall) -> pure True +prop_fromInteger_toInteger = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + fromInteger (toInteger x) === x + +prop_valid_quot = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + y /= 0 ==> isValidFinite $ x `quot` y +prop_getFinite_quot = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + y /= 0 ==> getFinite (x `quot` y) === getFinite x `quot` getFinite y + +prop_valid_rem = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + y /= 0 ==> isValidFinite $ x `rem` y +prop_getFinite_rem = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + y /= 0 ==> getFinite (x `rem` y) === getFinite x `rem` getFinite y + +prop_valid_div = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + y /= 0 ==> isValidFinite $ x `div` y +prop_getFinite_div = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + y /= 0 ==> getFinite (x `div` y) === getFinite x `div` getFinite y + +prop_valid_mod = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + y /= 0 ==> isValidFinite $ x `mod` y +prop_getFinite_mod = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) (Edgy y) -> + y /= 0 ==> getFinite (x `mod` y) === getFinite x `mod` getFinite y + +prop_force = forType $ \(_ :: Proxy a) -> + forLimit @a $ \_ (_ :: Proxy n) -> + ioProperty $ + evaluate (rnf @(Finite a n) (error "Expected exception") `seq` False) + `catch` (\(_ :: ErrorCall) -> pure True) + +prop_valid_packFinite = forType $ \(_ :: Proxy a) -> + forLimit @a $ \_ (_ :: Proxy n) -> + property $ \x -> + maybe True isValidFinite $ packFinite @n @a x +prop_getFinite_packFinite = forType $ \(_ :: Proxy a) -> + forLimit @a $ \_ (_ :: Proxy n) -> + property $ \x -> + maybe (property True) ((x ===) . getFinite) $ packFinite @n @a x +prop_finite_packFinite = forType $ \(_ :: Proxy a) -> + forLimit @a $ \_ (_ :: Proxy n) -> + property $ \x -> ioProperty $ + case packFinite @n @a x of + Nothing -> (evaluate (finite @n @a x) >> pure False) + `catch` \(_ :: ErrorCall) -> pure True + Just y -> evaluate (y == finite x) + +prop_valid_finites = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \_ (_ :: Proxy n) -> + property $ + all isValidFinite $ finites @n @a +prop_finites_minMax = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + n > 0 ==> minBound `elem` finites @n @a .&&. maxBound `elem` finites @n @a +prop_finites_ordered = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \_ (_ :: Proxy n) -> + finites @n @a === sort finites +prop_finites_all = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \_ (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + x -- could be discard + `seq` x `elem` finites @n @a + +prop_valid_modulo = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + property $ \x -> + isValidFinite $ modulo @n @a x +prop_getFinite_modulo = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + property $ \x -> + (toInteger x - toInteger (getFinite $ modulo @n @a x)) `mod` n === 0 + +prop_getFinite_equals = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + forPositiveLimit @a $ \_ (_ :: Proxy m) -> + property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) -> + (x `equals` y) === (getFinite x == getFinite y) + +prop_getFinite_cmp = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + forPositiveLimit @a $ \_ (_ :: Proxy m) -> + property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) -> + (x `cmp` y) === (getFinite x `compare` getFinite y) + +prop_valid_natToFinite = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forPositiveLimit @a $ \m (_ :: Proxy m) -> + n + 1 <= m ==> unsafeWithInequality @(n + 1) @m $ + property $ + isValidFinite $ natToFinite @n @m @a Proxy +prop_getFinite_natToFinite = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forPositiveLimit @a $ \m (_ :: Proxy m) -> + n + 1 <= m ==> unsafeWithInequality @(n + 1) @m $ + getFinite (natToFinite @n @m @a Proxy) === n + +prop_valid_weaken = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + property $ \(Edgy x :: Edgy a n) -> + isValidFinite $ weaken x +prop_finites_weaken = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + map (weaken @n @a) finites === init finites + +prop_valid_strengthen = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + property $ \(Edgy x :: Edgy a (n + 1)) -> + maybe True isValidFinite $ strengthen x +prop_finites_strengthen = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + map (strengthen @n @a) finites === map Just finites ++ [Nothing] + +prop_valid_shift = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + property $ \(Edgy x :: Edgy a n) -> + isValidFinite $ shift x +prop_finites_shift = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + map (shift @n @a) finites === drop 1 finites + +prop_valid_unshift = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + property $ \(Edgy x :: Edgy a (n + 1)) -> + maybe True isValidFinite $ unshift x +prop_finites_unshift = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + map (unshift @n @a) finites === [Nothing] ++ map Just finites + +prop_valid_weakenN = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forPositiveLimit @a $ \m (_ :: Proxy m) -> + n <= m ==> unsafeWithInequality @n @m $ + property $ \(Edgy x :: Edgy a n) -> + isValidFinite $ weakenN @n @m @a x +prop_finites_weakenN = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + n <= m ==> unsafeWithInequality @n @m $ + map (weakenN @n @m @a) finites === take n finites + +prop_valid_strengthenN = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + forLimit @a $ \_ (_ :: Proxy m) -> + property $ \(Edgy x :: Edgy a n) -> + maybe True isValidFinite $ strengthenN @n @m x +prop_finites_strengthenN = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + map (strengthenN @n @m @a) finites + === take n (map Just finites) ++ replicate (n - m) Nothing + +prop_valid_shiftN = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forPositiveLimit @a $ \m (_ :: Proxy m) -> + n <= m ==> unsafeWithInequality @n @m $ + property $ \(Edgy x :: Edgy a n) -> + isValidFinite $ shiftN @n @m @a x +prop_finites_shiftN = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + n <= m ==> unsafeWithInequality @n @m $ + map (shiftN @n @m @a) finites === drop (m - n) finites + +prop_valid_unshiftN = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + forLimit @a $ \_ (_ :: Proxy m) -> + property $ \(Edgy x :: Edgy a n) -> + maybe True isValidFinite $ unshiftN @n @m x +prop_finites_unshiftN = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + map (unshiftN @n @m @a) finites + === replicate (n - m) Nothing ++ drop (m - n) (map Just finites) + +prop_valid_weakenProxy = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \k (_ :: Proxy k) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + property $ \(Edgy x :: Edgy a n) -> + isValidFinite $ weakenProxy @n @k Proxy x +prop_finites_weakenProxy = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \k (_ :: Proxy k) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + map (weakenProxy @n @k @a Proxy) finites === take n finites + +prop_valid_strengthenProxy = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \k (_ :: Proxy k) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + property $ \(Edgy x :: Edgy a (n + k)) -> + maybe True isValidFinite $ strengthenProxy @n @k Proxy x +prop_finites_strengthenProxy = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \k (_ :: Proxy k) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + map (strengthenProxy @n @k @a Proxy) finites + === take n (map Just finites) ++ replicate k Nothing + +prop_valid_shiftProxy = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \k (_ :: Proxy k) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + property $ \(Edgy x :: Edgy a n) -> + isValidFinite $ shiftProxy @n @k Proxy x +prop_finites_shiftProxy = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \k (_ :: Proxy k) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + map (shiftProxy @n @k @a Proxy) finites === drop k finites + +prop_valid_unshiftProxy = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \k (_ :: Proxy k) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + property $ \(Edgy x :: Edgy a (n + k)) -> + maybe True isValidFinite $ unshiftProxy @n @k Proxy x +prop_finites_unshiftProxy = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \k (_ :: Proxy k) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + map (unshiftProxy @n @k @a Proxy) finites + === replicate k Nothing ++ map Just finites + +prop_strengthen_weaken = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + strengthen (weaken x) === Just x +prop_weaken_strengthen = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + property $ \(Edgy x :: Edgy a (n + 1)) -> + maybe True (== x) (weaken <$> strengthen x) + +prop_unshift_shift = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + property $ \(Edgy x :: Edgy a n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + unshift (shift x) === Just x +prop_shift_unshift = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @(n + 1) @a (n + 1) $ + property $ \(Edgy x :: Edgy a (n + 1)) -> + maybe True (== x) (shift <$> unshift x) + +prop_strengthenN_weakenN = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forPositiveLimit @a $ \m (_ :: Proxy m) -> + n <= m ==> unsafeWithInequality @n @m $ + property $ \(Edgy x :: Edgy a n) -> + strengthenN (weakenN @n @m x) === Just x +prop_weakenN_strengthenN = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \m (_ :: Proxy m) -> + m <= n ==> unsafeWithInequality @m @n $ + property $ \(Edgy x :: Edgy a n) -> + maybe True (== x) (weakenN <$> strengthenN @n @m x) + +prop_unshiftN_shiftN = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forPositiveLimit @a $ \m (_ :: Proxy m) -> + n <= m ==> unsafeWithInequality @n @m $ + property $ \(Edgy x :: Edgy a n) -> + unshiftN (shiftN @n @m x) === Just x +prop_shiftN_unshiftN = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \m (_ :: Proxy m) -> + m <= n ==> unsafeWithInequality @m @n $ + property $ \(Edgy x :: Edgy a n) -> + maybe True (== x) (shiftN <$> unshiftN @n @m x) + +prop_strengthenProxy_weakenProxy = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \k (_ :: Proxy k) -> + property $ \(Edgy x :: Edgy a n) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + strengthenProxy Proxy (weakenProxy @n @k Proxy x) === Just x +prop_weakenProxy_strengthenProxy = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \k (_ :: Proxy k) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + property $ \(Edgy x :: Edgy a (n + k)) -> + maybe True (== x) (weakenProxy Proxy <$> strengthenProxy @n @k Proxy x) + +prop_unshiftProxy_shiftProxy = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \k (_ :: Proxy k) -> + property $ \(Edgy x :: Edgy a n) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + unshiftProxy Proxy (shiftProxy @n @k Proxy x) === Just x +prop_shiftProxy_unshiftProxy = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \k (_ :: Proxy k) -> + unsafeWithKnownIntegral @(n + k) @a (n + k) $ + property $ \(Edgy x :: Edgy a (n + k)) -> + maybe True (== x) (shiftProxy Proxy <$> unshiftProxy @n @k Proxy x) + +prop_valid_add = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forPositiveLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n + m) @a (n + m) $ + property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) -> + isValidFinite $ add x y +prop_getFinite_add = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forPositiveLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n + m) @a (n + m) $ + property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) -> + getFinite (add x y) === getFinite x + getFinite y + +prop_valid_sub = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + forPositiveLimit @a $ \_ (_ :: Proxy m) -> + property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) -> + either isValidFinite isValidFinite $ sub x y +prop_getFinite_sub = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + forPositiveLimit @a $ \_ (_ :: Proxy m) -> + property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) -> + either (negate . toInteger . getFinite) (toInteger . getFinite) (sub x y) + === toInteger (getFinite x) - toInteger (getFinite y) +prop_sub_Left_0 = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \_ (_ :: Proxy n) -> + forPositiveLimit @a $ \_ (_ :: Proxy m) -> + property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) -> + sub x y =/= Left 0 + +prop_valid_multiply = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forPositiveLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $ + property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) -> + isValidFinite $ multiply x y +prop_getFinite_multiply = forType $ \(_ :: Proxy a) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + forPositiveLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $ + property $ \(Edgy x :: Edgy a n) (Edgy y :: Edgy a m) -> + getFinite (multiply x y) === getFinite x * getFinite y + +prop_valid_combineSum = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n + m) @a (n + m) $ + property $ \e -> + isValidFinite $ combineSum + $ bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) e +prop_finites_combineSum = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n + m) @a (n + m) $ + map (combineSum @n @m @a) (map Left finites ++ map Right finites) + === finites + +prop_valid_combineZero = forType $ \(_ :: Proxy a) -> + unsafeWithKnownIntegral @0 @a 0 $ + ioProperty $ evaluate (isValidFinite $ combineZero @a $ error "test") + `catch` \(ErrorCall msg) -> pure (msg == "test") +prop_finites_combineZero = forType $ \(_ :: Proxy a) -> + unsafeWithKnownIntegral @0 @a 0 $ + map (combineZero @a) [] === finites + +prop_valid_combineProduct = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $ + property $ \p -> + isValidFinite $ combineProduct + $ bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) p +prop_finites_combineProduct = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $ + map (combineProduct @n @m @a) [(x, y) | y <- finites, x <- finites] + === finites + +prop_valid_combineOne = forType $ \(_ :: Proxy a) -> + unsafeWithKnownIntegral @1 @a 1 $ + property $ isValidFinite $ combineOne @a () +prop_finites_combineOne = forType $ \(_ :: Proxy a) -> + unsafeWithKnownIntegral @1 @a 1 $ + property $ [combineOne @a ()] === finites + +prop_valid_combineExponential = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $ + property $ \(Blind (f :: Big a n -> Big a m)) -> + isValidFinite $ combineExponential (\x -> case f (Big x) of Big y -> y) +prop_finites_combineExponential = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + if m ^ n > 2000000 then property () else + m ^ n <= 10000 ==> + unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $ + property $ + [ combineExponential ((xs !!) . fromIntegral . getFinite @n @a) + | xs <- reverse <$> replicateM n (finites @m) + ] === finites + +prop_valid_separateSum = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n + m) @a (n + m) $ + property $ \(Edgy x :: Edgy a (n + m)) -> + either isValidFinite isValidFinite $ separateSum @n @m x +prop_finites_separateSum = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n + m) @a (n + m) $ + map (separateSum @n @m @a) finites === map Left finites ++ map Right finites + +prop_seq_separateZero = forType $ \(_ :: Proxy a) -> + unsafeWithKnownIntegral @0 @a 0 $ + ioProperty $ evaluate (absurd $ separateZero @a $ error "test") + `catch` \(ErrorCall msg) -> pure (msg == "test") +prop_finites_separateZero = forType $ \(_ :: Proxy a) -> + unsafeWithKnownIntegral @0 @a 0 $ + map (separateZero @a) finites === [] + +prop_valid_separateProduct = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $ + property $ \(Edgy x :: Edgy a (n GHC.TypeLits.* m)) -> + x -- could be discard + `seq` isValidFinite (fst $ separateProduct @n @m x) + .&&. isValidFinite (snd $ separateProduct @n @m x) +prop_finites_separateProduct = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $ + map (separateProduct @n @m @a) finites + === [(x, y) | y <- finites, x <- finites] + +prop_finites_separateOne = forType $ \(_ :: Proxy a) -> + unsafeWithKnownIntegral @1 @a 1 $ + map (separateOne @a) finites === [()] + +prop_valid_separateExponential = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $ + property $ \(Big f :: Big a (m ^ n)) (Big x :: Big a n) -> + f `seq` x -- could be discard + `seq` isValidFinite (separateExponential @n @m @a f x) +prop_finites_separateExponential = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + if m ^ n > 2000000 then property () else + m ^ n <= 10000 ==> + unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $ + map (<$> finites) (map (separateExponential @n @m @a) finites) + === [reverse xs | xs <- replicateM n finites] + +prop_combineSum_separateSum = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n + m) @a (n + m) $ + property $ \(Edgy x :: Edgy a (n + m)) -> + combineSum (separateSum @n @m x) === x +prop_separateSum_combineSum = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n + m) @a (n + m) $ + property $ \e -> + let x = bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) e in + separateSum (combineSum x) === x + +prop_combineProduct_separateProduct = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $ + property $ \(Edgy x :: Edgy a (n GHC.TypeLits.* m)) -> + x -- could be discard + `seq` combineProduct (separateProduct @n @m x) === x +prop_separateProduct_combineProduct = forType $ \(_ :: Proxy a) -> + forLimit @a $ \n (_ :: Proxy n) -> + forLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(n GHC.TypeLits.* m) @a (n * m) $ + property $ \p -> + let x = bimap (\(Edgy x :: Edgy a n) -> x) (\(Edgy y :: Edgy a m) -> y) p in + force x -- could be discard + `seq` separateProduct (combineProduct x) === x + +prop_combineOne_separateOne = forType $ \(_ :: Proxy a) -> + unsafeWithKnownIntegral @1 @a 1 $ + property $ \(Big x :: Big a 1) -> + combineOne (separateOne @a x) === x +prop_separateOne_combineOne = forType $ \(_ :: Proxy a) -> + unsafeWithKnownIntegral @1 @a 1 $ + property $ \x -> + separateOne (combineOne @a x) === x + +prop_separateExponential_combineExponential = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $ + property $ \(Blind (f :: Big a n -> Big a m)) -> + let f' x = case f (Big x) of Big y -> y in + force (f' <$> listToMaybe finites) -- could be discard + `seq` (separateExponential @n @m @a (combineExponential f') <$> finites) + === (f' <$> finites) +prop_combineExponential_separateExponential = forType $ \(_ :: Proxy a) -> + forSmallLimit @a $ \n (_ :: Proxy n) -> + forSmallLimit @a $ \m (_ :: Proxy m) -> + unsafeWithKnownIntegral @(m ^ n) @a (m ^ n) $ + property $ \(Big f :: Big a (m ^ n)) -> + f `seq` -- could be discard + combineExponential (separateExponential @n @m @a f) === f + +prop_valid_castFinite = forType $ \(_ :: Proxy b) -> + forType $ \(_ :: Proxy a) -> + forPositiveLimit @b $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @n @a n $ + property $ \(Edgy x :: Edgy a n) -> + isValidFinite $ castFinite @b x +prop_sym_castFinite = forType $ \(_ :: Proxy a) -> + forType $ \(_ :: Proxy b) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @n @b n $ + property $ \(Edgy x :: Edgy b n) -> + castFinite @b (castFinite @a x) === x +prop_trans_castFinite = forType $ \(_ :: Proxy a) -> + forType $ \(_ :: Proxy b) -> + forType $ \(_ :: Proxy c) -> + forPositiveLimit @a $ \n (_ :: Proxy n) -> + unsafeWithKnownIntegral @n @b n $ + unsafeWithKnownIntegral @n @c n $ + property $ \(Edgy x :: Edgy a n) -> + castFinite @c (castFinite @b x) === castFinite @c x + +return [] +main = $quickCheckAll >>= \case + True -> pure () + False -> exitFailure