type-natural 0.2.3.2 → 0.3.0.0

raw patch · 4 files changed

+360/−235 lines, 4 filesdep ~singletonsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: singletons

API changes (from Hackage documentation)

Files

• Data/Type/Natural.hs +124/−221
• Data/Type/Natural/Core.hs +132/−0
• Data/Type/Natural/Definitions.hs +94/−11
• type-natural.cabal +10/−3

@@ -1,7 +1,8 @@-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}-{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude   #-}-{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies, ScopedTypeVariables       #-}-{-# LANGUAGE TypeOperators, UndecidableInstances, StandaloneDeriving    #-}+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs     #-}+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude       #-}+{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators                   #-}+{-# LANGUAGE UndecidableInstances                                           #-} -- | Type level peano natural number, some arithmetic functions and their singletons. module Data.Type.Natural (-- * Re-exported modules.                           module Data.Singletons,@@ -40,7 +41,7 @@                           -- ** Type-level predicate & judgements                           Leq(..), (:<=), (:<<=), #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708-                          (:<<=$),(:<<=$$),(:<<=$$$), +                          (:<<=$),(:<<=$$),(:<<=$$$), #endif                           (%:<<=), LeqInstance,                           boolToPropLeq, boolToClassLeq, propToClassLeq,@@ -85,136 +86,66 @@                           sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14,                           sN15, sN16, sN17, sN18, sN19, sN20                          ) where-import           Data.Singletons+import Data.Singletons #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2,+                                Min, MinSym0, MinSym1, MinSym2, SOrd (..)) import Data.Singletons.TH      (singletons)-import Data.Singletons.Prelude hiding ((:<=), SOrd(..), MaxSym1, MaxSym0, MaxSym2-                                      , MinSym1, MinSym0, MinSym2, Max, Min) #endif+import           Data.Constraint           hiding ((:-)) import           Data.Type.Monomorphic-import           Prelude          (Int, Bool (..), Eq (..), Integral (..), Ord ((<)),-                                   Show (..), error, id, otherwise, ($), (.), undefined)-import qualified Prelude          as P+import           Language.Haskell.TH+import           Language.Haskell.TH.Quote+import           Prelude                   (Bool (..), Eq (..), Int,+                                            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+import           Unsafe.Coerce+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710+import Data.Type.Natural.Definitions hiding ((:<=))+-- import Data.Type.Natural.Proofs.GHC710+import Prelude (Num (..), Ord (..))+#else import Data.Type.Natural.Definitions--instance P.Num Nat where-  n - m = n - m-  n + m = n + m-  n * m = n * m-  abs = id-  signum Z = Z-  signum _ = S Z-  fromInteger 0             = Z-  fromInteger n | n P.< 0   = error "negative integer"-                | otherwise = S $ P.fromInteger (n P.- 1)------------------------------------------------------- ** Convenient synonyms-----------------------------------------------------#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708-sZ :: SNat Z-sZ = SZ--sS :: SNat n -> SNat (S n)-sS = SS--{-# DEPRECATED sZ, sS "Smart constructors are no longer needed in singletons; Use `SS` or `SZ` instead." #-}+-- import Data.Type.Natural.Proofs.GHC708 #endif-+import Data.Type.Natural.Core  ----------------------------------------------------- ** Type-level predicate & judgements.+-- * Conversion functions. ----------------------------------------------------- | Comparison via type-class.-class (n :: Nat) :<= (m :: Nat)-instance Z :<= n-instance (n :<= m) => S n :<= S m --- | Comparison via GADTs.-data Leq (n :: Nat) (m :: Nat) where-  ZeroLeq     :: SNat m -> Leq Zero m-  SuccLeqSucc :: Leq n m -> Leq (S n) (S m)--type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)--(%-) :: (m :<<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m)-n   %- SZ    = n-SS n %- SS m = n %- m-_    %- _    = error "impossible!"--infixl 6 %--deriving instance Show (SNat n)-deriving instance Eq (SNat n)--data (a :: Nat) :<: (b :: Nat) where-  ZeroLtSucc :: Zero :<: S m-  SuccLtSucc :: n :<: m -> S n :<: S m--deriving instance Show (a :<: b)------------------------------------------------------- * Total orderings on natural numbers.----------------------------------------------------propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m-propToBoolLeq _ = unsafeCoerce (Dict :: Dict ())-{-# INLINE propToBoolLeq #-}--boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m-boolToClassLeq _ = unsafeCoerce (Dict :: Dict ())-{-# INLINE boolToClassLeq #-}--propToClassLeq :: Leq n m -> LeqInstance n m-propToClassLeq _ = unsafeCoerce (Dict :: Dict ())-{-# INLINE propToClassLeq #-}--{---- | Below is the "proof" of the correctness of above:-propToBoolLeq :: Leq n m -> LeqTrueInstance n m-propToBoolLeq (ZeroLeq _) = Dict-propToBoolLeq (SuccLeqSucc leq) = case propToBoolLeq leq of Dict -> Dict-{-# RULES- "propToBoolLeq/unsafeCoerce" forall (x :: Leq n m) .-  propToBoolLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict ((n :<<= m) ~ True)- #-}--boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m-boolToClassLeq SZ     _      = Dict-boolToClassLeq (SS n) (SS m) = case boolToClassLeq n m of Dict -> Dict-boolToClassLeq _ _ = bugInGHC-{-# RULES- "boolToClassLeq/unsafeCoerce" forall (n :: SNat n) (m :: SNat m).-  boolToClassLeq n m = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)- #-}--propToClassLeq :: Leq n m -> LeqInstance n m-propToClassLeq (ZeroLeq _) = Dict-propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict-{-# RULES- "propToClassLeq/unsafeCoerce" forall (x :: Leq n m) .-  propToClassLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)- #-}--}--type LeqInstance n m = Dict (n :<= m)+-- | Convert integral numbers into 'Nat'+intToNat :: (Integral a, Ord a) => a -> Nat+intToNat 0 = Z+intToNat n+    | n < 0     = error "negative integer"+    | otherwise = S $ intToNat (n P.- 1) -boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m-boolToPropLeq SZ     m      = ZeroLeq m-boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m-boolToPropLeq _      _      = bugInGHC+-- | Convert 'Nat' into normal integers.+natToInt :: Integral n => Nat -> n+natToInt Z     = 0+natToInt (S n) = natToInt n P.+ 1 -leqRhs :: Leq n m -> SNat m-leqRhs (ZeroLeq m) = m-leqRhs (SuccLeqSucc leq) = sS $ leqRhs leq+-- | Convert 'SNat n' into normal integers.+sNatToInt :: P.Num n => SNat x -> n+sNatToInt SZ     = 0+sNatToInt (SS n) = sNatToInt n P.+ 1 -leqLhs :: Leq n m -> SNat n-leqLhs (ZeroLeq _) = sZ-leqLhs (SuccLeqSucc leq) = sS $ leqLhs leq+instance Monomorphicable (Sing :: Nat -> *) where+  type MonomorphicRep (Sing :: Nat -> *) = Int+  demote  (Monomorphic sn) = sNatToInt sn+  promote n+      | n < 0     = error "negative integer!"+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 708+      | n == 0    = Monomorphic sZ+      | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ sS sn+#else+      | n == 0    = Monomorphic SZ+      | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ SS sn+#endif  -------------------------------------------------- -- * Properties@@ -222,9 +153,9 @@ plusZR :: SNat n -> n :+: Z :=: n plusZR SZ     = Refl plusZR (SS n) =- start (sS n %+ sZ)-   =~= sS (n %+ sZ)-   === sS n          `because` cong' sS (plusZR n)+ start (SS n %+ SZ)+   =~= SS (n %+ SZ)+   === SS n          `because` cong' SS (plusZR n)  eqPreservesS :: n :=: m -> S n :=: S m eqPreservesS Refl = Refl@@ -250,31 +181,31 @@   start (l %:+ n)     === n %:+ l   `because` plusCommutative l n     === m %:+ l   `because` eq-    === l %:+ m   `because` plusCommutative m l +    === l %:+ m   `because` plusCommutative m l  sAndPlusOne :: SNat n -> S n :=: n :+: One sAndPlusOne SZ = Refl sAndPlusOne (SS n) =-  start (sS (sS n))-    === sS (n %+ sOne) `because` cong' sS (sAndPlusOne n)-    =~= sS n %+ sOne+  start (SS (SS n))+    === SS (n %+ sOne) `because` cong' SS (sAndPlusOne n)+    =~= SS n %+ sOne  plusAssociative :: SNat n -> SNat m -> SNat l                 -> n :+: (m :+: l) :=: (n :+: m) :+: l plusAssociative SZ     _ _ = Refl plusAssociative (SS n) m l =-  start (sS n %+ (m %+ l))-    =~= sS (n %+ (m %+ l))-    === sS ((n %+ m) %+ l)  `because` cong' sS (plusAssociative n m l)-    =~= sS (n %+ m) %+ l-    =~= (sS n %+ m) %+ l+  start (SS n %+ (m %+ l))+    =~= SS (n %+ (m %+ l))+    === SS ((n %+ m) %+ l)  `because` cong' SS (plusAssociative n m l)+    =~= SS (n %+ m) %+ l+    =~= (SS n %+ m) %+ l  plusSR :: SNat n -> SNat m -> S (n :+: m) :=: n :+: S m plusSR n m =-  start (sS (n %+ m))+  start (SS (n %+ m))     === (n %+ m) %+ sOne `because` sAndPlusOne (n %+ m)     === n %+ (m %+ sOne) `because` symmetry (plusAssociative n m sOne)-    === n %+ sS m        `because` plusCongL n (symmetry $ sAndPlusOne m)+    === n %+ SS m        `because` plusCongL n (symmetry $ sAndPlusOne m)  plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m' plusCongL _ Refl = Refl@@ -288,10 +219,10 @@ succPlusR :: SNat n -> SNat m -> n :+ S m :=: S (n :+ m) succPlusR SZ     _ = Refl succPlusR (SS n) m =-  start (sS n %+ sS m)-    =~= sS (n %+ sS m)-    === sS (sS (n %+ m)) `because` succCongEq (succPlusR n m)-    =~= sS (sS n %+ m)+  start (SS n %+ SS m)+    =~= SS (n %+ SS m)+    === SS (SS (n %+ m)) `because` succCongEq (succPlusR n m)+    =~= SS (SS n %+ m)  minusCongEq :: n :=: m -> SNat l -> n :-: l :=: m :-: l minusCongEq Refl _ = Refl@@ -299,33 +230,33 @@ minusNilpotent :: SNat n -> n :-: n :=: Zero minusNilpotent SZ = Refl minusNilpotent (SS n) =-  start (sS n %:- sS n)+  start (SS n %:- SS n)     =~= n %:- n-    === sZ     `because` minusNilpotent n+    === SZ     `because` minusNilpotent n  plusCommutative :: SNat n -> SNat m -> n :+: m :=: m :+: n plusCommutative SZ SZ     = Refl plusCommutative SZ (SS m) =-  start (sZ %+ sS m)-    =~= sS m-    === sS (m %+ sZ) `because` cong' sS (plusCommutative SZ m)-    =~= sS m %+ sZ+  start (SZ %+ SS m)+    =~= SS m+    === SS (m %+ SZ) `because` cong' SS (plusCommutative SZ m)+    =~= SS m %+ SZ plusCommutative (SS n) m =-  start (sS n %+ m)-    =~= sS (n %+ m)-    === sS (m %+ n)      `because` cong' sS (plusCommutative n m)+  start (SS n %+ m)+    =~= SS (n %+ m)+    === SS (m %+ n)      `because` cong' SS (plusCommutative n m)     === (m %+ n) %+ sOne `because` sAndPlusOne (m %+ n)     === m %+ (n %+ sOne) `because` symmetry (plusAssociative m n sOne)-    === m %+ sS n        `because` plusCongL m (symmetry $ sAndPlusOne n)+    === m %+ SS n        `because` plusCongL m (symmetry $ sAndPlusOne n)  eqSuccMinus :: ((m :<<= n) ~ True)             => SNat n -> SNat m -> (S n :-: m) :=: (S (n :-: m)) eqSuccMinus _      SZ     = Refl eqSuccMinus (SS n) (SS m) =-  start (sS (sS n) %:- sS m)-    =~= sS n %:- m-    === sS (n %:- m)       `because` eqSuccMinus n m-    =~= sS (sS n %:- sS m)+  start (SS (SS n) %:- SS m)+    =~= SS n %:- m+    === SS (n %:- m)       `because` eqSuccMinus n m+    =~= SS (SS n %:- SS m) eqSuccMinus _ _ = bugInGHC  plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n@@ -364,44 +295,45 @@ maxComm (SS n) (SS m) = case maxComm n m of Refl -> Refl  maxZR :: SNat n -> Max n Z :=: n-maxZR n = transitivity (maxComm n sZ) (maxZL n)+maxZR n = transitivity (maxComm n SZ) (maxZL n) -multPlusDistr :: SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: n :* m :+ n :* l+multPlusDistr :: forall n m l. SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: (n :* m) :+ (n :* l) multPlusDistr SZ     _ _ = Refl-multPlusDistr (SS n) m l = -  start (sS n %* (m %+ l))-    =~= n %* (m %+ l) %+ (m %+ l)-    === (n %* m) %+ (n %* l) %+ (m %+ l) `because` plusCongR (m %+ l) (multPlusDistr n m l)+multPlusDistr (SS (n :: SNat n')) m l =+  start (SS n %* (m %+ l))+    =~= (n %* (m %+ l)) %+ (m %+ l)+    === ((n %* m) %+ (n %* l)) %+ (m %+ l)+        `because` plusCongR (m %+ l) (multPlusDistr n m l :: n' :* (m :+ l) :=: (n' :* m) :+ (n' :* l))     === (n %* m) %+ (n %* l) %+ (l %+ m) `because` plusCongL ((n %* m) %+ (n %* l)) (plusCommutative m l)     === n %* m %+ (n %*l %+ (l %+ m))    `because` symmetry (plusAssociative (n %* m) (n %* l) (l %+ m))     === n %* l %+ (l %+ m) %+ n %* m     `because` plusCommutative (n %* m) (n %*l %+ (l %+ m))     === (n %* l %+ l) %+ m %+ n %* m     `because` plusCongR (n %* m) (plusAssociative (n %* l) l m)-    =~= (sS n %* l)   %+ m %+ n %* m-    === (sS n %* l)   %+ (m %+ (n %* m)) `because` symmetry (plusAssociative (sS n %* l) m (n %* m))-    === (sS n %* l)   %+ ((n %* m) %+ m) `because` plusCongL (sS n %* l) (plusCommutative m (n %* m))-    =~= (sS n %* l)   %+ (sS n %* m)-    === (sS n %* m)   %+ (sS n %* l)     `because` plusCommutative (sS n %* l) (sS n %* m)+    =~= (SS n %* l)   %+ m %+ n %* m+    === (SS n %* l)   %+ (m %+ (n %* m)) `because` symmetry (plusAssociative (SS n %* l) m (n %* m))+    === (SS n %* l)   %+ ((n %* m) %+ m) `because` plusCongL (SS n %* l) (plusCommutative m (n %* m))+    =~= (SS n %* l)   %+ (SS n %* m)+    === (SS n %* m)   %+ (SS n %* l)     `because` plusCommutative (SS n %* l) (SS n %* m) -plusMultDistr :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: n :* l :+ m :* l+plusMultDistr :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: (n :* l) :+ (m :* l) plusMultDistr SZ _ _ = Refl plusMultDistr (SS n) m l =   start ((SS n %+ m) %* l)-    =~= sS (n %+ m) %* l+    =~= SS (n %+ m) %* l     =~= (n %+ m) %* l %+ l     === n %* l  %+  m %* l  %+  l   `because` plusCongR l (plusMultDistr n m l)     === m %* l  %+  n %* l  %+  l   `because` plusCongR l (plusCommutative (n %* l) (m %* l))     === m %* l  %+ (n %* l  %+  l)  `because` symmetry (plusAssociative (m %* l) (n %*l) l)-    =~= m %* l  %+ (sS n %* l)-    === (sS n %* l)  %+  (m %* l)   `because` plusCommutative (m %* l) (sS n %* l)+    =~= m %* l  %+ (SS n %* l)+    === (SS n %* l)  %+  (m %* l)   `because` plusCommutative (m %* l) (SS n %* l)  multAssociative :: SNat n -> SNat m -> SNat l -> n :* (m :* l) :=: (n :* m) :* l multAssociative SZ     _ _ = Refl multAssociative (SS n) m l =-  start (sS n %* (m %* l))+  start (SS n %* (m %* l))     =~= n %* (m %* l) %+ (m %* l)     === (n %* m) %* l %+ (m %* l) `because` plusCongR (m %* l) (multAssociative n m l)     === (n %* m %+ m) %* l        `because` symmetry (plusMultDistr (n %* m) m l)-    =~= (sS n %* m) %* l+    =~= (SS n %* m) %* l  multZL :: SNat m -> Zero :* m :=: Zero multZL _ = Refl@@ -409,10 +341,10 @@ multZR :: SNat m -> m :* Zero :=: Zero multZR SZ = Refl multZR (SS n) =-  start (sS n %* sZ)-    =~= n %* sZ %+ sZ-    === sZ %+ sZ      `because` plusCongR sZ (multZR n)-    =~= sZ+  start (SS n %* SZ)+    =~= n %* SZ %+ SZ+    === SZ %+ SZ      `because` plusCongR SZ (multZR n)+    =~= SZ  multOneL :: SNat n -> One :* n :=: n multOneL n =@@ -424,10 +356,10 @@ multOneR :: SNat n -> n :* One :=: n multOneR SZ = Refl multOneR (SS n) =-  start (sS n %* sOne)+  start (SS n %* sOne)     =~= n %* sOne %+ sOne     === n %+ sOne         `because` plusCongR sOne (multOneR n)-    === sS n              `because` symmetry (sAndPlusOne n)+    === SS n              `because` symmetry (sAndPlusOne n)  multCongL :: SNat n -> m :=: l -> n :* m :=: n :* l multCongL _ Refl = Refl@@ -437,22 +369,22 @@  multComm :: SNat n -> SNat m -> n :* m :=: m :* n multComm SZ m =-  start (sZ %* m)-    =~= sZ-    === m %* sZ `because` symmetry (multZR m)+  start (SZ %* m)+    =~= SZ+    === m %* SZ `because` symmetry (multZR m) multComm (SS n) m =-  start (sS n %* m)+  start (SS n %* m)     =~= n %* m %+ m     === m %* n %+ m          `because` plusCongR m (multComm n m)     === m %* n %+ m %* sOne  `because` plusCongL (m %* n) (symmetry $ multOneR m)     === m %* (n %+ sOne)     `because` symmetry (multPlusDistr m n sOne)-    === m %* sS n            `because` multCongL m (symmetry $ sAndPlusOne n)+    === m %* SS n            `because` multCongL m (symmetry $ sAndPlusOne n)  plusNeutralR :: SNat n -> SNat m -> n :+ m :=: n -> m :=: Z plusNeutralR SZ m eq =   start m-    =~= sZ %:+ m-    === sZ       `because` eq+    =~= SZ %:+ m+    === SZ       `because` eq plusNeutralR (SS n) m eq = plusNeutralR n m $ succInjective eq  plusNeutralL :: SNat n -> SNat m -> n :+ m :=: m -> n :=: Z@@ -466,7 +398,7 @@ --------------------------------------------------  leqRefl :: SNat n -> Leq n n-leqRefl SZ = ZeroLeq sZ+leqRefl SZ = ZeroLeq SZ leqRefl (SS n) = SuccLeqSucc $ leqRefl n  leqSucc :: SNat n -> Leq n (S n)@@ -492,9 +424,9 @@ plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m) plusLeqL SZ     m = ZeroLeq $ coerce (symmetry $ plusZL m) m plusLeqL (SS n) m =-  start (sS n)-    =<= sS (n %+ m) `because` SuccLeqSucc (plusLeqL n m)-    =~= sS n %+ m+  start (SS n)+    =<= SS (n %+ m) `because` SuccLeqSucc (plusLeqL n m)+    =~= SS n %+ m  plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m) plusLeqR n m =@@ -502,7 +434,7 @@     Refl -> plusLeqL m n  minLeqL :: SNat n -> SNat m -> Leq (Min n m) n-minLeqL SZ m = case zAbsorbsMinL m of Refl -> ZeroLeq sZ+minLeqL SZ m = case zAbsorbsMinL m of Refl -> ZeroLeq SZ minLeqL n SZ = case zAbsorbsMinR n of Refl -> ZeroLeq n minLeqL (SS n) (SS m) = SuccLeqSucc (minLeqL n m) @@ -515,7 +447,7 @@ leqAnitsymmetric _ _ = bugInGHC  maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)-maxLeqL SZ m = ZeroLeq (sMax sZ m)+maxLeqL SZ m = ZeroLeq (sMax SZ m) maxLeqL n SZ = case maxZR n of                  Refl -> leqRefl n maxLeqL (SS n) (SS m) = SuccLeqSucc $ maxLeqL n m@@ -533,9 +465,9 @@ leqSnLeq :: Leq (S n) m -> Leq n m leqSnLeq (SuccLeqSucc leq) =   let n = leqLhs leq-      m = sS $ leqRhs leq+      m = SS $ leqRhs leq   in start n-       =<= sS n   `because` leqSucc n+       =<= SS n   `because` leqSucc n        =<= m      `because` SuccLeqSucc leq  leqPred :: Leq (S n) (S m) -> Leq n m@@ -546,36 +478,7 @@   case leqLhs leq of     SS _ -> leqSnnAbsurd leq     _    -> bugInGHC "cannot be occured"-  ------------------------------------------------------ * Conversion functions.--------------------------------------------------- --- | Convert integral numbers into 'Nat'-intToNat :: (Integral a, Ord a) => a -> Nat-intToNat 0 = Z-intToNat n-    | n < 0     = error "negative integer"-    | otherwise = S $ intToNat (n P.- 1)---- | Convert 'Nat' into normal integers.-natToInt :: Integral n => Nat -> n-natToInt Z     = 0-natToInt (S n) = natToInt n P.+ 1---- | Convert 'SNat n' into normal integers.-sNatToInt :: P.Num n => SNat x -> n-sNatToInt SZ     = 0-sNatToInt (SS n) = sNatToInt n P.+ 1--instance Monomorphicable (Sing :: Nat -> *) where-  type MonomorphicRep (Sing :: Nat -> *) = Int-  demote  (Monomorphic sn) = sNatToInt sn-  promote n-      | n < 0     = error "negative integer!"-      | n == 0    = Monomorphic sZ-      | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ sS sn- -------------------------------------------------- -- * Quasi Quoter --------------------------------------------------@@ -591,7 +494,7 @@                   }  -- | Quotesi-quoter for 'SNat'. This can be used for an expression, pattern and type.--- +-- --  For example: @[snat|12|] '%+' [snat| 5 |]@, @'sing' :: [snat| 12 |]@, @f [snat| 12 |] = \"hey\"@ snat :: QuasiQuoter snat = QuasiQuoter { quoteExp = P.foldr appE (conE 'SZ) . P.flip P.replicate (conE 'SS) . P.read

@@ -0,0 +1,132 @@+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs     #-}+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude       #-}+{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators                   #-}+{-# LANGUAGE UndecidableInstances                                           #-}+module Data.Type.Natural.Core where+import Data.Singletons+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2,+                                Min, MinSym0, MinSym1, MinSym2, SOrd (..))+import Data.Singletons.TH      (singletons)+#endif+import           Data.Constraint           hiding ((:-))+import           Data.Type.Monomorphic+import           Language.Haskell.TH+import           Language.Haskell.TH.Quote+import           Prelude                   (Bool (..), Eq (..), Int,+                                            Integral (..), Ord ((<)), Show (..),+                                            error, id, otherwise, undefined,+                                            ($), (.))+import qualified Prelude                   as P+import           Proof.Equational+import           Unsafe.Coerce+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710+import Data.Type.Natural.Definitions hiding ((:<=))+import Prelude                       (Num (..))+#else+import Data.Type.Natural.Definitions+#endif+++--------------------------------------------------+-- ** Convenient synonyms+--------------------------------------------------++#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+sZ :: SNat Z+sZ = SZ++sS :: SNat n -> SNat (S n)+sS = SS++{-# DEPRECATED sZ, sS "Smart constructors are no longer needed in singletons; Use `SS` or `SZ` instead." #-}+#endif++--------------------------------------------------+-- ** Type-level predicate & judgements.+--------------------------------------------------+-- | Comparison via type-class.+class (n :: Nat) :<= (m :: Nat)+instance Z :<= n+instance (n :<= m) => S n :<= S m++-- | Comparison via GADTs.+data Leq (n :: Nat) (m :: Nat) where+  ZeroLeq     :: SNat m -> Leq Zero m+  SuccLeqSucc :: Leq n m -> Leq (S n) (S m)++type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)++(%-) :: (m :<<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m)+n   %- SZ    = n+SS n %- SS m = n %- m+_    %- _    = error "impossible!"++infixl 6 %-+deriving instance Show (SNat n)+deriving instance Eq (SNat n)++data (a :: Nat) :<: (b :: Nat) where+  ZeroLtSucc :: Zero :<: S m+  SuccLtSucc :: n :<: m -> S n :<: S m++deriving instance Show (a :<: b)++--------------------------------------------------+-- * Total orderings on natural numbers.+--------------------------------------------------+propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m+propToBoolLeq _ = unsafeCoerce (Dict :: Dict ())+{-# INLINE propToBoolLeq #-}++boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m+boolToClassLeq _ = unsafeCoerce (Dict :: Dict ())+{-# INLINE boolToClassLeq #-}++propToClassLeq :: Leq n m -> LeqInstance n m+propToClassLeq _ = unsafeCoerce (Dict :: Dict ())+{-# INLINE propToClassLeq #-}++{-+-- | Below is the "proof" of the correctness of above:+propToBoolLeq :: Leq n m -> LeqTrueInstance n m+propToBoolLeq (ZeroLeq _) = Dict+propToBoolLeq (SuccLeqSucc leq) = case propToBoolLeq leq of Dict -> Dict+{-# RULES+ "propToBoolLeq/unsafeCoerce" forall (x :: Leq n m) .+  propToBoolLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict ((n :<<= m) ~ True)+ #-}++boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m+boolToClassLeq SZ     _      = Dict+boolToClassLeq (SS n) (SS m) = case boolToClassLeq n m of Dict -> Dict+boolToClassLeq _ _ = bugInGHC+{-# RULES+ "boolToClassLeq/unsafeCoerce" forall (n :: SNat n) (m :: SNat m).+  boolToClassLeq n m = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)+ #-}++propToClassLeq :: Leq n m -> LeqInstance n m+propToClassLeq (ZeroLeq _) = Dict+propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict+{-# RULES+ "propToClassLeq/unsafeCoerce" forall (x :: Leq n m) .+  propToClassLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)+ #-}+-}++type LeqInstance n m = Dict (n :<= m)++boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m+boolToPropLeq SZ     m      = ZeroLeq m+boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m+boolToPropLeq _      _      = bugInGHC++leqRhs :: Leq n m -> SNat m+leqRhs (ZeroLeq m) = m+leqRhs (SuccLeqSucc leq) = sS $ leqRhs leq++leqLhs :: Leq n m -> SNat n+leqLhs (ZeroLeq _) = sZ+leqLhs (SuccLeqSucc leq) = sS $ leqLhs leq

@@ -4,12 +4,26 @@ {-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving  #-} {-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators         #-} {-# LANGUAGE UndecidableInstances                                 #-}-module Data.Type.Natural.Definitions where+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ > 708+{-# LANGUAGE InstanceSigs #-}+#endif+module Data.Type.Natural.Definitions+       (module Data.Type.Natural.Definitions,+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710+        module Data.Singletons.Prelude+#endif+       ) where #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+import Data.Singletons.TH (singletons)+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710+import Data.Singletons.Prelude+import Prelude                 (Num (..), Ord (..))+#else import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2,                                 Min, MinSym0, MinSym1, MinSym2, SOrd (..))-import Data.Singletons.TH      (singletons) #endif+import Data.Singletons.TH (singletons)+#endif import           Data.Constraint           hiding ((:-)) import           Data.Type.Monomorphic import           Data.Typeable             (Typeable)@@ -28,7 +42,7 @@ -------------------------------------------------- singletons [d|  data Nat = Z | S Nat-            deriving (Show, Eq, Ord)+            deriving (Show, Eq)  |]  #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708@@ -40,6 +54,7 @@ -- ** Arithmetic functions. -------------------------------------------------- +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 710 singletons [d|  -- | Minimum function.  min :: Nat -> Nat -> Nat@@ -56,7 +71,54 @@  max (S n) (S m) = S (max n m)  |] +instance P.Ord Nat where+  Z   <= _   = True+  S _ <= Z   = False+  S n <= S m = n P.<= m++  min = min+  max = max+#else singletons [d|+  instance P.Ord Nat where+     Z   <= _   = True+     S _ <= Z   = False+     S n <= S m = n <= m++     min Z     Z     = Z+     min Z     (S _) = Z+     min (S _) Z     = Z+     min (S m) (S n) = S (min m n)++     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)+ |]+#endif++#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710+singletons [d|+  instance P.Num Nat where+    Z   + n = n+    S m + n = S (m + n)++    n   - Z   = n+    S n - S m = n - m+    Z   - S _ = Z++    Z   * _ = Z+    S n * m = n * m + m++    abs n = n++    signum Z = Z+    signum (S n) = S Z++    fromInteger n = if n == 0 then Z else S (fromInteger (n-1))+ |]+#else+singletons [d|  (+) :: Nat -> Nat -> Nat  Z   + n = n  S m + n = S (m + n)@@ -69,31 +131,52 @@  (*) :: Nat -> Nat -> Nat  Z   * _ = Z  S n * m = n * m + m+ |] +infixl 6 %:-, -++infixl 6 %:+, :+++infixl 7 %:*, :*++instance P.Num Nat where+  n - m = n - m+  n + m = n + m+  n * m = n * m+  abs = id+  signum Z = Z+  signum _ = S Z+  fromInteger 0             = Z+  fromInteger n | n P.< 0   = error "negative integer"+                | otherwise = S $ P.fromInteger (n P.- 1)++#endif++type n :-: m = n :- m+type n :+: m = n :+ m++infixl 6 :-:, :+:++singletons [d|  (**) :: Nat -> Nat -> Nat  n ** Z = S Z  n ** S m = (n ** m) * n  |] -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 :*:, %*, %:*, :*+infixl 6 %+  -- | Type-level multiplication. type n :*: m = n :* m+infixl 7 :*:  -- | Multiplication for singleton numbers. (%*) :: SNat n -> SNat m -> SNat (n :*: m) (%*) = (%:*)+infixl 7 %*  -- | Type-level exponentiation. type n :**: m = n :** m

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.2.3.2+version:             0.3.0.0 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@@ -14,6 +14,9 @@ category:            Math build-type:          Simple cabal-version:       >=1.8+tested-with:         GHC == 7.8.3, GHC == 7.8.4,+                     GHC == 7.10.2+ source-repository head   Type: git   Location: git://github.com/konn/type-natural.git@@ -21,7 +24,8 @@  library   exposed-modules:     Data.Type.Natural, Data.Type.Ordinal-  other-modules:       Data.Type.Natural.Definitions+  other-modules:       Data.Type.Natural.Definitions,+                       Data.Type.Natural.Core   build-depends:       base                     >= 4       && < 5                ,       equational-reasoning     == 0.2.*                ,       monomorphic              >= 0.0.3@@ -30,4 +34,7 @@   if impl(ghc < 7.8)     build-depends:     singletons               == 0.8.*   else-    build-depends:     singletons               >= 1.0    && < 1.2+    if impl(ghc < 7.10)+      build-depends:     singletons               == 1.*+    else +      build-depends:     singletons               == 2.0.*