fin 0.2.1 → 0.3

raw patch · 6 files changed

+94/−206 lines, 6 filesdep ~basedep ~bifunctorsdep ~deepseqPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, bifunctors, deepseq, some

API changes (from Hackage documentation)

Files

• ChangeLog.md +6/−0
• fin.cabal +9/−8
• src/Data/Fin.hs +56/−0
• src/Data/Fin/Enum.hs +0/−177
• src/Data/Type/Nat.hs +23/−0
• test/Inspection.hs +0/−21

@@ -1,3 +1,9 @@+## 0.3++- Remove `Data.Fin.Enum` module. It didn't work as well as hoped.+- Add `EqP` and `OrdP` instances.+- Add `GShow Fin` instance.+ ## 0.2.1  - Add `boring` instances

@@ -1,6 +1,6 @@ cabal-version:      >=1.10 name:               fin-version:            0.2.1+version:            0.3 synopsis:           Nat and Fin: peano naturals and finite numbers category:           Data, Dependent Types, Singletons, Math description:@@ -63,9 +63,11 @@    || ==8.4.4    || ==8.6.5    || ==8.8.4-   || ==8.10.4-   || ==9.0.1-   || ==9.2.1+   || ==8.10.7+   || ==9.0.2+   || ==9.2.7+   || ==9.4.4+   || ==9.6.1  source-repository head   type:     git@@ -78,7 +80,6 @@   hs-source-dirs:   src   exposed-modules:     Data.Fin-    Data.Fin.Enum     Data.Nat     Data.Type.Nat     Data.Type.Nat.LE@@ -87,13 +88,13 @@    other-modules:    TrustworthyCompat   build-depends:-      base           >=4.7     && <4.17+      base           >=4.7     && <4.19     , boring         >=0.2     && <0.3     , dec            >=0.0.4   && <0.1     , deepseq        >=1.3.0.2 && <1.5     , hashable       >=1.2.7.0 && <1.5     , QuickCheck     >=2.13.2  && <2.15-    , some           >=1.0.3   && <1.1+    , some           >=1.0.4   && <1.1     , universe-base  >=1.1.2   && <1.2    if !impl(ghc >=8.2)@@ -126,7 +127,7 @@   build-depends:       base     , fin-    , inspection-testing  >=0.2.0.1 && <0.5+    , inspection-testing  >=0.2.0.1 && <0.6     , tagged    if !impl(ghc >=8.0)

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP                  #-} {-# LANGUAGE DataKinds            #-} {-# LANGUAGE DeriveDataTypeable   #-} {-# LANGUAGE EmptyCase            #-}@@ -53,6 +54,7 @@  import Control.DeepSeq    (NFData (..)) import Data.Bifunctor     (bimap)+import Data.GADT.Show     (GShow (..)) import Data.Hashable      (Hashable (..)) import Data.List.NonEmpty (NonEmpty (..)) import Data.Proxy         (Proxy (..))@@ -61,6 +63,11 @@ import GHC.Exception      (ArithException (..), throw) import Numeric.Natural    (Natural) +#if MIN_VERSION_some(1,0,5)+import Data.EqP  (EqP (..))+import Data.OrdP (OrdP (..))+#endif+ import qualified Data.Boring           as Boring import qualified Data.List.NonEmpty    as NE import qualified Data.Type.Nat         as N@@ -71,10 +78,14 @@ -- $setup -- >>> import Data.List (genericLength) -- >>> import Data.List.NonEmpty (NonEmpty (..))+-- >>> import Data.Foldable (traverse_) -- >>> import Numeric.Natural (Natural) -- >>> import qualified Data.Type.Nat as N -- >>> import qualified Data.Universe.Class as U -- >>> import qualified Data.Universe.Helpers as U+-- >>> import Data.EqP (eqp)+-- >>> import Data.OrdP (comparep)+-- >>> :set -XTypeApplications  ------------------------------------------------------------------------------- -- Type@@ -93,11 +104,56 @@ deriving instance Eq (Fin n) deriving instance Ord (Fin n) +#if MIN_VERSION_some(1,0,5)++-- |+--+-- >>> eqp FZ FZ+-- True+--+-- >>> eqp FZ (FS FZ)+-- False+--+-- >>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]+-- [True,False,False,False,False,False]+-- [False,True,False,False,False,False]+-- [False,False,True,False,False,False]+-- [False,False,False,True,False,False]+--+-- @since 0.2.2+--+instance EqP Fin where+    eqp FZ     FZ     = True+    eqp FZ     (FS _) = False+    eqp (FS _) FZ     = False+    eqp (FS n) (FS m) = eqp n m++-- |+--+-- >>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]+-- [EQ,LT,LT,LT,LT,LT]+-- [GT,EQ,LT,LT,LT,LT]+-- [GT,GT,EQ,LT,LT,LT]+-- [GT,GT,GT,EQ,LT,LT]+--+-- @since 0.2.2+instance OrdP Fin where+    comparep FZ     FZ     = EQ+    comparep FZ     (FS _) = LT+    comparep (FS _) FZ     = GT+    comparep (FS n) (FS m) = comparep n m++#endif+ -- | 'Fin' is printed as 'Natural'. -- -- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec' instance Show (Fin n) where     showsPrec d  = showsPrec d . toNatural++-- | @since 0.2.2+instance GShow Fin where+    gshowsPrec = showsPrec  -- | Operations module @n@. --

