fin 0.2 → 0.2.1

raw patch · 8 files changed

+142/−37 lines, 8 filesdep +boringdep +somedep ~basedep ~hashabledep ~inspection-testingPVP ok

version bump matches the API change (PVP)

Dependencies added: boring, some

Dependency ranges changed: base, hashable, inspection-testing, semigroups

API changes (from Hackage documentation)

Files

• ChangeLog.md +8/−0
• fin.cabal +7/−4
• src/Data/Fin.hs +11/−2
• src/Data/Nat.hs +6/−9
• src/Data/Type/Nat.hs +78/−16
• src/Data/Type/Nat/LE.hs +15/−3
• src/Data/Type/Nat/LE/ReflStep.hs +13/−1
• src/TrustworthyCompat.hs +4/−2

@@ -1,3 +1,11 @@+## 0.2.1++- Add `boring` instances+- Explicitly implement `>=` and `>` for `Nat`.+- `<=`, `>=` and `min` for `Nat` are lazier+- Add `NFData (SNat n)` instance+- Add `GEq`, `GCompare`, `GNFData`, `GShow` (from `some` package) instances for `SNat`.+ ## 0.2  - `SNat` is now what was called `InlineInduction`.

@@ -1,6 +1,6 @@ cabal-version:      >=1.10 name:               fin-version:            0.2+version:            0.2.1 synopsis:           Nat and Fin: peano naturals and finite numbers category:           Data, Dependent Types, Singletons, Math description:@@ -65,6 +65,7 @@    || ==8.8.4    || ==8.10.4    || ==9.0.1+   || ==9.2.1  source-repository head   type:     git@@ -86,18 +87,20 @@    other-modules:    TrustworthyCompat   build-depends:-      base           >=4.7     && <4.16+      base           >=4.7     && <4.17+    , boring         >=0.2     && <0.3     , dec            >=0.0.4   && <0.1     , deepseq        >=1.3.0.2 && <1.5-    , hashable       >=1.2.7.0 && <1.4+    , hashable       >=1.2.7.0 && <1.5     , QuickCheck     >=2.13.2  && <2.15+    , some           >=1.0.3   && <1.1     , universe-base  >=1.1.2   && <1.2    if !impl(ghc >=8.2)     build-depends: bifunctors >=5.5.3 && <5.6    if !impl(ghc >=8.0)-    build-depends: semigroups >=0.18.5 && <0.20+    build-depends: semigroups >=0.18.5 && <0.21    if !impl(ghc >=7.10)     build-depends:

@@ -61,6 +61,7 @@ import GHC.Exception      (ArithException (..), throw) import Numeric.Natural    (Natural) +import qualified Data.Boring           as Boring import qualified Data.List.NonEmpty    as NE import qualified Data.Type.Nat         as N import qualified Data.Universe.Class   as U@@ -213,6 +214,14 @@     hashWithSalt salt = hashWithSalt salt . cata (0 :: Integer) succ  -------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | @since 0.2.1+instance n ~ 'Z => Boring.Absurd (Fin n) where+    absurd = absurd++------------------------------------------------------------------------------- -- QuickCheck ------------------------------------------------------------------------------- @@ -239,8 +248,8 @@  instance (n ~ 'S m, N.SNatI m) => QC.Function (Fin n) where     function = case N.snat :: N.SNat m of-        N.SZ -> QC.functionMap (\FZ -> ()) (\() -> FZ)-        N.SS -> QC.functionMap isMin       (maybe FZ FS)+        N.SZ -> QC.functionMap (\_ -> ()) (\() -> FZ)+        N.SS -> QC.functionMap isMin      (maybe FZ FS)  -- TODO: https://github.com/nick8325/quickcheck/pull/283 -- newtype Fun b m = Fun { getFun :: (Fin ('S m) -> b) -> Fin ('S m) QC.:-> b }

