fin 0.0.1 → 0.0.2

raw patch · 6 files changed

+132/−64 lines, 6 filesdep +bifunctorsdep ~hashabledep ~inspection-testingdep ~semigroupssetup-changedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: bifunctors

Dependency ranges changed: hashable, inspection-testing, semigroups

API changes (from Hackage documentation)

Files

• ChangeLog.md +5/−0
• Setup.hs +0/−2
• fin.cabal +50/−57
• src/Data/Fin.hs +64/−0
• src/Data/Fin/Enum.hs +12/−4
• src/Data/Type/Nat.hs +1/−1

@@ -1,5 +1,10 @@ # Revision history for boring +## 0.0.2++- In `Fin` add: `append` and `split`+- Add `(Enum a, Enum b) => Enum (Either a b)` instance+ ## 0.0.1  - GHC-8.4.1 / base-4.11 support

@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain

@@ -1,6 +1,8 @@-name:                fin-version:             0.0.1-synopsis:            Nat and Fin: peano naturals and finite numbers+cabal-version:      >=1.10+name:               fin+version:            0.0.2+synopsis:           Nat and Fin: peano naturals and finite numbers+category:           Data description:   This package provides two simple types, and some tools to work with them.   Also on type level as @DataKinds@.@@ -31,40 +33,34 @@   . Is a great package, but uses @GHC.TypeLits@.   .   * [type-natural](https://hackage.haskell.org/package/type-natural) depends-    on @singletons@ package. @fin@ will try to stay light on the dependencies,-    and support as many GHC versions as practical.+  on @singletons@ package. @fin@ will try to stay light on the dependencies,+  and support as many GHC versions as practical.   .   * [peano](https://hackage.haskell.org/package/peano) is very incomplete   .   * [nat](https://hackage.haskell.org/package/nat) as well.   .   * [PeanoWitnesses](https://hackage.haskell.org/package/PeanoWitnesses)-    doesn't use @DataKinds@.+  doesn't use @DataKinds@.   .   * [type-combinators](https://hackage.haskell.org/package/type-combinators)-    is big package too.+  is big package too. -homepage:            https://github.com/phadej/vec-bug-reports:         https://github.com/phadej/vec/issues-license:             BSD3-license-file:        LICENSE-author:              Oleg Grenrus <oleg.grenrus@iki.fi>-maintainer:          Oleg.Grenrus <oleg.grenrus@iki.fi>-copyright:           (c) 2017 Oleg Grenrus-category:            Data-build-type:          Simple-extra-source-files:  ChangeLog.md-cabal-version:       >=1.10+homepage:           https://github.com/phadej/vec+bug-reports:        https://github.com/phadej/vec/issues+license:            BSD3+license-file:       LICENSE+author:             Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>+copyright:          (c) 2017 Oleg Grenrus+build-type:         Simple+extra-source-files: ChangeLog.md tested-with:-  GHC==7.8.4,-  GHC==7.10.3,-  GHC==8.0.2,-  GHC==8.2.2,-  GHC==8.4.1+  GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4  source-repository head-  type:      git-  location:  https://github.com/phadej/vec.git+  type:     git+  location: https://github.com/phadej/vec.git  library   exposed-modules:@@ -72,49 +68,46 @@     Data.Fin.Enum     Data.Nat     Data.Type.Nat+   build-depends:-    base     >=4.7     && <4.12,-    deepseq  >=1.3.0.2 && <1.5,-    hashable >=1.2.7.0 && <1.3+      base      >=4.7     && <4.13+    , deepseq   >=1.3.0.2 && <1.5+    , hashable  >=1.2.7.0 && <1.3 -  if !impl(ghc >= 8.0)-    build-depends:-      semigroups >=0.18.4 && <0.19+  if !impl(ghc >=8.2)+    build-depends: bifunctors >=5.5.3 && <5.6 -  if !impl(ghc >= 7.10)+  if !impl(ghc >=8.0)+    build-depends: semigroups >=0.18.4 && <0.19++  if !impl(ghc >=7.10)     build-depends:-       nats >=1.1.2 && <1.2,-       void >=0.7.2 && <0.8+        nats  >=1.1.2 && <1.2+      , void  >=0.7.2 && <0.8 -  ghc-options:         -Wall -fprint-explicit-kinds-  hs-source-dirs:      src-  default-language:    Haskell2010+  ghc-options:      -Wall -fprint-explicit-kinds+  hs-source-dirs:   src+  default-language: Haskell2010 -  -- dump-core-  -- if impl(ghc >= 8.0)-  --  build-depends: dump-core-  --  ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html+-- dump-core+-- if impl(ghc >= 8.0)+--  build-depends: dump-core+--  ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html  test-suite inspection-  type:                exitcode-stdio-1.0-  main-is:             Inspection.hs-  ghc-options:         -Wall -fprint-explicit-kinds-  hs-source-dirs:      test-  default-language:    Haskell2010+  type:             exitcode-stdio-1.0+  main-is:          Inspection.hs+  ghc-options:      -Wall -fprint-explicit-kinds+  hs-source-dirs:   test+  default-language: Haskell2010   build-depends:-    base,-    fin,-    tagged,-    inspection-testing >= 0.2.0.1 && <0.3+      base+    , fin+    , inspection-testing  >=0.2.0.1 && <0.5+    , tagged -  if !impl(ghc >= 8.0)+  if !impl(ghc >=8.0)     buildable: False    -- useful for development   ghc-options:-  -- -dsuppress-idinfo-  -- -dsuppress-coercions-  -- -dsuppress-type-applications-  -- -dsuppress-module-prefixes-  -- -dsuppress-type-signatures-  -- -dsuppress-uniques

@@ -28,11 +28,17 @@     inlineUniverse1,     absurd,     boring,+    -- * Plus+    weakenLeft,+    weakenRight,+    append,+    split,     -- * Aliases     fin0, fin1, fin2, fin3, fin4, fin5, fin6, fin7, fin8, fin9,     ) where  import Control.DeepSeq    (NFData (..))+import Data.Bifunctor     (bimap) import Data.Hashable      (Hashable (..)) import Data.List.NonEmpty (NonEmpty (..)) import Data.Proxy         (Proxy (..))@@ -283,6 +289,64 @@ -- 0 boring :: Fin N.Nat1 boring = Z++-------------------------------------------------------------------------------+-- Append & Split+-------------------------------------------------------------------------------++weakenLeft :: forall n m. N.InlineInduction n => Proxy m -> Fin n -> Fin (N.Plus n m)+weakenLeft _ = getWeakenLeft (N.inlineInduction start step :: WeakenLeft m n) where+    start :: WeakenLeft m 'N.Z+    start = WeakenLeft absurd++    step :: WeakenLeft m p -> WeakenLeft m ('N.S p)+    step (WeakenLeft go) = WeakenLeft $ \n -> case n of+        Z    -> Z+        S n' -> S (go n')++newtype WeakenLeft m n = WeakenLeft { getWeakenLeft :: Fin n -> Fin (N.Plus n m) }++weakenRight :: forall n m. N.InlineInduction n => Proxy n -> Fin m -> Fin (N.Plus n m)+weakenRight _ = getWeakenRight (N.inlineInduction start step :: WeakenRight m n) where+    start = WeakenRight id+    step (WeakenRight go) = WeakenRight $ \x -> S $ go x++newtype WeakenRight m n = WeakenRight { getWeakenRight :: Fin m -> Fin (N.Plus n m) }++-- | Append two 'Fin's together.+--+-- >>> append (Left fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))+-- 2+--+-- >>> append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))+-- 7+--+append :: forall n m. N.InlineInduction n => Either (Fin n) (Fin m) -> Fin (N.Plus n m)+append (Left n)  = weakenLeft (Proxy :: Proxy m) n+append (Right m) = weakenRight (Proxy :: Proxy n) m++-- | Inverse of 'append'.+--+-- >>> split fin2 :: Either (Fin N.Nat2) (Fin N.Nat3)+-- Right 0+--+-- >>> split fin1 :: Either (Fin N.Nat2) (Fin N.Nat3)+-- Left 1+--+-- >>> map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)]+-- [Left 0,Left 1,Right 0,Right 1,Right 2]+--+split :: forall n m. N.InlineInduction n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)+split = getSplit (N.inlineInduction start step) where+    start :: Split m 'N.Z+    start = Split Right++    step :: Split m p -> Split m ('N.S p)+    step (Split go) = Split $ \x -> case x of+        Z    -> Left Z+        S x' -> bimap S id $ go x'++newtype Split m n = Split { getSplit :: Fin (N.Plus n m) -> Either (Fin n) (Fin m) }  ------------------------------------------------------------------------------- -- Aliases

@@ -27,10 +27,11 @@  import Prelude hiding (Enum (..)) -import Data.Fin     (Fin)-import Data.Nat     (Nat)-import Data.Proxy   (Proxy (..))-import GHC.Generics ((:+:) (..), M1 (..), U1 (..), V1)+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@@ -86,6 +87,13 @@  -- | 'Ordering' ~ 3 instance Enum Ordering++-- | 'Either' ~ @+@+instance (Enum a, Enum b, N.InlineInduction (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

@@ -341,7 +341,7 @@ proofMultZeroN :: Mult Nat0 n :~: Nat0 proofMultZeroN = Refl --- | @n * 0 = n@+-- | @n * 0 = 0@ proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0 proofMultNZero _ =     getProofMultNZero (induction (ProofMultNZero Refl) step :: ProofMultNZero n)