type-natural 0.2.1.2 → 0.2.1.3

raw patch · 3 files changed

+180/−127 lines, 3 filesdep ~singletonsPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: singletons

API changes (from Hackage documentation)

Files

• Data/Type/Natural.hs +36/−123
• Data/Type/Natural/Definitions.hs +140/−0
• type-natural.cabal +4/−4

@@ -8,6 +8,9 @@                           -- * Natural Numbers                           -- | Peano natural numbers. It will be promoted to the type-level natural number.                           Nat(..),+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+                          SSym0, SSym1, ZSym0,+#endif                           -- | Singleton type for 'Nat'.                           SNat, Sing (SZ, SS),                           -- ** Smart constructors@@ -16,10 +19,29 @@                           sZ, sS,                           -- ** Arithmetic functions and their singletons.                           min, Min, sMin, max, Max, sMax,-                          (:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*),-                          (:-:), (:-), (%:-), (%-),+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+                          MinSym0, MinSym1, MinSym2,+                          MaxSym0, MaxSym1, MaxSym2,+#endif+                          (:+:), (:+),+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+                          (:+$), (:+$$), (:+$$$),+#endif+                          (%+), (%:+), (:*:),+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+                          (:*), (:*$), (:*$$), (:*$$$),+#endif+                          (%:*), (%*), (:-:), (:-),+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+                          (:-$), (:-$$), (:-$$$),+#endif+                          (%:-), (%-),                           -- ** Type-level predicate & judgements-                          Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance,+                          Leq(..), (:<=), (:<<=),+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+                          (:<<=$),(:<<=$$),(:<<=$$$), +#endif+                          (%:<<=), LeqInstance,                           boolToPropLeq, boolToClassLeq, propToClassLeq,                           LeqTrueInstance, propToBoolLeq,                           -- * Conversion functions@@ -45,10 +67,20 @@                           twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty,                           Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten,                           Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty,+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+                          ZeroSym0, OneSym0, TwoSym0, ThreeSym0, FourSym0, FiveSym0, SixSym0,+                          SevenSym0, EightSym0, NineSym0, TenSym0, ElevenSym0, TwelveSym0,+                          ThirteenSym0, FourteenSym0, FifteenSym0, SixteenSym0, SeventeenSym0,+                          EighteenSym0, NineteenSym0, TwentySym0,+#endif                           sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven,                           sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty,                           n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, n12, n13, n14, n15, n16, n17, n18, n19, n20,                           N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20,+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708++                          N0Sym0, N1Sym0, N2Sym0, N3Sym0, N4Sym0, N5Sym0, N6Sym0, N7Sym0, N8Sym0, N9Sym0, N10Sym0, N11Sym0, N12Sym0, N13Sym0, N14Sym0, N15Sym0, N16Sym0, N17Sym0, N18Sym0, N19Sym0, N20Sym0,+#endif                           sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14,                           sN15, sN16, sN17, sN18, sN19, sN20                          ) where@@ -67,49 +99,7 @@ import Language.Haskell.TH.Quote import Unsafe.Coerce import Language.Haskell.TH------------------------------------------------------- * Natural numbers and its singleton type----------------------------------------------------singletons [d|- data Nat = Z | S Nat-            deriving (Show, Eq, Ord)- |]------------------------------------------------------- ** Arithmetic functions.-----------------------------------------------------singletons [d|- -- | Minimum function.- min :: Nat -> Nat -> Nat- min Z     Z     = Z- min Z     (S _) = Z- min (S _) Z     = Z- min (S m) (S n) = S (min m n)-- -- | Maximum function.- max :: Nat -> Nat -> Nat- max Z     Z     = Z- max Z     (S n) = S n- max (S n) Z     = S n- max (S n) (S m) = S (max n m)- |]--singletons [d|- (+) :: Nat -> Nat -> Nat- Z   + n = n- S m + n = S (m + n)-- (-) :: Nat -> Nat -> Nat- n   - Z   = n- S n - S m = n - m- Z   - S _ = Z-- (*) :: Nat -> Nat -> Nat- Z   * _ = Z- S n * m = n * m + m- |]+import Data.Type.Natural.Definitions  instance P.Num Nat where   n - m = n - m@@ -122,78 +112,9 @@   fromInteger n | n P.< 0   = error "negative integer"                 | otherwise = S $ P.fromInteger (n P.- 1) -infixl 6 :-:, %:-, ---type n :-: m = n :- m-infixl 6 :+:, %+, %:+, :+--type n :+: m = n :+ m---- | Addition for singleton numbers.-(%+) :: SNat n -> SNat m -> SNat (n :+: m)-(%+) = (%:+)--infixl 7 :*:, %*, %:*, :*---- | Type-level multiplication.-type n :*: m = n :* m---- | Multiplication for singleton numbers.-(%*) :: SNat n -> SNat m -> SNat (n :*: m)-(%*) = (%:*)- -------------------------------------------------- -- ** Convenient synonyms ---------------------------------------------------singletons [d|- zero, one, two, three, four, five, six, seven, eight, nine, ten :: Nat           - eleven, twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty :: Nat           - zero      = Z- one       = S zero- two       = S one- three     = S two- four      = S three- five      = S four- six       = S five- seven     = S six- eight     = S seven- nine      = S eight- ten       = S nine- eleven    = S ten- twelve    = S eleven- thirteen  = S twelve- fourteen  = S thirteen- fifteen   = S fourteen- sixteen   = S fifteen- seventeen = S sixteen- eighteen  = S seventeen- nineteen  = S eighteen- twenty    = S nineteen- n0, n1, n2, n3, n4, n5, n6, n7, n8, n9 :: Nat- n10, n11, n12, n13, n14, n15, n16, n17 :: Nat- n18, n19, n20 :: Nat- n0  = zero- n1  = one- n2  = two- n3  = three- n4  = four- n5  = five- n6  = six- n7  = seven- n8  = eight- n9  = nine- n10 = ten- n11 = eleven- n12 = twelve- n13 = thirteen- n14 = fourteen- n15 = fifteen- n16 = sixteen- n17 = seventeen- n18 = eighteen- n19 = nineteen- n20 = twenty- |]  #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 sZ :: SNat Z@@ -213,14 +134,6 @@ class (n :: Nat) :<= (m :: Nat) instance Z :<= n instance (n :<= m) => S n :<= S m---- | Boolean-valued type-level comparison function.-singletons [d|- (<<=) :: Nat -> Nat -> Bool- Z   <<= _   = True- S _ <<= Z   = False- S n <<= S m = n <<= m- |]  -- | Comparison via GADTs. data Leq (n :: Nat) (m :: Nat) where

