{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.Nat (
Nat(..),
toNatural,
fromNatural,
cata,
explicitShow,
explicitShowsPrec,
SNat(..),
snatToNat,
snatToNatural,
SNatI(..),
snat,
withSNat,
reify,
reflect,
reflectToNum,
eqNat,
EqNat,
discreteNat,
cmpNat,
induction1,
unfoldedFix,
Plus,
Mult,
Mult2,
DivMod2,
ToGHC,
FromGHC,
nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9,
Nat0, Nat1, Nat2, Nat3, Nat4, Nat5, Nat6, Nat7, Nat8, Nat9,
proofPlusZeroN,
proofPlusNZero,
proofMultZeroN,
proofMultNZero,
proofMultOneN,
proofMultNOne,
) where
import Control.DeepSeq (NFData (..))
import Data.Boring (Boring (..))
import Data.Function (fix)
import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..))
import Data.GADT.DeepSeq (GNFData (..))
import Data.GADT.Show (GShow (..))
import Data.Proxy (Proxy (..))
import Data.Type.Dec (Dec (..))
import Data.Typeable (Typeable)
import Numeric.Natural (Natural)
#if MIN_VERSION_some(1,0,5)
import Data.EqP (EqP (..))
import Data.OrdP (OrdP (..))
import Data.GADT.Compare (defaultCompare, defaultEq)
#endif
import qualified GHC.TypeLits as GHC
import Unsafe.Coerce (unsafeCoerce)
import Data.Nat
import TrustworthyCompat
data SNat (n :: Nat) where
SZ :: SNat 'Z
SS :: SNatI n => SNat ('S n)
deriving (Typeable)
deriving instance Show (SNat p)
class SNatI (n :: Nat) where
induction
:: f 'Z
-> (forall m. SNatI m => f m -> f ('S m))
-> f n
instance SNatI 'Z where
induction :: forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f 'Z
induction f 'Z
n forall (m :: Nat). SNatI m => f m -> f ('S m)
_c = f 'Z
n
instance SNatI n => SNatI ('S n) where
induction :: forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f ('S n)
induction f 'Z
n forall (m :: Nat). SNatI m => f m -> f ('S m)
c = forall (m :: Nat). SNatI m => f m -> f ('S m)
c (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction f 'Z
n forall (m :: Nat). SNatI m => f m -> f ('S m)
c)
snat :: SNatI n => SNat n
snat :: forall (n :: Nat). SNatI n => SNat n
snat = forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction SNat 'Z
SZ (\SNat m
_ -> forall (n :: Nat). SNatI n => SNat ('S n)
SS)
withSNat :: SNat n -> (SNatI n => r) -> r
withSNat :: forall (n :: Nat) r. SNat n -> (SNatI n => r) -> r
withSNat SNat n
SZ SNatI n => r
k = SNatI n => r
k
withSNat SNat n
SS SNatI n => r
k = SNatI n => r
k
reflect :: forall n proxy. SNatI n => proxy n -> Nat
reflect :: forall (n :: Nat) (proxy :: Nat -> *). SNatI n => proxy n -> Nat
reflect proxy n
_ = forall a (n :: Nat). Konst a n -> a
unKonst (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (forall a (n :: Nat). a -> Konst a n
Konst Nat
Z) (forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Konst a n -> Konst b m
kmap Nat -> Nat
S) :: Konst Nat n)
reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m
reflectToNum :: forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
reflectToNum proxy n
_ = forall a (n :: Nat). Konst a n -> a
unKonst (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (forall a (n :: Nat). a -> Konst a n
Konst m
0) (forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Konst a n -> Konst b m
kmap (m
1forall a. Num a => a -> a -> a
+)) :: Konst m n)
reify :: forall r. Nat -> (forall n. SNatI n => Proxy n -> r) -> r
reify :: forall r.
Nat -> (forall (n :: Nat). SNatI n => Proxy @Nat n -> r) -> r
reify Nat
Z forall (n :: Nat). SNatI n => Proxy @Nat n -> r
f = forall (n :: Nat). SNatI n => Proxy @Nat n -> r
f (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy 'Z)
reify (S Nat
n) forall (n :: Nat). SNatI n => Proxy @Nat n -> r
f = forall r.
Nat -> (forall (n :: Nat). SNatI n => Proxy @Nat n -> r) -> r
reify Nat
n (\(Proxy @Nat n
_p :: Proxy n) -> forall (n :: Nat). SNatI n => Proxy @Nat n -> r
f (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy ('S n)))
snatToNat :: forall n. SNat n -> Nat
snatToNat :: forall (n :: Nat). SNat n -> Nat
snatToNat SNat n
SZ = Nat
Z
snatToNat SNat n
SS = forall a (n :: Nat). Konst a n -> a
unKonst (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (forall a (n :: Nat). a -> Konst a n
Konst Nat
Z) (forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Konst a n -> Konst b m
kmap Nat -> Nat
S) :: Konst Nat n)
snatToNatural :: forall n. SNat n -> Natural
snatToNatural :: forall (n :: Nat). SNat n -> Natural
snatToNatural SNat n
SZ = Natural
0
snatToNatural SNat n
SS = forall a (n :: Nat). Konst a n -> a
unKonst (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (forall a (n :: Nat). a -> Konst a n
Konst Natural
0) (forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Konst a n -> Konst b m
kmap forall a. Enum a => a -> a
succ) :: Konst Natural n)
eqNat :: forall n m. (SNatI n, SNatI m) => Maybe (n :~: m)
eqNat :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Maybe ((:~:) @Nat n m)
eqNat = forall (n :: Nat).
NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)
getNatEq forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (forall (n :: Nat).
(forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)) -> NatEq n
NatEq forall (p :: Nat). SNatI p => Maybe ((:~:) @Nat 'Z p)
start) (\NatEq m
p -> forall (n :: Nat).
(forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)) -> NatEq n
NatEq (forall (p :: Nat) (q :: Nat).
SNatI q =>
NatEq p -> Maybe ((:~:) @Nat ('S p) q)
step NatEq m
p)) where
start :: forall p. SNatI p => Maybe ('Z :~: p)
start :: forall (p :: Nat). SNatI p => Maybe ((:~:) @Nat 'Z p)
start = case forall (n :: Nat). SNatI n => SNat n
snat :: SNat p of
SNat p
SZ -> forall a. a -> Maybe a
Just forall {k} (a :: k). (:~:) @k a a
Refl
SNat p
SS -> forall a. Maybe a
Nothing
step :: forall p q. SNatI q => NatEq p -> Maybe ('S p :~: q)
step :: forall (p :: Nat) (q :: Nat).
SNatI q =>
NatEq p -> Maybe ((:~:) @Nat ('S p) q)
step NatEq p
hind = case forall (n :: Nat). SNatI n => SNat n
snat :: SNat q of
SNat q
SZ -> forall a. Maybe a
Nothing
SNat q
SS -> forall (p :: Nat) (q :: Nat).
SNatI q =>
NatEq p -> Maybe ((:~:) @Nat ('S p) ('S q))
step' NatEq p
hind
step' :: forall p q. SNatI q => NatEq p -> Maybe ('S p :~: 'S q)
step' :: forall (p :: Nat) (q :: Nat).
SNatI q =>
NatEq p -> Maybe ((:~:) @Nat ('S p) ('S q))
step' (NatEq forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat p m)
hind) = do
(:~:) @Nat p q
Refl <- forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat p m)
hind :: Maybe (p :~: q)
forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (a :: k). (:~:) @k a a
Refl
newtype NatEq n = NatEq { forall (n :: Nat).
NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)
getNatEq :: forall m. SNatI m => Maybe (n :~: m) }
discreteNat :: forall n m. (SNatI n, SNatI m) => Dec (n :~: m)
discreteNat :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Dec ((:~:) @Nat n m)
discreteNat = forall (n :: Nat).
DiscreteNat n -> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m)
getDiscreteNat forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (forall (n :: Nat).
(forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m))
-> DiscreteNat n
DiscreteNat forall (p :: Nat). SNatI p => Dec ((:~:) @Nat 'Z p)
start) (\DiscreteNat m
p -> forall (n :: Nat).
(forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m))
-> DiscreteNat n
DiscreteNat (forall (p :: Nat) (q :: Nat).
SNatI q =>
DiscreteNat p -> Dec ((:~:) @Nat ('S p) q)
step DiscreteNat m
p))
where
start :: forall p. SNatI p => Dec ('Z :~: p)
start :: forall (p :: Nat). SNatI p => Dec ((:~:) @Nat 'Z p)
start = case forall (n :: Nat). SNatI n => SNat n
snat :: SNat p of
SNat p
SZ -> forall a. a -> Dec a
Yes forall {k} (a :: k). (:~:) @k a a
Refl
SNat p
SS -> forall a. Neg a -> Dec a
No forall a b. (a -> b) -> a -> b
$ \(:~:) @Nat 'Z p
p -> case (:~:) @Nat 'Z p
p of {}
step :: forall p q. SNatI q => DiscreteNat p -> Dec ('S p :~: q)
step :: forall (p :: Nat) (q :: Nat).
SNatI q =>
DiscreteNat p -> Dec ((:~:) @Nat ('S p) q)
step DiscreteNat p
rec = case forall (n :: Nat). SNatI n => SNat n
snat :: SNat q of
SNat q
SZ -> forall a. Neg a -> Dec a
No forall a b. (a -> b) -> a -> b
$ \(:~:) @Nat ('S p) q
p -> case (:~:) @Nat ('S p) q
p of {}
SNat q
SS -> forall (p :: Nat) (q :: Nat).
SNatI q =>
DiscreteNat p -> Dec ((:~:) @Nat ('S p) ('S q))
step' DiscreteNat p
rec
step' :: forall p q. SNatI q => DiscreteNat p -> Dec ('S p :~: 'S q)
step' :: forall (p :: Nat) (q :: Nat).
SNatI q =>
DiscreteNat p -> Dec ((:~:) @Nat ('S p) ('S q))
step' (DiscreteNat forall (m :: Nat). SNatI m => Dec ((:~:) @Nat p m)
rec) = case forall (m :: Nat). SNatI m => Dec ((:~:) @Nat p m)
rec :: Dec (p :~: q) of
Yes (:~:) @Nat p q
Refl -> forall a. a -> Dec a
Yes forall {k} (a :: k). (:~:) @k a a
Refl
No Neg ((:~:) @Nat p q)
np -> forall a. Neg a -> Dec a
No forall a b. (a -> b) -> a -> b
$ \(:~:) @Nat ('S p) ('S q)
Refl -> Neg ((:~:) @Nat p q)
np forall {k} (a :: k). (:~:) @k a a
Refl
newtype DiscreteNat n = DiscreteNat { forall (n :: Nat).
DiscreteNat n -> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m)
getDiscreteNat :: forall m. SNatI m => Dec (n :~: m) }
instance TestEquality SNat where
testEquality :: forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> Maybe ((:~:) @Nat a b)
testEquality SNat a
SZ SNat b
SZ = forall a. a -> Maybe a
Just forall {k} (a :: k). (:~:) @k a a
Refl
testEquality SNat a
SZ SNat b
SS = forall a. Maybe a
Nothing
testEquality SNat a
SS SNat b
SZ = forall a. Maybe a
Nothing
testEquality SNat a
SS SNat b
SS = forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Maybe ((:~:) @Nat n m)
eqNat
type family EqNat (n :: Nat) (m :: Nat) where
EqNat 'Z 'Z = 'True
EqNat ('S n) ('S m) = EqNat n m
EqNat n m = 'False
#if !MIN_VERSION_base(4,11,0)
type instance n == m = EqNat n m
#endif
instance SNatI n => Boring (SNat n) where
boring :: SNat n
boring = forall (n :: Nat). SNatI n => SNat n
snat
instance GShow SNat where
gshowsPrec :: forall (p :: Nat). Int -> SNat p -> ShowS
gshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec
instance NFData (SNat n) where
rnf :: SNat n -> ()
rnf SNat n
SZ = ()
rnf SNat n
SS = ()
instance GNFData SNat where
grnf :: forall (n :: Nat). SNat n -> ()
grnf = forall a. NFData a => a -> ()
rnf
instance GEq SNat where
geq :: forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> Maybe ((:~:) @Nat a b)
geq = forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality @k f =>
f a -> f b -> Maybe ((:~:) @k a b)
testEquality
instance GCompare SNat where
gcompare :: forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> GOrdering @Nat a b
gcompare SNat a
SZ SNat b
SZ = forall {k} (a :: k). GOrdering @k a a
GEQ
gcompare SNat a
SZ SNat b
SS = forall {k} (a :: k) (b :: k). GOrdering @k a b
GLT
gcompare SNat a
SS SNat b
SZ = forall {k} (a :: k) (b :: k). GOrdering @k a b
GGT
gcompare SNat a
SS SNat b
SS = forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
GOrdering @Nat n m
cmpNat
instance Eq (SNat a) where
SNat a
_ == :: SNat a -> SNat a -> Bool
== SNat a
_ = Bool
True
instance Ord (SNat a) where
compare :: SNat a -> SNat a -> Ordering
compare SNat a
_ SNat a
_ = Ordering
EQ
#if MIN_VERSION_some(1,0,5)
instance EqP SNat where eqp :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Bool
eqp = forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq @k f =>
f a -> f b -> Bool
defaultEq
instance OrdP SNat where comparep :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Ordering
comparep = forall {k} (f :: k -> *) (a :: k) (b :: k).
GCompare @k f =>
f a -> f b -> Ordering
defaultCompare
#endif
cmpNat :: forall n m. (SNatI n, SNatI m) => GOrdering n m
cmpNat :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
GOrdering @Nat n m
cmpNat = forall (n :: Nat).
NatCmp n -> forall (m :: Nat). SNatI m => GOrdering @Nat n m
getNatCmp forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (forall (n :: Nat).
(forall (m :: Nat). SNatI m => GOrdering @Nat n m) -> NatCmp n
NatCmp forall (p :: Nat). SNatI p => GOrdering @Nat 'Z p
start) (\NatCmp m
p -> forall (n :: Nat).
(forall (m :: Nat). SNatI m => GOrdering @Nat n m) -> NatCmp n
NatCmp (forall (p :: Nat) (q :: Nat).
SNatI q =>
NatCmp p -> GOrdering @Nat ('S p) q
step NatCmp m
p)) where
start :: forall p. SNatI p => GOrdering 'Z p
start :: forall (p :: Nat). SNatI p => GOrdering @Nat 'Z p
start = case forall (n :: Nat). SNatI n => SNat n
snat :: SNat p of
SNat p
SZ -> forall {k} (a :: k). GOrdering @k a a
GEQ
SNat p
SS -> forall {k} (a :: k) (b :: k). GOrdering @k a b
GLT
step :: forall p q. SNatI q => NatCmp p -> GOrdering ('S p) q
step :: forall (p :: Nat) (q :: Nat).
SNatI q =>
NatCmp p -> GOrdering @Nat ('S p) q
step NatCmp p
hind = case forall (n :: Nat). SNatI n => SNat n
snat :: SNat q of
SNat q
SZ -> forall {k} (a :: k) (b :: k). GOrdering @k a b
GGT
SNat q
SS -> forall (p :: Nat) (q :: Nat).
SNatI q =>
NatCmp p -> GOrdering @Nat ('S p) ('S q)
step' NatCmp p
hind
step' :: forall p q. SNatI q => NatCmp p -> GOrdering ('S p) ('S q)
step' :: forall (p :: Nat) (q :: Nat).
SNatI q =>
NatCmp p -> GOrdering @Nat ('S p) ('S q)
step' (NatCmp forall (m :: Nat). SNatI m => GOrdering @Nat p m
hind) = case forall (m :: Nat). SNatI m => GOrdering @Nat p m
hind :: GOrdering p q of
GOrdering @Nat p q
GEQ -> forall {k} (a :: k). GOrdering @k a a
GEQ
GOrdering @Nat p q
GLT -> forall {k} (a :: k) (b :: k). GOrdering @k a b
GLT
GOrdering @Nat p q
GGT -> forall {k} (a :: k) (b :: k). GOrdering @k a b
GGT
newtype NatCmp n = NatCmp { forall (n :: Nat).
NatCmp n -> forall (m :: Nat). SNatI m => GOrdering @Nat n m
getNatCmp :: forall m. SNatI m => GOrdering n m }
newtype Konst a (n :: Nat) = Konst { forall a (n :: Nat). Konst a n -> a
unKonst :: a }
kmap :: (a -> b) -> Konst a n -> Konst b m
kmap :: forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Konst a n -> Konst b m
kmap = coerce :: forall a b. Coercible @(*) a b => a -> b
coerce
newtype Flipped f a (b :: Nat) = Flip { forall (f :: Nat -> * -> *) a (b :: Nat). Flipped f a b -> f b a
unflip :: f b a }
induction1
:: forall n f a. SNatI n
=> f 'Z a
-> (forall m. SNatI m => f m a -> f ('S m) a)
-> f n a
induction1 :: forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
induction1 f 'Z a
z forall (m :: Nat). SNatI m => f m a -> f ('S m) a
f = forall (f :: Nat -> * -> *) a (b :: Nat). Flipped f a b -> f b a
unflip (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (forall (f :: Nat -> * -> *) a (b :: Nat). f b a -> Flipped f a b
Flip f 'Z a
z) (\(Flip f m a
x) -> forall (f :: Nat -> * -> *) a (b :: Nat). f b a -> Flipped f a b
Flip (forall (m :: Nat). SNatI m => f m a -> f ('S m) a
f f m a
x)))
{-# INLINE induction1 #-}
unfoldedFix :: forall n a proxy. SNatI n => proxy n -> (a -> a) -> a
unfoldedFix :: forall (n :: Nat) a (proxy :: Nat -> *).
SNatI n =>
proxy n -> (a -> a) -> a
unfoldedFix proxy n
_ = forall a (n :: Nat). Fix a n -> (a -> a) -> a
getFix (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction Fix a 'Z
start forall (m :: Nat). Fix a m -> Fix a ('S m)
step :: Fix a n) where
start :: Fix a 'Z
start :: Fix a 'Z
start = forall a (n :: Nat). ((a -> a) -> a) -> Fix a n
Fix forall a. (a -> a) -> a
fix
step :: Fix a m -> Fix a ('S m)
step :: forall (m :: Nat). Fix a m -> Fix a ('S m)
step (Fix (a -> a) -> a
go) = forall a (n :: Nat). ((a -> a) -> a) -> Fix a n
Fix forall a b. (a -> b) -> a -> b
$ \a -> a
f -> a -> a
f ((a -> a) -> a
go a -> a
f)
newtype Fix a (n :: Nat) = Fix { forall a (n :: Nat). Fix a n -> (a -> a) -> a
getFix :: (a -> a) -> a }
type family ToGHC (n :: Nat) :: GHC.Nat where
ToGHC 'Z = 0
ToGHC ('S n) = 1 GHC.+ ToGHC n
type family FromGHC (n :: GHC.Nat) :: Nat where
FromGHC 0 = 'Z
FromGHC n = 'S (FromGHC (n GHC.- 1))
type family Plus (n :: Nat) (m :: Nat) :: Nat where
Plus 'Z m = m
Plus ('S n) m = 'S (Plus n m)
type family Mult (n :: Nat) (m :: Nat) :: Nat where
Mult 'Z m = 'Z
Mult ('S n) m = Plus m (Mult n m)
type family Mult2 (n :: Nat) :: Nat where
Mult2 'Z = 'Z
Mult2 ('S n) = 'S ('S (Mult2 n))
type family DivMod2 (n :: Nat) :: (Nat, Bool) where
DivMod2 'Z = '( 'Z, 'False)
DivMod2 ('S 'Z) = '( 'Z, 'True)
DivMod2 ('S ('S n)) = DivMod2' (DivMod2 n)
type family DivMod2' (p :: (Nat, Bool)) :: (Nat, Bool) where
DivMod2' '(n, b) = '( 'S n, b)
type Nat0 = 'Z
type Nat1 = 'S Nat0
type Nat2 = 'S Nat1
type Nat3 = 'S Nat2
type Nat4 = 'S Nat3
type Nat5 = 'S Nat4
type Nat6 = 'S Nat5
type Nat7 = 'S Nat6
type Nat8 = 'S Nat7
type Nat9 = 'S Nat8
proofPlusZeroN :: Plus Nat0 n :~: n
proofPlusZeroN :: forall (n :: Nat). (:~:) @Nat (Plus 'Z n) n
proofPlusZeroN = forall {k} (a :: k). (:~:) @k a a
Refl
proofPlusNZero :: SNatI n => Plus n Nat0 :~: n
proofPlusNZero :: forall (n :: Nat). SNatI n => (:~:) @Nat (Plus n 'Z) n
proofPlusNZero = forall (n :: Nat). ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n
getProofPlusNZero forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (forall (n :: Nat). (:~:) @Nat (Plus n 'Z) n -> ProofPlusNZero n
ProofPlusNZero forall {k} (a :: k). (:~:) @k a a
Refl) forall (m :: Nat). ProofPlusNZero m -> ProofPlusNZero ('S m)
step where
step :: forall m. ProofPlusNZero m -> ProofPlusNZero ('S m)
step :: forall (m :: Nat). ProofPlusNZero m -> ProofPlusNZero ('S m)
step (ProofPlusNZero (:~:) @Nat (Plus m 'Z) m
Refl) = forall (n :: Nat). (:~:) @Nat (Plus n 'Z) n -> ProofPlusNZero n
ProofPlusNZero forall {k} (a :: k). (:~:) @k a a
Refl
{-# NOINLINE [1] proofPlusNZero #-}
{-# RULES "Nat: n + 0 = n" proofPlusNZero = unsafeCoerce (Refl :: () :~: ()) #-}
newtype ProofPlusNZero n = ProofPlusNZero { forall (n :: Nat). ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n
getProofPlusNZero :: Plus n Nat0 :~: n }
proofMultZeroN :: Mult Nat0 n :~: Nat0
proofMultZeroN :: forall (n :: Nat). (:~:) @Nat (Mult 'Z n) 'Z
proofMultZeroN = forall {k} (a :: k). (:~:) @k a a
Refl
proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0
proofMultNZero :: forall (n :: Nat) (proxy :: Nat -> *).
SNatI n =>
proxy n -> (:~:) @Nat (Mult n 'Z) 'Z
proofMultNZero proxy n
_ =
forall (n :: Nat). ProofMultNZero n -> (:~:) @Nat (Mult n 'Z) 'Z
getProofMultNZero (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (forall (n :: Nat). (:~:) @Nat (Mult n 'Z) 'Z -> ProofMultNZero n
ProofMultNZero forall {k} (a :: k). (:~:) @k a a
Refl) forall (m :: Nat). ProofMultNZero m -> ProofMultNZero ('S m)
step :: ProofMultNZero n)
where
step :: forall m. ProofMultNZero m -> ProofMultNZero ('S m)
step :: forall (m :: Nat). ProofMultNZero m -> ProofMultNZero ('S m)
step (ProofMultNZero (:~:) @Nat (Mult m 'Z) 'Z
Refl) = forall (n :: Nat). (:~:) @Nat (Mult n 'Z) 'Z -> ProofMultNZero n
ProofMultNZero forall {k} (a :: k). (:~:) @k a a
Refl
{-# NOINLINE [1] proofMultNZero #-}
{-# RULES "Nat: n * 0 = n" proofMultNZero = unsafeCoerce (Refl :: () :~: ()) #-}
newtype ProofMultNZero n = ProofMultNZero { forall (n :: Nat). ProofMultNZero n -> (:~:) @Nat (Mult n 'Z) 'Z
getProofMultNZero :: Mult n Nat0 :~: Nat0 }
proofMultOneN :: SNatI n => Mult Nat1 n :~: n
proofMultOneN :: forall (n :: Nat). SNatI n => (:~:) @Nat (Mult Nat1 n) n
proofMultOneN = forall (n :: Nat). SNatI n => (:~:) @Nat (Plus n 'Z) n
proofPlusNZero
{-# NOINLINE [1] proofMultOneN #-}
{-# RULES "Nat: 1 * n = n" proofMultOneN = unsafeCoerce (Refl :: () :~: ()) #-}
proofMultNOne :: SNatI n => Mult n Nat1 :~: n
proofMultNOne :: forall (n :: Nat). SNatI n => (:~:) @Nat (Mult n Nat1) n
proofMultNOne = forall (n :: Nat). ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n
getProofMultNOne forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (forall (n :: Nat). (:~:) @Nat (Mult n Nat1) n -> ProofMultNOne n
ProofMultNOne forall {k} (a :: k). (:~:) @k a a
Refl) forall (m :: Nat). ProofMultNOne m -> ProofMultNOne ('S m)
step where
step :: forall m. ProofMultNOne m -> ProofMultNOne ('S m)
step :: forall (m :: Nat). ProofMultNOne m -> ProofMultNOne ('S m)
step (ProofMultNOne (:~:) @Nat (Mult m Nat1) m
Refl) = forall (n :: Nat). (:~:) @Nat (Mult n Nat1) n -> ProofMultNOne n
ProofMultNOne forall {k} (a :: k). (:~:) @k a a
Refl
{-# NOINLINE [1] proofMultNOne #-}
{-# RULES "Nat: n * 1 = n" proofMultNOne = unsafeCoerce (Refl :: () :~: ()) #-}
newtype ProofMultNOne n = ProofMultNOne { forall (n :: Nat). ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n
getProofMultNOne :: Mult n Nat1 :~: n }