type-natural 0.7.1.4 → 0.8.0.0

raw patch · 14 files changed

+935/−760 lines, 14 filesdep −monomorphicdep ~constraintsdep ~equational-reasoningdep ~ghc-typelits-presburgerPVP ok

version bump matches the API change (PVP)

Dependencies removed: monomorphic

Dependency ranges changed: constraints, equational-reasoning, ghc-typelits-presburger, singletons, template-haskell

API changes (from Hackage documentation)

Files

• Data/Type/Natural.hs +65/−71
• Data/Type/Natural/Builtin.hs +84/−72
• Data/Type/Natural/Class.hs +2/−2
• Data/Type/Natural/Class/Arithmetic.hs +245/−220
• Data/Type/Natural/Class/Order.hs +206/−191
• Data/Type/Natural/Compat.hs +0/−8
• Data/Type/Natural/Core.hs +17/−29
• Data/Type/Natural/Definitions.hs +20/−37
• Data/Type/Natural/Singleton/Compat.hs +35/−0
• Data/Type/Natural/Singleton/Compat/TH.hs +39/−0
• Data/Type/Ordinal.hs +93/−49
• Data/Type/Ordinal/Builtin.hs +38/−14
• Data/Type/Ordinal/Peano.hs +32/−15
• type-natural.cabal +59/−52