@@ -1,177 +0,0 @@-{-# LANGUAGE ConstraintKinds       #-}-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE DefaultSignatures     #-}-{-# LANGUAGE EmptyCase             #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds             #-}-{-# LANGUAGE Safe                  #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeFamilies          #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE UndecidableInstances  #-}--- |------ This module is designed to be imported qualified:------ @--- import qualified Data.Fin.Enum as E--- @----module Data.Fin.Enum (-    Enum (..),-    -- * Generic implementation-    gfrom, GFrom,-    gto, GTo,-    GEnumSize,-    ) where--import Prelude hiding (Enum (..))--import Data.Bifunctor (bimap)-import Data.Fin       (Fin (..))-import Data.Nat       (Nat (..))-import Data.Proxy     (Proxy (..))-import GHC.Generics   (M1 (..), U1 (..), V1, (:+:) (..))--import qualified Data.Fin      as F-import qualified Data.Type.Nat as N-import qualified Data.Void     as V-import qualified GHC.Generics  as G---- $setup--- >>> import qualified Data.Fin as F---- | Generic enumerations.------ /Examples:/------ >>> from ()--- 0------ >>> to 0 :: ()--- ()------ >>> to 0 :: Bool--- False------ >>> map to F.universe :: [Bool]--- [False,True]------ >>> map (to . (+1) . from) [LT, EQ, GT] :: [Ordering] -- Num Fin is modulo arithmetic--- [EQ,GT,LT]----class Enum a where-    -- | The size of an enumeration.-    type EnumSize a :: Nat-    type EnumSize a = GEnumSize a--    -- | Converts a value to its index.-    from :: a -> Fin (EnumSize a)-    default from :: (G.Generic a, GFrom a, EnumSize a ~ GEnumSize a) => a -> Fin (EnumSize a)-    from = gfrom--    -- | Converts from index to the original value.-    to :: Fin (EnumSize a) -> a-    default to :: (G.Generic a, GTo a, EnumSize a ~ GEnumSize a) => Fin (EnumSize a) -> a-    to = gto---- | 'Void' ~ 0-instance Enum V.Void where-    -- this should be written by hand to work with all @base@-    type EnumSize V.Void = N.Nat0-    from = V.absurd-    to   = F.absurd---- | () ~ 1-instance Enum ()---- | 'Bool' ~ 2-instance Enum Bool---- | 'Ordering' ~ 3-instance Enum Ordering---- | 'Either' ~ @+@-instance (Enum a, Enum b, N.SNatI (EnumSize a)) => Enum (Either a b) where-    type EnumSize (Either a b) = N.Plus (EnumSize a) (EnumSize b)--    to   = bimap to to . F.split-    from = F.append . bimap from from------------------------------------------------------------------------------------ EnumSize------------------------------------------------------------------------------------ | Compute the size from the type.-type GEnumSize a = EnumSizeRep (G.Rep a) N.Nat0--type family EnumSizeRep (a :: * -> *) (n :: Nat) :: Nat where-    EnumSizeRep (a :+: b )   n = EnumSizeRep a (EnumSizeRep b n)-    EnumSizeRep V1           n = n-    EnumSizeRep (M1 _d _c a) n = EnumSizeRep a n-    EnumSizeRep U1           n = 'S n-    -- No instance for K1 or :*:------------------------------------------------------------------------------------ From------------------------------------------------------------------------------------ | Generic version of 'from'.-gfrom :: (G.Generic a, GFrom a) => a -> Fin (GEnumSize a)-gfrom = \x -> gfromRep (G.from x) (Proxy :: Proxy N.Nat0)---- | Constraint for the class that computes 'gfrom'.-type GFrom a = GFromRep (G.Rep a)--class GFromRep (a :: * -> *)  where-    gfromRep  :: a x     -> Proxy n -> Fin (EnumSizeRep a n)-    gfromSkip :: Proxy a -> Fin n   -> Fin (EnumSizeRep a n)--instance (GFromRep a, GFromRep b) => GFromRep (a :+: b) where-    gfromRep (L1 a) n = gfromRep a (prSkip n) where-        prSkip :: Proxy n -> Proxy (EnumSizeRep b n)-        prSkip  _ = Proxy-    gfromRep (R1 b) n = gfromSkip (Proxy :: Proxy a) (gfromRep b n)--    gfromSkip _ n = gfromSkip (Proxy :: Proxy a) (gfromSkip (Proxy :: Proxy b) n)--instance GFromRep a => GFromRep (M1 d c a) where-    gfromRep (M1 a) n = gfromRep a n-    gfromSkip _     n = gfromSkip (Proxy :: Proxy a) n--instance GFromRep V1 where-    gfromRep  v _ = case v of {}-    gfromSkip _ n = n--instance GFromRep U1 where-    gfromRep U1 _ = FZ-    gfromSkip _ n = FS n------------------------------------------------------------------------------------ To------------------------------------------------------------------------------------ | Generic version of 'to'.-gto :: (G.Generic a, GTo a) => Fin (GEnumSize a) -> a-gto = \x -> G.to $ gtoRep x id F.absurd---- | Constraint for the class that computes 'gto'.-type GTo a = GToRep (G.Rep a)--class GToRep (a :: * -> *) where-    gtoRep :: Fin (EnumSizeRep a n) -> (a x -> r) -> (Fin n -> r) -> r--instance (GToRep a, GToRep b) => GToRep (a :+: b) where-    gtoRep n s k = gtoRep n (s . L1) $ \r -> gtoRep r (s . R1) k--instance GToRep a => GToRep (M1 d c a) where-    gtoRep n s = gtoRep n (s . M1)--instance GToRep V1 where-    gtoRep n _ k = k n--instance GToRep U1 where-    gtoRep FZ     s _ = s U1-    gtoRep (FS n) _ k = k n

@@ -76,6 +76,12 @@ import Data.Typeable     (Typeable) import Numeric.Natural   (Natural) +#if MIN_VERSION_some(1,0,5)+import Data.EqP          (EqP (..))+import Data.OrdP         (OrdP (..))+import Data.GADT.Compare (defaultCompare, defaultEq)+#endif+ import qualified GHC.TypeLits as GHC  import Unsafe.Coerce (unsafeCoerce)@@ -266,6 +272,7 @@ instance GNFData SNat where     grnf = rnf + -- | @since 0.2.1 instance GEq SNat where     geq = testEquality@@ -276,6 +283,22 @@     gcompare SZ SS = GLT     gcompare SS SZ = GGT     gcompare SS SS = cmpNat++-- | @since 0.2.2+instance Eq (SNat a) where+    _ == _ = True++-- | @since 0.2.2+instance Ord (SNat a) where+    compare _ _ = EQ++#if MIN_VERSION_some(1,0,5)+-- | @since 0.2.2+instance EqP SNat where eqp = defaultEq++-- | @since 0.2.2+instance OrdP SNat where comparep = defaultCompare+#endif  -- | Decide equality of type-level numbers. --

@@ -17,7 +17,6 @@ import Test.Inspection  import qualified Data.Fin      as F-import qualified Data.Fin.Enum as E import qualified Data.Type.Nat as N  import Unsafe.Coerce (unsafeCoerce)@@ -51,26 +50,6 @@  inspect $ 'lhsInline === 'rhs inspect $ 'lhsNormal =/= 'rhs------------------------------------------------------------------------------------ Enum------------------------------------------------------------------------------------ | Note: GHC 8.0 (but not GHC 8.2?) seems to be--- so smart, it reuses dictionary value.------ Therefore, we define own local Ordering'-data Ordering' = LT' | EQ' | GT' deriving (Generic)--lhsEnum :: Ordering' -> F.Fin N.Nat3-lhsEnum = E.gfrom--rhsEnum :: Ordering' -> F.Fin N.Nat3-rhsEnum LT' = FZ-rhsEnum EQ' = FS FZ-rhsEnum GT' = FS (FS FZ)--inspect $ 'lhsEnum ==- 'rhsEnum  ------------------------------------------------------------------------------- -- Proofs