@@ -63,18 +63,15 @@     compare (S _) Z     = GT     compare (S n) (S m) = compare n m -    Z   < Z   = False-    Z   < S _ = True-    S _ < Z   = False-    S n < S m = n < m--    Z   <= Z   = True-    Z   <= S _ = True+    Z   <= _   = True     S _ <= Z   = False     S n <= S m = n <= m -    min Z     Z     = Z-    min Z     (S _) = Z+    n <  m = not (m <= n)+    n >  m = not (n <= m)+    n >= m = m <= n++    min Z     _     = Z     min (S _) Z     = Z     min (S n) (S m) = S (min n m) 

@@ -38,6 +38,7 @@     eqNat,     EqNat,     discreteNat,+    cmpNat,     -- * Induction     induction1,     -- ** Example: unfoldedFix@@ -64,20 +65,21 @@     proofMultNOne,     )  where -import Data.Function   (fix)-import Data.Proxy      (Proxy (..))-import Data.Type.Dec   (Dec (..))-import Data.Typeable   (Typeable)-import Numeric.Natural (Natural)+import Control.DeepSeq   (NFData (..))+import Data.Boring       (Boring (..))+import Data.Function     (fix)+import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..))+import Data.GADT.DeepSeq (GNFData (..))+import Data.GADT.Show    (GShow (..))+import Data.Proxy        (Proxy (..))+import Data.Type.Dec     (Dec (..))+import Data.Typeable     (Typeable)+import Numeric.Natural   (Natural)  import qualified GHC.TypeLits as GHC  import Unsafe.Coerce (unsafeCoerce) -#if !MIN_VERSION_base(4,11,0)-import Data.Type.Equality (type (==))-#endif- import Data.Nat import TrustworthyCompat @@ -88,6 +90,7 @@ -- >>> import Data.Type.Equality -- >>> import Control.Applicative (Const (..)) -- >>> import Data.Coerce (coerce)+-- >>> import Data.GADT.Compare (GOrdering (..))  ------------------------------------------------------------------------------- -- SNat@@ -246,6 +249,65 @@ type instance n == m = EqNat n m #endif +-- | @since 0.2.1+instance SNatI n => Boring (SNat n) where+    boring = snat++-- | @since 0.2.1+instance GShow SNat where+    gshowsPrec = showsPrec++-- | @since 0.2.1+instance NFData (SNat n) where+    rnf SZ = ()+    rnf SS = ()++-- | @since 0.2.1+instance GNFData SNat where+    grnf = rnf++-- | @since 0.2.1+instance GEq SNat where+    geq = testEquality++-- | @since 0.2.1+instance GCompare SNat where+    gcompare SZ SZ = GEQ+    gcompare SZ SS = GLT+    gcompare SS SZ = GGT+    gcompare SS SS = cmpNat++-- | Decide equality of type-level numbers.+--+-- >>> cmpNat :: GOrdering Nat3 (Plus Nat1 Nat2)+-- GEQ+--+-- >>> cmpNat :: GOrdering Nat3 (Mult Nat2 Nat2)+-- GLT+--+-- >>> cmpNat :: GOrdering Nat5 (Mult Nat2 Nat2)+-- GGT+--+cmpNat :: forall n m. (SNatI n, SNatI m) => GOrdering n m+cmpNat = getNatCmp $ induction (NatCmp start) (\p -> NatCmp (step p)) where+    start :: forall p. SNatI p => GOrdering 'Z p+    start = case snat :: SNat p of+        SZ -> GEQ+        SS -> GLT++    step :: forall p q. SNatI q => NatCmp p -> GOrdering ('S p) q+    step hind = case snat :: SNat q of+        SZ -> GGT+        SS -> step' hind++    step' :: forall p q. SNatI q => NatCmp p -> GOrdering ('S p) ('S q)+    step' (NatCmp hind) = case hind :: GOrdering p q of+        GEQ -> GEQ+        GLT -> GLT+        GGT -> GGT++newtype NatCmp n = NatCmp { getNatCmp :: forall m. SNatI m => GOrdering n m }+ ------------------------------------------------------------------------------- -- Induction -------------------------------------------------------------------------------@@ -295,7 +357,7 @@ -- | Convert to GHC 'GHC.Nat'. -- -- >>> :kind! ToGHC Nat5--- ToGHC Nat5 :: GHC.Nat+-- ToGHC Nat5 :: GHC.Nat... -- = 5 -- type family ToGHC (n :: Nat) :: GHC.Nat where@@ -343,13 +405,13 @@  -- | Division by two. 'False' is 0 and 'True' is 1 as a remainder. ----- >>> :kind! DivMod2 Nat7--- DivMod2 Nat7 :: (Nat, Bool)--- = '( 'S ('S ('S 'Z)), 'True)+-- >>> :kind! DivMod2 Nat7 == '(Nat3, True)+-- DivMod2 Nat7 == '(Nat3, True) :: Bool+-- = 'True ----- >>> :kind! DivMod2 Nat4--- DivMod2 Nat4 :: (Nat, Bool)--- = '( 'S ('S 'Z), 'False)+-- >>> :kind! DivMod2 Nat4 == '(Nat2, False)+-- DivMod2 Nat4 == '(Nat2, False) :: Bool+-- = 'True -- type family DivMod2 (n :: Nat) :: (Nat, Bool) where     DivMod2 'Z          = '( 'Z, 'False)

