singleton-nats 0.4.0.4 → 0.4.1

raw patch · 4 files changed

+46/−56 lines, 4 filesnew-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +11/−0
• Data/Nat.hs +26/−53
• README.md +5/−0
• singleton-nats.cabal +4/−3

@@ -0,0 +1,11 @@+# 0.4.1 [2018.05.02]+* Add a `Num Nat` instance.+* Implement `signum` in the `PNum`/`SNum` instances for `Nat`.+* Define defunctionalization symbols for `Lit`.+* Define `someNatVal`.++# 0.4.0.4 [2018.01.09]+* Allow `singletons-2.4`.++# 0.4.0.3 [2017.11.03]+* Allow `singletons-2.3`.

@@ -11,24 +11,28 @@   , NatMul   , NatMinus   , NatAbs+  , NatSignum   , natPlus   , natMul   , natMinus   , natAbs+  , natSignum+  , someNatVal   , SNat   , Data.Singletons.Prelude.Sing(SS, SZ)   , Data.Singletons.Prelude.PNum   , Data.Singletons.Prelude.SNum   , SSym0(..)-  , SSym1(..)-  , ZSym0(..)+  , SSym1+  , ZSym0   , Lit+  , LitSym0(..)+  , LitSym1   , SLit   , sLit) where  import Data.Singletons.TH import Data.Singletons.Prelude-import Unsafe.Coerce import qualified GHC.TypeLits as Lit  $(singletons [d|@@ -39,16 +43,31 @@   natPlus (S a) b = S (natPlus a b)    natMul :: Nat -> Nat -> Nat-  natMul Z     b = Z+  natMul Z     _ = Z   natMul (S a) b = natPlus b (natMul a b)    natMinus :: Nat -> Nat -> Nat-  natMinus Z     b     = Z+  natMinus Z     _     = Z   natMinus (S a) (S b) = natMinus a b   natMinus a     Z     = a    natAbs :: Nat -> Nat   natAbs n = n++  natSignum :: Nat -> Nat+  natSignum Z     = Z+  natSignum (S _) = S Z++  instance Num Nat where+    (+) = natPlus+    (-) = natMinus+    (*) = natMul+    abs = natAbs+    signum = natSignum+    fromInteger n+      = if n == 0+           then Z+           else S (fromInteger (n - 1))   |])  #if !(MIN_VERSION_singletons(2,4,0))@@ -61,58 +80,11 @@ instance Ord (SNat n) where   compare _ _ = EQ -#if MIN_VERSION_singletons(2,3,0)-instance PNum Nat where-#else-instance PNum ('Proxy :: Proxy Nat) where-#endif-#if MIN_VERSION_singletons(2,4,0)-  type a + b = NatPlus a b-  type a - b = NatMinus a b-  type a * b = NatMul a b-#else-  type a :+ b = NatPlus a b-  type a :- b = NatMinus a b-  type a :* b = NatMul a b-#endif-  type Abs a = NatAbs a-  type Signum (a :: Nat) = Error "Data.Nat: signum not implemented"-  type FromInteger (a :: Lit.Nat) = Lit a--instance SNum Nat where-#if MIN_VERSION_singletons(2,4,0)-  (%+) = sNatPlus-  (%*) = sNatMul-  (%-) = sNatMinus-#else-  (%:+) = sNatPlus-  (%:*) = sNatMul-  (%:-) = sNatMinus-#endif-  sAbs  = sNatAbs-  sSignum = case toSing "Data.Nat: signum not implemented" of-    SomeSing s -> sError s-  sFromInteger n = case n -#if MIN_VERSION_singletons(2,4,0)-                          %==-#else-                          %:==-#endif-                               (sing :: Sing 0) of-    STrue  -> unsafeCoerce SZ-    SFalse -> unsafeCoerce (SS (sFromInteger (n-#if MIN_VERSION_singletons(2,4,0)-                                                %--#else-                                                %:--#endif-                                                    (sing :: Sing 1))))- {-| Converts a runtime 'Integer' to an existentially wrapped 'Nat'. Returns 'Nothing' if the argument is negative -} someNatVal :: Integer -> Maybe (SomeSing Nat) someNatVal n = case Lit.someNatVal n of-  Just (Lit.SomeNat (pn :: Proxy n)) -> Just (SomeSing (sFromInteger (sing :: Sing n)))+  Just (Lit.SomeNat (_ :: Proxy n)) -> Just (SomeSing (sFromInteger (sing :: Sing n)))   Nothing -> Nothing  {-| Provides a shorthand for 'Nat'-s using "GHC.TypeLits", for example:@@ -125,6 +97,7 @@ type family Lit n where   Lit 0 = Z   Lit n = S (Lit (n Lit.- 1))+$(genDefunSymbols [''Lit])  type SLit n = Sing (Lit n) 

@@ -0,0 +1,5 @@+# singleton-nats++[![Hackage](https://img.shields.io/hackage/v/singleton-nats.svg)](https://hackage.haskell.org/package/singleton-nats) [![Build Status](https://secure.travis-ci.org/AndrasKovacs/singleton-nats.svg)](http://travis-ci.org/AndrasKovacs/singleton-nats)++Unary natural numbers relying on the singletons infrastructure.

@@ -1,6 +1,5 @@- name:                singleton-nats-version:             0.4.0.4+version:             0.4.1 synopsis:            Unary natural numbers relying on the singletons infrastructure. description:         Unary natural number relying on the <https://hackage.haskell.org/package/singletons singletons> infrastructure. More information about the general usage of singletons can be found on the <https://github.com/goldfirere/singletons singletons github> page. category:            Data, Dependent Types@@ -14,7 +13,8 @@  build-type:          Simple cabal-version:       >=1.10-tested-with:         GHC == 8.0.1, GHC == 8.2.1, GHC == 8.4.1+tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.2+extra-source-files:  CHANGELOG.md, README.md  source-repository head   type: git@@ -29,3 +29,4 @@     singletons >= 2.2 && < 2.5    default-language:    Haskell2010+  ghc-options:         -Wall -Wno-unticked-promoted-constructors