bin 0.1.1 → 0.1.2

raw patch · 7 files changed

+199/−47 lines, 7 filesdep +boringdep +somedep ~basedep ~hashablePVP ok

version bump matches the API change (PVP)

Dependencies added: boring, some

Dependency ranges changed: base, hashable

API changes (from Hackage documentation)

Files

• ChangeLog.md +7/−0
• bin.cabal +7/−4
• src/Data/Bin/Pos.hs +18/−0
• src/Data/BinP/PosP.hs +21/−0
• src/Data/Type/Bin.hs +84/−33
• src/Data/Type/BinP.hs +58/−8
• src/TrustworthyCompat.hs +4/−2

@@ -1,5 +1,12 @@ # Version history for bin +## 0.1.2++- Add `boring` instances+- Add `EqBinP` and `EqBin` type families+- Add `NFData` instances+- Add `GEq`, `GNFData`, `GShow` (from `some` package) instances for `SBin` and `SBinP`.+ ## 0.1.1  - Explicitly mark all modules as Safe or Trustworthy.

@@ -1,6 +1,6 @@ cabal-version:      2.2 name:               bin-version:            0.1.1+version:            0.1.2 synopsis:           Bin: binary natural numbers. category:           Data, Dependent Types, Singletons, Math description:@@ -43,6 +43,7 @@    || ==8.8.4    || ==8.10.4    || ==9.0.1+   || ==9.2.1  source-repository head   type:     git@@ -64,17 +65,19 @@    other-modules:    TrustworthyCompat   build-depends:-    , base        >=4.7     && <4.16+    , base        >=4.7     && <4.17+    , boring      ^>=0.2     , dec         ^>=0.0.3     , deepseq     >=1.3.0.2 && <1.5     , fin         ^>=0.2-    , hashable    >=1.2.7.0 && <1.4+    , hashable    >=1.2.7.0 && <1.5     , QuickCheck  ^>=2.14.2+    , some        ^>=1.0.3    if !impl(ghc >=7.10)     build-depends: nats ^>=1.1.2 -  if impl(ghc >= 9.0)+  if impl(ghc >=9.0)     -- these flags may abort compilation with GHC-8.10     -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295     ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode

