type-natural-0.2.1.2: Data/Type/Natural.hs
{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}
{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-}
{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies, ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators, UndecidableInstances, StandaloneDeriving #-}
-- | Type level peano natural number, some arithmetic functions and their singletons.
module Data.Type.Natural (-- * Re-exported modules.
module Data.Singletons,
-- * Natural Numbers
-- | Peano natural numbers. It will be promoted to the type-level natural number.
Nat(..),
-- | Singleton type for 'Nat'.
SNat, Sing (SZ, SS),
-- ** Smart constructors
-- | WARNING: Smart constructors are deprecated as of singletons 0.10,
-- so these are provided only for backward compatibility.
sZ, sS,
-- ** Arithmetic functions and their singletons.
min, Min, sMin, max, Max, sMax,
(:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*),
(:-:), (:-), (%:-), (%-),
-- ** Type-level predicate & judgements
Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance,
boolToPropLeq, boolToClassLeq, propToClassLeq,
LeqTrueInstance, propToBoolLeq,
-- * Conversion functions
natToInt, intToNat, sNatToInt,
-- * Quasi quotes for natural numbers
nat, snat,
-- * Properties of natural numbers
succCongEq, plusCongR, plusCongL, succPlusL, succPlusR,
plusZR, plusZL, eqPreservesS, plusAssociative,
multAssociative, multComm, multZL, multZR, multOneL,
multOneR, snEqZAbsurd, succInjective, plusInjectiveL, plusInjectiveR,
plusMultDistr, multPlusDistr, multCongL, multCongR,
sAndPlusOne, plusCommutative, minusCongEq, minusNilpotent,
eqSuccMinus, plusMinusEqL, plusMinusEqR,
zAbsorbsMinR, zAbsorbsMinL, plusSR, plusNeutralR, plusNeutralL,
leqRhs, leqLhs, minComm, maxZL, maxComm, maxZR,
-- * Properties of ordering 'Leq'
leqRefl, leqSucc, leqTrans, plusMonotone, plusLeqL, plusLeqR,
minLeqL, minLeqR, leqAnitsymmetric, maxLeqL, maxLeqR,
leqSnZAbsurd, leqnZElim, leqSnLeq, leqPred, leqSnnAbsurd,
-- * Useful type synonyms and constructors
zero, one, two, three, four, five, six, seven, eight, nine, ten, eleven,
twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty,
Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten,
Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty,
sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven,
sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty,
n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, n12, n13, n14, n15, n16, n17, n18, n19, n20,
N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20,
sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14,
sN15, sN16, sN17, sN18, sN19, sN20
) where
import Data.Singletons
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
import Data.Singletons.TH (singletons)
import Data.Singletons.Prelude hiding ((:<=), SOrd(..), MaxSym1, MaxSym0, MaxSym2
, MinSym1, MinSym0, MinSym2, Max, Min)
#endif
import Data.Type.Monomorphic
import Prelude (Int, Bool (..), Eq (..), Integral (..), Ord ((<)),
Show (..), error, id, otherwise, ($), (.), undefined)
import qualified Prelude as P
import Proof.Equational
import Data.Constraint hiding ((:-))
import Language.Haskell.TH.Quote
import Unsafe.Coerce
import Language.Haskell.TH
--------------------------------------------------
-- * Natural numbers and its singleton type
--------------------------------------------------
singletons [d|
data Nat = Z | S Nat
deriving (Show, Eq, Ord)
|]
--------------------------------------------------
-- ** Arithmetic functions.
--------------------------------------------------
singletons [d|
-- | Minimum function.
min :: Nat -> Nat -> Nat
min Z Z = Z
min Z (S _) = Z
min (S _) Z = Z
min (S m) (S n) = S (min m n)
-- | Maximum function.
max :: Nat -> Nat -> Nat
max Z Z = Z
max Z (S n) = S n
max (S n) Z = S n
max (S n) (S m) = S (max n m)
|]
singletons [d|
(+) :: Nat -> Nat -> Nat
Z + n = n
S m + n = S (m + n)
(-) :: Nat -> Nat -> Nat
n - Z = n
S n - S m = n - m
Z - S _ = Z
(*) :: Nat -> Nat -> Nat
Z * _ = Z
S n * m = n * m + m
|]
instance P.Num Nat where
n - m = n - m
n + m = n + m
n * m = n * m
abs = id
signum Z = Z
signum _ = S Z
fromInteger 0 = Z
fromInteger n | n P.< 0 = error "negative integer"
| otherwise = S $ P.fromInteger (n P.- 1)
infixl 6 :-:, %:-, -
type n :-: m = n :- m
infixl 6 :+:, %+, %:+, :+
type n :+: m = n :+ m
-- | Addition for singleton numbers.
(%+) :: SNat n -> SNat m -> SNat (n :+: m)
(%+) = (%:+)
infixl 7 :*:, %*, %:*, :*
-- | Type-level multiplication.
type n :*: m = n :* m
-- | Multiplication for singleton numbers.
(%*) :: SNat n -> SNat m -> SNat (n :*: m)
(%*) = (%:*)
--------------------------------------------------
-- ** Convenient synonyms
--------------------------------------------------
singletons [d|
zero, one, two, three, four, five, six, seven, eight, nine, ten :: Nat
eleven, twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty :: Nat
zero = Z
one = S zero
two = S one
three = S two
four = S three
five = S four
six = S five
seven = S six
eight = S seven
nine = S eight
ten = S nine
eleven = S ten
twelve = S eleven
thirteen = S twelve
fourteen = S thirteen
fifteen = S fourteen
sixteen = S fifteen
seventeen = S sixteen
eighteen = S seventeen
nineteen = S eighteen
twenty = S nineteen
n0, n1, n2, n3, n4, n5, n6, n7, n8, n9 :: Nat
n10, n11, n12, n13, n14, n15, n16, n17 :: Nat
n18, n19, n20 :: Nat
n0 = zero
n1 = one
n2 = two
n3 = three
n4 = four
n5 = five
n6 = six
n7 = seven
n8 = eight
n9 = nine
n10 = ten
n11 = eleven
n12 = twelve
n13 = thirteen
n14 = fourteen
n15 = fifteen
n16 = sixteen
n17 = seventeen
n18 = eighteen
n19 = nineteen
n20 = twenty
|]
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
sZ :: SNat Z
sZ = SZ
sS :: SNat n -> SNat (S n)
sS = SS
{-# DEPRECATED sZ, sS "Smart constructors are no longer needed in singletons; Use `SS` or `SZ` instead." #-}
#endif
--------------------------------------------------
-- ** Type-level predicate & judgements.
--------------------------------------------------
-- | Comparison via type-class.
class (n :: Nat) :<= (m :: Nat)
instance Z :<= n
instance (n :<= m) => S n :<= S m
-- | Boolean-valued type-level comparison function.
singletons [d|
(<<=) :: Nat -> Nat -> Bool
Z <<= _ = True
S _ <<= Z = False
S n <<= S m = n <<= m
|]
-- | Comparison via GADTs.
data Leq (n :: Nat) (m :: Nat) where
ZeroLeq :: SNat m -> Leq Zero m
SuccLeqSucc :: Leq n m -> Leq (S n) (S m)
type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)
(%-) :: (m :<<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m)
n %- SZ = n
SS n %- SS m = n %- m
_ %- _ = error "impossible!"
infixl 6 %-
deriving instance Show (SNat n)
deriving instance Eq (SNat n)
data (a :: Nat) :<: (b :: Nat) where
ZeroLtSucc :: Zero :<: S m
SuccLtSucc :: n :<: m -> S n :<: S m
deriving instance Show (a :<: b)
--------------------------------------------------
-- * Total orderings on natural numbers.
--------------------------------------------------
propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m
propToBoolLeq _ = unsafeCoerce (Dict :: Dict ())
{-# INLINE propToBoolLeq #-}
boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
boolToClassLeq _ = unsafeCoerce (Dict :: Dict ())
{-# INLINE boolToClassLeq #-}
propToClassLeq :: Leq n m -> LeqInstance n m
propToClassLeq _ = unsafeCoerce (Dict :: Dict ())
{-# INLINE propToClassLeq #-}
{-
-- | Below is the "proof" of the correctness of above:
propToBoolLeq :: Leq n m -> LeqTrueInstance n m
propToBoolLeq (ZeroLeq _) = Dict
propToBoolLeq (SuccLeqSucc leq) = case propToBoolLeq leq of Dict -> Dict
{-# RULES
"propToBoolLeq/unsafeCoerce" forall (x :: Leq n m) .
propToBoolLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict ((n :<<= m) ~ True)
#-}
boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
boolToClassLeq SZ _ = Dict
boolToClassLeq (SS n) (SS m) = case boolToClassLeq n m of Dict -> Dict
boolToClassLeq _ _ = bugInGHC
{-# RULES
"boolToClassLeq/unsafeCoerce" forall (n :: SNat n) (m :: SNat m).
boolToClassLeq n m = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)
#-}
propToClassLeq :: Leq n m -> LeqInstance n m
propToClassLeq (ZeroLeq _) = Dict
propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict
{-# RULES
"propToClassLeq/unsafeCoerce" forall (x :: Leq n m) .
propToClassLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)
#-}
-}
type LeqInstance n m = Dict (n :<= m)
boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m
boolToPropLeq SZ m = ZeroLeq m
boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m
boolToPropLeq _ _ = bugInGHC
leqRhs :: Leq n m -> SNat m
leqRhs (ZeroLeq m) = m
leqRhs (SuccLeqSucc leq) = sS $ leqRhs leq
leqLhs :: Leq n m -> SNat n
leqLhs (ZeroLeq _) = sZ
leqLhs (SuccLeqSucc leq) = sS $ leqLhs leq
--------------------------------------------------
-- * Properties
--------------------------------------------------
plusZR :: SNat n -> n :+: Z :=: n
plusZR SZ = Refl
plusZR (SS n) =
start (sS n %+ sZ)
=~= sS (n %+ sZ)
=== sS n `because` cong' sS (plusZR n)
eqPreservesS :: n :=: m -> S n :=: S m
eqPreservesS Refl = Refl
plusZL :: SNat n -> Z :+: n :=: n
plusZL _ = Refl
succCongEq :: n :=: m -> S n :=: S m
succCongEq Refl = Refl
snEqZAbsurd :: S n :=: Z -> a
snEqZAbsurd _ = bugInGHC "impossible!"
succInjective :: S n :=: S m -> n :=: m
succInjective Refl = Refl
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 $ succInjective eq
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` plusCommutative l n
=== m %:+ l `because` eq
=== l %:+ m `because` plusCommutative m l
sAndPlusOne :: SNat n -> S n :=: n :+: One
sAndPlusOne SZ = Refl
sAndPlusOne (SS n) =
start (sS (sS n))
=== sS (n %+ sOne) `because` cong' sS (sAndPlusOne n)
=~= sS n %+ sOne
plusAssociative :: SNat n -> SNat m -> SNat l
-> n :+: (m :+: l) :=: (n :+: m) :+: l
plusAssociative SZ _ _ = Refl
plusAssociative (SS n) m l =
start (sS n %+ (m %+ l))
=~= sS (n %+ (m %+ l))
=== sS ((n %+ m) %+ l) `because` cong' sS (plusAssociative n m l)
=~= sS (n %+ m) %+ l
=~= (sS n %+ m) %+ l
plusSR :: SNat n -> SNat m -> S (n :+: m) :=: n :+: S m
plusSR n m =
start (sS (n %+ m))
=== (n %+ m) %+ sOne `because` sAndPlusOne (n %+ m)
=== n %+ (m %+ sOne) `because` symmetry (plusAssociative n m sOne)
=== n %+ sS m `because` plusCongL n (symmetry $ sAndPlusOne m)
plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m'
plusCongL _ Refl = Refl
plusCongR :: SNat n -> m :=: m' -> m :+ n :=: m' :+ n
plusCongR _ Refl = Refl
succPlusL :: SNat n -> SNat m -> S n :+ m :=: S (n :+ m)
succPlusL _ _ = Refl
succPlusR :: SNat n -> SNat m -> n :+ S m :=: S (n :+ m)
succPlusR SZ _ = Refl
succPlusR (SS n) m =
start (sS n %+ sS m)
=~= sS (n %+ sS m)
=== sS (sS (n %+ m)) `because` succCongEq (succPlusR n m)
=~= sS (sS n %+ m)
minusCongEq :: n :=: m -> SNat l -> n :-: l :=: m :-: l
minusCongEq Refl _ = Refl
minusNilpotent :: SNat n -> n :-: n :=: Zero
minusNilpotent SZ = Refl
minusNilpotent (SS n) =
start (sS n %:- sS n)
=~= n %:- n
=== sZ `because` minusNilpotent n
plusCommutative :: SNat n -> SNat m -> n :+: m :=: m :+: n
plusCommutative SZ SZ = Refl
plusCommutative SZ (SS m) =
start (sZ %+ sS m)
=~= sS m
=== sS (m %+ sZ) `because` cong' sS (plusCommutative SZ m)
=~= sS m %+ sZ
plusCommutative (SS n) m =
start (sS n %+ m)
=~= sS (n %+ m)
=== sS (m %+ n) `because` cong' sS (plusCommutative n m)
=== (m %+ n) %+ sOne `because` sAndPlusOne (m %+ n)
=== m %+ (n %+ sOne) `because` symmetry (plusAssociative m n sOne)
=== m %+ sS n `because` plusCongL m (symmetry $ sAndPlusOne n)
eqSuccMinus :: ((m :<<= n) ~ True)
=> SNat n -> SNat m -> (S n :-: m) :=: (S (n :-: m))
eqSuccMinus _ SZ = Refl
eqSuccMinus (SS n) (SS m) =
start (sS (sS n) %:- sS m)
=~= sS n %:- m
=== sS (n %:- m) `because` eqSuccMinus n m
=~= sS (sS n %:- sS m)
eqSuccMinus _ _ = bugInGHC
plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n
plusMinusEqL SZ m = minusNilpotent m
plusMinusEqL (SS n) m =
case propToBoolLeq (plusLeqR n m) of
Dict -> transitivity (eqSuccMinus (n %+ m) m) (eqPreservesS $ plusMinusEqL n m)
plusMinusEqR :: SNat n -> SNat m -> (m :+: n) :-: m :=: n
plusMinusEqR n m = transitivity (minusCongEq (plusCommutative m n) m) (plusMinusEqL n m)
zAbsorbsMinR :: SNat n -> Min n Z :=: Z
zAbsorbsMinR SZ = Refl
zAbsorbsMinR (SS n) =
case zAbsorbsMinR n of
Refl -> Refl
zAbsorbsMinL :: SNat n -> Min Z n :=: Z
zAbsorbsMinL SZ = Refl
zAbsorbsMinL (SS n) = case zAbsorbsMinL n of Refl -> Refl
minComm :: SNat n -> SNat m -> Min n m :=: Min m n
minComm SZ SZ = Refl
minComm SZ (SS _) = Refl
minComm (SS _) SZ = Refl
minComm (SS n) (SS m) = case minComm n m of Refl -> Refl
maxZL :: SNat n -> Max Z n :=: n
maxZL SZ = Refl
maxZL (SS _) = Refl
maxComm :: SNat n -> SNat m -> (Max n m) :=: (Max m n)
maxComm SZ SZ = Refl
maxComm SZ (SS _) = Refl
maxComm (SS _) SZ = Refl
maxComm (SS n) (SS m) = case maxComm n m of Refl -> Refl
maxZR :: SNat n -> Max n Z :=: n
maxZR n = transitivity (maxComm n sZ) (maxZL n)
multPlusDistr :: SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: n :* m :+ n :* l
multPlusDistr SZ _ _ = Refl
multPlusDistr (SS n) m l =
start (sS n %* (m %+ l))
=~= n %* (m %+ l) %+ (m %+ l)
=== (n %* m) %+ (n %* l) %+ (m %+ l) `because` plusCongR (m %+ l) (multPlusDistr n m l)
=== (n %* m) %+ (n %* l) %+ (l %+ m) `because` plusCongL ((n %* m) %+ (n %* l)) (plusCommutative m l)
=== n %* m %+ (n %*l %+ (l %+ m)) `because` symmetry (plusAssociative (n %* m) (n %* l) (l %+ m))
=== n %* l %+ (l %+ m) %+ n %* m `because` plusCommutative (n %* m) (n %*l %+ (l %+ m))
=== (n %* l %+ l) %+ m %+ n %* m `because` plusCongR (n %* m) (plusAssociative (n %* l) l m)
=~= (sS n %* l) %+ m %+ n %* m
=== (sS n %* l) %+ (m %+ (n %* m)) `because` symmetry (plusAssociative (sS n %* l) m (n %* m))
=== (sS n %* l) %+ ((n %* m) %+ m) `because` plusCongL (sS n %* l) (plusCommutative m (n %* m))
=~= (sS n %* l) %+ (sS n %* m)
=== (sS n %* m) %+ (sS n %* l) `because` plusCommutative (sS n %* l) (sS n %* m)
plusMultDistr :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: n :* l :+ m :* l
plusMultDistr SZ _ _ = Refl
plusMultDistr (SS n) m l =
start ((SS n %+ m) %* l)
=~= sS (n %+ m) %* l
=~= (n %+ m) %* l %+ l
=== n %* l %+ m %* l %+ l `because` plusCongR l (plusMultDistr n m l)
=== m %* l %+ n %* l %+ l `because` plusCongR l (plusCommutative (n %* l) (m %* l))
=== m %* l %+ (n %* l %+ l) `because` symmetry (plusAssociative (m %* l) (n %*l) l)
=~= m %* l %+ (sS n %* l)
=== (sS n %* l) %+ (m %* l) `because` plusCommutative (m %* l) (sS n %* l)
multAssociative :: SNat n -> SNat m -> SNat l -> n :* (m :* l) :=: (n :* m) :* l
multAssociative SZ _ _ = Refl
multAssociative (SS n) m l =
start (sS n %* (m %* l))
=~= n %* (m %* l) %+ (m %* l)
=== (n %* m) %* l %+ (m %* l) `because` plusCongR (m %* l) (multAssociative n m l)
=== (n %* m %+ m) %* l `because` symmetry (plusMultDistr (n %* m) m l)
=~= (sS n %* m) %* l
multZL :: SNat m -> Zero :* m :=: Zero
multZL _ = Refl
multZR :: SNat m -> m :* Zero :=: Zero
multZR SZ = Refl
multZR (SS n) =
start (sS n %* sZ)
=~= n %* sZ %+ sZ
=== sZ %+ sZ `because` plusCongR sZ (multZR n)
=~= sZ
multOneL :: SNat n -> One :* n :=: n
multOneL n =
start (sOne %* n)
=~= sZero %* n %+ n
=~= sZero %:+ n
=~= n
multOneR :: SNat n -> n :* One :=: n
multOneR SZ = Refl
multOneR (SS n) =
start (sS n %* sOne)
=~= n %* sOne %+ sOne
=== n %+ sOne `because` plusCongR sOne (multOneR n)
=== sS n `because` symmetry (sAndPlusOne n)
multCongL :: SNat n -> m :=: l -> n :* m :=: n :* l
multCongL _ Refl = Refl
multCongR :: SNat n -> m :=: l -> m :* n :=: l :* n
multCongR _ Refl = Refl
multComm :: SNat n -> SNat m -> n :* m :=: m :* n
multComm SZ m =
start (sZ %* m)
=~= sZ
=== m %* sZ `because` symmetry (multZR m)
multComm (SS n) m =
start (sS n %* m)
=~= n %* m %+ m
=== m %* n %+ m `because` plusCongR m (multComm n m)
=== m %* n %+ m %* sOne `because` plusCongL (m %* n) (symmetry $ multOneR m)
=== m %* (n %+ sOne) `because` symmetry (multPlusDistr m n sOne)
=== m %* sS n `because` multCongL m (symmetry $ sAndPlusOne n)
plusNeutralR :: SNat n -> SNat m -> n :+ m :=: n -> m :=: Z
plusNeutralR SZ m eq =
start m
=~= sZ %:+ m
=== sZ `because` eq
plusNeutralR (SS n) m eq = plusNeutralR n m $ succInjective eq
plusNeutralL :: SNat n -> SNat m -> n :+ m :=: m -> n :=: Z
plusNeutralL n m eq = plusNeutralR m n $
start (m %:+ n)
=== n %:+ m `because` plusCommutative m n
=== m `because` eq
--------------------------------------------------
-- * Properties of 'Leq'
--------------------------------------------------
leqRefl :: SNat n -> Leq n n
leqRefl SZ = ZeroLeq sZ
leqRefl (SS n) = SuccLeqSucc $ leqRefl n
leqSucc :: SNat n -> Leq n (S n)
leqSucc SZ = ZeroLeq sOne
leqSucc (SS n) = SuccLeqSucc $ leqSucc n
leqTrans :: Leq n m -> Leq m l -> Leq n l
leqTrans (ZeroLeq _) leq = ZeroLeq $ leqRhs leq
leqTrans (SuccLeqSucc nLeqm) (SuccLeqSucc mLeql) = SuccLeqSucc $ leqTrans nLeqm mLeql
leqTrans _ _ = error "impossible!"
instance Preorder Leq where
reflexivity = leqRefl
transitivity = leqTrans
plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)
plusMonotone (ZeroLeq m) (ZeroLeq k) = ZeroLeq (m %+ k)
plusMonotone (ZeroLeq m) (SuccLeqSucc leq) =
case plusSR m (leqRhs leq) of
Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq
plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'
plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)
plusLeqL SZ m = ZeroLeq $ coerce (symmetry $ plusZL m) m
plusLeqL (SS n) m =
start (sS n)
=<= sS (n %+ m) `because` SuccLeqSucc (plusLeqL n m)
=~= sS n %+ m
plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)
plusLeqR n m =
case plusCommutative n m of
Refl -> plusLeqL m n
minLeqL :: SNat n -> SNat m -> Leq (Min n m) n
minLeqL SZ m = case zAbsorbsMinL m of Refl -> ZeroLeq sZ
minLeqL n SZ = case zAbsorbsMinR n of Refl -> ZeroLeq n
minLeqL (SS n) (SS m) = SuccLeqSucc (minLeqL n m)
minLeqR :: SNat n -> SNat m -> Leq (Min n m) m
minLeqR n m = case minComm n m of Refl -> minLeqL m n
leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m
leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl
leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreservesS $ leqAnitsymmetric leq1 leq2
leqAnitsymmetric _ _ = bugInGHC
maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)
maxLeqL SZ m = ZeroLeq (sMax sZ m)
maxLeqL n SZ = case maxZR n of
Refl -> leqRefl n
maxLeqL (SS n) (SS m) = SuccLeqSucc $ maxLeqL n m
maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)
maxLeqR n m = case maxComm n m of
Refl -> maxLeqL m n
leqSnZAbsurd :: Leq (S n) Z -> a
leqSnZAbsurd _ = error "cannot be occured"
leqnZElim :: Leq n Z -> n :=: Z
leqnZElim (ZeroLeq SZ) = Refl
leqSnLeq :: Leq (S n) m -> Leq n m
leqSnLeq (SuccLeqSucc leq) =
let n = leqLhs leq
m = sS $ leqRhs leq
in start n
=<= sS n `because` leqSucc n
=<= m `because` SuccLeqSucc leq
leqPred :: Leq (S n) (S m) -> Leq n m
leqPred (SuccLeqSucc leq) = leq
leqSnnAbsurd :: Leq (S n) n -> a
leqSnnAbsurd (SuccLeqSucc leq) =
case leqLhs leq of
SS _ -> leqSnnAbsurd leq
_ -> bugInGHC "cannot be occured"
--------------------------------------------------
-- * Conversion functions.
--------------------------------------------------
-- | Convert integral numbers into 'Nat'
intToNat :: (Integral a, Ord a) => a -> Nat
intToNat 0 = Z
intToNat n
| n < 0 = error "negative integer"
| otherwise = S $ intToNat (n P.- 1)
-- | Convert 'Nat' into normal integers.
natToInt :: Integral n => Nat -> n
natToInt Z = 0
natToInt (S n) = natToInt n P.+ 1
-- | Convert 'SNat n' into normal integers.
sNatToInt :: P.Num n => SNat x -> n
sNatToInt SZ = 0
sNatToInt (SS n) = sNatToInt n P.+ 1
instance Monomorphicable (Sing :: Nat -> *) where
type MonomorphicRep (Sing :: Nat -> *) = Int
demote (Monomorphic sn) = sNatToInt sn
promote n
| n < 0 = error "negative integer!"
| n == 0 = Monomorphic sZ
| otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ sS sn
--------------------------------------------------
-- * Quasi Quoter
--------------------------------------------------
-- | Quotesi-quoter for 'Nat'. This can be used for an expression, pattern and type.
--
-- for example: @sing :: SNat ([nat| 2 |] :+ [nat| 5 |])@
nat :: QuasiQuoter
nat = QuasiQuoter { quoteExp = P.foldr appE (conE 'Z) . P.flip P.replicate (conE 'S) . P.read
, quotePat = P.foldr (\a b -> conP a [b]) (conP 'Z []) . P.flip P.replicate 'S . P.read
, quoteType = P.foldr appT (conT 'Z) . P.flip P.replicate (conT 'S) . P.read
, quoteDec = error "not implemented"
}
-- | Quotesi-quoter for 'SNat'. This can be used for an expression, pattern and type.
--
-- For example: @[snat|12|] '%+' [snat| 5 |]@, @'sing' :: [snat| 12 |]@, @f [snat| 12 |] = \"hey\"@
snat :: QuasiQuoter
snat = QuasiQuoter { quoteExp = P.foldr appE (conE 'SZ) . P.flip P.replicate (conE 'SS) . P.read
, quotePat = P.foldr (\a b -> conP a [b]) (conP 'SZ []) . P.flip P.replicate 'SS . P.read
, quoteType = appT (conT ''SNat) . P.foldr appT (conT 'Z) . P.flip P.replicate (conT 'S) . P.read
, quoteDec = error "not implemented"
}