singleton-nats 0.4.0.1 → 0.4.0.2

raw patch · 2 files changed

+57/−36 lines, 2 filesdep ~basedep ~singletonsPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base, singletons

API changes (from Hackage documentation)

Files

• Data/Nat.hs +27/−6
• singleton-nats.cabal +30/−30

@@ -1,7 +1,8 @@ {-# LANGUAGE   UndecidableInstances, ScopedTypeVariables, DataKinds,   FlexibleInstances, GADTs, TypeFamilies, TemplateHaskell,-  InstanceSigs, TypeOperators, PolyKinds #-}+  InstanceSigs, TypeOperators, PolyKinds, StandaloneDeriving,+  FlexibleContexts, AllowAmbiguousTypes #-}  module Data.Nat (     Nat(..)@@ -21,7 +22,8 @@   , SSym1(..)   , ZSym0(..)   , Lit-  , SLit ) where+  , SLit+  , sLit) where  import Data.Singletons.TH import Data.Singletons.Prelude@@ -46,9 +48,17 @@    natAbs :: Nat -> Nat   natAbs n = n-  |])                                +  |]) -instance PNum ('KProxy :: KProxy Nat) where+deriving instance Show (SNat n)++instance Eq (SNat n) where+  (==) _ _ = True++instance Ord (SNat n) where+  compare _ _ = EQ++instance PNum ('Proxy :: Proxy Nat) where   type a :+ b = NatPlus a b   type a :- b = NatMinus a b   type a :* b = NatMul a b@@ -56,7 +66,7 @@   type Signum (a :: Nat) = Error "Data.Nat: signum not implemented"   type FromInteger (a :: Lit.Nat) = Lit a -instance SNum ('KProxy :: KProxy Nat) where  +instance SNum Nat where     (%:+) = sNatPlus   (%:*) = sNatMul   (%:-) = sNatMinus@@ -69,7 +79,7 @@  {-| Converts a runtime 'Integer' to an existentially wrapped 'Nat'. Returns 'Nothing' if the argument is negative -}-someNatVal :: Integer -> Maybe (SomeSing (KindOf Z))+someNatVal :: Integer -> Maybe (SomeSing Nat) someNatVal n = case Lit.someNatVal n of   Just (Lit.SomeNat (pn :: Proxy n)) -> Just (SomeSing (sFromInteger (sing :: Sing n)))   Nothing -> Nothing@@ -86,4 +96,15 @@   Lit n = S (Lit (n Lit.- 1))  type SLit n = Sing (Lit n)++{-| Shorthand for 'SNat' literals using `TypeApplications`.++>>> :set -XTypeApplications+>>> sLit @5+SS (SS (SS (SS (SS SZ))))++-}++sLit :: forall (n :: Lit.Nat). SingI (Lit n) => Sing (Lit n)+sLit = sing 

@@ -1,31 +1,31 @@-
-name:                singleton-nats
-version:             0.4.0.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
-homepage:            https://github.com/AndrasKovacs/singleton-nats
-bug-reports:         https://github.com/AndrasKovacs/singleton-nats/issues
-license:             BSD3
-license-file:        LICENSE
-author:              András Kovács
-maintainer:          puttamalac@gmail.com
-copyright:           2015 András Kovács
-
-build-type:          Simple
-cabal-version:       >=1.10
-tested-with:         GHC == 7.10.2
-
-source-repository head
-  type: git
-  location: https://github.com/AndrasKovacs/singleton-nats.git
-
-library
-  exposed-modules:
-    Data.Nat
-
-  build-depends:
-    base >=4.8.1.0 && <4.9,
-    singletons >= 2.0.1
-
++name:                singleton-nats+version:             0.4.0.2+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+homepage:            https://github.com/AndrasKovacs/singleton-nats+bug-reports:         https://github.com/AndrasKovacs/singleton-nats/issues+license:             BSD3+license-file:        LICENSE+author:              András Kovács+maintainer:          puttamalac@gmail.com+copyright:           2015 András Kovács++build-type:          Simple+cabal-version:       >=1.10+tested-with:         GHC == 8.0.1++source-repository head+  type: git+  location: https://github.com/AndrasKovacs/singleton-nats.git++library+  exposed-modules:+    Data.Nat++  build-depends:+    base >=4.8.1.0 && <5,+    singletons >= 2.2 && < 2.3+   default-language:    Haskell2010