@@ -16,16 +16,16 @@                           min, Min, sMin, max, Max, sMax,                           MinSym0, MinSym1, MinSym2,                           MaxSym0, MaxSym1, MaxSym2,-                          (:+:), (:+),-                          (:+$), (:+$$), (:+$$$),-                          (%+), (%:+), (:*), (:*:),-                          (:*$), (:*$$), (:*$$$),-                          (%:*), (%*), (:-:), (:-),-                          (:**:), (:**), (%:**), (%**),-                          (:-$), (:-$$), (:-$$$),-                          (%:-), (%-),+                          type (+),+                          type (+@#@$), type (+@#@$$), type (+@#@$$$),+                          (%+), type (*),+                          type (*@#@$), type (*@#@$$), type (*@#@$$$),+                          (%*), type (-),+                          type (**), (%**),+                          type (-@#@$), type (-@#@$$), type (-@#@$$$),+                          (%-),                            -- ** Type-level predicate & judgements-                          Leq(..), (:<=), LeqInstance,+                          Leq(..), type (<=), LeqInstance,                           boolToPropLeq, boolToClassLeq, propToClassLeq,                           propToBoolLeq,                           -- * Conversion functions@@ -61,17 +61,17 @@                           sN15, sN16, sN17, sN18, sN19, sN20                          )        where-import Data.Type.Natural.Class hiding (One, Zero, sOne, sZero)-import Data.Type.Natural.Core-import Data.Type.Natural.Definitions hiding ((:<=))+import Data.Type.Natural.Singleton.Compat+ import Data.Singletons-import Data.Singletons.Prelude.Ord import Data.Singletons.Decide-import Data.Type.Monomorphic-import Proof.Equational-import Proof.Propositional hiding (Not)+import Data.Type.Natural.Class       hiding (One, Zero, sOne, sZero)+import Data.Type.Natural.Core+import Data.Type.Natural.Definitions hiding (type (<=)) import Data.Void import Language.Haskell.TH.Quote+import Proof.Equational+import Proof.Propositional           hiding (Not)  -------------------------------------------------- -- * Conversion functions.@@ -94,14 +94,6 @@ sNatToInt SZ     = 0 sNatToInt (SS n) = sNatToInt n + 1 -instance Monomorphicable (Sing :: Nat -> *) where-  type MonomorphicRep (Sing :: Nat -> *) = Integer-  demote  (Monomorphic sn) = sNatToInt sn-  promote n-      | n < 0     = error "negative integer!"-      | n == 0    = Monomorphic SZ-      | otherwise = withPolymorhic (n - 1) $ \sn -> Monomorphic $ SS sn- -------------------------------------------------- -- * Properties --------------------------------------------------@@ -109,24 +101,24 @@ -- | Since 0.5.0.0 instance IsPeano Nat where   {-# SPECIALISE instance IsPeano Nat #-}-  induction base _step SZ = base+  induction base _step SZ    = base   induction base step (SS n) = step n (induction base step n)    plusMinus n SZ =-    start (n %:+ SZ %:- SZ)-      === (n %:- SZ)        `because` minusCongL (plusZeroR n) SZ +    start (n %+ SZ %- SZ)+      === (n %- SZ)        `because` minusCongL (plusZeroR n) SZ       =~= n   plusMinus n (SS m) =-    start (n %:+ SS m %:- SS m)-      === SS (n %:+ m) %:- SS m `because` minusCongL (plusSuccR n m) (SS m)-      =~= (n %:+ m) %:- m+    start (n %+ SS m %- SS m)+      === SS (n %+ m) %- SS m `because` minusCongL (plusSuccR n m) (SS m)+      =~= (n %+ m) %- m       === n                     `because` plusMinus n m    succInj Refl = Refl   succOneCong = Refl   succNonCyclic _ a = case a of {} -  plusZeroL _   = Refl  +  plusZeroL _   = Refl   plusSuccL _ _ = Refl    multZeroL _   = Refl@@ -137,55 +129,57 @@ snEqZAbsurd :: SingI n => 'S n :~: 'Z -> a snEqZAbsurd = absurd . succNonCyclic sing -plusInjectiveL :: SNat n -> SNat m -> SNat l -> n :+ m :~: n :+ l -> m :~: l+plusInjectiveL :: SNat n -> SNat m -> SNat l -> n + m :~: n + l -> m :~: l plusInjectiveL SZ     _ _ Refl = Refl plusInjectiveL (SS n) m l eq   = plusInjectiveL n m l $ succInj eq -plusInjectiveR :: SNat n -> SNat m -> SNat l -> n :+ l :~: m :+ l -> n :~: m+plusInjectiveR :: SNat n -> SNat m -> SNat l -> n + l :~: m + l -> n :~: m plusInjectiveR n m l eq = plusInjectiveL l n m $-  start (l %:+ n)-    === n %:+ l   `because` plusComm l n-    === m %:+ l   `because` eq-    === l %:+ m   `because` plusComm m l+  start (l %+ n)+    === n %+ l   `because` plusComm l n+    === m %+ l   `because` eq+    === l %+ m   `because` plusComm m l -reflToSEqual :: SNat n -> SNat m -> n :~: m -> IsTrue (n :== m)+reflToSEqual :: SNat n -> SNat m -> n :~: m -> IsTrue (n == m) reflToSEqual SZ     _      Refl = Witness reflToSEqual (SS n) (SS m) Refl = reflToSEqual n m Refl-reflToSEqual (SS _) SZ refl = case refl of {}+reflToSEqual (SS _) SZ refl     = case refl of {} -sequalToRefl :: SNat n -> SNat m -> IsTrue (n :== m) -> n :~: m+sequalToRefl :: SNat n -> SNat m -> IsTrue (n == m) -> n :~: m sequalToRefl SZ     SZ     Witness = Refl sequalToRefl SZ     (SS _) witness = case witness of {} sequalToRefl (SS n) (SS m) Witness = succCong $ sequalToRefl n m Witness sequalToRefl (SS _) SZ     witness = case witness of {} -snequalToNoRefl :: SNat n -> SNat m -> IsTrue (Not (n :== m)) -> n :~: m -> Void-snequalToNoRefl SZ     _ Witness = \case  {}-snequalToNoRefl (SS _) _ Witness = \case  {}+snequalToNoRefl :: SNat n -> SNat m -> IsTrue (Not (n == m)) -> n :~: m -> Void+snequalToNoRefl SZ     _      Witness = \case  {}+snequalToNoRefl (SS _) SZ     Witness = \case {}+snequalToNoRefl (SS n) (SS m) Witness = \case+  Refl -> snequalToNoRefl n m Witness  Refl -sequalSym :: SNat n -> SNat m -> (n :== m) :~: (m :== n)+sequalSym :: SNat n -> SNat m -> (n == m) :~: (m == n) sequalSym SZ SZ         = Refl sequalSym SZ (SS _)     = Refl sequalSym (SS _) SZ     = Refl sequalSym (SS n) (SS m) = sequalSym n m -sleqFlip :: SNat n -> SNat m -> (n :~: m -> Void) -> (m :<= n) :~: Not (n :<= m)+sleqFlip :: SNat n -> SNat m -> (n :~: m -> Void) -> (m <= n) :~: Not (n <= m) sleqFlip SZ     SZ     neq = absurd $ neq Refl sleqFlip SZ     (SS _) _   = Refl sleqFlip (SS _) SZ     _   = Refl sleqFlip (SS n) (SS m) neq = sleqFlip n m (neq . succCong) -sLeqReflexive :: SNat n -> SNat m -> IsTrue (n :== m) -> IsTrue (n :<= m)+sLeqReflexive :: SNat n -> SNat m -> IsTrue (n == m) -> IsTrue (n <= m) sLeqReflexive SZ     _      Witness = Witness sLeqReflexive (SS n) (SS m) Witness = sLeqReflexive n m Witness-sLeqReflexive (SS _) SZ  witness = case witness of {}+sLeqReflexive (SS _) SZ  witness    = case witness of {} -nonSLeqToLT :: (n :<= m) ~ 'False => SNat n -> SNat m -> Compare m n :~: 'LT+nonSLeqToLT :: (n <= m) ~ 'False => SNat n -> SNat m -> Compare m n :~: 'LT nonSLeqToLT n m = withRefl (sequalSym n m) $-  case m %:== n of+  case m %== n of     STrue -> case sLeqReflexive n m Witness of {}     SFalse ->-      case m %:<= n of+      case m %<= n of         STrue  -> Refl         SFalse -> case sleqFlip n m $ snequalToNoRefl n m Witness of {} @@ -198,46 +192,46 @@   viewLeq (SS _) SZ     a       = case a of {}    ltToLeq n m Refl =-    case n %:== m of-      SFalse -> case n %:<= m of+    case n %== m of+      SFalse -> case n %<= m of         STrue -> Witness   eqlCmpEQ n m Refl =-    case n %:== m of+    case n %== m of       STrue  -> Refl       SFalse -> absurd $ snequalToNoRefl n m Witness Refl    eqToRefl n m Refl =-    case n %:== m of-      STrue -> sequalToRefl n m Witness-      SFalse -> case n %:<= m of {}+    case n %== m of+      STrue  -> sequalToRefl n m Witness+      SFalse -> case n %<= m of {}    leqToCmp n m Witness =-    case n %:== m of+    case n %== m of       STrue  -> Left $ sequalToRefl n m Witness       SFalse -> Right Refl    cmpZero _ = Refl    flipCompare n m =-    case n %:== m of+    case n %== m of       STrue -> withRefl (sequalSym n m) Refl       SFalse -> withRefl (sequalSym n m) $-        case n %:<= m of+        case n %<= m of           STrue -> withRefl (sleqFlip n m (snequalToNoRefl n m Witness)) $-            case m %:<= n of+            case m %<= n of               SFalse -> Refl           SFalse -> withRefl (sleqFlip n m (snequalToNoRefl n m Witness)) $-            case m %:<= n of+            case m %<= n of               STrue -> Refl -  minLeqL SZ SZ     = Witness-  minLeqL SZ (SS _) = Witness-  minLeqL (SS _) SZ = Witness+  minLeqL SZ SZ         = Witness+  minLeqL SZ (SS _)     = Witness+  minLeqL (SS _) SZ     = Witness   minLeqL (SS n) (SS m) = minLeqL n m -  minLeqR SZ SZ     = Witness-  minLeqR SZ (SS _) = Witness-  minLeqR (SS _) SZ = Witness+  minLeqR SZ SZ         = Witness+  minLeqR SZ (SS _)     = Witness+  minLeqR (SS _) SZ     = Witness   minLeqR (SS n) (SS m) = minLeqR n m    minLargest SZ     _      _  _ _       = Witness@@ -271,13 +265,13 @@   lneqReversed _ _ = Refl   lneqSuccLeq _ _ = Refl -plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :~: n+plusMinusEqL :: SNat n -> SNat m -> ((n + m) - m) :~: n plusMinusEqL = plusMinus -plusNeutralR :: SNat n -> SNat m -> n :+ m :~: n -> m :~: 'Z+plusNeutralR :: SNat n -> SNat m -> n + m :~: n -> m :~: 'Z plusNeutralR n m npmn = plusEqCancelL n m SZ (npmn `trans` sym (plusZeroR n)) -plusNeutralL :: SNat n -> SNat m -> n :+ m :~: m -> n :~: 'Z+plusNeutralL :: SNat n -> SNat m -> n + m :~: m -> n :~: 'Z plusNeutralL n m npmm = plusNeutralR m n (plusComm m n `trans` npmm)  --------------------------------------------------@@ -286,7 +280,7 @@  -- | Quotesi-quoter for 'SNat'. This can be used for an expression. -----  For example: @[snat|12|] '%:+' [snat| 5 |]@.+--  For example: @[snat|12|] '%+' [snat| 5 |]@. snat :: QuasiQuoter snat = mkSNatQQ [t| Nat |] 

@@ -25,28 +25,28 @@          IsPeano(..),          inductionNat,          -- * QuasiQuotes-         snat+         snat,+         -- * Re-exports+         module Data.Type.Natural.Singleton.Compat        )        where+import Data.Type.Natural.Singleton.Compat import Data.Type.Natural.Class  import           Data.Singletons.Decide       (SDecide (..)) import           Data.Singletons.Decide       (Decision (..))-import           Data.Singletons.Prelude      (PNum (..), SNum (..), Sing (..))+import           Data.Singletons.Prelude      (Sing (..), SingKind(..)) import           Data.Singletons.Prelude      (SingI (..))-import           Data.Singletons.Prelude      (SingKind (..), SomeSing (..)) import           Data.Singletons.Prelude.Enum (PEnum (..), SEnum (..)) import           Data.Singletons.Prelude.Ord  (POrd (..), SOrd (..)) import           Data.Singletons.TH           (sCases) import           Data.Singletons.TypeLits     (withKnownNat) import           Data.Type.Equality           ((:~:) (..))-import           Data.Type.Monomorphic        (Monomorphic (..))-import           Data.Type.Monomorphic        (Monomorphicable (..)) import           Data.Type.Natural            (Nat (S, Z), Sing (SS, SZ)) import qualified Data.Type.Natural            as PN import           Data.Void                    (absurd) import           Data.Void                    (Void)-import           GHC.TypeLits                 (type (+), type (<=), type (<=?))+import           GHC.TypeLits                 (type (<=?)) import qualified GHC.TypeLits                 as TL import           Language.Haskell.TH.Quote    (QuasiQuoter) import           Proof.Equational             (coerce, withRefl)@@ -77,8 +77,15 @@ sFromPeano SZ      = sing sFromPeano (SS sn) = sSucc (sFromPeano sn) -toPeanoInjective :: ToPeano n :~: ToPeano m -> n :~: m-toPeanoInjective Refl = Refl+toPeanoInjective :: forall n m. (TL.KnownNat n, TL.KnownNat m)+                 => ToPeano n :~: ToPeano m -> n :~: m+toPeanoInjective tPnEqtPm =+  let sn = sing :: Sing n+      sm = sing :: Sing m+  in start sn+       === sFromPeano (sToPeano sn) `because` sym (fromToPeano sn)+       === sFromPeano (sToPeano sm) `because` congFromPeano tPnEqtPm+       === sm                       `because` fromToPeano sm  -- trustMe :: a :~: b -- trustMe = unsafeCoerce (Refl :: () :~: ())@@ -141,31 +148,31 @@ fromPeanoSuccCong :: Sing n -> FromPeano ('S n) :~: Succ (FromPeano n) fromPeanoSuccCong _sn = Refl -fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n :+ m) :~: FromPeano n :+ FromPeano m+fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n PN.+ m) :~: FromPeano n TL.+ FromPeano m fromPeanoPlusCong SZ _ = Refl fromPeanoPlusCong (SS sn) sm =-  start (sFromPeano (SS sn %:+ sm))-    =~= sFromPeano (SS (sn %:+ sm))-    === sSucc (sFromPeano (sn %:+ sm))           `because` fromPeanoSuccCong (sn %:+ sm)-    === sSucc (sFromPeano sn  %:+ sFromPeano sm) `because` congSucc (fromPeanoPlusCong sn sm)-    =~= sSucc (sFromPeano sn) %:+ sFromPeano sm-    =~= sFromPeano (SS sn)    %:+ sFromPeano sm+  start (sFromPeano (SS sn %+ sm))+    =~= sFromPeano (SS (sn %+ sm))+    === sSucc (sFromPeano (sn %+ sm))           `because` fromPeanoSuccCong (sn %+ sm)+    === sSucc (sFromPeano sn  %+ sFromPeano sm) `because` congSucc (fromPeanoPlusCong sn sm)+    =~= sSucc (sFromPeano sn) %+ sFromPeano sm+    =~= sFromPeano (SS sn)    %+ sFromPeano sm -toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n + m) :~: ToPeano n :+ ToPeano m+toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n TL.+ m) :~: ToPeano n PN.+ ToPeano m toPeanoPlusCong sn sm =   case viewNat sn of     IsZero -> Refl     IsSucc pn ->-      start (sToPeano (sSucc pn %:+ sm))-        =~= sToPeano (sSucc (pn %:+ sm))-        === SS (sToPeano (pn %:+ sm))-            `because` toPeanoSuccCong (pn %:+ sm)-        === SS (sToPeano pn %:+ sToPeano sm)+      start (sToPeano (sSucc pn %+ sm))+        =~= sToPeano (sSucc (pn %+ sm))+        === SS (sToPeano (pn %+ sm))+            `because` toPeanoSuccCong (pn %+ sm)+        === SS (sToPeano pn %+ sToPeano sm)             `because` succCong (toPeanoPlusCong pn sm)-        =~= SS (sToPeano pn) %:+ sToPeano sm-        === (sToPeano (sSucc pn) %:+ sToPeano sm)+        =~= SS (sToPeano pn) %+ sToPeano sm+        === (sToPeano (sSucc pn) %+ sToPeano sm)             `because` plusCongL (sym (toPeanoSuccCong pn)) (sToPeano sm)-        =~= sToPeano sn %:+ sToPeano sm+        =~= sToPeano sn %+ sToPeano sm  fromPeanoZeroCong :: FromPeano 'Z :~: 0 fromPeanoZeroCong = Refl@@ -179,60 +186,60 @@ toPeanoOneCong :: ToPeano 1 :~: PN.One toPeanoOneCong = Refl -natPlusCongR :: Sing r -> n :~: m -> n + r :~: m + r+natPlusCongR :: Sing r -> n :~: m -> n TL.+ r :~: m TL.+ r natPlusCongR _ Refl = Refl -fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n PN.:* m) :~: FromPeano n :* FromPeano m+fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n PN.* m) :~: FromPeano n TL.* FromPeano m fromPeanoMultCong SZ _ = Refl fromPeanoMultCong (SS psn) sm =-  start (sFromPeano (SS psn %:* sm))-    =~= sFromPeano (psn %:* sm %:+ sm)-    === sFromPeano (psn %:* sm) %:+ sFromPeano sm-        `because` fromPeanoPlusCong (psn %:* sm) sm-    === sFromPeano psn %:* sFromPeano sm %:+ sFromPeano sm+  start (sFromPeano (SS psn %* sm))+    =~= sFromPeano (psn %* sm %+ sm)+    === sFromPeano (psn %* sm) %+ sFromPeano sm+        `because` fromPeanoPlusCong (psn %* sm) sm+    === sFromPeano psn %* sFromPeano sm %+ sFromPeano sm         `because` natPlusCongR (sFromPeano sm) (fromPeanoMultCong psn sm)-    =~= sSucc (sFromPeano psn) %:* sFromPeano sm-    =~= sFromPeano (SS psn)    %:* sFromPeano sm+    =~= sSucc (sFromPeano psn) %* sFromPeano sm+    =~= sFromPeano (SS psn)    %* sFromPeano sm  -toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n PN.:* m) :~: ToPeano n PN.:* ToPeano m+toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n TL.* m) :~: ToPeano n PN.* ToPeano m toPeanoMultCong sn sm =   case viewNat sn of     IsZero -> Refl     IsSucc psn ->-      start (sToPeano (sSucc psn %:* sm))-        =~= sToPeano (psn %:* sm %:+ sm)-        === sToPeano (psn %:* sm) %:+ sToPeano sm-            `because` toPeanoPlusCong (psn %:* sm) sm-        === sToPeano psn %:* sToPeano sm %:+ sToPeano sm+      start (sToPeano (sSucc psn %* sm))+        =~= sToPeano (psn %* sm %+ sm)+        === sToPeano (psn %* sm) %+ sToPeano sm+            `because` toPeanoPlusCong (psn %* sm) sm+        === sToPeano psn %* sToPeano sm %+ sToPeano sm             `because` plusCongL (toPeanoMultCong psn sm) (sToPeano sm)-        =~= SS (sToPeano psn) %:* sToPeano sm-        === sToPeano (sSucc psn) %:* sToPeano sm+        =~= SS (sToPeano psn) %* sToPeano sm+        === sToPeano (sSucc psn) %* sToPeano sm             `because` multCongL (sym (toPeanoSuccCong psn)) (sToPeano sm) -infix 4 %:<=?-(%:<=?) :: Sing (n :: TL.Nat) -> Sing m -> Sing (n <=? m)-n %:<=? m = case sCompare n m of+infix 4 %<=?+(%<=?) :: Sing (n :: TL.Nat) -> Sing m -> Sing (n <=? m)+n %<=? m = case sCompare n m of   SLT -> STrue   SEQ -> STrue   SGT -> SFalse -natLeqSuccEq :: Sing n -> Sing m -> ((n + 1) <=? (m + 1)) :~: (n <=? m)+natLeqSuccEq :: Sing n -> Sing m -> ((n TL.+ 1) <=? (m TL.+ 1)) :~: (n <=? m) natLeqSuccEq _ _ = Refl  leqqCong :: n :~: m -> l :~: z -> (n <=? l) :~: (m <=? z) leqqCong Refl Refl = Refl -leqCong :: n :~: m -> l :~: z -> (n :<= l) :~: (m :<= z)+leqCong :: n :~: m -> l :~: z -> (n PN.<= l) :~: (m PN.<= z) leqCong Refl Refl = Refl -fromPeanoMonotone :: ((n :<= m) ~ 'True) => Sing n -> Sing m -> (FromPeano n <=? FromPeano m) :~: 'True+fromPeanoMonotone :: ((n PN.<= m) ~ 'True) => Sing n -> Sing m -> (FromPeano n <=? FromPeano m) :~: 'True fromPeanoMonotone SZ _ = Refl fromPeanoMonotone (SS n) (SS m) =-   start (sFromPeano (SS n) %:<=? sFromPeano (SS m))-     === (sSucc (sFromPeano n) %:<=? sSucc (sFromPeano m))+   start (sFromPeano (SS n) %<=? sFromPeano (SS m))+     === (sSucc (sFromPeano n) %<=? sSucc (sFromPeano m))       `because` leqqCong  (fromPeanoSuccCong n) (fromPeanoSuccCong m)-     === (sFromPeano n %:<=? sFromPeano m)+     === (sFromPeano n %<=? sFromPeano m)       `because` natLeqSuccEq (sFromPeano n) (sFromPeano m)      === STrue       `because` fromPeanoMonotone n m@@ -240,7 +247,7 @@ fromPeanoMonotone _ _ = bugInGHC #endif -natLeqZero :: (n <= 0) => Sing n -> n :~: 0+natLeqZero :: (n TL.<= 0) => Sing n -> n :~: 0 natLeqZero Zero = Refl natLeqZero _    = error "natLeqZero : bug in ghc" @@ -250,7 +257,7 @@ natSuccPred :: ((n :~: 0) -> Void) -> Succ (Pred n) :~: n natSuccPred _ = Refl -myLeqPred :: Sing n -> Sing m -> ('S n :<= 'S m) :~: (n :<= m)+myLeqPred :: Sing n -> Sing m -> ('S n PN.<= 'S m) :~: (n PN.<= m) myLeqPred SZ _          = Refl myLeqPred (SS _) (SS _) = Refl myLeqPred (SS _) SZ     = Refl@@ -258,8 +265,8 @@ toPeanoCong :: a :~: b -> ToPeano a :~: ToPeano b toPeanoCong Refl = Refl -toPeanoMonotone :: (n <= m)-                => Sing n -> Sing m -> ((ToPeano n) :<= (ToPeano m)) :~: 'True+toPeanoMonotone :: (n TL.<= m)+                => Sing n -> Sing m -> ((ToPeano n) PN.<= (ToPeano m)) :~: 'True toPeanoMonotone sn sm =   case sn %~ (sing :: Sing 0) of     Proved eql -> withRefl eql Refl@@ -268,18 +275,18 @@       Disproved mPos ->         let pn = sPred sn             pm = sPred sm-        in start (sToPeano sn %:<= sToPeano sm)-             === (sToPeano (sSucc pn) %:<= sToPeano (sSucc pm))+        in start (sToPeano sn %<= sToPeano sm)+             === (sToPeano (sSucc pn) %<= sToPeano (sSucc pm))                  `because` leqCong (toPeanoCong $ sym $ natSuccPred nPos)                                    (toPeanoCong $ sym $ natSuccPred mPos)-             === (SS (sToPeano pn) %:<= SS (sToPeano pm))+             === (SS (sToPeano pn) %<= SS (sToPeano pm))                  `because` leqCong (toPeanoSuccCong pn) (toPeanoSuccCong pm)-             === (sToPeano pn %:<= sToPeano pm)+             === (sToPeano pn %<= sToPeano pm)                  `because` myLeqPred (sToPeano pn) (sToPeano pm)              === STrue `because` toPeanoMonotone pn pm  -- | Induction scheme for built-in @'TL.Nat'@.-inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n+inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m TL.+ 1)) -> Sing n -> p n inductionNat base step sn =   case viewNat sn of     IsZero    -> base@@ -288,6 +295,10 @@  instance IsPeano TL.Nat where   {-# SPECIALISE instance IsPeano TL.Nat #-}++  toNatural = fromIntegral . fromSing+  fromNatural = toSing . fromIntegral+   predSucc _ = Refl   plusMinus _ _ = Refl   succInj Refl = Refl@@ -397,29 +408,30 @@   lneqSuccLeq n m =     case sCompare n m of       SEQ ->-        start (n %:< m)+        start (n %< m)           =~= SFalse-          === (sSucc n %:<= n) `because` sym (succLeqAbsurd' n)-          === (sSucc n %:<= m) `because` sLeqCongR (sSucc n) (eqToRefl n m Refl)+          === (sSucc n %<= n) `because` sym (succLeqAbsurd' n)+          === (sSucc n %<= m) `because` sLeqCongR (sSucc n) (eqToRefl n m Refl)       SLT -> withWitness (ltToSuccLeq n m Refl) $-        start (n %:< m)+        start (n %< m)           =~= STrue-          =~= (sSucc n %:<= m)+          =~= (sSucc n %<= m)       SGT ->-        case sSucc n %:<= m of+        case sSucc n %<= m of           SFalse -> Refl           STrue  -> eliminate $ succLeqToLT n m Witness -instance Monomorphicable (Sing :: TL.Nat -> *) where-  type MonomorphicRep (Sing :: TL.Nat -> *) = Integer-  demote  (Monomorphic sn) = fromSing sn-  {-# INLINE demote #-}+-- instance Monomorphicable (Sing :: TL.Nat -> *) where+--   type MonomorphicRep (Sing :: TL.Nat -> *) = Integer+--   demote  (Monomorphic sn) = fromSing sn+--   {-# INLINE demote #-} -  promote n = case toSing n of SomeSing k -> Monomorphic k-  {-# INLINE promote #-}+--   promote n = case toSing n of SomeSing k -> Monomorphic k+--   {-# INLINE promote #-}  -- | Quotesi-quoter for singleton types for @'GHC.TypeLits.Nat'@. This can be used for an expression. -----  For example: @[snat|12|] '%:+' [snat| 5 |]@.+--  For example: @[snat|12|] '%+' [snat| 5 |]@. snat :: QuasiQuoter snat = mkSNatQQ [t| TL.Nat |]+

@@ -9,8 +9,8 @@ import Data.Type.Natural.Class.Order  import Data.Singletons.Prelude   (FromInteger, Sing, sing)-import Language.Haskell.TH-import Language.Haskell.TH.Quote+import Language.Haskell.TH       (ExpQ, TypeQ, litT, numTyLit, sigT)+import Language.Haskell.TH.Quote (QuasiQuoter (..))  -- | Quasiquoter generateor for specific peano-types. --

@@ -1,22 +1,38 @@-{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts        #-}+{-# LANGUAGE CPP, DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts   #-} {-# LANGUAGE FlexibleInstances, GADTs, KindSignatures                      #-} {-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies            #-}-{-# LANGUAGE TypeInType, ViewPatterns                                      #-}+{-# LANGUAGE TypeInType, ViewPatterns , ExplicitNamespaces                 #-} module Data.Type.Natural.Class.Arithmetic        (Zero, One, S, sZero, sOne, ZeroOrSucc(..),         plusCong, plusCongR, plusCongL, succCong,         multCong, multCongL, multCongR,         minusCong, minusCongL, minusCongR,         IsPeano(..), pattern Zero, pattern Succ,+        module Data.Type.Natural.Singleton.Compat        ) where-import Data.Singletons.Decide-import Data.Singletons.Prelude-import Data.Singletons.Prelude.Enum-import Data.Type.Equality-import Data.Void-import Proof.Equational+import Data.Type.Natural.Singleton.Compat+  (type (/=), type (==), type (+), type (*), type (-)+  ,type (/=@#@$) ,type (/=@#@$$), type (/=@#@$$$)+  ,type (==@#@$) ,type (==@#@$$), type (==@#@$$$)+  ,type (+@#@$) ,type (+@#@$$), type (+@#@$$$)+  ,type (*@#@$) ,type (*@#@$$), type (*@#@$$$)+  ,type (-@#@$) ,type (-@#@$$), type (-@#@$$$)+  ,(%==), (%/=), (%+), (%*), (%-)+  , FromInteger, FromIntegerSym0, FromIntegerSym1+  ,SNum(..), PNum(..)+  ) +import Data.Functor.Const           (Const (..))+import Data.Singletons.Decide       (SDecide (..))+import Data.Singletons.Prelude      (Apply, SingI (..), SingKind (..),+                                     SomeSing (..), Sing)+import Data.Singletons.Prelude.Enum (Pred, SEnum (..), Succ, sPred, sSucc)+import Data.Type.Equality           ((:~:) (..))+import Data.Void                    (Void, absurd)+import Numeric.Natural              (Natural)+import Proof.Equational             (because, coerce, start, sym, trans, (===))+ type family Zero nat :: nat where   Zero nat = FromInteger 0 @@ -37,34 +53,34 @@ predCong :: n :~: m -> Pred n :~: Pred m predCong Refl = Refl -plusCong :: n :~: m -> n' :~: m' -> n :+ n' :~: m :+ m'+plusCong :: n :~: m -> n' :~: m' -> n + n' :~: m + m' plusCong Refl Refl = Refl -plusCongL :: n :~: m -> Sing k -> n :+ k :~: m :+ k+plusCongL :: n :~: m -> Sing k -> n + k :~: m + k plusCongL Refl _ = Refl -plusCongR :: Sing k -> n :~: m -> k :+ n :~: k :+ m+plusCongR :: Sing k -> n :~: m -> k + n :~: k + m plusCongR _ Refl = Refl  succCong :: n :~: m -> S n :~: S m succCong Refl = Refl -multCong :: n :~: m -> l :~: k -> n :* l :~: m :* k+multCong :: n :~: m -> l :~: k -> n * l :~: m * k multCong Refl Refl = Refl -multCongL :: n :~: m -> Sing k -> n :* k :~: m :* k+multCongL :: n :~: m -> Sing k -> n * k :~: m * k multCongL Refl _ = Refl -multCongR :: Sing k -> n :~: m -> k :* n :~: k :* m+multCongR :: Sing k -> n :~: m -> k * n :~: k * m multCongR _ Refl = Refl -minusCong :: n :~: m -> l :~: k -> n :- l :~: m :- k+minusCong :: n :~: m -> l :~: k -> n - l :~: m - k minusCong Refl Refl = Refl -minusCongL :: n :~: m -> Sing k -> n :- k :~: m :- k+minusCongL :: n :~: m -> Sing k -> n - k :~: m - k minusCongL Refl _ = Refl -minusCongR :: Sing k -> n :~: m -> k :- n :~: k :- m+minusCongR :: Sing k -> n :~: m -> k - n :~: k - m minusCongR _ Refl = Refl  data ZeroOrSucc (n :: nat) where@@ -80,42 +96,42 @@ newtype IdentityR op e (n :: nat) = IdentityR { idRProof :: Apply (op n) e :~: n } newtype IdentityL op e (n :: nat) = IdentityL { idLProof :: Apply (op e) n :~: n } -type PlusZeroR (n :: nat) = IdentityR (:+$$) (Zero nat) n+type PlusZeroR (n :: nat) = IdentityR (+@#@$$) (Zero nat) n newtype PlusSuccR (n :: nat) =-  PlusSuccR { plusSuccRProof :: forall m. Sing m -> n :+ S m :~: S (n :+ m) }+  PlusSuccR { plusSuccRProof :: forall m. Sing m -> n + S m :~: S (n + m) } -type PlusZeroL (n :: nat) = IdentityL (:+$$) (Zero nat) n+type PlusZeroL (n :: nat) = IdentityL (+@#@$$) (Zero nat) n newtype PlusSuccL (m :: nat) =-  PlusSuccL { plusSuccLProof :: forall n. Sing n -> S n :+ m :~: S (n :+ m) }+  PlusSuccL { plusSuccLProof :: forall n. Sing n -> S n + m :~: S (n + m) }  newtype Comm op n = Comm { commProof :: forall m. Sing m -> Apply (op n) m :~: Apply (op m) n } -type PlusComm = Comm (:+$$)+type PlusComm = Comm (+@#@$$) -newtype MultZeroL (n :: nat) =  MultZeroL { multZeroLProof :: Zero nat :* n :~: Zero nat }+newtype MultZeroL (n :: nat) =  MultZeroL { multZeroLProof :: Zero nat * n :~: Zero nat } newtype MultZeroR (n :: nat) =-  MultZeroR { multZeroRProof :: n :* Zero nat :~: Zero nat }+  MultZeroR { multZeroRProof :: n * Zero nat :~: Zero nat } -newtype MultSuccL (m :: nat) = MultSuccL { multSuccLProof :: forall n. Sing n -> S n :* m :~: n :* m :+ m }-newtype MultSuccR (n :: nat) = MultSuccR { multSuccRProof :: forall m. Sing m -> n :* S m :~: n :* m :+ n }+newtype MultSuccL (m :: nat) = MultSuccL { multSuccLProof :: forall n. Sing n -> S n * m :~: n * m + m }+newtype MultSuccR (n :: nat) = MultSuccR { multSuccRProof :: forall m. Sing m -> n * S m :~: n * m + n }  newtype PlusMultDistrib (n :: nat) =   PlusMultDistrib { plusMultDistribProof :: forall m l. Sing m -> Sing l-                                         -> (n :+ m) :* l :~: n :* l :+ m :* l+                                         -> (n + m) * l :~: (n * l) + (m * l)                   }  newtype PlusEqCancelL (n :: nat) =   PlusEqCancelL { plusEqCancelLProof :: forall m l . Sing m -> Sing l-                                                       -> n :+ m :~: n :+ l -> m :~: l }+                                                       -> n + m :~: n + l -> m :~: l } -newtype SuccPlusL (n :: nat) = SuccPlusL { proofSuccPlusL :: Succ n :~: One nat :+ n }+newtype SuccPlusL (n :: nat) = SuccPlusL { proofSuccPlusL :: Succ n :~: One nat + n } newtype MultEqCancelR n =   MultEqCancelR { proofMultEqCancelR :: forall m l. Sing m -> Sing l-                                        -> n :* Succ l :~: m :* Succ l+                                        -> n * Succ l :~: m * Succ l                                         -> n :~: m                 } -class (SDecide nat, SNum nat, SEnum nat)+class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind nat)     => IsPeano nat where   {-# MINIMAL succOneCong, succNonCyclic, predSucc, plusMinus,               succInj, ( (plusZeroL, plusSuccL) | (plusZeroR, plusZeroL))@@ -128,15 +144,15 @@   succInj' _ _  = succInj   succNonCyclic :: Sing n -> Succ n :~: Zero nat -> Void   induction     :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k-  plusMinus :: Sing (n :: nat) -> Sing m -> n :+ m :- m :~: n+  plusMinus :: Sing (n :: nat) -> Sing m -> n + m - m :~: n -  plusMinus' :: Sing (n :: nat) -> Sing m -> n :+ m :- n :~: m+  plusMinus' :: Sing (n :: nat) -> Sing m -> n + m - n :~: m   plusMinus'  n m =-    start (n %:+ m %:- n)-      === m %:+ n %:- n   `because` minusCongL (plusComm n m) n+    start (n %+ m %- n)+      === m %+ n %- n   `because` minusCongL (plusComm n m) n       === m               `because` plusMinus m n -  plusZeroL :: Sing n -> (Zero nat :+ n) :~: n+  plusZeroL :: Sing n -> (Zero nat + n) :~: n   plusZeroL sn = idLProof (induction base step sn)     where       base :: PlusZeroL (Zero nat)@@ -144,27 +160,27 @@        step :: Sing (n :: nat) -> PlusZeroL n -> PlusZeroL (S n)       step sk (IdentityL ih) = IdentityL $-        start (sZero %:+ sS sk)-          === sS (sZero %:+ sk) `because` plusSuccR sZero sk+        start (sZero %+ sS sk)+          === sS (sZero %+ sk) `because` plusSuccR sZero sk           === sS sk             `because` succCong ih -  plusSuccL :: Sing n -> Sing m -> S n :+ m :~: S (n :+ m :: nat)+  plusSuccL :: Sing n -> Sing m -> S n + m :~: S (n + m :: nat)   plusSuccL sn0 sm0 = plusSuccLProof (induction base step sm0) sn0     where       base :: PlusSuccL (Zero nat)       base = PlusSuccL $ \sn ->-        start (sS sn %:+ sZero)+        start (sS sn %+ sZero)           === sS sn             `because` plusZeroR (sS sn)-          === sS (sn %:+ sZero) `because` succCong (sym $ plusZeroR sn)+          === sS (sn %+ sZero) `because` succCong (sym $ plusZeroR sn)        step :: Sing (n :: nat) -> PlusSuccL n -> PlusSuccL (S n)       step sm (PlusSuccL ih) = PlusSuccL $ \sn ->-        start (sS sn %:+ sS sm)-        === sS (sS sn %:+ sm)   `because` plusSuccR (sS sn) sm-        === sS (sS (sn %:+ sm)) `because` succCong (ih sn)-        === sS (sn %:+ sS sm)   `because` succCong (sym $ plusSuccR sn sm)+        start (sS sn %+ sS sm)+        === sS (sS sn %+ sm)   `because` plusSuccR (sS sn) sm+        === sS (sS (sn %+ sm)) `because` succCong (ih sn)+        === sS (sn %+ sS sm)   `because` succCong (sym $ plusSuccR sn sm) -  plusZeroR :: Sing n -> (n :+ Zero nat) :~: n+  plusZeroR :: Sing n -> (n + Zero nat) :~: n   plusZeroR sn = idRProof (induction base step sn)     where       base :: PlusZeroR (Zero nat)@@ -172,64 +188,64 @@        step :: Sing (n :: nat) -> PlusZeroR n -> PlusZeroR (S n)       step sk (IdentityR ih) = IdentityR $-        start (sS sk %:+ sZero)-          === sS (sk %:+ sZero) `because` plusSuccL sk sZero+        start (sS sk %+ sZero)+          === sS (sk %+ sZero) `because` plusSuccL sk sZero           === sS sk             `because` succCong ih -  plusSuccR :: Sing n -> Sing m -> n :+ S m :~: S (n :+ m :: nat)+  plusSuccR :: Sing n -> Sing m -> n + S m :~: S (n + m :: nat)   plusSuccR sn0 = plusSuccRProof (induction base step sn0)     where       base :: PlusSuccR (Zero nat)       base = PlusSuccR $ \sk ->-        start (sZero %:+ sS sk)+        start (sZero %+ sS sk)           === sS sk             `because` plusZeroL (sS sk)-          === sS (sZero %:+ sk) `because` succCong (sym $ plusZeroL sk)+          === sS (sZero %+ sk) `because` succCong (sym $ plusZeroL sk)        step :: Sing (n :: nat) -> PlusSuccR n -> PlusSuccR (S n)       step sn (PlusSuccR ih) = PlusSuccR $ \sk ->-        start (sS sn %:+ sS sk)-        === sS (sn %:+ sS sk)    `because` plusSuccL sn (sS sk)-        === sS (sS (sn %:+ sk))  `because` succCong (ih sk)-        === sS (sS sn %:+ sk)    `because` succCong (sym $ plusSuccL sn sk)+        start (sS sn %+ sS sk)+        === sS (sn %+ sS sk)    `because` plusSuccL sn (sS sk)+        === sS (sS (sn %+ sk))  `because` succCong (ih sk)+        === sS (sS sn %+ sk)    `because` succCong (sym $ plusSuccL sn sk) -  plusComm  :: Sing n -> Sing m -> n :+ m :~: (m :: nat) :+ n+  plusComm  :: Sing n -> Sing m -> n + m :~: (m :: nat) + n   plusComm sn0 = commProof (induction base step sn0)     where       base :: PlusComm (Zero nat)       base = Comm $ \sk ->-        start (sZero %:+ sk)+        start (sZero %+ sk)           === sk             `because` plusZeroL sk-          === (sk %:+ sZero) `because` sym (plusZeroR sk)+          === (sk %+ sZero) `because` sym (plusZeroR sk)        step :: Sing (n :: nat) -> PlusComm n -> PlusComm (S n)       step sn (Comm ih) = Comm $ \sk ->-        start (sS sn %:+ sk)-          === sS (sn %:+ sk) `because` plusSuccL sn sk-          === sS (sk %:+ sn) `because` succCong (ih sk)-          === sk %:+ sS sn   `because` sym (plusSuccR sk sn)+        start (sS sn %+ sk)+          === sS (sn %+ sk) `because` plusSuccL sn sk+          === sS (sk %+ sn) `because` succCong (ih sk)+          === sk %+ sS sn   `because` sym (plusSuccR sk sn)    plusAssoc :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l-            -> (n :+ m) :+ l :~: n :+ (m :+ l)+            -> (n + m) + l :~: n + (m + l)   plusAssoc sn m l = assocProof (induction base step sn) m l     where-      base :: Assoc (:+$$) (Zero nat)+      base :: Assoc (+@#@$$) (Zero nat)       base = Assoc $ \ sk sl ->-        start ((sZero %:+ sk) %:+ sl)-          === sk %:+ sl+        start ((sZero %+ sk) %+ sl)+          === sk %+ sl               `because` plusCongL (plusZeroL sk) sl-          === (sZero %:+ (sk %:+ sl))-              `because` sym (plusZeroL (sk %:+ sl))+          === (sZero %+ (sk %+ sl))+              `because` sym (plusZeroL (sk %+ sl)) -      step :: forall k . Sing (k :: nat) -> Assoc (:+$$) k -> Assoc (:+$$) (S k)+      step :: forall k . Sing (k :: nat) -> Assoc (+@#@$$) k -> Assoc (+@#@$$) (S k)       step sk (Assoc ih) = Assoc $ \ sl su ->-        start ((sS sk %:+ sl) %:+ su)-        ===   (sS (sk %:+ sl) %:+ su) `because` plusCongL (plusSuccL sk sl) su-        ===   sS (sk %:+ sl %:+ su)   `because` plusSuccL (sk %:+ sl) su-        ===   sS (sk %:+ (sl %:+ su)) `because` succCong (ih sl su)-        ===   sS sk %:+ (sl %:+ su)   `because` sym (plusSuccL sk (sl %:+ su))+        start ((sS sk %+ sl) %+ su)+        ===   (sS (sk %+ sl) %+ su) `because` plusCongL (plusSuccL sk sl) su+        ===   sS (sk %+ sl %+ su)   `because` plusSuccL (sk %+ sl) su+        ===   sS (sk %+ (sl %+ su)) `because` succCong (ih sl su)+        ===   sS sk %+ (sl %+ su)   `because` sym (plusSuccL sk (sl %+ su))  -  multZeroL :: Sing n -> Zero nat :* n :~: Zero nat+  multZeroL :: Sing n -> Zero nat * n :~: Zero nat   multZeroL sn0 = multZeroLProof $ induction base step sn0     where       base :: MultZeroL (Zero nat)@@ -237,41 +253,41 @@        step :: Sing (k :: nat) -> MultZeroL k ->  MultZeroL (S k)       step sk (MultZeroL ih) = MultZeroL $-        start (sZero %:* sS sk)-        === sZero %:* sk %:+ sZero  `because` multSuccR sZero sk-        === sZero %:* sk            `because` plusZeroR (sZero %:* sk)+        start (sZero %* sS sk)+        === sZero %* sk %+ sZero  `because` multSuccR sZero sk+        === sZero %* sk            `because` plusZeroR (sZero %* sk)         === sZero                   `because` ih -  multSuccL :: Sing (n :: nat) -> Sing m -> S n :* m :~: n :* m :+ m+  multSuccL :: Sing (n :: nat) -> Sing m -> S n * m :~: n * m + m   multSuccL sn0 sm0 = multSuccLProof (induction base step sm0) sn0     where       base :: MultSuccL (Zero nat)       base = MultSuccL $ \sk ->-        start (sS sk %:* sZero)+        start (sS sk %* sZero)           === sZero                  `because` multZeroR (sS sk)-          === sk %:* sZero           `because` sym (multZeroR sk)-          === sk %:* sZero %:+ sZero `because` sym (plusZeroR (sk %:* sZero))+          === sk %* sZero           `because` sym (multZeroR sk)+          === sk %* sZero %+ sZero `because` sym (plusZeroR (sk %* sZero))        step :: Sing (m :: nat) -> MultSuccL m -> MultSuccL (S m)       step sm (MultSuccL ih) = MultSuccL $ \sk ->-        start (sS sk %:* sS sm)-          === sS sk %:* sm       %:+ sS sk+        start (sS sk %* sS sm)+          === sS sk %* sm       %+ sS sk               `because` multSuccR (sS sk) sm-          === (sk %:* sm %:+ sm) %:+ sS sk+          === (sk %* sm %+ sm) %+ sS sk               `because` plusCongL (ih sk) (sS sk)-          === sS ((sk %:* sm %:+ sm) %:+ sk)-              `because` plusSuccR (sk %:* sm %:+ sm) sk-          === sS (sk %:* sm %:+ (sm %:+ sk))-              `because` succCong (plusAssoc (sk %:* sm) sm sk)-          === sS (sk %:* sm %:+ (sk %:+ sm))-              `because` succCong (plusCongR (sk %:* sm) (plusComm sm sk))-          === sS ((sk %:* sm %:+ sk) %:+ sm)-              `because` succCong (sym $ plusAssoc (sk %:* sm) sk sm)-          === sS ((sk %:* sS sm) %:+ sm)+          === sS ((sk %* sm %+ sm) %+ sk)+              `because` plusSuccR (sk %* sm %+ sm) sk+          === sS (sk %* sm %+ (sm %+ sk))+              `because` succCong (plusAssoc (sk %* sm) sm sk)+          === sS (sk %* sm %+ (sk %+ sm))+              `because` succCong (plusCongR (sk %* sm) (plusComm sm sk))+          === sS ((sk %* sm %+ sk) %+ sm)+              `because` succCong (sym $ plusAssoc (sk %* sm) sk sm)+          === sS ((sk %* sS sm) %+ sm)               `because` succCong (plusCongL (sym $ multSuccR sk sm) sm)-          === sk %:* sS sm %:+ sS sm `because` sym (plusSuccR (sk %:* sS sm) sm)+          === sk %* sS sm %+ sS sm `because` sym (plusSuccR (sk %* sS sm) sm) -  multZeroR :: Sing n -> n :* Zero nat :~: Zero nat+  multZeroR :: Sing n -> n * Zero nat :~: Zero nat   multZeroR sn0 = multZeroRProof $ induction base step sn0     where       base :: MultZeroR (Zero nat)@@ -279,180 +295,180 @@        step :: Sing (k :: nat) -> MultZeroR k ->  MultZeroR (S k)       step sk (MultZeroR ih) = MultZeroR $-        start (sS sk %:* sZero)-        === sk %:* sZero %:+ sZero  `because` multSuccL sk sZero-        === sk %:* sZero            `because` plusZeroR (sk %:* sZero)+        start (sS sk %* sZero)+        === sk %* sZero %+ sZero  `because` multSuccL sk sZero+        === sk %* sZero            `because` plusZeroR (sk %* sZero)         === sZero                   `because` ih -  multSuccR :: Sing n -> Sing m -> n :* S m :~: n :* m :+ (n :: nat)+  multSuccR :: Sing n -> Sing m -> n * S m :~: n * m + (n :: nat)   multSuccR sn0 = multSuccRProof $ induction base step sn0     where       base :: MultSuccR (Zero nat)       base = MultSuccR $ \sk ->-        start (sZero %:* sS sk)+        start (sZero %* sS sk)           === sZero               `because` multZeroL (sS sk)-          === sZero %:* sk+          === sZero %* sk               `because` sym (multZeroL sk)-          === sZero %:* sk %:+ sZero-              `because` sym (plusZeroR (sZero %:* sk))+          === sZero %* sk %+ sZero+              `because` sym (plusZeroR (sZero %* sk))         step :: Sing (n :: nat) -> MultSuccR n -> MultSuccR (S n)       step sn (MultSuccR ih) = MultSuccR $ \sk ->-        start (sS sn %:* sS sk)-          === sn %:* sS sk %:+ sS sk+        start (sS sn %* sS sk)+          === sn %* sS sk %+ sS sk               `because` multSuccL sn (sS sk)-          === sS (sn %:* sS sk %:+ sk)-              `because` plusSuccR (sn %:* sS sk) sk-          === sS (sn %:* sk %:+ sn %:+ sk)+          === sS (sn %* sS sk %+ sk)+              `because` plusSuccR (sn %* sS sk) sk+          === sS (sn %* sk %+ sn %+ sk)               `because` succCong (plusCongL (ih sk) sk)-          === sS (sn %:* sk %:+ (sn %:+ sk))-              `because` succCong (plusAssoc (sn %:* sk) sn sk)-          === sS (sn %:* sk %:+ (sk %:+ sn))-              `because` succCong (plusCongR (sn %:* sk) (plusComm sn sk))-          === sS (sn %:* sk %:+ sk %:+ sn)-              `because` succCong (sym $ plusAssoc (sn %:* sk) sk sn)-          === sS (sS sn %:* sk %:+ sn)+          === sS (sn %* sk %+ (sn %+ sk))+              `because` succCong (plusAssoc (sn %* sk) sn sk)+          === sS (sn %* sk %+ (sk %+ sn))+              `because` succCong (plusCongR (sn %* sk) (plusComm sn sk))+          === sS (sn %* sk %+ sk %+ sn)+              `because` succCong (sym $ plusAssoc (sn %* sk) sk sn)+          === sS (sS sn %* sk %+ sn)               `because` succCong (plusCongL (sym $ multSuccL sn sk) sn)-          === sS sn %:* sk %:+ sS sn-              `because` sym (plusSuccR (sS sn %:* sk) sn)+          === sS sn %* sk %+ sS sn+              `because` sym (plusSuccR (sS sn %* sk) sn)  -  multComm  :: Sing (n :: nat) -> Sing m -> n :* m :~: m :* n+  multComm  :: Sing (n :: nat) -> Sing m -> n * m :~: m * n   multComm sn0 = commProof (induction base step sn0)     where-      base :: Comm (:*$$) (Zero nat)+      base :: Comm (*@#@$$) (Zero nat)       base = Comm $ \sk ->-        start (sZero %:* sk)+        start (sZero %* sk)           === sZero           `because` multZeroL sk-          === sk %:* sZero    `because` sym (multZeroR sk)+          === sk %* sZero    `because` sym (multZeroR sk) -      step :: Sing (n :: nat) -> Comm (:*$$) n -> Comm (:*$$) (S n)+      step :: Sing (n :: nat) -> Comm (*@#@$$) n -> Comm (*@#@$$) (S n)       step sn (Comm ih) = Comm $ \sk ->-        start (sS sn %:* sk)-          === sn %:* sk %:+ sk `because` multSuccL sn sk-          === sk %:* sn %:+ sk `because` plusCongL (ih sk) sk-          === sk %:* sS sn     `because` sym (multSuccR sk sn)+        start (sS sn %* sk)+          === sn %* sk %+ sk `because` multSuccL sn sk+          === sk %* sn %+ sk `because` plusCongL (ih sk) sk+          === sk %* sS sn     `because` sym (multSuccR sk sn) -  multOneR :: Sing n -> n :* One nat :~: n+  multOneR :: Sing n -> n * One nat :~: n   multOneR sn =-    start (sn %:* sOne)-      === sn %:* sS sZero      `because` multCongR sn (sym $ succOneCong)-      === sn %:* sZero %:+ sn  `because` multSuccR sn sZero-      === sZero %:+ sn         `because` plusCongL (multZeroR sn) sn+    start (sn %* sOne)+      === sn %* sS sZero      `because` multCongR sn (sym $ succOneCong)+      === sn %* sZero %+ sn  `because` multSuccR sn sZero+      === sZero %+ sn         `because` plusCongL (multZeroR sn) sn       === sn                   `because` plusZeroL sn -  multOneL :: Sing n -> One nat :* n :~: n+  multOneL :: Sing n -> One nat * n :~: n   multOneL sn =-    start (sOne %:* sn)-      === sn %:* sOne   `because` multComm sOne sn+    start (sOne %* sn)+      === sn %* sOne   `because` multComm sOne sn       === sn            `because` multOneR sn    plusMultDistrib :: Sing (n :: nat) -> Sing m -> Sing l-                -> (n :+ m) :* l :~: n :* l :+ m :* l+                -> (n + m) * l :~: (n * l) + (m * l)   plusMultDistrib sn0 = plusMultDistribProof $ induction base step sn0     where       base :: PlusMultDistrib (Zero nat)       base = PlusMultDistrib $ \sk sl ->-        start ((sZero %:+ sk) %:* sl)-          === (sk %:* sl)+        start ((sZero %+ sk) %* sl)+          === (sk %* sl)               `because` multCongL (plusZeroL sk) sl-          === sZero %:+ (sk %:* sl)-              `because` sym (plusZeroL (sk %:* sl))-          === sZero %:* sl %:+ sk %:* sl-              `because` plusCongL (sym $ multZeroL sl) (sk %:* sl)+          === sZero %+ (sk %* sl)+              `because` sym (plusZeroL (sk %* sl))+          === sZero %* sl %+ sk %* sl+              `because` plusCongL (sym $ multZeroL sl) (sk %* sl)        step :: Sing (n :: nat) -> PlusMultDistrib n -> PlusMultDistrib (S n)       step sn (PlusMultDistrib ih) = PlusMultDistrib $ \sk sl ->-        start ((sS sn %:+ sk) %:* sl)-          === (sS (sn %:+ sk) %:* sl)           `because` multCongL (plusSuccL sn sk) sl-          === (sn %:+ sk) %:* sl %:+ sl         `because` multSuccL (sn %:+ sk) sl-          === (sn %:* sl %:+ sk %:* sl) %:+ sl  `because` plusCongL (ih sk sl) sl-          === sn %:* sl %:+ (sk %:* sl %:+ sl)  `because` plusAssoc (sn %:* sl) (sk %:* sl) sl-          === sn %:* sl %:+ (sl %:+ sk %:* sl)  `because` plusCongR (sn %:* sl) (plusComm (sk %:* sl) sl)-          === (sn %:* sl %:+ sl) %:+ sk %:* sl  `because` sym (plusAssoc (sn %:* sl) sl (sk %:* sl))-          === (sS sn %:* sl) %:+ sk %:* sl      `because` plusCongL (sym $ multSuccL sn sl) (sk %:* sl)+        start ((sS sn %+ sk) %* sl)+          === (sS (sn %+ sk) %* sl)           `because` multCongL (plusSuccL sn sk) sl+          === (sn %+ sk) %* sl %+ sl         `because` multSuccL (sn %+ sk) sl+          === ((sn %* sl) %+ (sk %* sl)) %+ sl  `because` plusCongL (ih sk sl) sl+          === sn %* sl %+ (sk %* sl %+ sl)  `because` plusAssoc (sn %* sl) (sk %* sl) sl+          === sn %* sl %+ (sl %+ (sk %* sl))  `because` plusCongR (sn %* sl) (plusComm (sk %* sl) sl)+          === (sn %* sl %+ sl) %+ (sk %* sl)  `because` sym (plusAssoc (sn %* sl) sl (sk %* sl))+          === (sS sn %* sl) %+ (sk %* sl)     `because` plusCongL (sym $ multSuccL sn sl) (sk %* sl)    multPlusDistrib :: Sing (n :: nat) -> Sing m -> Sing l-                -> n :* (m :+ l) :~: n :* m :+ n :* l+                -> n * (m + l) :~: (n * m) + (n * l)   multPlusDistrib n m l =-    start (n %:* (m %:+ l))-      === (m %:+ l) %:* n     `because` multComm n (m %:+ l)-      === m %:* n %:+ l %:* n `because` plusMultDistrib m l n-      === n %:* m %:+ n %:* l `because` plusCong (multComm m n) (multComm l n)+    start (n %* (m %+ l))+      === (m %+ l) %* n     `because` multComm n (m %+ l)+      === m %* n %+ l %* n `because` plusMultDistrib m l n+      === n %* m %+ n %* l `because` plusCong (multComm m n) (multComm l n) -  minusNilpotent :: Sing n -> n :- n :~: Zero nat+  minusNilpotent :: Sing n -> n - n :~: Zero nat   minusNilpotent n =-    start (n %:- n)-      === (sZero %:+ n) %:- n  `because` minusCongL (sym $ plusZeroL n) n+    start (n %- n)+      === (sZero %+ n) %- n  `because` minusCongL (sym $ plusZeroL n) n       === sZero                `because` plusMinus sZero n    multAssoc :: Sing (n :: nat) -> Sing m -> Sing l-            -> (n :* m) :* l :~: n :* (m :* l)+            -> (n * m) * l :~: n * (m * l)   multAssoc sn0 = assocProof $ induction base step sn0     where-      base :: Assoc (:*$$) (Zero nat)+      base :: Assoc (*@#@$$) (Zero nat)       base = Assoc $ \ m l ->-        start (sZero %:* m %:* l)-          === sZero %:* l  `because` multCongL (multZeroL m) l+        start (sZero %* m %* l)+          === sZero %* l  `because` multCongL (multZeroL m) l           === sZero        `because` multZeroL l-          === sZero %:*  (m %:* l) `because` sym (multZeroL (m %:* l))+          === sZero %*  (m %* l) `because` sym (multZeroL (m %* l)) -      step :: Sing (n :: nat) -> Assoc (:*$$) n -> Assoc (:*$$) (S n)+      step :: Sing (n :: nat) -> Assoc (*@#@$$) n -> Assoc (*@#@$$) (S n)       step n _ = Assoc $ \ m l ->-        start (sS n %:* m %:* l)-          === (n %:* m %:+ m) %:* l        `because` multCongL (multSuccL n m) l-          === n %:* m %:* l %:+ m %:* l    `because` plusMultDistrib (n %:* m) m l-          === n %:* (m %:* l) %:+ m %:* l  `because` plusCongL (multAssoc n m l) (m %:* l)-          === sS n %:* (m %:* l)           `because` sym (multSuccL n (m %:* l))+        start (sS n %* m %* l)+          === (n %* m %+ m) %* l        `because` multCongL (multSuccL n m) l+          === n %* m %* l %+ m %* l    `because` plusMultDistrib (n %* m) m l+          === n %* (m %* l) %+ m %* l  `because` plusCongL (multAssoc n m l) (m %* l)+          === sS n %* (m %* l)           `because` sym (multSuccL n (m %* l)) -  plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> n :+ m :~: n :+ l -> m :~: l+  plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> n + m :~: n + l -> m :~: l   plusEqCancelL = plusEqCancelLProof . induction base step     where       base :: PlusEqCancelL (Zero nat)       base = PlusEqCancelL $ \l m nlnm ->-        start l === sZero %:+ l `because` sym (plusZeroL l)-                === sZero %:+ m `because` nlnm+        start l === sZero %+ l `because` sym (plusZeroL l)+                === sZero %+ m `because` nlnm                 === m           `because` plusZeroL m        step :: Sing (n :: nat) -> PlusEqCancelL n -> PlusEqCancelL (Succ n)       step n (PlusEqCancelL ih) = PlusEqCancelL $ \l m snlsnm ->         succInj $ ih (sS l) (sS m) $-          start (n %:+ sS l)-            ===  sS (n %:+ l)  `because` plusSuccR n l-            ===  sS n %:+ l    `because` sym (plusSuccL n l)-            ===  sS n %:+ m    `because` snlsnm-            ===  sS (n %:+ m)  `because` plusSuccL n m-            ===  n %:+ sS m    `because` sym (plusSuccR n m)+          start (n %+ sS l)+            ===  sS (n %+ l)  `because` plusSuccR n l+            ===  sS n %+ l    `because` sym (plusSuccL n l)+            ===  sS n %+ m    `because` snlsnm+            ===  sS (n %+ m)  `because` plusSuccL n m+            ===  n %+ sS m    `because` sym (plusSuccR n m) -  plusEqCancelR :: forall n m l . Sing (n :: nat) -> Sing m -> Sing l -> n :+ l :~: m :+ l -> n :~: m+  plusEqCancelR :: forall n m l . Sing (n :: nat) -> Sing m -> Sing l -> n + l :~: m + l -> n :~: m   plusEqCancelR n m l nlml = plusEqCancelL l n m $-    start (l %:+ n)-      === (n %:+ l) `because` plusComm l n-      === (m %:+ l) `because` nlml-      === (l %:+ m) `because` plusComm m l+    start (l %+ n)+      === (n %+ l) `because` plusComm l n+      === (m %+ l) `because` nlml+      === (l %+ m) `because` plusComm m l -  succAndPlusOneL :: Sing n -> Succ n :~: One nat :+ n+  succAndPlusOneL :: Sing n -> Succ n :~: One nat + n   succAndPlusOneL = proofSuccPlusL . induction base step     where       base :: SuccPlusL (Zero nat)       base = SuccPlusL $              start (sSucc sZero)                === sOne           `because` succOneCong-               === sOne %:+ sZero `because` sym (plusZeroR sOne)+               === sOne %+ sZero `because` sym (plusZeroR sOne)        step :: Sing (n :: nat) -> SuccPlusL n -> SuccPlusL (Succ n)       step sn (SuccPlusL ih) = SuccPlusL $         start (sSucc (sSucc sn))-          === sSucc (sOne %:+ sn) `because` succCong ih-          === sOne %:+ sSucc sn   `because` sym (plusSuccR sOne sn)+          === sSucc (sOne %+ sn) `because` succCong ih+          === sOne %+ sSucc sn   `because` sym (plusSuccR sOne sn) -  succAndPlusOneR :: Sing n -> Succ n :~: n :+ One nat+  succAndPlusOneR :: Sing n -> Succ n :~: n + One nat   succAndPlusOneR n =     start (sSucc n)-      === sOne %:+ n `because` succAndPlusOneL n-      === n %:+ sOne `because` plusComm sOne n+      === sOne %+ n `because` succAndPlusOneL n+      === n %+ sOne `because` plusComm sOne n    predSucc :: Sing n -> Pred (Succ n) :~: (n :: nat) @@ -462,13 +478,13 @@       base = IsZero       step sn _ = IsSucc sn -  plusEqZeroL :: Sing n -> Sing m -> n :+ m :~: Zero nat -> n :~: Zero nat+  plusEqZeroL :: Sing n -> Sing m -> n + m :~: Zero nat -> n :~: Zero nat   plusEqZeroL n m Refl =     case zeroOrSucc n of-      IsZero -> Refl-      IsSucc pn -> absurd $ succNonCyclic (pn %:+ m) (sym $ plusSuccL pn m)+      IsZero    -> Refl+      IsSucc pn -> absurd $ succNonCyclic (pn %+ m) (sym $ plusSuccL pn m) -  plusEqZeroR :: Sing n -> Sing m -> n :+ m :~: Zero nat -> m :~: Zero nat+  plusEqZeroR :: Sing n -> Sing m -> n + m :~: Zero nat -> m :~: Zero nat   plusEqZeroR n m = plusEqZeroL m n . trans (plusComm m n)    predUnique :: Sing (n :: nat) -> Sing m -> Succ n :~: m -> n :~: Pred m@@ -476,66 +492,75 @@     start n === (sPred (sSucc n)) `because` sym (predSucc n)             === sPred m           `because` predCong snEm -  multEqSuccElimL :: Sing (n :: nat) -> Sing m -> Sing l -> n :* m :~: Succ l -> n :~: Succ (Pred n)+  multEqSuccElimL :: Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> n :~: Succ (Pred n)   multEqSuccElimL n m l nmEsl =     case zeroOrSucc n of       IsZero -> absurd $ succNonCyclic l $ sym $-                start sZero === sZero %:* m `because` sym (multZeroL m)+                start sZero === sZero %* m `because` sym (multZeroL m)                             === sSucc l     `because` nmEsl       IsSucc pn -> succCong (predUnique pn n Refl) -  multEqSuccElimR :: Sing (n :: nat) -> Sing m -> Sing l -> n :* m :~: Succ l -> m :~: Succ (Pred m)+  multEqSuccElimR :: Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> m :~: Succ (Pred m)   multEqSuccElimR n m l nmEsl =     multEqSuccElimL m n l (multComm m n `trans` nmEsl) -  minusZero :: Sing n -> n :- Zero nat :~: n+  minusZero :: Sing n -> n - Zero nat :~: n   minusZero n =-    start (n %:- sZero)-      === (n %:+ sZero) %:- sZero+    start (n %- sZero)+      === (n %+ sZero) %- sZero              `because` minusCongL (sym $ plusZeroR n) sZero       === n  `because` plusMinus n sZero -  multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> n :* Succ l :~: m :* Succ l -> n :~: m+  multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> n * Succ l :~: m * Succ l -> n :~: m   multEqCancelR = proofMultEqCancelR . induction base step     where       base :: MultEqCancelR (Zero nat)       base = MultEqCancelR $ \m l zslmsl ->-        sym $ plusEqZeroR (m %:* l) m $ sym $ start sZero-          === sZero %:* l            `because` sym (multZeroL l)-          === sZero %:* l %:+ sZero  `because` sym (plusZeroR (sZero %:* l))-          === sZero %:* sSucc l      `because` sym (multSuccR sZero l)-          === m     %:* sSucc l      `because` zslmsl-          === m %:* l %:+ m          `because` multSuccR m l+        sym $ plusEqZeroR (m %* l) m $ sym $ start sZero+          === sZero %* l            `because` sym (multZeroL l)+          === sZero %* l %+ sZero  `because` sym (plusZeroR (sZero %* l))+          === sZero %* sSucc l      `because` sym (multSuccR sZero l)+          === m     %* sSucc l      `because` zslmsl+          === m %* l %+ m          `because` multSuccR m l        step :: Sing (n :: nat) -> MultEqCancelR n -> MultEqCancelR (Succ n)       step n (MultEqCancelR ih) = MultEqCancelR $ \m l snmssnl ->         let m' = sPred m-            pf = start (m %:* sSucc l)-                   === sSucc n %:* sSucc l         `because` sym snmssnl-                   === n %:* sSucc l %:+ sSucc l   `because` multSuccL n (sSucc l)-                   === sSucc (n %:* sSucc l %:+ l) `because` plusSuccR (n %:* sSucc l) l-            sm'Em = multEqSuccElimL m (sSucc l) (n %:* sSucc l %:+ l) pf-            pf' = ih m' l $ plusEqCancelR (n %:* sSucc l) (m' %:* sSucc l) (sSucc l) $-                  start (n %:* sSucc l %:+ sSucc l)-                    === sSucc (n %:* sSucc l %:+ l)  `because` plusSuccR (n %:* sSucc l) l-                    === m %:* sSucc l                `because` sym pf-                    === sSucc m' %:* sSucc l         `because` multCongL sm'Em (sSucc l)-                    === (m' %:* sSucc l %:+ sSucc l) `because` multSuccL m' (sSucc l)+            pf = start (m %* sSucc l)+                   === sSucc n %* sSucc l         `because` sym snmssnl+                   === n %* sSucc l %+ sSucc l   `because` multSuccL n (sSucc l)+                   === sSucc (n %* sSucc l %+ l) `because` plusSuccR (n %* sSucc l) l+            sm'Em = multEqSuccElimL m (sSucc l) (n %* sSucc l %+ l) pf+            pf' = ih m' l $ plusEqCancelR (n %* sSucc l) (m' %* sSucc l) (sSucc l) $+                  start (n %* sSucc l %+ sSucc l)+                    === sSucc (n %* sSucc l %+ l)  `because` plusSuccR (n %* sSucc l) l+                    === m %* sSucc l                `because` sym pf+                    === sSucc m' %* sSucc l         `because` multCongL sm'Em (sSucc l)+                    === (m' %* sSucc l %+ sSucc l) `because` multSuccL m' (sSucc l)         in succCong pf' `trans` sym sm'Em    succPred :: Sing n -> (n :~: Zero nat -> Void) -> Succ (Pred n) :~: n   succPred n nonZero =     case zeroOrSucc n of-      IsZero -> absurd $ nonZero Refl+      IsZero    -> absurd $ nonZero Refl       IsSucc n' -> sym $ succCong $ predUnique n' n Refl -  multEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> Succ n :* m :~: Succ n :* l -> m :~: l+  multEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> Succ n * m :~: Succ n * l -> m :~: l   multEqCancelL n m l snmEsnl =     multEqCancelR m l n $     multComm m (sSucc n) `trans` snmEsnl `trans` multComm (sSucc n) l    sPred' :: proxy n -> Sing (Succ n) -> Sing (n :: nat)   sPred' pxy sn = coerce (succInj $ succCong $ predSucc (sPred' pxy sn)) (sPred sn)++  toNatural :: Sing (n :: nat) -> Natural+  toNatural = getConst . induction (Const 0) (\_ (Const k) -> (Const k + 1))++  fromNatural :: Natural -> SomeSing nat+  fromNatural 0 = SomeSing sZero+  fromNatural n =+    case fromNatural (n - 1) of+      SomeSing sn -> SomeSing (Succ sn)  pattern Zero :: forall nat (n :: nat). IsPeano nat => n ~ Zero nat => Sing n pattern Zero <- (zeroOrSucc -> IsZero) where

@@ -1,44 +1,59 @@-{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts         #-}-{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures                       #-}+{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, ExplicitNamespaces       #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures     #-} {-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes  #-} {-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, TypeInType #-} module Data.Type.Natural.Class.Order        (PeanoOrder(..), DiffNat(..), LeqView(..),         FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR,         sLeqCongL, sLeqCongR, sLeqCong,-        (:-.), (%:-.), minPlusTruncMinus, truncMinusLeq+        type (-.), (%-.), minPlusTruncMinus, truncMinusLeq,+        module Data.Type.Natural.Singleton.Compat        ) where import Data.Type.Natural.Class.Arithmetic+import Data.Type.Natural.Singleton.Compat (type (<), type (<=), type (<=@#@$),+                                           type (<=@#@$$), type (<=@#@$$$),+                                           type (<@#@$), type (<@#@$$),+                                           type (<@#@$$$), type (>), type (>=),+                                           type (>=@#@$), type (>=@#@$$),+                                           type (>=@#@$$$), type (>@#@$),+                                           type (>@#@$$), type (>@#@$$$),+                                           type Min, type Max, type Compare,+                                           type MinSym0, type MinSym1, type MinSym2,+                                           type MaxSym0, type MaxSym1, type MaxSym2,+                                           type CompareSym0, type CompareSym1, type CompareSym2,+                                           Sing (SLT, SEQ, SGT), SOrd(..), POrd(..),+                                           LTSym0, GTSym0, EQSym0,+                                           (%<), (%<=), (%>), (%>=)) -import Data.Singletons.Decide-import Data.Singletons.Prelude-import Data.Singletons.Prelude.Enum-import Data.Singletons.TH-import Data.Type.Equality-import Data.Void-import Proof.Equational-import Proof.Propositional+import Data.Singletons.Prelude      (Sing (SFalse, STrue), sing, withSingI)+import Data.Singletons.Prelude.Enum (Pred, SEnum (..), Succ)+import Data.Singletons.TH           (singletonsOnly)+import Data.Type.Equality           ((:~:) (..))+import Data.Void                    (Void, absurd)+import Proof.Equational             (because, coerce, start, sym, trans,+                                     withRefl, (===), (=~=))+import Proof.Propositional          (IsTrue (..), eliminate, withWitness)  data LeqView (n :: nat) (m :: nat) where   LeqZero :: Sing n -> LeqView (Zero nat) n-  LeqSucc :: Sing n -> Sing m -> IsTrue (n :<= m) -> LeqView (Succ n) (Succ m)+  LeqSucc :: Sing n -> Sing m -> IsTrue (n <= m) -> LeqView (Succ n) (Succ m)  data DiffNat n m where-  DiffNat :: Sing n -> Sing m -> DiffNat n (n :+ m)+  DiffNat :: Sing n -> Sing m -> DiffNat n (n + m) -newtype LeqWitPf n = LeqWitPf { leqWitPf :: forall m. Sing m -> IsTrue (n :<= m) -> DiffNat n m }-newtype LeqStepPf n = LeqStepPf { leqStepPf :: forall m l. Sing m -> Sing l -> n :+ l :~: m -> IsTrue (n :<= m) }+newtype LeqWitPf n = LeqWitPf { leqWitPf :: forall m. Sing m -> IsTrue (n <= m) -> DiffNat n m }+newtype LeqStepPf n = LeqStepPf { leqStepPf :: forall m l. Sing m -> Sing l -> n + l :~: m -> IsTrue (n <= m) }  succDiffNat :: IsPeano nat             => Sing n -> Sing m -> DiffNat (n :: nat) m -> DiffNat (Succ n) (Succ m) succDiffNat _ _ (DiffNat n m) = coerce (plusSuccL n m) $ DiffNat (sSucc n) m  coerceLeqL :: forall (n :: nat) m l . IsPeano nat => n :~: m -> Sing l-           -> IsTrue (n :<= l) -> IsTrue (m :<= l)+           -> IsTrue (n <= l) -> IsTrue (m <= l) coerceLeqL Refl _ Witness = Witness  coerceLeqR :: forall (n :: nat) m l . IsPeano nat =>  Sing l -> n :~: m-           -> IsTrue (l :<= n) -> IsTrue (l :<= m)+           -> IsTrue (l <= n) -> IsTrue (l <= m) coerceLeqR _ Refl Witness = Witness  singletonsOnly [d|@@ -54,13 +69,13 @@ compareCongR :: Sing (a :: k) -> b :~: c -> Compare a b :~: Compare a c compareCongR _ Refl = Refl -sLeqCong :: a :~: b -> c :~: d -> (a :<= c) :~: (b :<= d)+sLeqCong :: a :~: b -> c :~: d -> (a <= c) :~: (b <= d) sLeqCong Refl Refl = Refl -sLeqCongL :: a :~: b -> Sing c -> (a :<= c) :~: (b :<= c)+sLeqCongL :: a :~: b -> Sing c -> (a <= c) :~: (b <= c) sLeqCongL Refl _ = Refl -sLeqCongR :: Sing a -> b :~: c -> (a :<= b) :~: (a :<= c)+sLeqCongR :: Sing a -> b :~: c -> (a <= b) :~: (a <= c) sLeqCongR _ Refl = Refl  newtype LTSucc n = LTSucc { proofLTSucc :: Compare n (Succ n) :~: 'LT }@@ -83,7 +98,7 @@               (leqToMin, geqToMin | minLeqL, minLeqR, minLargest),               (leqToMax, geqToMax | maxLeqL, maxLeqR, maxLeast) #-} -  leqToCmp :: Sing (a :: nat) -> Sing b -> IsTrue (a :<= b)+  leqToCmp :: Sing (a :: nat) -> Sing b -> IsTrue (a <= b)            -> Either (a :~: b) (Compare a b :~: 'LT)   eqlCmpEQ :: Sing (a :: nat) -> Sing b -> a :~: b -> Compare a b :~: 'EQ   eqToRefl :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'EQ -> a :~: b@@ -98,49 +113,49 @@       === sCompare a b `because` sym aLTb       === SEQ          `because` eqlCmpEQ a b aEQb -  leqNeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (a :<= b) -> (a :~: b -> Void) -> Compare a b :~: 'LT+  leqNeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (a <= b) -> (a :~: b -> Void) -> Compare a b :~: 'LT   leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb  -  succLeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (S a :<= b) -> Compare a b :~: 'LT+  succLeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (S a <= b) -> Compare a b :~: 'LT   succLeqToLT a b saLEQb =     case leqWitness (sSucc a) b saLEQb of       DiffNat _ k -> let aLEQb = leqStep a b (sSucc k) $-                                 start (a %:+ sSucc k)-                                   === sSucc (a %:+ k) `because` plusSuccR a k-                                   === sSucc a %:+ k   `because` sym (plusSuccL a k)+                                 start (a %+ sSucc k)+                                   === sSucc (a %+ k) `because` plusSuccR a k+                                   === sSucc a %+ k   `because` sym (plusSuccL a k)                                    =~= b                          aNEQb aeqb = succNonCyclic k $ plusEqCancelL a (sSucc k) sZero $-                                     start (a %:+ sSucc k)-                                      === sSucc (a %:+ k) `because` plusSuccR a k-                                      === (sSucc a) %:+ k `because` sym (plusSuccL a k)+                                     start (a %+ sSucc k)+                                      === sSucc (a %+ k) `because` plusSuccR a k+                                      === sSucc a %+ k `because` sym (plusSuccL a k)                                       =~= b                                       === a               `because` sym aeqb-                                      === a %:+ sZero     `because` sym (plusZeroR a)+                                      === a %+ sZero     `because` sym (plusZeroR a)                      in leqNeqToLT a b aLEQb aNEQb    ltToLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT-          -> IsTrue (a :<= b)+          -> IsTrue (a <= b)    gtToLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'GT-          -> IsTrue (b :<= a)+          -> IsTrue (b <= a)   gtToLeq n m nGTm = ltToLeq m n $     start (sCompare m n) === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m)                          === sFlipOrdering SGT            `because` congFlipOrdering nGTm                          =~= SLT    ltToSuccLeq :: Sing (a :: nat) -> Sing b -> Compare a b :~: 'LT-              -> IsTrue (Succ a :<= b)+              -> IsTrue (Succ a <= b)   ltToSuccLeq n m nLTm =      leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm)    cmpZero :: Sing a -> Compare (Zero nat) (Succ a) :~: 'LT   cmpZero sn = leqToLT sZero (sSucc sn) $ leqStep (sSucc sZero) (sSucc sn) sn $-               start (sSucc sZero %:+ sn)-                 === sSucc (sZero %:+ sn) `because` plusSuccL sZero sn+               start (sSucc sZero %+ sn)+                 === sSucc (sZero %+ sn) `because` plusSuccL sZero sn                  === sSucc sn             `because` succCong (plusZeroL sn) -  leqToGT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ b :<= a)+  leqToGT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ b <= a)               -> Compare a b :~: 'GT   leqToGT a b sbLEQa =     start (sCompare a b)@@ -189,15 +204,15 @@                DiffNat _ k ->                  sym $ succLeqToLT (sSucc n) (sSucc m) $                  leqStep (sSucc (sSucc n)) (sSucc m) k $-                 start (sSucc (sSucc n) %:+ k)-                   === sSucc (sSucc n %:+ k)    `because` plusSuccL (sSucc n) k+                 start (sSucc (sSucc n) %+ k)+                   === sSucc (sSucc n %+ k)    `because` plusSuccL (sSucc n) k                    =~= sSucc m       SGT -> case leqWitness (sSucc m) n $ ltToSuccLeq m n (sym $ flipCompare n m) of                DiffNat _ k ->                  let pf = (succLeqToLT (sSucc m) (sSucc n) $                           leqStep (sSucc (sSucc m)) (sSucc n) k $-                          start (sSucc (sSucc m) %:+ k)-                            === sSucc (sSucc m %:+ k)    `because` plusSuccL (sSucc m) k+                          start (sSucc (sSucc m) %+ k)+                            === sSucc (sSucc m %+ k)    `because` plusSuccL (sSucc m) k                             =~= sSucc n)                  in start (sCompare n m)                       =~= SGT@@ -245,7 +260,7 @@         in start (sCompare n (sSucc m'))              === SLT `because` cmpSuccStepR n m' nLTm -  leqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ a :<= b)+  leqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ a <= b)            -> Compare a b :~: 'LT   leqToLT n m snLEQm =     case leqToCmp (sSucc n) m snLEQm of@@ -255,20 +270,20 @@           === SLT `because` ltSucc n       Right nLTm -> ltSuccLToLT n m nLTm -  leqZero :: Sing n -> IsTrue (Zero nat :<= n)+  leqZero :: Sing n -> IsTrue (Zero nat <= n)   leqZero sn =     case zeroOrSucc sn of-      IsZero   -> leqRefl sn+      IsZero    -> leqRefl sn       IsSucc pn -> ltToLeq sZero sn $ cmpZero pn -  leqSucc :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> IsTrue (Succ n :<= Succ m)+  leqSucc :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (Succ n <= Succ m)   leqSucc n m nLEQm =     case leqToCmp n m nLEQm of       Left  eql  -> withRefl eql $ leqRefl (sSucc n)       Right nLTm -> ltToLeq (sSucc n) (sSucc m) $ sym (cmpSucc n m) `trans` nLTm -  fromLeqView :: LeqView (n :: nat) m -> IsTrue (n :<= m)-  fromLeqView (LeqZero n) = leqZero n+  fromLeqView :: LeqView (n :: nat) m -> IsTrue (n <= m)+  fromLeqView (LeqZero n)         = leqZero n   fromLeqView (LeqSucc n m nLEQm) = leqSucc n m nLEQm    leqViewRefl :: Sing (n :: nat) -> LeqView n n@@ -280,7 +295,7 @@       step n (LeqViewRefl nLEQn) =         LeqViewRefl $ LeqSucc n n (fromLeqView nLEQn) -  viewLeq :: forall n m . Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> LeqView n m+  viewLeq :: forall n m . Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> LeqView n m   viewLeq n m nLEQm =     case (zeroOrSucc n, leqToCmp n m nLEQm) of       (IsZero, _)    -> LeqZero m@@ -291,7 +306,7 @@              n'LTm' = cmpSucc n' m' `trans` compareCongR n (sym sm'EQm) `trans` nLTm          in coerce (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm' -  leqWitness :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> DiffNat n m+  leqWitness :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> DiffNat n m   leqWitness = leqWitPf . induction base step     where       base :: LeqWitPf (Zero nat)@@ -304,7 +319,7 @@           LeqSucc (_ :: Sing n') pm nLEQpm ->             succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: n) pm nLEQpm -  leqStep :: Sing (n :: nat) -> Sing m -> Sing l -> n :+ l :~: m -> IsTrue (n :<= m)+  leqStep :: Sing (n :: nat) -> Sing m -> Sing l -> n + l :~: m -> IsTrue (n <= m)   leqStep = leqStepPf . induction base step     where       base :: LeqStepPf (Zero nat)@@ -314,165 +329,165 @@       step n (LeqStepPf ih) =         LeqStepPf $ \k l snPlEqk ->         let kEQspk = start k-                       === sSucc n %:+ l   `because` sym snPlEqk-                       === sSucc (n %:+ l) `because` plusSuccL n l-            pk = n %:+ l+                       === sSucc n %+ l   `because` sym snPlEqk+                       === sSucc (n %+ l) `because` plusSuccL n l+            pk = n %+ l         in coerceLeqR (sSucc n) (sym kEQspk) $ leqSucc n pk $ ih pk l Refl -  leqNeqToSuccLeq :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> (n :~: m -> Void) -> IsTrue (Succ n :<= m)+  leqNeqToSuccLeq :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> (n :~: m -> Void) -> IsTrue (Succ n <= m)   leqNeqToSuccLeq n m nLEQm nNEQm =     case leqWitness n m nLEQm of       DiffNat _ k ->         case zeroOrSucc k of           IsZero -> absurd $ nNEQm $ sym $ plusZeroR n           IsSucc k' -> leqStep (sSucc n) m k' $-            start (sSucc n %:+ k')-              === sSucc (n %:+ k') `because` plusSuccL n k'-              === n %:+ sSucc k'   `because` sym (plusSuccR n k')+            start (sSucc n %+ k')+              === sSucc (n %+ k') `because` plusSuccL n k'+              === n %+ sSucc k'   `because` sym (plusSuccR n k')               =~= m -  leqRefl :: Sing (n :: nat) -> IsTrue (n :<= n)+  leqRefl :: Sing (n :: nat) -> IsTrue (n <= n)   leqRefl sn = leqStep sn sn sZero (plusZeroR sn) -  leqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> IsTrue (n :<= Succ m)+  leqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (n <= Succ m)   leqSuccStepR n m nLEQm =     case leqWitness n m nLEQm of       DiffNat _ k -> leqStep n (sSucc m) (sSucc k) $-        start (n %:+ sSucc k) === sSucc (n %:+ k) `because` plusSuccR n k =~= sSucc m+        start (n %+ sSucc k) === sSucc (n %+ k) `because` plusSuccR n k =~= sSucc m -  leqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n :<= m) -> IsTrue (n :<= m)+  leqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n <= m) -> IsTrue (n <= m)   leqSuccStepL n m snLEQm =      leqTrans n (sSucc n) m (leqSuccStepR n n $ leqRefl n) snLEQm -  leqReflexive :: Sing (n :: nat) -> Sing m -> n :~: m -> IsTrue (n :<= m)+  leqReflexive :: Sing (n :: nat) -> Sing m -> n :~: m -> IsTrue (n <= m)   leqReflexive n _ Refl = leqRefl n -  leqTrans :: Sing (n :: nat) -> Sing m -> Sing l -> IsTrue (n :<= m) -> IsTrue (m :<= l) -> IsTrue (n :<= l)+  leqTrans :: Sing (n :: nat) -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue (m <= l) -> IsTrue (n <= l)   leqTrans n m k nLEm mLEk =     case leqWitness n m nLEm of       DiffNat _ mMn -> case leqWitness m k mLEk of-        DiffNat _ kMn -> leqStep n k (mMn %:+ kMn) (sym $ plusAssoc n mMn kMn)+        DiffNat _ kMn -> leqStep n k (mMn %+ kMn) (sym $ plusAssoc n mMn kMn) -  leqAntisymm :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> IsTrue (m :<= n) -> n :~: m+  leqAntisymm :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (m <= n) -> n :~: m   leqAntisymm n m nLEm mLEn =     case (leqWitness n m nLEm, leqWitness m n mLEn) of       (DiffNat _ mMn, DiffNat _ nMm) ->-        let pEQ0 = plusEqCancelL n (mMn %:+ nMm) sZero $-                   start (n %:+ (mMn %:+ nMm))-                     === (n %:+ mMn) %:+ nMm+        let pEQ0 = plusEqCancelL n (mMn %+ nMm) sZero $+                   start (n %+ (mMn %+ nMm))+                     === (n %+ mMn) %+ nMm                          `because` sym (plusAssoc n mMn nMm)-                     =~= m %:+ nMm+                     =~= m %+ nMm                      =~= n-                     === n %:+ sZero+                     === n %+ sZero                          `because` sym (plusZeroR n)             nMmEQ0 = plusEqZeroL mMn nMm pEQ0          in sym $ start m-             =~= n %:+ mMn-             === n %:+ sZero  `because` plusCongR n nMmEQ0+             =~= n %+ mMn+             === n %+ sZero  `because` plusCongR n nMmEQ0              === n            `because` plusZeroR n    plusMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k-               -> IsTrue (n :<= m) -> IsTrue (l :<= k)-               -> IsTrue (n :+ l :<= m :+ k)+               -> IsTrue (n <= m) -> IsTrue (l <= k)+               -> IsTrue ((n + l) <= (m + k))   plusMonotone n m l k nLEm lLEk =     case (leqWitness n m nLEm, leqWitness l k lLEk) of       (DiffNat _ mMINn, DiffNat _ kMINl) ->-        let r = mMINn %:+ kMINl-        in leqStep (n %:+ l) (m %:+ k) r $-           start (n %:+ l %:+ r)-             === n %:+ (l %:+ r)+        let r = mMINn %+ kMINl+        in leqStep (n %+ l) (m %+ k) r $+           start (n %+ l %+ r)+             === n %+ (l %+ r)                  `because` plusAssoc n l r-             =~= n %:+ (l %:+ (mMINn %:+ kMINl))-             === n %:+ (l %:+ (kMINl %:+ mMINn))+             =~= n %+ (l %+ (mMINn %+ kMINl))+             === n %+ (l %+ (kMINl %+ mMINn))                  `because` plusCongR n (plusCongR l (plusComm mMINn kMINl))-             === n %:+ ((l %:+ kMINl) %:+ mMINn)+             === n %+ ((l %+ kMINl) %+ mMINn)                  `because` plusCongR n (sym $ plusAssoc l kMINl mMINn)-             =~= n %:+ (k %:+ mMINn)-             === n %:+ (mMINn %:+ k)+             =~= n %+ (k %+ mMINn)+             === n %+ (mMINn %+ k)                  `because` plusCongR n (plusComm k mMINn)-             === n %:+ mMINn %:+ k+             === n %+ mMINn %+ k                  `because` sym (plusAssoc n mMINn k)-             =~= m %:+ k+             =~= m %+ k -  leqZeroElim :: Sing n -> IsTrue (n :<= Zero nat) -> n :~: Zero nat+  leqZeroElim :: Sing n -> IsTrue (n <= Zero nat) -> n :~: Zero nat   leqZeroElim n nLE0 =     case viewLeq n sZero nLE0 of-      LeqZero _ -> Refl+      LeqZero _      -> Refl       LeqSucc _ pZ _ -> absurd $ succNonCyclic pZ Refl -  plusMonotoneL :: Sing (n :: nat) -> Sing m -> Sing (l :: nat) -> IsTrue (n :<= m)-           -> IsTrue (n :+ l :<= m :+ l)+  plusMonotoneL :: Sing (n :: nat) -> Sing m -> Sing (l :: nat) -> IsTrue (n <= m)+           -> IsTrue ((n + l) <= (m + l))   plusMonotoneL n m l leq = plusMonotone n m l l leq (leqRefl l) -  plusMonotoneR :: Sing n -> Sing m -> Sing (l :: nat) -> IsTrue (m :<= l)-           -> IsTrue (n :+ m :<= n :+ l)+  plusMonotoneR :: Sing n -> Sing m -> Sing (l :: nat) -> IsTrue (m <= l)+           -> IsTrue ((n + m) <= (n + l))   plusMonotoneR n m l leq = plusMonotone n n m l (leqRefl n) leq -  plusLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= n :+ m)-  plusLeqL n m = leqStep n (n %:+ m) m Refl+  plusLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n <= (n + m))+  plusLeqL n m = leqStep n (n %+ m) m Refl -  plusLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n :+ m)-  plusLeqR n m = leqStep m (n %:+ m) n $ plusComm m n+  plusLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m <= (n + m))+  plusLeqR n m = leqStep m (n %+ m) n $ plusComm m n    plusCancelLeqR :: Sing (n :: nat) -> Sing m -> Sing l-                 -> IsTrue (n :+ l :<= m :+ l)-                 -> IsTrue (n :<= m)+                 -> IsTrue ((n + l) <= (m + l))+                 -> IsTrue (n <= m)   plusCancelLeqR n m l nlLEQml =-    case leqWitness (n %:+ l) (m %:+ l) nlLEQml of+    case leqWitness (n %+ l) (m %+ l) nlLEQml of       DiffNat _ k ->-        let pf = plusEqCancelR (n %:+ k) m l $-                 start ((n %:+ k) %:+ l)-                   === n %:+ (k %:+ l) `because` plusAssoc n k l-                   === n %:+ (l %:+ k) `because` plusCongR n (plusComm k l)-                   === n %:+ l %:+ k   `because` sym (plusAssoc n l k)-                   =~= m %:+ l+        let pf = plusEqCancelR (n %+ k) m l $+                 start ((n %+ k) %+ l)+                   === n %+ (k %+ l) `because` plusAssoc n k l+                   === n %+ (l %+ k) `because` plusCongR n (plusComm k l)+                   === n %+ l %+ k   `because` sym (plusAssoc n l k)+                   =~= m %+ l         in leqStep n m k pf    plusCancelLeqL :: Sing (n :: nat) -> Sing m -> Sing l-                 -> IsTrue (n :+ m :<= n :+ l)-                 -> IsTrue (m :<= l)+                 -> IsTrue ((n + m) <= (n + l))+                 -> IsTrue (m <= l)   plusCancelLeqL n m l nmLEQnl =     plusCancelLeqR m l n $-    coerceLeqL (plusComm n m) (l %:+ n) $-    coerceLeqR (n %:+ m) (plusComm n l) nmLEQnl+    coerceLeqL (plusComm n m) (l %+ n) $+    coerceLeqR (n %+ m) (plusComm n l) nmLEQnl -  succLeqZeroAbsurd :: Sing n -> IsTrue (S n :<= Zero nat) -> Void+  succLeqZeroAbsurd :: Sing n -> IsTrue (S n <= Zero nat) -> Void   succLeqZeroAbsurd n leq =     succNonCyclic n (leqZeroElim (sSucc n) leq) -  succLeqZeroAbsurd' :: Sing n -> (S n :<= Zero nat) :~: 'False+  succLeqZeroAbsurd' :: Sing n -> (S n <= Zero nat) :~: 'False   succLeqZeroAbsurd' n =-    case sSucc n %:<= sZero of+    case sSucc n %<= sZero of       STrue  -> absurd $ succLeqZeroAbsurd n Witness       SFalse -> Refl -  succLeqAbsurd :: Sing (n :: nat) -> IsTrue (S n :<= n) -> Void+  succLeqAbsurd :: Sing (n :: nat) -> IsTrue (S n <= n) -> Void   succLeqAbsurd n snLEQn =     eliminate $       start SLT         === sCompare n n `because` sym (succLeqToLT n n snLEQn)         === SEQ          `because` eqlCmpEQ n n Refl -  succLeqAbsurd' :: Sing (n :: nat) -> (S n :<= n) :~: 'False+  succLeqAbsurd' :: Sing (n :: nat) -> (S n <= n) :~: 'False   succLeqAbsurd' n =-    case sSucc n %:<= n of-      STrue -> absurd $ succLeqAbsurd n Witness+    case sSucc n %<= n of+      STrue  -> absurd $ succLeqAbsurd n Witness       SFalse -> Refl -  notLeqToLeq :: ((n :<= m) ~ 'False) => Sing (n :: nat) -> Sing m -> IsTrue (m :<= n)+  notLeqToLeq :: ((n <= m) ~ 'False) => Sing (n :: nat) -> Sing m -> IsTrue (m <= n)   notLeqToLeq n m =     case sCompare n m of       SLT -> eliminate $ ltToLeq n m Refl       SEQ -> eliminate $ leqReflexive n m $ eqToRefl n m Refl       SGT -> gtToLeq n m Refl -  leqSucc' :: Sing (n :: nat) -> Sing m -> (n :<= m) :~: (Succ n :<= Succ m)+  leqSucc' :: Sing (n :: nat) -> Sing m -> (n <= m) :~: (Succ n <= Succ m)   leqSucc' n m =-    case n %:<= m of+    case n %<= m of       STrue -> withWitness (leqSucc n m Witness) Refl       SFalse ->-        case sSucc n %:<= sSucc m of+        case sSucc n %<= sSucc m of           SFalse -> Refl           STrue  ->             case viewLeq (sSucc n) (sSucc m) Witness of@@ -480,48 +495,48 @@               LeqSucc n' m' Witness ->                 eliminate $                 start STrue-                  =~= (n' %:<= m')-                  === (n  %:<= m)   `because` sLeqCong (succInj' n' n Refl) (succInj' m' m Refl)+                  =~= (n' %<= m')+                  === (n  %<= m)   `because` sLeqCong (succInj' n' n Refl) (succInj' m' m Refl)                   =~= SFalse -  leqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> Min n m :~: n+  leqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> Min n m :~: n   leqToMin n m nLEQm =      leqAntisymm (sMin n m) n (minLeqL n m)                  (minLargest n n m (leqRefl n) nLEQm) -  geqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> Min n m :~: m+  geqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Min n m :~: m   geqToMin n m mLEQn =      leqAntisymm (sMin n m) m (minLeqR n m)                  (minLargest m n m mLEQn (leqRefl m))    minComm :: Sing (n :: nat) -> Sing m -> Min n m :~: Min m n   minComm n m =-    case n %:<= m of+    case n %<= m of       STrue -> start (sMin n m) === n        `because` leqToMin n m Witness                                 === sMin m n `because` sym (geqToMin m n Witness)       SFalse -> start (sMin n m) === m        `because` geqToMin n m (notLeqToLeq n m)                                  === sMin m n `because` sym (leqToMin m n $ notLeqToLeq n m) -  minLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m :<= n)+  minLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m <= n)   minLeqL n m =-    case n %:<= m of+    case n %<= m of       STrue  -> leqReflexive (sMin n m) n $ leqToMin n m Witness       SFalse -> let mLEQn = notLeqToLeq n m                 in leqTrans (sMin n m) m n                      (leqReflexive (sMin n m) m (geqToMin n m mLEQn)) $                      mLEQn -  minLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m :<= m)+  minLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m <= m)   minLeqR n m = leqTrans (sMin n m) (sMin m n) m                   (leqReflexive (sMin n m) (sMin m n) $ minComm n m)                   (minLeqL m n)    minLargest :: Sing (l :: nat) ->  Sing n -> Sing m-             -> IsTrue (l :<= n) -> IsTrue (l :<= m)-             -> IsTrue (l :<= Min n m)+             -> IsTrue (l <= n) -> IsTrue (l <= m)+             -> IsTrue (l <= Min n m)   minLargest l n m lLEQn lLEQm =     withSingI l $ withSingI n $ withSingI m $ withSingI (sMin n m) $-    case n %:<= m of+    case n %<= m of       STrue -> leqTrans l n (sMin n m) lLEQn $                leqReflexive sing sing  $ sym $ leqToMin n m Witness       SFalse ->@@ -529,41 +544,41 @@         in leqTrans l m (sMin n m) lLEQm $            leqReflexive sing sing  $ sym $ geqToMin n m mLEQn -  leqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> Max n m :~: m+  leqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> Max n m :~: m   leqToMax n m nLEQm =      leqAntisymm (sMax n m) m (maxLeast m n m nLEQm (leqRefl m)) (maxLeqR n m) -  geqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> Max n m :~: n+  geqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Max n m :~: n   geqToMax n m mLEQn =      leqAntisymm (sMax n m) n (maxLeast n n m (leqRefl n) mLEQn) (maxLeqL n m)    maxComm :: Sing (n :: nat) -> Sing m -> Max n m :~: Max m n   maxComm n m =-    case n %:<= m of+    case n %<= m of       STrue -> start (sMax n m) === m        `because` leqToMax n m Witness                                 === sMax m n `because` sym (geqToMax m n Witness)       SFalse -> start (sMax n m) === n        `because` geqToMax n m (notLeqToLeq n m)                                  === sMax m n `because` sym (leqToMax m n $ notLeqToLeq n m) -  maxLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= Max n m)+  maxLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m <= Max n m)   maxLeqR n m =-    case n %:<= m of+    case n %<= m of       STrue  -> leqReflexive m (sMax n m) $ sym $ leqToMax n m Witness       SFalse -> let mLEQn = notLeqToLeq n m                 in leqTrans m n (sMax n m) mLEQn                      (leqReflexive n (sMax n m) (sym $ geqToMax n m mLEQn)) -  maxLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= Max n m)+  maxLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n <= Max n m)   maxLeqL n m = leqTrans n (sMax m n) (sMax n m)                   (maxLeqR m n)                   (leqReflexive (sMax m n) (sMax n m) $ maxComm m n)    maxLeast :: Sing (l :: nat) ->  Sing n -> Sing m-             -> IsTrue (n :<= l) -> IsTrue (m :<= l)-             -> IsTrue (Max n m :<= l)+             -> IsTrue (n <= l) -> IsTrue (m <= l)+             -> IsTrue (Max n m <= l)   maxLeast l n m lLEQn lLEQm =     withSingI l $ withSingI n $ withSingI m $ withSingI (sMax n m) $-    case n %:<= m of+    case n %<= m of       STrue -> leqTrans (sMax n m) m l                (leqReflexive sing sing  $ leqToMax n m Witness)                lLEQm@@ -573,56 +588,56 @@            (leqReflexive sing sing  $ geqToMax n m mLEQn)            lLEQn -  leqReversed  :: Sing (n :: nat) -> Sing m -> (n :<= m) :~: (m :>= n)-  lneqSuccLeq  :: Sing (n :: nat) -> Sing m -> (n :< m)  :~: (Succ n :<= m)-  lneqReversed :: Sing (n :: nat) -> Sing m -> (n :< m)  :~: (m :> n)+  leqReversed  :: Sing (n :: nat) -> Sing m -> (n <= m) :~: (m >= n)+  lneqSuccLeq  :: Sing (n :: nat) -> Sing m -> (n < m)  :~: (Succ n <= m)+  lneqReversed :: Sing (n :: nat) -> Sing m -> (n < m)  :~: (m > n) -  lneqToLT :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n :< m)+  lneqToLT :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n < m)            -> Compare n m :~: 'LT   lneqToLT n m nLNEm =     succLeqToLT n m $ coerce (lneqSuccLeq n m) nLNEm    ltToLneq :: Sing (n :: nat) -> Sing (m :: nat) -> Compare n m :~: 'LT-           -> IsTrue (n :< m)+           -> IsTrue (n < m)   ltToLneq n m nLTm =     coerce (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm -  lneqZero :: Sing (a :: nat) -> IsTrue (Zero nat :< Succ a)+  lneqZero :: Sing (a :: nat) -> IsTrue (Zero nat < Succ a)   lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n -  lneqSucc :: Sing (n :: nat) -> IsTrue (n :< Succ n)+  lneqSucc :: Sing (n :: nat) -> IsTrue (n < Succ n)   lneqSucc n = ltToLneq n (sSucc n) $ ltSucc n    succLneqSucc :: Sing (n :: nat) -> Sing (m :: nat)-               -> (n :< m) :~: (Succ n :< Succ m)+               -> (n < m) :~: (Succ n < Succ m)   succLneqSucc n m =-    start (n %:< m)-      === (sSucc n %:<= m)               `because` lneqSuccLeq n m-      === (sSucc (sSucc n) %:<= sSucc m) `because` leqSucc' (sSucc n) m-      === (sSucc n %:< sSucc m)          `because` sym (lneqSuccLeq (sSucc n) (sSucc m))+    start (n %< m)+      === (sSucc n %<= m)               `because` lneqSuccLeq n m+      === (sSucc (sSucc n) %<= sSucc m) `because` leqSucc' (sSucc n) m+      === (sSucc n %< sSucc m)          `because` sym (lneqSuccLeq (sSucc n) (sSucc m)) -  lneqRightPredSucc :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n :< m)+  lneqRightPredSucc :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n < m)                     -> m :~: Succ (Pred m)   lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm -  lneqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n :< m) -> IsTrue (n :< m)+  lneqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n < m) -> IsTrue (n < m)   lneqSuccStepL n m snLNEQm =     coerce (sym $ lneqSuccLeq n m) $     leqSuccStepL (sSucc n) m $     coerce (lneqSuccLeq (sSucc n) m) snLNEQm -  lneqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n :< m) -> IsTrue (n :< Succ m)+  lneqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n < m) -> IsTrue (n < Succ m)   lneqSuccStepR n m nLNEQm =     coerce (sym $ lneqSuccLeq n (sSucc m)) $     leqSuccStepR (sSucc n) m $     coerce (lneqSuccLeq n m) nLNEQm    plusStrictMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k-                     -> IsTrue (n :< m) -> IsTrue (l :< k)-                     -> IsTrue (n :+ l :< m :+ k)+                     -> IsTrue (n < m) -> IsTrue (l < k)+                     -> IsTrue ((n + l) < (m + k))   plusStrictMonotone n m l k nLNm lLNk =-    coerce (sym $ lneqSuccLeq (n %:+ l) (m %:+ k)) $-      flip coerceLeqL (m %:+ k) (plusSuccL n l) $+    coerce (sym $ lneqSuccLeq (n %+ l) (m %+ k)) $+      flip coerceLeqL (m %+ k) (plusSuccL n l) $       plusMonotone (sSucc n) m l k         (coerce (lneqSuccLeq n m) nLNm)         (leqTrans l (sSucc l) k (leqSuccStepR l l (leqRefl l)) $@@ -640,67 +655,67 @@   minZeroR  :: Sing n -> Min n (Zero nat) :~: Zero nat   minZeroR n = geqToMin n sZero (leqZero n) -  minusSucc :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> Succ n :- m :~: Succ (n :- m)+  minusSucc :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Succ n - m :~: Succ (n - m)   minusSucc n m mLEQn =     case leqWitness m n mLEQn of       DiffNat _ k ->-        start (sSucc n %:- m)-          =~= sSucc (m %:+ k) %:- m-          === (m %:+ sSucc k) %:- m  `because` minusCongL (sym $ plusSuccR m k) m-          === (sSucc k %:+ m) %:- m  `because` minusCongL (plusComm m (sSucc k)) m+        start (sSucc n %- m)+          =~= sSucc (m %+ k) %- m+          === (m %+ sSucc k) %- m  `because` minusCongL (sym $ plusSuccR m k) m+          === (sSucc k %+ m) %- m  `because` minusCongL (plusComm m (sSucc k)) m           === sSucc k                `because` plusMinus (sSucc k) m-          === sSucc (k %:+ m %:- m)  `because` succCong (sym $ plusMinus k m)-          === sSucc (m %:+ k %:- m)  `because` succCong (minusCongL (plusComm k m) m)-          =~= sSucc (n %:- m)+          === sSucc (k %+ m %- m)  `because` succCong (sym $ plusMinus k m)+          === sSucc (m %+ k %- m)  `because` succCong (minusCongL (plusComm k m) m)+          =~= sSucc (n %- m) -  lneqZeroAbsurd :: Sing n -> IsTrue (n :< Zero nat) -> Void+  lneqZeroAbsurd :: Sing n -> IsTrue (n < Zero nat) -> Void   lneqZeroAbsurd n leq =     succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq) -  minusPlus :: forall (n :: nat) m .PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m :<= n)-            -> n :- m :+ m :~: n+  minusPlus :: forall (n :: nat) m .PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m <= n)+            -> n - m + m :~: n   minusPlus n m mLEQn =     case leqWitness m n mLEQn of       DiffNat _ k ->-        start (n %:- m %:+ m)-          =~= m %:+ k %:- m %:+ m-          === k %:+ m %:- m %:+ m  `because` plusCongL (minusCongL (plusComm m k) m) m-          === k %:+ m              `because` plusCongL (plusMinus k m) m-          === m %:+ k              `because` plusComm  k m+        start (n %- m %+ m)+          =~= m %+ k %- m %+ m+          === k %+ m %- m %+ m  `because` plusCongL (minusCongL (plusComm m k) m) m+          === k %+ m              `because` plusCongL (plusMinus k m) m+          === m %+ k              `because` plusComm  k m           =~= n  -- | Natural subtraction, truncated to zero if m > n.-type n :-. m = Subt n m (m :<= n)+type n -. m = Subt n m (m <= n) type family Subt (n :: nat) (m :: nat) (b :: Bool) :: nat where-  Subt n          m 'True  = n :- m+  Subt n          m 'True  = n - m   Subt (n :: nat) m 'False = Zero nat-infixl 6 :-.+infixl 6 -. -(%:-.) :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing (n :-. m)-n %:-. m =-  case m %:<= n of-    STrue -> n %:- m+(%-.) :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing (n -. m)+n %-. m =+  case m %<= n of+    STrue  -> n %- m     SFalse -> sZero  minPlusTruncMinus :: (PeanoOrder nat) => Sing (n :: nat) -> Sing (m :: nat)-                  -> Min n m :+ (n :-. m) :~: n+                  -> Min n m + (n -. m) :~: n minPlusTruncMinus n m =-  case m %:<= n of+  case m %<= n of     STrue ->-      start (sMin n m %:+ (n %:-. m))-        === m %:+ (n %:-. m) `because` plusCongL (geqToMin n m Witness) (n %:-. m)-        =~= m %:+ (n %:- m)-        === (n %:- m) %:+ m  `because` plusComm m (n %:- m)+      start (sMin n m %+ (n %-. m))+        === m %+ (n %-. m) `because` plusCongL (geqToMin n m Witness) (n %-. m)+        =~= m %+ (n %- m)+        === (n %- m) %+ m  `because` plusComm m (n %- m)         === n                `because` minusPlus n m Witness     SFalse ->-      start (sMin n m %:+ (n %:-. m))-        =~= sMin n m %:+ sZero+      start (sMin n m %+ (n %-. m))+        =~= sMin n m %+ sZero         === sMin n m  `because` plusZeroR (sMin n m)         === n         `because` leqToMin n m (notLeqToLeq m n) -truncMinusLeq :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (n :-. m :<= n)+truncMinusLeq :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue ((n -. m) <= n) truncMinusLeq n m =-  case m %:<= n of-    STrue  -> leqStep (n %:-. m) n m $ minusPlus n m Witness+  case m %<= n of+    STrue  -> leqStep (n %-. m) n m $ minusPlus n m Witness     SFalse -> leqZero n 

@@ -1,8 +0,0 @@-{-# LANGUAGE CPP #-}-module Data.Type.Natural.Compat (bugInGHC) where-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-import Data.Singletons.Prelude (bugInGHC)-#else-bugInGHC :: a-bugInGHC = error "GHC case-analysis error!"-#endif

@@ -1,19 +1,15 @@ {-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-} {-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude   #-} {-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables                 #-}-{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies          #-}-{-# LANGUAGE TypeOperators, UndecidableInstances                        #-}+{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators            #-}+{-# LANGUAGE UndecidableInstances                                       #-} module Data.Type.Natural.Core where-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-import Data.Type.Natural.Compat-#endif+import Data.Type.Natural.Definitions -import Data.Constraint               hiding ((:-))-import Data.Promotion.Prelude.Ord    ((:<=))-import Data.Type.Natural.Definitions hiding ((:<=))-import Prelude                       (Bool (..), Eq (..), Show (..), ($))-import Proof.Propositional           (IsTrue)-import Unsafe.Coerce+import Data.Constraint     (Dict (..))+import Prelude             (Bool (..), Eq (..), Show (..), ($))+import Proof.Propositional (IsTrue)+import Unsafe.Coerce       (unsafeCoerce)  -------------------------------------------------- -- ** Type-level predicate & judgements.@@ -23,17 +19,11 @@   ZeroLeq     :: SNat m -> Leq Zero m   SuccLeqSucc :: Leq n m -> Leq ('S n) ('S m) -type LeqTrueInstance a b = IsTrue (a :<= b)--(%-) :: (m :<= n) ~ 'True => SNat n -> SNat m -> SNat (n :-: m)-n   %- SZ    = n-SS n %- SS m = n %- m-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-_    %- _    = bugInGHC-#endif+type LeqTrueInstance a b = IsTrue (a <= b) -infixl 6 %-+#if !MIN_VERSION_singletons(2,4,0) deriving instance Show (SNat n)+#endif deriving instance Eq (SNat n)  data (a :: Nat) :<: (b :: Nat) where@@ -49,7 +39,7 @@ propToBoolLeq _ = unsafeCoerce (Dict :: Dict ()) {-# INLINE propToBoolLeq #-} -boolToClassLeq :: (n :<= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m+boolToClassLeq :: (n <= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m boolToClassLeq _ = unsafeCoerce (Dict :: Dict ()) {-# INLINE boolToClassLeq #-} @@ -63,7 +53,7 @@ propToBoolLeq (ZeroLeq _) = Dict propToBoolLeq (SuccLeqSucc leq) = case propToBoolLeq leq of Dict -> Dict -boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m+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@@ -73,19 +63,17 @@ propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict -} -type LeqInstance n m = IsTrue (n :<= m)+type LeqInstance n m = IsTrue (n <= m) -boolToPropLeq :: (n :<= m) ~ 'True => SNat n -> SNat m -> Leq 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-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800-boolToPropLeq _      _     = bugInGHC-#endif  leqRhs :: Leq n m -> SNat m-leqRhs (ZeroLeq m) = m+leqRhs (ZeroLeq m)       = m leqRhs (SuccLeqSucc leq) = SS $ leqRhs leq  leqLhs :: Leq n m -> SNat n-leqLhs (ZeroLeq _) = SZ+leqLhs (ZeroLeq _)       = SZ leqLhs (SuccLeqSucc leq) = SS $ leqLhs leq+

@@ -1,17 +1,20 @@-{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, FlexibleContexts     #-}-{-# LANGUAGE FlexibleInstances, GADTs, InstanceSigs, KindSignatures   #-}-{-# LANGUAGE MultiParamTypeClasses, PolyKinds, RankNTypes             #-}-{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-}-{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances        #-}+{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, EmptyCase                 #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, InstanceSigs      #-}+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes  #-}+{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell      #-}+{-# LANGUAGE TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-} module Data.Type.Natural.Definitions        (module Data.Type.Natural.Definitions,-        module Data.Singletons.Prelude+        module Data.Singletons.Prelude,+        module Data.Type.Natural.Singleton.Compat        ) where+import Data.Type.Natural.Singleton.Compat+ import Data.Promotion.Prelude.Enum import Data.Singletons.Prelude import Data.Singletons.Prelude.Enum-import Data.Singletons.TH           (singletons)-import Data.Typeable                (Typeable)+import Data.Singletons.TH+import Data.Typeable  -------------------------------------------------- -- * Natural numbers and its singleton type@@ -48,6 +51,7 @@      max (S n) Z     = S n      max (S n) (S m) = S (max n m)  |]+ singletons [d|   instance Num Nat where     Z   + n = n@@ -62,7 +66,7 @@      abs n = n -    signum Z = Z+    signum Z     = Z     signum (S _) = S Z      fromInteger n = if n == 0 then Z else S (fromInteger (n-1))@@ -70,46 +74,25 @@  singletons [d|   instance Enum Nat where-    succ n = S n-    pred Z = Z+    succ = S+    pred Z     = Z     pred (S n) = n     toEnum n = if n == 0 then Z else S (toEnum (n - 1))-    fromEnum Z = 0+    fromEnum Z     = 0     fromEnum (S n) = 1 + fromEnum n  |] -type n :-: m = n :- m-type n :+: m = n :+ m--infixl 6 :-:, :+:- singletons [d|  (**) :: Nat -> Nat -> Nat  _ ** Z = S Z  n ** S m = (n ** m) * n  |]----- | Addition for singleton numbers.-(%+) :: SNat n -> SNat m -> SNat (n :+: m)-(%+) = (%:+)-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+#if !MIN_VERSION_singletons(2,4,0)+type (**) a b = a :** b --- | Exponentiation for singleton numbers.-(%**) :: SNat n -> SNat m -> SNat (n :**: m)+(%**) :: SNat n -> SNat m -> SNat (n ** m) (%**) = (%:**)+#endif  singletons [d|  zero, one, two, three, four, five, six, seven, eight, nine, ten :: Nat

@@ -0,0 +1,35 @@+{-# LANGUAGE CPP, ExplicitNamespaces, TemplateHaskell, TypeInType #-}+-- | Compatibility layer for singletons+module Data.Type.Natural.Singleton.Compat+       (+       module Data.Singletons.Prelude.Eq,+       module Data.Singletons.Prelude.Num,+       module Data.Singletons.Prelude.Ord,+#if !MIN_VERSION_singletons(2,4,0)+       module Data.Type.Natural.Singleton.Compat+#endif+       )+       where++#if !MIN_VERSION_singletons(2,4,0)+import Data.Type.Natural.Singleton.Compat.TH+#endif++import Data.Singletons.Prelude.Eq+import Data.Singletons.Prelude.Num+import Data.Singletons.Prelude.Ord++#if !MIN_VERSION_singletons(2,4,0)+generateCompat Nothing ''SOrd "<"+generateCompat Nothing ''SOrd ">"+generateCompat Nothing ''SOrd "<="+generateCompat Nothing ''SOrd ">="++generateCompat Nothing ''SEq "/="+generateCompat Nothing ''SEq "=="++generateCompat Nothing ''SNum "+"+generateCompat Nothing ''SNum "-"+generateCompat Nothing ''SNum "*"+#endif+

@@ -0,0 +1,39 @@+{-# LANGUAGE TemplateHaskell #-}+module Data.Type.Natural.Singleton.Compat.TH where+import Control.Applicative ((<|>))+import Control.Monad       (forM, zipWithM)+import Data.Maybe          (fromMaybe)+import Data.Singletons+import Language.Haskell.TH++generateCompat :: Maybe Fixity -> Name -> String -> DecsQ+generateCompat mfix cls opname = do+  mfix' <- reifyFixity (mkName opname)+  Just oldOpName <- lookupTypeName  $ ":" ++ opname+  Just oldSingName <- lookupValueName $ "%:" ++ opname+  Just oldCur1Name <- lookupTypeName  $ ":" ++ opname ++ "$"+  Just oldCur2Name <- lookupTypeName  $ ":" ++ opname ++ "$$"+  Just oldCur3Name <- lookupTypeName  $ ":" ++ opname ++ "$$$"+  let newOpName = mkName opname+      newSingName = mkName $ "%" ++ opname+      newCur1Name = mkName $ opname ++ "@#@$"+      newCur2Name = mkName $ opname ++ "@#@$$"+      newCur3Name = mkName $ opname ++ "@#@$$$"+  cur12 <- zipWithM (\old new -> tySynD new [] (conT old))+           [oldCur1Name, oldCur2Name]+           [newCur1Name, newCur2Name]+  [a, b] <- mapM newName ["a", "b"]+  cur3 <- tySynD newCur3Name (map PlainTV [a,b])+          $ infixT (varT a) oldCur3Name (varT b)+  nat <- newName "nat"+  tysyn <- tySynD newOpName [PlainTV a, PlainTV b] $+           infixT (varT a) oldOpName (varT b)+  sig <- sigD newSingName $+         forallT [PlainTV nat, KindedTV a (VarT nat), KindedTV b (VarT nat)]+         (sequence [[t| $(conT cls) $(varT nat) |]])+         [t| Sing $(varT a) -> Sing $(varT b) -> Sing $(infixT (varT a) newOpName (varT b)) |]+  defn <- funD newSingName [clause [] (normalB $ varE oldSingName) [] ]+  fixes <- fmap (fromMaybe []) $ forM (mfix <|> mfix') $ \fixity ->+    return [InfixD fixity newOpName, InfixD  fixity newSingName]+  return (sig : defn : tysyn : cur12 ++ [cur3] ++ fixes)+

@@ -12,30 +12,36 @@          -- $quasiquotes          mkOrdinalQQ, odPN, odLit,          -- * Conversion from cardinals to ordinals.-         sNatToOrd', sNatToOrd, ordToInt, ordToSing,-         unsafeFromInt, inclusion, inclusion',+         sNatToOrd', sNatToOrd,+         ordToNatural, unsafeNaturalToOrd', unsafeNaturalToOrd,+         reallyUnsafeNaturalToOrd,+         naturalToOrd, naturalToOrd',+         ordToSing,  inclusion, inclusion',          -- * Ordinal arithmetics          (@+), enumOrdinal,          -- * Elimination rules for @'Ordinal' 'Z'@.-         absurdOrd, vacuousOrd+         absurdOrd, vacuousOrd,+         -- * Deprecated combinators+         ordToInt, unsafeFromInt, unsafeFromInt'        ) where-import           Data.Kind+import Data.Type.Natural.Singleton.Compat+ import           Data.List                    (genericDrop, genericTake)+import           Data.Maybe                   (fromMaybe) import           Data.Ord                     (comparing) import           Data.Singletons.Decide import           Data.Singletons.Prelude import           Data.Singletons.Prelude.Enum import           Data.Type.Equality-import           Data.Type.Monomorphic import qualified Data.Type.Natural            as PN import           Data.Type.Natural.Builtin    () import           Data.Type.Natural.Class import           Data.Typeable                (Typeable) import           Data.Void                    (absurd)-import           GHC.TypeLits                 (type (+)) import qualified GHC.TypeLits                 as TL import           Language.Haskell.TH          hiding (Type) import           Language.Haskell.TH.Quote+import           Numeric.Natural import           Proof.Equational import           Proof.Propositional import           Unsafe.Coerce@@ -48,9 +54,9 @@ -- --   Since 0.6.0.0 data Ordinal (n :: nat) where-  OLt :: (IsPeano nat, (n :< m) ~ 'True) => Sing (n :: nat) -> Ordinal m+  OLt :: (IsPeano nat, (n < m) ~ 'True) => Sing (n :: nat) -> Ordinal m -fromOLt :: forall nat n m. (PeanoOrder nat, (Succ n :< Succ m) ~ 'True, SingI m)+fromOLt :: forall nat n m. (PeanoOrder nat, (Succ n < Succ m) ~ 'True, SingI m)         => Sing (n :: nat) -> Ordinal m fromOLt  n =   withRefl (sym $ succLneqSucc n (sing :: Sing m)) $@@ -60,7 +66,7 @@ -- --   Since 0.6.0.0 pattern OZ :: forall nat (n :: nat). IsPeano nat-           => (Zero nat :< n) ~ 'True => Ordinal n+           => (Zero nat < n) ~ 'True => Ordinal n pattern OZ <- OLt Zero where   OZ = OLt sZero @@ -79,17 +85,11 @@ -- |  Class synonym for Peano numerals with ordinals. -- --  Since 0.5.0.0-class (PeanoOrder nat, Monomorphicable (Sing :: nat -> *),-       Integral (MonomorphicRep (Sing :: nat -> *)),-       Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat-instance (PeanoOrder nat, Monomorphicable (Sing :: nat -> *),-       Integral (MonomorphicRep (Sing :: nat -> *)),-       Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat+class (PeanoOrder nat, SingKind nat) => HasOrdinal nat+instance (PeanoOrder nat, SingKind nat) => HasOrdinal nat  instance (HasOrdinal nat, SingI (n :: nat))       => Num (Ordinal n) where-  {-# SPECIALISE instance SingI n => Num (Ordinal (n :: PN.Nat))  #-}-  {-# SPECIALISE instance SingI n => Num (Ordinal (n :: TL.Nat))  #-}   _ + _ = error "Finite ordinal is not closed under addition."   _ - _ = error "Ordinal subtraction is not defined"   negate OZ = OZ@@ -104,14 +104,10 @@ -- deriving instance Read (Ordinal n) => Read (Ordinal (Succ n)) instance (SingI n, HasOrdinal nat)         => Show (Ordinal (n :: nat)) where-  {-# SPECIALISE instance SingI n => Show (Ordinal (n :: PN.Nat))  #-}-  {-# SPECIALISE instance SingI n => Show (Ordinal (n :: TL.Nat))  #-}-  showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToInt o) . showString " / " . showsPrec d (demote $ Monomorphic (sing :: Sing n)))+  showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToInt o) . showString " / " . showsPrec d (toNatural (sing :: Sing n)))  instance (HasOrdinal nat)          => Eq (Ordinal (n :: nat)) where-  {-# SPECIALISE instance Eq (Ordinal (n :: PN.Nat))  #-}-  {-# SPECIALISE instance Eq (Ordinal (n :: TL.Nat))  #-}   o == o' = ordToInt o == ordToInt o'  instance (HasOrdinal nat) => Ord (Ordinal (n :: nat)) where@@ -167,35 +163,74 @@     sNatToOrd (sing :: Sing m)   {-# INLINE maxBound #-} +{-# DEPRECATED unsafeFromInt "Use unsafeNaturalToOrd instead" #-}+-- | Since 0.8.0.0 unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat))-              => MonomorphicRep (Sing :: nat -> *) -> Ordinal n-unsafeFromInt n =-    case promote (n :: MonomorphicRep (Sing :: nat -> *)) of-      Monomorphic sn ->-           case sn %:< (sing :: Sing n) of-             STrue -> sNatToOrd' (sing :: Sing n) sn-             SFalse -> error "Bound over!"+              => Int -> Ordinal n+unsafeFromInt = unsafeNaturalToOrd . fromIntegral +-- | Converts @'Natural'@s into @'Ordinal n'@.+--   If the given natural is greater or equal to @n@, raises exception.+--+--   Since 0.8.0.0+unsafeNaturalToOrd :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat))+                  => Natural -> Ordinal n+unsafeNaturalToOrd k =+    fromMaybe (error "unsafeNaturalToOrd Out of bound") $+    naturalToOrd k++{-# DEPRECATED unsafeFromInt' "Use unsafeNaturalToOrd' instead" #-}+-- | Since 0.8.0.0 unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n)-              => proxy nat -> MonomorphicRep (Sing :: nat -> *) -> Ordinal n-unsafeFromInt' _ n =-    case promote (n :: MonomorphicRep (Sing :: nat -> *)) of-      Monomorphic sn ->-           case sn %:< (sing :: Sing n) of-             STrue -> sNatToOrd' (sing :: Sing n) sn+              => proxy nat -> Int -> Ordinal n+unsafeFromInt' p = unsafeNaturalToOrd' p . fromIntegral++-- | Since 0.8.0.0+unsafeNaturalToOrd' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n)+                   => proxy nat -> Natural -> Ordinal n+unsafeNaturalToOrd' _ n =+    case fromNatural n of+      SomeSing sn ->+           case sn %< (sing :: Sing n) of+             STrue  -> sNatToOrd' (sing :: Sing n) sn              SFalse -> error "Bound over!" +{-# WARNING reallyUnsafeNaturalToOrd "This function may violate type safety. Use with care!" #-}+-- | Converts @'Natural'@s into @'Ordinal' n@, WITHOUT any boundary check.+--   This function may easily violate type-safety. Use with care!+reallyUnsafeNaturalToOrd :: forall pxy nat (n :: nat). (HasOrdinal nat, SingI n)+                         => pxy nat -> Natural -> Ordinal n+reallyUnsafeNaturalToOrd _ k =+  case fromNatural k of+    SomeSing (sk :: Sing (k :: nat)) ->+      withRefl (unsafeCoerce (Refl :: () :~: ()) :: (k < n) :~: 'True) $+      OLt sk+ -- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@. -- --   Since 0.5.0.0-sNatToOrd' :: (PeanoOrder nat, (m :< n) ~ 'True) => Sing (n :: nat) -> Sing m -> Ordinal n-sNatToOrd' _ m = OLt m+sNatToOrd' :: (PeanoOrder nat, (m < n) ~ 'True) => Sing (n :: nat) -> Sing m -> Ordinal n+sNatToOrd' _ = OLt {-# INLINE sNatToOrd' #-}  -- | 'sNatToOrd'' with @n@ inferred.-sNatToOrd :: (PeanoOrder nat, SingI (n :: nat), (m :< n) ~ 'True) => Sing m -> Ordinal n+sNatToOrd :: (PeanoOrder nat, SingI (n :: nat), (m < n) ~ 'True) => Sing m -> Ordinal n sNatToOrd = sNatToOrd' sing +-- | Since 0.8.0.0+naturalToOrd :: forall nat n. (HasOrdinal nat, SingI n)+             => Natural -> Maybe (Ordinal (n :: nat))+naturalToOrd = naturalToOrd' (sing :: Sing n)++naturalToOrd' :: HasOrdinal nat+              => Sing (n :: nat) -> Natural -> Maybe (Ordinal n)+naturalToOrd' sn k =+  case fromNatural k of+    SomeSing sk ->+      case sk %< sn of+        STrue -> Just (OLt sk)+        _     -> Nothing+ -- | Convert @Ordinal n@ into monomorphic @Sing@ -- -- Since 0.5.0.0@@ -203,35 +238,43 @@ ordToSing (OLt n) = SomeSing n {-# INLINE ordToSing #-} --- | Convert ordinal into @Int@.-ordToInt :: (HasOrdinal nat, int ~ MonomorphicRep (Sing :: nat -> *))+{-# DEPRECATED ordToInt "Use ordToNatural instead." #-}+-- | Convert ordinal into @'Int'@.+ordToInt :: (HasOrdinal nat)          => Ordinal (n :: nat)-         -> int-ordToInt (OLt n) = demote $ Monomorphic n-{-# SPECIALISE ordToInt :: Ordinal (n :: PN.Nat) -> Integer #-}-{-# SPECIALISE ordToInt :: Ordinal (n :: TL.Nat) -> Integer #-}+         -> Int+ordToInt = fromIntegral . ordToNatural+{-# SPECIALISE ordToInt :: Ordinal (n :: PN.Nat) -> Int #-}+{-# SPECIALISE ordToInt :: Ordinal (n :: TL.Nat) -> Int #-} +ordToNatural :: HasOrdinal nat+             => Ordinal (n :: nat)+             -> Natural+ordToNatural (OLt n) = toNatural n+{-# SPECIALISE ordToNatural :: Ordinal (n :: PN.Nat) -> Natural #-}+{-# SPECIALISE ordToNatural :: Ordinal (n :: TL.Nat) -> Natural #-}+ -- | Inclusion function for ordinals. -- --   Since 0.7.0.0 (constraint was weakened since last released)-inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m+inclusion' :: (n <= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m inclusion' _ = unsafeCoerce {-# INLINE inclusion' #-}  -- | Inclusion function for ordinals with codomain inferred. -- --   Since 0.7.0.0 (constraint was weakened since last released)-inclusion :: ((n :<= m) ~ 'True) => Ordinal n -> Ordinal m-inclusion on = unsafeCoerce on+inclusion :: ((n <= m) ~ 'True) => Ordinal n -> Ordinal m+inclusion = unsafeCoerce {-# INLINE inclusion #-}   -- | Ordinal addition. (@+) :: forall n m. (PeanoOrder nat, SingI (n :: nat), SingI m)-     => Ordinal n -> Ordinal m -> Ordinal (n :+ m)+     => Ordinal n -> Ordinal m -> Ordinal (n + m) OLt k @+ OLt l =   let (n, m) = (n :: Sing n, m :: Sing m)-  in withWitness (plusStrictMonotone k n l m Witness Witness) $ OLt $ k %:+ l+  in withWitness (plusStrictMonotone k n l m Witness Witness) $ OLt $ k %+ l  -- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. --@@ -272,3 +315,4 @@ odPN  = mkOrdinalQQ [t| PN.Nat |] -- | Quasiquoter for ordinal indexed by built-in numeral @'GHC.TypeLits.Nat'@. odLit = mkOrdinalQQ [t| TL.Nat |]+

@@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleInstances, GADTs    #-} {-# LANGUAGE KindSignatures, PatternSynonyms, TypeInType, TypeOperators #-}+{-# OPTIONS_GHC -Wno-warnings-deprecations #-} -- | Module providing the same API as 'Data.Type.Ordinal' but specialised to --   GHC's builtin @'Nat'@. --   @@ -11,20 +12,24 @@          -- $quasiquotes          od,          -- * Conversion from cardinals to ordinals.-         sNatToOrd', sNatToOrd, ordToInt,-         unsafeFromInt, inclusion, inclusion',+         sNatToOrd', sNatToOrd, ordToNatural,+         unsafeNaturalToOrd, naturalToOrd, naturalToOrd',+         inclusion, inclusion',          -- * Ordinal arithmetics          (@+), enumOrdinal,          -- * Elimination rules for @'Ordinal' 0'@.-         absurdOrd, vacuousOrd+         absurdOrd, vacuousOrd,+         -- * Deprecated combinators+         ordToInt, unsafeFromInt        ) where-import           Data.Kind-import           Data.Singletons.Prelude      (POrd (..), Sing (..))+import qualified Data.Type.Natural.Singleton.Compat as SC++import Numeric.Natural (Natural)+import           Data.Singletons (SingI, Sing) import           Data.Singletons.Prelude.Enum (PEnum (..)) import qualified Data.Type.Ordinal            as O import           GHC.TypeLits import           Language.Haskell.TH.Quote    (QuasiQuoter)-import           Data.Type.Monomorphic  -- | Set-theoretic (finite) ordinals: --@@ -42,7 +47,7 @@ --   but it is due to the limitation of GHC's current exhaustiveness checker. --    --   Since 0.7.0.0-pattern OLt :: () => forall  (n1 :: Nat). ((n1 :< t) ~ 'True)+pattern OLt :: () => forall  (n1 :: Nat). ((n1 SC.< t) ~ 'True)             => Sing n1 -> O.Ordinal t pattern OLt n = O.OLt n @@ -50,7 +55,7 @@ --    --   Since 0.7.0.0 pattern OZ :: forall  (n :: Nat). ()-           => (0 :< n) ~ 'True => O.Ordinal n+           => (0 SC.< n) ~ 'True => O.Ordinal n pattern OZ = O.OZ  -- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal.@@ -83,40 +88,59 @@ -- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@. --    --   Since 0.7.0.0-sNatToOrd' :: (m :< n) ~ 'True => Sing n -> Sing m -> Ordinal n+sNatToOrd' :: (m SC.< n) ~ 'True => Sing n -> Sing m -> Ordinal n sNatToOrd' = O.sNatToOrd' {-# INLINE sNatToOrd' #-}  -- | 'sNatToOrd'' with @n@ inferred. --    --   Since 0.7.0.0-sNatToOrd :: (KnownNat n, (m :< n) ~ 'True) => Sing m -> Ordinal n+sNatToOrd :: (KnownNat n, (m SC.< n) ~ 'True) => Sing m -> Ordinal n sNatToOrd = O.sNatToOrd {-# INLINE sNatToOrd #-} +{-# DEPRECATED ordToInt "Use ordToNatural instead" #-} -- | Convert ordinal into @Int@. --    --   Since 0.7.0.0-ordToInt :: Ordinal n -> Integer+ordToInt :: Ordinal n -> Int ordToInt = O.ordToInt {-# INLINE ordToInt #-} +{-# DEPRECATED unsafeFromInt "Use unsafeNaturalToOrd instead" #-} unsafeFromInt :: KnownNat n-              => MonomorphicRep (Sing :: Nat -> Type) -> Ordinal n+              => Int -> Ordinal n unsafeFromInt = O.unsafeFromInt {-# INLINE unsafeFromInt #-} +ordToNatural :: Ordinal (n :: Nat) -> Natural+ordToNatural = O.ordToNatural+{-# INLINE ordToNatural #-}+++naturalToOrd :: SingI (n :: Nat) => Natural -> Maybe (Ordinal n)+naturalToOrd = O.naturalToOrd+{-# INLINE naturalToOrd #-}++naturalToOrd' :: Sing (n :: Nat) -> Natural -> Maybe (Ordinal n)+naturalToOrd' = O.naturalToOrd'+{-# INLINE naturalToOrd' #-}++unsafeNaturalToOrd :: SingI (n :: Nat) => Natural -> Ordinal n+unsafeNaturalToOrd = O.unsafeNaturalToOrd+{-# INLINE unsafeNaturalToOrd #-}+ -- | Inclusion function for ordinals. -- --   Since 0.7.0.0-inclusion :: (n :<= m) ~ 'True => Ordinal n -> Ordinal m+inclusion :: (n SC.<= m) ~ 'True => Ordinal n -> Ordinal m inclusion = O.inclusion {-# INLINE inclusion #-}  -- | Inclusion function for ordinals with codomain inferred. -- --   Since 0.7.0.0-inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m+inclusion' :: (n SC.<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m inclusion' = O.inclusion' {-# INLINE inclusion' #-} 

@@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleInstances, GADTs    #-} {-# LANGUAGE KindSignatures, PatternSynonyms, TypeInType, TypeOperators #-}+{-# OPTIONS_GHC -Wno-warnings-deprecations #-} -- | Module providing the same API as 'Data.Type.Ordinal' but specialised to --   peano numeral @'Nat'@. --   @@ -11,20 +12,23 @@          -- $quasiquotes          od,          -- * Conversion from cardinals to ordinals.-         sNatToOrd', sNatToOrd, ordToInt,-         unsafeFromInt, inclusion, inclusion',+         sNatToOrd', sNatToOrd, inclusion, inclusion',+         ordToNatural, unsafeNaturalToOrd, naturalToOrd, naturalToOrd',          -- * Ordinal arithmetics          (@+), enumOrdinal,          -- * Elimination rules for @'Ordinal' 'Z'@.-         absurdOrd, vacuousOrd+         absurdOrd, vacuousOrd,+         -- * Deprecated Combinators+         ordToInt, unsafeFromInt        ) where-import           Data.Kind-import           Data.Singletons.Prelude      (POrd (..), SingI, Sing (..))+import Data.Type.Natural.Singleton.Compat++import Numeric.Natural (Natural)+import           Data.Singletons.Prelude      (SingI, Sing (..)) import           Data.Singletons.Prelude.Enum (PEnum (..)) import qualified Data.Type.Ordinal            as O import           Data.Type.Natural import           Language.Haskell.TH.Quote    (QuasiQuoter)-import           Data.Type.Monomorphic  -- | Set-theoretic (finite) ordinals: --@@ -42,7 +46,7 @@ --   but it is due to the limitation of GHC's current exhaustiveness checker. --    --   Since 0.7.0.0-pattern OLt :: () => forall  (n1 :: Nat). ((n1 :< t) ~ 'True)+pattern OLt :: () => forall  (n1 :: Nat). ((n1 < t) ~ 'True)             => Sing n1 -> O.Ordinal t pattern OLt n = O.OLt n @@ -50,7 +54,7 @@ --    --   Since 0.7.0.0 pattern OZ :: forall  (n :: Nat). ()-           => ('Z :< n) ~ 'True => O.Ordinal n+           => ('Z < n) ~ 'True => O.Ordinal n pattern OZ = O.OZ  -- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal.@@ -83,47 +87,47 @@ -- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@. --    --   Since 0.7.0.0-sNatToOrd' :: (m :< n) ~ 'True => Sing n -> Sing m -> Ordinal n+sNatToOrd' :: (m < n) ~ 'True => Sing n -> Sing m -> Ordinal n sNatToOrd' = O.sNatToOrd' {-# INLINE sNatToOrd' #-}  -- | 'sNatToOrd'' with @n@ inferred. --    --   Since 0.7.0.0-sNatToOrd :: (SingI n, (m :< n) ~ 'True) => Sing m -> Ordinal n+sNatToOrd :: (SingI n, (m < n) ~ 'True) => Sing m -> Ordinal n sNatToOrd = O.sNatToOrd {-# INLINE sNatToOrd #-}  -- | Convert ordinal into @Int@. --    --   Since 0.7.0.0-ordToInt :: Ordinal n -> Integer+ordToInt :: Ordinal n -> Int ordToInt = O.ordToInt {-# INLINE ordToInt #-}  unsafeFromInt :: SingI n-              => MonomorphicRep (Sing :: Nat -> Type) -> Ordinal n+              => Int -> Ordinal n unsafeFromInt = O.unsafeFromInt {-# INLINE unsafeFromInt #-}  -- | Inclusion function for ordinals. -- --   Since 0.7.0.0-inclusion :: (n :<= m) ~ 'True => Ordinal n -> Ordinal m+inclusion :: (n <= m) ~ 'True => Ordinal n -> Ordinal m inclusion = O.inclusion {-# INLINE inclusion #-}  -- | Inclusion function for ordinals with codomain inferred. -- --   Since 0.7.0.0-inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m+inclusion' :: (n <= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m inclusion' = O.inclusion' {-# INLINE inclusion' #-}  -- | Ordinal addition. -- --   Since 0.7.0.0-(@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)+(@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n + m) (@+) = (O.@+) {-# INLINE (@+) #-} @@ -147,3 +151,16 @@ vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a vacuousOrd = O.vacuousOrd {-# INLINE vacuousOrd #-}++ordToNatural :: Ordinal (n :: Nat) -> Natural+ordToNatural = O.ordToNatural+{-# INLINE ordToNatural #-}++unsafeNaturalToOrd :: SingI (n :: Nat) => Natural -> Ordinal n+unsafeNaturalToOrd = O.unsafeNaturalToOrd++naturalToOrd :: SingI (n :: Nat) => Natural -> Maybe (Ordinal n)+naturalToOrd = O.naturalToOrd++naturalToOrd' :: Sing (n :: Nat) -> Natural -> Maybe (Ordinal n)+naturalToOrd' = O.naturalToOrd'

@@ -1,57 +1,64 @@-name: type-natural-version: 0.7.1.4-cabal-version: >=1.10-build-type: Simple-license: BSD3-license-file: LICENSE-copyright: (C) Hiromi ISHII 2013-2014-maintainer: konn.jinro_at_gmail.com-homepage: https://github.com/konn/type-natural-synopsis: Type-level natural and proofs of their properties.-description:-    Type-level natural numbers and proofs of their properties.-    .-    Version 0.6+ supports __GHC 8+ only__.-    .-    __Use 0.5.* with ~ GHC 7.10.3__.-category: Math-author: Hiromi ISHII-tested-with: GHC ==8.0.2 GHC ==8.2.2+-- Initial type-natural.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/ +name:                type-natural+version:             0.8.0.0+synopsis:            Type-level natural and proofs of their properties.+description:         Type-level natural numbers and proofs of their properties.+                     .+                     Version 0.6+ supports __GHC 8+ only__.+                     .+                     __Use 0.5.* with ~ GHC 7.10.3__.+homepage:            https://github.com/konn/type-natural+license:             BSD3+license-file:        LICENSE+author:              Hiromi ISHII+maintainer:          konn.jinro_at_gmail.com+copyright:           (C) Hiromi ISHII 2013-2014+category:            Math+build-type:          Simple+cabal-version:       >= 1.10+tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1+ source-repository head-    type: git-    location: git://github.com/konn/type-natural.git+  Type: git+  Location: git://github.com/konn/type-natural.git + library-    -    if impl(ghc >=8.0.0)-        ghc-options: -Wno-redundant-constraints-    exposed-modules:-        Data.Type.Natural-        Data.Type.Ordinal-        Data.Type.Ordinal.Builtin-        Data.Type.Ordinal.Peano-        Data.Type.Natural.Builtin-        Data.Type.Natural.Class-        Data.Type.Natural.Class.Arithmetic-        Data.Type.Natural.Class.Order-    build-depends:-        base >=4 && <4.10,-        equational-reasoning >=0.4.1.1 && <0.6,-        monomorphic >=0.0.3 && <0.1,-        template-haskell >=2.8 && <2.12,-        constraints >=0.3 && <0.10,-        ghc-typelits-natnormalise >=0.4 && <0.6,-        ghc-typelits-presburger >=0.1.1 && <0.2,-        singletons >=2.2 && <2.4-    default-language: Haskell2010-    default-extensions: DataKinds PolyKinds ConstraintKinds GADTs-                        ScopedTypeVariables TemplateHaskell TypeFamilies TypeOperators-                        MultiParamTypeClasses UndecidableInstances FlexibleContexts-                        FlexibleInstances-    other-modules:-        Data.Type.Natural.Definitions-        Data.Type.Natural.Core-        Data.Type.Natural.Compat-    ghc-options: -Wall -O2 -fno-warn-orphans+  ghc-options:         -Wall -O2 -fno-warn-orphans+  if impl(ghc >= 8.0.0)+    ghc-options:       -Wno-redundant-constraints+  exposed-modules:     Data.Type.Natural+                     , Data.Type.Ordinal+                     , Data.Type.Ordinal.Builtin+                     , Data.Type.Ordinal.Peano+                     , Data.Type.Natural.Builtin+                     , Data.Type.Natural.Class+                     , Data.Type.Natural.Class.Arithmetic+                     , Data.Type.Natural.Class.Order+  other-modules:       Data.Type.Natural.Definitions+                     , Data.Type.Natural.Core+                     , Data.Type.Natural.Singleton.Compat+                     , Data.Type.Natural.Singleton.Compat.TH+  build-depends:       base                      == 4.*+                     , equational-reasoning      >= 0.4.1.1+                     , template-haskell          >= 2.8+                     , constraints               >= 0.3+                     , ghc-typelits-natnormalise >= 0.4+                     , ghc-typelits-presburger   >= 0.2.0.0+                     , singletons               >= 2.2 && < 2.5 +  default-language:    Haskell2010+  default-extensions:  DataKinds+                       PolyKinds+                       ConstraintKinds+                       GADTs+                       ScopedTypeVariables+                       TemplateHaskell+                       TypeFamilies+                       TypeOperators+                       MultiParamTypeClasses+                       UndecidableInstances+                       FlexibleContexts+                       FlexibleInstances