diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs --- a/Data/Type/Natural.hs +++ b/Data/Type/Natural.hs @@ -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 |] diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs --- a/Data/Type/Natural/Builtin.hs +++ b/Data/Type/Natural/Builtin.hs @@ -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 |] + diff --git a/Data/Type/Natural/Class.hs b/Data/Type/Natural/Class.hs --- a/Data/Type/Natural/Class.hs +++ b/Data/Type/Natural/Class.hs @@ -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. -- diff --git a/Data/Type/Natural/Class/Arithmetic.hs b/Data/Type/Natural/Class/Arithmetic.hs --- a/Data/Type/Natural/Class/Arithmetic.hs +++ b/Data/Type/Natural/Class/Arithmetic.hs @@ -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 diff --git a/Data/Type/Natural/Class/Order.hs b/Data/Type/Natural/Class/Order.hs --- a/Data/Type/Natural/Class/Order.hs +++ b/Data/Type/Natural/Class/Order.hs @@ -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 diff --git a/Data/Type/Natural/Compat.hs b/Data/Type/Natural/Compat.hs deleted file mode 100644 --- a/Data/Type/Natural/Compat.hs +++ /dev/null @@ -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 diff --git a/Data/Type/Natural/Core.hs b/Data/Type/Natural/Core.hs --- a/Data/Type/Natural/Core.hs +++ b/Data/Type/Natural/Core.hs @@ -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 + diff --git a/Data/Type/Natural/Definitions.hs b/Data/Type/Natural/Definitions.hs --- a/Data/Type/Natural/Definitions.hs +++ b/Data/Type/Natural/Definitions.hs @@ -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 diff --git a/Data/Type/Natural/Singleton/Compat.hs b/Data/Type/Natural/Singleton/Compat.hs new file mode 100644 --- /dev/null +++ b/Data/Type/Natural/Singleton/Compat.hs @@ -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 + diff --git a/Data/Type/Natural/Singleton/Compat/TH.hs b/Data/Type/Natural/Singleton/Compat/TH.hs new file mode 100644 --- /dev/null +++ b/Data/Type/Natural/Singleton/Compat/TH.hs @@ -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) + diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs --- a/Data/Type/Ordinal.hs +++ b/Data/Type/Ordinal.hs @@ -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 |] + diff --git a/Data/Type/Ordinal/Builtin.hs b/Data/Type/Ordinal/Builtin.hs --- a/Data/Type/Ordinal/Builtin.hs +++ b/Data/Type/Ordinal/Builtin.hs @@ -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' #-} diff --git a/Data/Type/Ordinal/Peano.hs b/Data/Type/Ordinal/Peano.hs --- a/Data/Type/Ordinal/Peano.hs +++ b/Data/Type/Ordinal/Peano.hs @@ -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' diff --git a/type-natural.cabal b/type-natural.cabal --- a/type-natural.cabal +++ b/type-natural.cabal @@ -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