@@ -49,9 +49,9 @@     proofZeroLEZero,     ) where -import Data.Type.Dec      (Dec (..), Decidable (..), Neg)-import Data.Typeable      (Typeable)-import Data.Void          (absurd)+import Data.Boring   (Boring (..), Absurd (..))+import Data.Type.Dec (Dec (..), Decidable (..), Neg)+import Data.Typeable (Typeable)  import Data.Type.Nat import TrustworthyCompat@@ -162,6 +162,18 @@ -- leSwap' :: LEProof n m -> LEProof ('S m) n -> void leSwap' p (LESucc q) = case p of LESucc p' -> leSwap' p' q++-------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | @since 0.2.1+instance LE n m => Boring (LEProof n m) where+    boring = leProof++-- | @since 0.2.1+instance (LE m n, n' ~ 'S n) => Absurd (LEProof n' m) where+    absurd = leSwap' leProof  ------------------------------------------------------------------------------- -- Dedidablity

@@ -36,9 +36,9 @@     proofZeroLEZero,     ) where +import Data.Boring   (Absurd (..), Boring (..)) import Data.Type.Dec (Dec (..), Decidable (..), Neg) import Data.Typeable (Typeable)-import Data.Void     (absurd)  import qualified Control.Category as C @@ -150,6 +150,18 @@ leSwap' :: LEProof n m -> LEProof ('S m) n -> void leSwap' p LERefl     = case p of LEStep p' -> leSwap' (leStepL p') LERefl leSwap' p (LEStep q) = leSwap' (leStepL p) q++-------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | @since 0.2.1+instance (ZeroSucc.LE n m, SNatI m) => Boring (LEProof n m) where+    boring = fromZeroSucc ZeroSucc.leProof++-- | @since 0.2.1+instance (ZeroSucc.LE m n, n' ~ 'S n, SNatI n) => Absurd (LEProof n' m) where+    absurd = ZeroSucc.leSwap' ZeroSucc.leProof . toZeroSucc  ------------------------------------------------------------------------------- -- Decidability

@@ -1,9 +1,11 @@-{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE Trustworthy        #-} module TrustworthyCompat (     (:~:) (..),     TestEquality (..),     coerce,+    type (==), ) where  import Data.Coerce        (coerce)-import Data.Type.Equality (TestEquality (..), (:~:) (..))+import Data.Type.Equality (TestEquality (..), type (==), (:~:) (..))