@@ -32,12 +32,14 @@        (Bounded (..), Eq, Int, Integer, Ord (..), Show (..), ShowS, String,        fmap, fromIntegral, map, showParen, showString, ($), (.)) +import Control.DeepSeq (NFData (..)) import Data.Bin        (Bin (..), BinP (..)) import Data.BinP.PosP  (PosP (..)) import Data.Typeable   (Typeable) import Numeric.Natural (Natural)  import qualified Data.BinP.PosP  as PP+import qualified Data.Boring     as Boring import qualified Data.Type.Bin   as B import qualified Data.Type.BinP  as BP import qualified Test.QuickCheck as QC@@ -79,6 +81,10 @@     minBound = Pos minBound     maxBound = Pos maxBound +-- | @since 0.1.2+instance NFData (Pos b) where+    rnf (Pos p) = rnf p+ ------------------------------------------------------------------------------- -- QuickCheck -------------------------------------------------------------------------------@@ -185,6 +191,18 @@ -- weakenRight1 :: SBinPI b => Pos ('BP b) -> Pos (Succ'' b) weakenRight1 (Pos b) = Pos (PP.weakenRight1 b)++-------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | @since 0.1.2+instance b ~ 'BP 'BE => Boring.Boring (Pos b) where+    boring = boring++-- | @since 0.1.2+instance b ~ 'BZ => Boring.Absurd (Pos b) where+    absurd = absurd  ------------------------------------------------------------------------------- -- Universe

@@ -35,6 +35,7 @@        Ordering (..), Show (..), ShowS, String, either, fmap, fromIntegral, map,        showParen, showString, ($), (*), (+), (++), (.)) +import Control.DeepSeq (NFData (..)) import Data.Bin        (BinP (..)) import Data.Nat        (Nat (..)) import Data.Proxy      (Proxy (..))@@ -43,6 +44,7 @@ import Numeric.Natural (Natural)  import qualified Data.Bin        as B+import qualified Data.Boring     as Boring import qualified Data.Type.Bin   as B import qualified Data.Type.BinP  as BP import qualified Data.Type.Nat   as N@@ -107,6 +109,17 @@         SB0 -> There0 maxBound         SB1 -> There1 maxBound +-- | @since 0.1.2+instance NFData (PosP b) where+    rnf (PosP p) = rnf p++-- | @since 0.1.2+instance NFData (PosP' n b) where+    rnf (AtEnd w)  = rnf w+    rnf (Here w)   = rnf w+    rnf (There1 p) = rnf p+    rnf (There0 p) = rnf p+ ------------------------------------------------------------------------------- -- QuickCheck -------------------------------------------------------------------------------@@ -277,6 +290,14 @@     B.SBE -> map AtEnd W.universe     B.SB0 -> map There0 universe'     B.SB1 -> map Here W.universe ++ map There1 universe'++-------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | @since 0.1.2+instance b ~ 'BE => Boring.Boring (PosP b) where+    boring = boring  ------------------------------------------------------------------------------- -- Helpers

@@ -6,6 +6,7 @@ {-# LANGUAGE KindSignatures       #-} {-# LANGUAGE RankNTypes           #-} {-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE StandaloneDeriving   #-} {-# LANGUAGE TypeFamilies         #-} {-# LANGUAGE TypeOperators        #-} {-# LANGUAGE UndecidableInstances #-}@@ -28,6 +29,7 @@     reflectToNum,     -- * Type equality     eqBin,+    EqBin,     -- * Induction     induction,     -- * Arithmetic@@ -49,12 +51,17 @@     Bin0, Bin1, Bin2, Bin3, Bin4, Bin5, Bin6, Bin7, Bin8, Bin9,     ) where -import Data.Bin        (Bin (..), BinP (..))-import Data.Nat        (Nat (..))-import Data.Proxy      (Proxy (..))-import Data.Type.BinP  (SBinP (..), SBinPI (..))-import Data.Typeable   (Typeable)-import Numeric.Natural (Natural)+import Control.DeepSeq   (NFData (..))+import Data.Bin          (Bin (..), BinP (..))+import Data.Boring       (Boring (..))+import Data.GADT.Compare (GEq (..))+import Data.GADT.DeepSeq (GNFData (..))+import Data.GADT.Show    (GShow (..))+import Data.Nat          (Nat (..))+import Data.Proxy        (Proxy (..))+import Data.Type.BinP    (SBinP (..), SBinPI (..))+import Data.Typeable     (Typeable)+import Numeric.Natural   (Natural)  import qualified Data.Type.BinP as BP import qualified Data.Type.Nat  as N@@ -63,10 +70,11 @@ import TrustworthyCompat  -- $setup--- >>> :set -XDataKinds+-- >>> :set -XDataKinds -XExplicitNamespaces -XTypeOperators -- >>> import Data.Bin--- >>> import Data.Type.BinP (BinP2, BinP3)+-- >>> import Data.Type.BinP (BinP2, BinP3, BinP9) -- >>> import Data.Nat (Nat (..))+-- >>> import Data.Type.Equality (type (==)) -- >>> import qualified Data.Type.BinP as BP -- >>> import qualified Data.Type.Nat as N -- >>> import qualified GHC.TypeLits as GHC@@ -81,6 +89,8 @@     SBP :: SBinPI b => SBin ('BP b)   deriving (Typeable) +deriving instance Show (SBin b)+ ------------------------------------------------------------------------------- -- Implicits -------------------------------------------------------------------------------@@ -168,6 +178,16 @@             return Refl     testEquality _   _   = Nothing +-- | @since 0.1.2+type family EqBin (n :: Bin) (m :: Bin) where+    EqBin 'BZ     'BZ     = 'True+    EqBin ('BP n) ('BP m) = BP.EqBinP n m+    EqBin n       m       = 'False++#if !MIN_VERSION_base(4,11,0)+type instance n == m = EqBin n m+#endif+ ------------------------------------------------------------------------------- -- Induction -------------------------------------------------------------------------------@@ -197,7 +217,7 @@ -- | Convert to GHC 'GHC.Nat'. -- -- >>> :kind! ToGHC Bin5--- ToGHC Bin5 :: GHC.Nat+-- ToGHC Bin5 :: GHC.Nat... -- = 5 -- type family ToGHC (b :: Bin) :: GHC.Nat where@@ -266,13 +286,14 @@  -- | Multiply by two. ----- >>> :kind! Mult2 Bin0--- Mult2 Bin0 :: Bin--- = 'BZ+-- >>> :kind! Mult2 Bin0 == Bin0+-- Mult2 Bin0 == Bin0 :: Bool+-- = 'True ----- >>> :kind! Mult2 Bin7--- Mult2 Bin7 :: Bin--- = 'BP ('B0 ('B1 BinP3))+-- >>> :kind! Mult2 Bin3 == Bin6+-- Mult2 Bin3 == Bin6 :: Bool+-- = 'True+-- type family Mult2 (b :: Bin) :: Bin where     Mult2 'BZ     = 'BZ     Mult2 ('BP n) = 'BP ('B0 n)@@ -283,9 +304,10 @@ -- Mult2Plus1 Bin0 :: BinP -- = 'BE ----- >>> :kind! Mult2Plus1 Bin5--- Mult2Plus1 Bin5 :: BinP--- = 'B1 ('B1 BinP2)+-- >>> :kind! Mult2Plus1 Bin4 == BinP9+-- Mult2Plus1 Bin4 == BinP9 :: Bool+-- = 'True+-- type family Mult2Plus1 (b :: Bin) :: BinP where     Mult2Plus1 'BZ     = 'BE     Mult2Plus1 ('BP n) = ('B1 n)@@ -331,17 +353,17 @@ -- Pred BP.BinP1 :: Bin -- = 'BZ ----- >>> :kind! Pred BP.BinP5--- Pred BP.BinP5 :: Bin--- = 'BP ('B0 ('B0 BP.BinP1))+-- >>> :kind! Pred BP.BinP5 == Bin4+-- Pred BP.BinP5 == Bin4 :: Bool+-- = 'True ----- >>> :kind! Pred BP.BinP8--- Pred BP.BinP8 :: Bin--- = 'BP ('B1 ('B1 'BE))+-- >>> :kind! Pred BP.BinP8 == Bin7+-- Pred BP.BinP8 == Bin7 :: Bool+-- = 'True ----- >>> :kind! Pred BP.BinP6--- Pred BP.BinP6 :: Bin--- = 'BP ('B1 ('B0 'BE))+-- >>> :kind! Pred BP.BinP6 == Bin5+-- Pred BP.BinP6 == Bin5 :: Bool+-- = 'True -- type family Pred (b :: BinP) :: Bin where     Pred 'BE     = 'BZ@@ -359,18 +381,47 @@  -- | Addition. ----- >>> :kind! Plus Bin7 Bin7--- Plus Bin7 Bin7 :: Bin--- = 'BP ('B0 ('B1 ('B1 'BE)))+-- >>> :kind! Plus Bin3 Bin3 == Bin6+-- Plus Bin3 Bin3 == Bin6 :: Bool+-- = 'True ----- >>> :kind! Mult2 Bin7--- Mult2 Bin7 :: Bin--- = 'BP ('B0 ('B1 BinP3))+-- >>> :kind! Mult2 Bin3 == Bin6+-- Mult2 Bin3 == Bin6 :: Bool+-- = 'True -- type family Plus (a :: Bin) (b :: Bin) :: Bin where     Plus 'BZ     b       = b     Plus a       'BZ     = a     Plus ('BP a) ('BP b) = 'BP (BP.Plus a b)++-------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | @since 0.1.2+instance SBinI b => Boring (SBin b) where+    boring = sbin++-------------------------------------------------------------------------------+-- some+-------------------------------------------------------------------------------++-- | @since 0.1.2+instance GShow SBin where+    gshowsPrec = showsPrec++-- | @since 0.1.2+instance NFData (SBin n) where+    rnf SBZ = ()+    rnf SBP = ()++-- | @since 0.1.2+instance GNFData SBin where+    grnf = rnf++-- | @since 0.1.2+instance GEq SBin where+    geq = testEquality  ------------------------------------------------------------------------------- --- Aliases of Bin

@@ -6,6 +6,7 @@ {-# LANGUAGE KindSignatures       #-} {-# LANGUAGE RankNTypes           #-} {-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE StandaloneDeriving   #-} {-# LANGUAGE TypeFamilies         #-} {-# LANGUAGE TypeOperators        #-} {-# LANGUAGE UndecidableInstances #-}@@ -28,6 +29,7 @@     reflectToNum,     -- * Type equality     eqBinP,+    EqBinP,     -- * Induction     induction,     -- * Arithmetic@@ -45,11 +47,16 @@     BinP1, BinP2, BinP3, BinP4, BinP5, BinP6, BinP7, BinP8, BinP9,     ) where -import Data.BinP       (BinP (..))-import Data.Nat        (Nat (..))-import Data.Proxy      (Proxy (..))-import Data.Typeable   (Typeable)-import Numeric.Natural (Natural)+import Control.DeepSeq   (NFData (..))+import Data.BinP         (BinP (..))+import Data.Boring       (Boring (..))+import Data.GADT.Compare (GEq (..))+import Data.GADT.DeepSeq (GNFData (..))+import Data.GADT.Show    (GShow (..))+import Data.Nat          (Nat (..))+import Data.Proxy        (Proxy (..))+import Data.Typeable     (Typeable)+import Numeric.Natural   (Natural)  import qualified Data.Type.Nat as N import qualified GHC.TypeLits  as GHC@@ -71,15 +78,17 @@     SB1 :: SBinPI b => SBinP ('B1 b)   deriving (Typeable) +deriving instance Show (SBinP b)+ ------------------------------------------------------------------------------- -- Implicits -------------------------------------------------------------------------------  -- | Let constraint solver construct 'SBinP'. class                SBinPI (b :: BinP) where sbinp :: SBinP b-instance             SBinPI 'BE          where sbinp = SBE-instance SBinPI b => SBinPI ('B0 b)      where sbinp = SB0-instance SBinPI b => SBinPI ('B1 b)      where sbinp = SB1+instance             SBinPI 'BE         where sbinp = SBE+instance SBinPI b => SBinPI ('B0 b)     where sbinp = SB0+instance SBinPI b => SBinPI ('B1 b)     where sbinp = SB1  ------------------------------------------------------------------------------- -- Conversions@@ -146,6 +155,17 @@      testEquality _ _ = Nothing +-- | @since 0.1.2+type family EqBinP (n :: BinP) (m :: BinP) where+    EqBinP 'BE 'BE         = 'True+    EqBinP ('B0 n) ('B0 m) = EqBinP n m+    EqBinP ('B1 n) ('B1 m) = EqBinP n m+    EqBinP n       m       = 'False++#if !MIN_VERSION_base(4,11,0)+type instance n == m = EqBinP n m+#endif+ ------------------------------------------------------------------------------- -- Convert to GHC Nat -------------------------------------------------------------------------------@@ -249,6 +269,36 @@         SBE -> e         SB0 -> o go         SB1 -> i go++-------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | @since 0.1.2+instance SBinPI b => Boring (SBinP b) where+    boring = sbinp++-------------------------------------------------------------------------------+-- some+-------------------------------------------------------------------------------++-- | @since 0.1.2+instance GShow SBinP where+    gshowsPrec = showsPrec++-- | @since 0.1.2+instance NFData (SBinP n) where+    rnf SBE = ()+    rnf SB0 = ()+    rnf SB1 = ()++-- | @since 0.1.2+instance GNFData SBinP where+    grnf = rnf++-- | @since 0.1.2+instance GEq SBinP where+    geq = testEquality  ------------------------------------------------------------------------------- -- Aliases of BinP

@@ -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 (==), (:~:) (..))