lean-peano 0.1.0.0 → 0.1.0.1

raw patch · 4 files changed

+47/−9 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +4/−0
• lean-peano.cabal +2/−2
• src/Numeric/Peano.hs +11/−5
• src/Numeric/Peano/Typelevel.hs +30/−2

@@ -1,1 +1,5 @@+[![Hackage](https://img.shields.io/hackage/v/lean-peano.svg)](https://hackage.haskell.org/package/lean-peano)+ # lean-peano++Implementation of peano numbers (with all relevant instances) with minimal dependencies.

@@ -7,8 +7,8 @@ -- hash: 64e91e616abbba7139ad4f000d8a6a1505b2a315175f0489493a319d6a76ac89  name:           lean-peano-version:        0.1.0.0-description:    Please see the README on GitHub at <https://github.com/githubuser/lean-peano#readme>+version:        0.1.0.1+description:    Please see the README on GitHub at <https://github.com/oisdk/lean-peano#readme> homepage:       https://github.com/oisdk/lean-peano#readme bug-reports:    https://github.com/oisdk/lean-peano/issues author:         Donnacha Oisín Kidney

@@ -68,6 +68,11 @@     | S Nat     deriving (Eq,Generic,Data,Typeable) +-- | A right fold over the naturals.+-- Alternatively, a function which converts a natural into+-- a Church natural.+--+-- prop> foldrNat S Z n === n foldrNat :: (a -> a) -> a -> Nat -> a foldrNat f k = go   where@@ -75,12 +80,13 @@     go (S n) = f (go n) {-# INLINE foldrNat #-} -foldlNat :: (a -> a) -> a -> Nat -> a-foldlNat f = go+-- | A strict left fold over the naturals.+foldlNat' :: (a -> a) -> a -> Nat -> a+foldlNat' f = go   where     go !b Z = b     go !b (S n) = go (f b) n-{-# INLINE foldlNat #-}+{-# INLINE foldlNat' #-}  -- | As lazy as possible instance Ord Nat where@@ -171,7 +177,7 @@     succ = S     pred (S n) = n     pred Z = error "pred called on zero nat"-    fromEnum = foldlNat succ 0+    fromEnum = foldlNat' succ 0     toEnum m       | m < 0 = error "cannot convert negative number to Peano"       | otherwise = go m@@ -205,7 +211,7 @@ -- >>> 5 `div` 2 -- 2 instance Integral Nat where-    toInteger = foldlNat succ 0+    toInteger = foldlNat' succ 0     quotRem _ Z = (maxBound, error "divide by zero")     quotRem x y = qr Z x y       where

@@ -7,18 +7,35 @@  {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} -module Numeric.Peano.Typelevel where+-- | Simple type-level Peano naturals.+module Numeric.Peano.Typelevel+  ( type (==)+  , type FromLit+  , type ToLit+  , type Compare+  , type (<=)+  , type (<)+  , type Min+  , type Max+  , type (+)+  , type (*)+  , type (-)+  , type (%)+  , type (/)+  ) where  import           GHC.TypeLits  (ErrorMessage (..), TypeError)-import qualified GHC.TypeLits  as Lit+import qualified GHC.TypeNats  as Lit import           Numeric.Peano +-- | Equality of type-level naturals. type family (==) (n :: Nat) (m :: Nat) :: Bool where     Z == Z = True     S n == S m = n == m     Z == S _ = False     S _ == Z = False +-- | Conversion of numeric literals to naturals. type family FromLit (n :: Lit.Nat) :: Nat where     FromLit 0 = Z     FromLit n = FromLit2 (Lit.Mod n 2) (FromLit (Lit.Div n 2))@@ -27,51 +44,61 @@     FromLit2 0 n = n     FromLit2 1 n = S n +-- | Conversion of naturals to numeric literals. type family ToLit (n :: Nat) :: Lit.Nat where     ToLit Z = 0     ToLit (S n) = 1 Lit.+ (ToLit n) +-- | Comparison of type-level naturals. type family Compare (n :: Nat) (m :: Nat) :: Ordering where     Compare Z Z         = EQ     Compare (S n) (S m) = Compare n m     Compare Z (S _)     = LT     Compare (S _) Z     = GT +-- | '<=' on type-level naturals. type family (<=) (n :: Nat) (m :: Nat) :: Bool where     Z   <= _   = True     S _ <= Z   = False     S n <= S m = n <= m +-- | '<' on type-level naturals. type family (<) (n :: Nat) (m :: Nat) :: Bool where     _ < Z = False     n < S m = n <= m +-- | The minimum of two type-level naturals. type family Min (n :: Nat) (m :: Nat) :: Nat where     Min Z _ = Z     Min _ Z = Z     Min (S n) (S m) = S (Min n m) +-- | The maximum of two type-level naturals. type family Max (n :: Nat) (m :: Nat) :: Nat where     Max Z m = m     Max n Z = n     Max (S n) (S m) = S (Max n m) +-- | Addition of type-level naturals. infixl 6 + type family (+) (n :: Nat) (m :: Nat) :: Nat where     Z + m = m     S n + m = S (n + m) +-- | Multiplication of type-level naturals. infixl 7 * type family (*) (n :: Nat) (m :: Nat) :: Nat where     Z   * _ = Z     S n * m = m + n * m +-- | Subtraction of type-level naturals. infixl 6 - type family (-) (n :: Nat) (m :: Nat) :: Nat where     n   - Z   = n     S n - S m = n - m     Z   - S _ = Z +-- | Remainder on type-level naturals. type family (%) (n :: Nat) (m :: Nat) :: Nat where     _ % Z = TypeError (Text "divide by zero")     n % m = Rem' n m n m@@ -81,6 +108,7 @@     Rem' n m (S n') (S m') = Rem' n m n' m'     Rem' n m Z (S _) = n +-- | Division on type-level naturals. type family (/) (n :: Nat) (m :: Nat) :: Nat where     _ / Z = TypeError (Text "divide by zero")     n / m = Div' m n m