singleton-nats 0.3.1.0 → 0.4.0.0

raw patch · 2 files changed

+70/−52 lines, 2 filesdep ~singletonsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: singletons

API changes (from Hackage documentation)

Files

• Data/Nat.hs +48/−30
• singleton-nats.cabal +22/−22

@@ -1,60 +1,78 @@ {-# LANGUAGE   UndecidableInstances, ScopedTypeVariables, DataKinds,   FlexibleInstances, GADTs, TypeFamilies, TemplateHaskell,-  TypeOperators #-}+  InstanceSigs, TypeOperators, PolyKinds #-}  module Data.Nat (     Nat(..)+  , NatPlus+  , NatMul+  , NatMinus+  , NatAbs   , natPlus   , natMul+  , natMinus+  , natAbs   , SNat-  , Data.Singletons.Prelude.Sing(SS, SZ)    -  , (:*)-  , (:*$)-  , (:*$$)-  , (:+)    -  , (:+$)-  , (:+$$)+  , Data.Singletons.Prelude.Sing(SS, SZ)+  , Data.Singletons.Prelude.PNum+  , Data.Singletons.Prelude.SNum       , SSym0(..)   , SSym1(..)   , ZSym0(..)-  , (%:+)-  , (%:*)   , Lit   , SLit ) where  import Data.Singletons.TH import Data.Singletons.Prelude-import qualified GHC.TypeLits as Lit+import Unsafe.Coerce+import qualified GHC.TypeLits as Lit    $(singletons [d|   data Nat = Z | S Nat deriving (Eq, Show, Ord) -  (+) :: Nat -> Nat -> Nat-  Z + b = b-  S a + b = S (a + b)+  natPlus :: Nat -> Nat -> Nat+  natPlus Z     b = b+  natPlus (S a) b = S (natPlus a b) -  (*) :: Nat -> Nat -> Nat-  Z * b = Z-  S a * b = b + (a * b) |])+  natMul :: Nat -> Nat -> Nat+  natMul Z     b = Z+  natMul (S a) b = natPlus b (natMul a b) -{-| This is the plain value-level version of addition on Nats. There's rarely a reason to use this;-it's included for completeness. -}-natPlus :: Nat -> Nat -> Nat-natPlus = (Data.Nat.+)+  natMinus :: Nat -> Nat -> Nat+  natMinus Z     b     = Z+  natMinus (S a) (S b) = natMinus a b+  natMinus a     Z     = a -{-| Similarly to 'natPlus', this one is included for completeness. -}-natMul :: Nat -> Nat -> Nat-natMul = (Data.Nat.*)+  natAbs :: Nat -> Nat+  natAbs n = n+  |])                                 +instance PNum ('KProxy :: KProxy Nat) where+  type a :+ b = NatPlus a b+  type a :- b = NatMinus a b+  type a :* b = NatMul a b+  type Abs a = NatAbs a+  type Signum (a :: Nat) = Error "Data.Nat: signum not implemented"+  type FromInteger (a :: Lit.Nat) = Lit a++instance SNum ('KProxy :: KProxy Nat) where  +  (%:+) = sNatPlus+  (%:*) = sNatMul+  (%:-) = sNatMinus+  sAbs  = sNatAbs  +  sSignum = case toSing "Data.Nat: signum not implemented" of+    SomeSing s -> sError s    +  sFromInteger n = case n %:== (sing :: Sing 0) of+    STrue  -> unsafeCoerce SZ+    SFalse -> unsafeCoerce (SS (sFromInteger (n %:- (sing :: Sing 1))))+ {-| Converts a runtime 'Integer' to an existentially wrapped 'Nat'. Returns 'Nothing' if the argument is negative -}-someNat :: Integer -> Maybe (SomeSing (KindOf Z))-someNat n | n < 0 = Nothing-someNat n = Just (go n) where  -  go 0 = SomeSing SZ-  go n = case go (n - 1) of-    SomeSing sn -> SomeSing (SS sn)+someNatVal :: Integer -> Maybe (SomeSing (KindOf Z))+someNatVal n = case Lit.someNatVal n of+  Just (Lit.SomeNat (pn :: Proxy n)) -> Just (SomeSing (sFromInteger (sing :: Sing n)))+  Nothing -> Nothing  {-| Provides a shorthand for 'Nat'-s using "GHC.TypeLits", for example: 

@@ -1,23 +1,23 @@--name:                singleton-nats-version:             0.3.1.0-synopsis:            Unary natural numbers relying on the singletons infrastructure.         -license:             BSD3-license-file:        LICENSE-author:              András Kovács-maintainer:          puttamalac@gmail.com-copyright:           2015 András Kovács-category:            Data-build-type:          Simple--cabal-version:       >=1.10--library-  exposed-modules:-    Data.Nat--  build-depends:       -    base >=4.7 && <4.9,-    singletons >= 1-+
+name:                singleton-nats
+version:             0.4.0.0
+synopsis:            Unary natural numbers relying on the singletons infrastructure.         
+license:             BSD3
+license-file:        LICENSE
+author:              András Kovács
+maintainer:          puttamalac@gmail.com
+copyright:           2015 András Kovács
+category:            Data
+build-type:          Simple
+
+cabal-version:       >=1.10
+
+library
+  exposed-modules:
+    Data.Nat
+
+  build-depends:       
+    base >=4.7 && <4.9,
+    singletons >= 2.0.1
+
   default-language:    Haskell2010