@@ -0,0 +1,140 @@+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude   #-}+{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies, ScopedTypeVariables       #-}+{-# LANGUAGE TypeOperators, UndecidableInstances, StandaloneDeriving    #-}+module Data.Type.Natural.Definitions where+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+import Data.Singletons.TH      (singletons)+import Data.Singletons.Prelude hiding ((:<=), SOrd(..), MaxSym1, MaxSym0, MaxSym2+                                      , MinSym1, MinSym0, MinSym2, Max, Min)+#endif+import           Data.Type.Monomorphic+import           Prelude          (Int, Bool (..), Eq (..), Integral (..), Ord ((<)),+                                   Show (..), error, id, otherwise, ($), (.), undefined)+import qualified Prelude          as P+import           Proof.Equational+import Data.Constraint hiding ((:-))+import Language.Haskell.TH.Quote+import Unsafe.Coerce+import Language.Haskell.TH++--------------------------------------------------+-- * Natural numbers and its singleton type+--------------------------------------------------+singletons [d|+ data Nat = Z | S Nat+            deriving (Show, Eq, Ord)+ |]++--------------------------------------------------+-- ** Arithmetic functions.+--------------------------------------------------++singletons [d|+ -- | Minimum function.+ min :: Nat -> Nat -> Nat+ min Z     Z     = Z+ min Z     (S _) = Z+ min (S _) Z     = Z+ min (S m) (S n) = S (min m n)++ -- | Maximum function.+ max :: Nat -> Nat -> Nat+ max Z     Z     = Z+ max Z     (S n) = S n+ max (S n) Z     = S n+ max (S n) (S m) = S (max n m)+ |]++singletons [d|+ (+) :: Nat -> Nat -> Nat+ Z   + n = n+ S m + n = S (m + n)++ (-) :: Nat -> Nat -> Nat+ n   - Z   = n+ S n - S m = n - m+ Z   - S _ = Z++ (*) :: Nat -> Nat -> Nat+ Z   * _ = Z+ S n * m = n * m + m+ |]++infixl 6 :-:, %:-, -++type n :-: m = n :- m+infixl 6 :+:, %+, %:+, :+++type n :+: m = n :+ m++-- | Addition for singleton numbers.+(%+) :: SNat n -> SNat m -> SNat (n :+: m)+(%+) = (%:+)++infixl 7 :*:, %*, %:*, :*++-- | Type-level multiplication.+type n :*: m = n :* m++-- | Multiplication for singleton numbers.+(%*) :: SNat n -> SNat m -> SNat (n :*: m)+(%*) = (%:*)++singletons [d|+ zero, one, two, three, four, five, six, seven, eight, nine, ten :: Nat           + eleven, twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty :: Nat           + zero      = Z+ one       = S zero+ two       = S one+ three     = S two+ four      = S three+ five      = S four+ six       = S five+ seven     = S six+ eight     = S seven+ nine      = S eight+ ten       = S nine+ eleven    = S ten+ twelve    = S eleven+ thirteen  = S twelve+ fourteen  = S thirteen+ fifteen   = S fourteen+ sixteen   = S fifteen+ seventeen = S sixteen+ eighteen  = S seventeen+ nineteen  = S eighteen+ twenty    = S nineteen+ n0, n1, n2, n3, n4, n5, n6, n7, n8, n9 :: Nat+ n10, n11, n12, n13, n14, n15, n16, n17 :: Nat+ n18, n19, n20 :: Nat+ n0  = zero+ n1  = one+ n2  = two+ n3  = three+ n4  = four+ n5  = five+ n6  = six+ n7  = seven+ n8  = eight+ n9  = nine+ n10 = ten+ n11 = eleven+ n12 = twelve+ n13 = thirteen+ n14 = fourteen+ n15 = fifteen+ n16 = sixteen+ n17 = seventeen+ n18 = eighteen+ n19 = nineteen+ n20 = twenty+ |]++-- | Boolean-valued type-level comparison function.+singletons [d|+ (<<=) :: Nat -> Nat -> Bool+ Z   <<= _   = True+ S _ <<= Z   = False+ S n <<= S m = n <<= m+ |]

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.2.1.2+version:             0.2.1.3 synopsis:            Type-level natural and proofs of their properties. description:         Type-level natural numbers and proofs of their properties. homepage:            https://github.com/konn/type-natural@@ -10,7 +10,7 @@ license-file:        LICENSE author:              Hiromi ISHII maintainer:          konn.jinro_at_gmail.com-copyright:           (C) Hiromi ISHII 2013+copyright:           (C) Hiromi ISHII 2013-2014 category:            Math build-type:          Simple cabal-version:       >=1.8@@ -21,7 +21,7 @@  library   exposed-modules:     Data.Type.Natural, Data.Type.Ordinal-  -- other-modules:       +  other-modules:       Data.Type.Natural.Definitions   build-depends:       base                     >= 4       && < 5                ,       equational-reasoning     == 0.2.*                ,       monomorphic              >= 0.0.3@@ -30,4 +30,4 @@   if impl(ghc < 7.8)     build-depends:     singletons               == 0.8.*   else-    build-depends:     singletons               >= 0.10    && < 1.0+    build-depends:     singletons               >= 1.0    && < 1.1