{-# 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.EqP (EqP (..))
import Data.Function (fix)
import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..), defaultCompare, defaultEq)
import Data.GADT.DeepSeq (GNFData (..))
import Data.GADT.Show (GShow (..))
import Data.OrdP (OrdP (..))
import Data.Proxy (Proxy (..))
import Data.Type.Dec (Dec (..))
import Data.Typeable (Typeable)
import Numeric.Natural (Natural)
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 = f n -> f ('S n)
forall (m :: Nat). SNatI m => f m -> f ('S m)
c (f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction f 'Z
n f m -> f ('S m)
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 = SNat 'Z
-> (forall (m :: Nat). SNatI m => SNat m -> SNat ('S m)) -> SNat n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction SNat 'Z
SZ (\SNat m
_ -> SNat ('S 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 = r
SNatI n => r
k
withSNat SNat n
SS SNatI n => r
k = r
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
_ = Konst Nat n -> Nat
forall a (n :: Nat). Konst a n -> a
unKonst (Konst Nat 'Z
-> (forall (m :: Nat). SNatI m => Konst Nat m -> Konst Nat ('S m))
-> Konst Nat n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (Nat -> Konst Nat 'Z
forall a (n :: Nat). a -> Konst a n
Konst Nat
Z) ((Nat -> Nat) -> Konst Nat m -> Konst Nat ('S m)
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
_ = Konst m n -> m
forall a (n :: Nat). Konst a n -> a
unKonst (Konst m 'Z
-> (forall (m :: Nat). SNatI m => Konst m m -> Konst m ('S m))
-> Konst m n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (m -> Konst m 'Z
forall a (n :: Nat). a -> Konst a n
Konst m
0) ((m -> m) -> Konst m m -> Konst m ('S m)
forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Konst a n -> Konst b m
kmap (m
1m -> m -> m
forall 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 = Proxy @Nat 'Z -> r
forall (n :: Nat). SNatI n => Proxy @Nat n -> r
f (Proxy @Nat 'Z
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy 'Z)
reify (S Nat
n) forall (n :: Nat). SNatI n => Proxy @Nat n -> r
f = Nat -> (forall (n :: Nat). SNatI n => Proxy @Nat n -> r) -> r
forall r.
Nat -> (forall (n :: Nat). SNatI n => Proxy @Nat n -> r) -> r
reify Nat
n (\(Proxy @Nat n
_p :: Proxy n) -> Proxy @Nat ('S n) -> r
forall (n :: Nat). SNatI n => Proxy @Nat n -> r
f (Proxy @Nat ('S n)
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 = Konst Nat n -> Nat
forall a (n :: Nat). Konst a n -> a
unKonst (Konst Nat 'Z
-> (forall (m :: Nat). SNatI m => Konst Nat m -> Konst Nat ('S m))
-> Konst Nat n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (Nat -> Konst Nat 'Z
forall a (n :: Nat). a -> Konst a n
Konst Nat
Z) ((Nat -> Nat) -> Konst Nat m -> Konst Nat ('S m)
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 = Konst Natural n -> Natural
forall a (n :: Nat). Konst a n -> a
unKonst (Konst Natural 'Z
-> (forall (m :: Nat).
SNatI m =>
Konst Natural m -> Konst Natural ('S m))
-> Konst Natural n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (Natural -> Konst Natural 'Z
forall a (n :: Nat). a -> Konst a n
Konst Natural
0) ((Natural -> Natural) -> Konst Natural m -> Konst Natural ('S m)
forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Konst a n -> Konst b m
kmap Natural -> Natural
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 = NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)
forall (n :: Nat).
NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)
getNatEq (NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m))
-> NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)
forall a b. (a -> b) -> a -> b
$ NatEq 'Z
-> (forall (m :: Nat). SNatI m => NatEq m -> NatEq ('S m))
-> NatEq n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction ((forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat 'Z m)) -> NatEq 'Z
forall (n :: Nat).
(forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)) -> NatEq n
NatEq Maybe ((:~:) @Nat 'Z m)
forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat 'Z m)
start) (\NatEq m
p -> (forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat ('S m) m))
-> NatEq ('S m)
forall (n :: Nat).
(forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)) -> NatEq n
NatEq (NatEq m -> Maybe ((:~:) @Nat ('S m) m)
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 (m :: Nat). SNatI m => Maybe ((:~:) @Nat 'Z m)
start = case SNat p
forall (n :: Nat). SNatI n => SNat n
snat :: SNat p of
SNat p
SZ -> (:~:) @Nat 'Z p -> Maybe ((:~:) @Nat 'Z p)
forall a. a -> Maybe a
Just (:~:) @Nat 'Z p
(:~:) @Nat 'Z 'Z
forall {k} (a :: k). (:~:) @k a a
Refl
SNat p
SS -> Maybe ((:~:) @Nat 'Z p)
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 SNat q
forall (n :: Nat). SNatI n => SNat n
snat :: SNat q of
SNat q
SZ -> Maybe ((:~:) @Nat ('S p) q)
forall a. Maybe a
Nothing
SNat q
SS -> NatEq p -> Maybe ((:~:) @Nat ('S p) ('S n))
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 <- Maybe ((:~:) @Nat p q)
forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat p m)
hind :: Maybe (p :~: q)
(:~:) @Nat ('S p) ('S q) -> Maybe ((:~:) @Nat ('S p) ('S q))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (:~:) @Nat ('S p) ('S p)
(:~:) @Nat ('S p) ('S q)
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 = DiscreteNat n -> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m)
forall (n :: Nat).
DiscreteNat n -> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m)
getDiscreteNat (DiscreteNat n
-> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m))
-> DiscreteNat n
-> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m)
forall a b. (a -> b) -> a -> b
$ DiscreteNat 'Z
-> (forall (m :: Nat).
SNatI m =>
DiscreteNat m -> DiscreteNat ('S m))
-> DiscreteNat n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction ((forall (m :: Nat). SNatI m => Dec ((:~:) @Nat 'Z m))
-> DiscreteNat 'Z
forall (n :: Nat).
(forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m))
-> DiscreteNat n
DiscreteNat Dec ((:~:) @Nat 'Z m)
forall (m :: Nat). SNatI m => Dec ((:~:) @Nat 'Z m)
start) (\DiscreteNat m
p -> (forall (m :: Nat). SNatI m => Dec ((:~:) @Nat ('S m) m))
-> DiscreteNat ('S m)
forall (n :: Nat).
(forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m))
-> DiscreteNat n
DiscreteNat (DiscreteNat m -> Dec ((:~:) @Nat ('S m) m)
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 (m :: Nat). SNatI m => Dec ((:~:) @Nat 'Z m)
start = case SNat p
forall (n :: Nat). SNatI n => SNat n
snat :: SNat p of
SNat p
SZ -> (:~:) @Nat 'Z p -> Dec ((:~:) @Nat 'Z p)
forall a. a -> Dec a
Yes (:~:) @Nat 'Z p
(:~:) @Nat 'Z 'Z
forall {k} (a :: k). (:~:) @k a a
Refl
SNat p
SS -> Neg ((:~:) @Nat 'Z p) -> Dec ((:~:) @Nat 'Z p)
forall a. Neg a -> Dec a
No (Neg ((:~:) @Nat 'Z p) -> Dec ((:~:) @Nat 'Z p))
-> Neg ((:~:) @Nat 'Z p) -> Dec ((:~:) @Nat 'Z p)
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 SNat q
forall (n :: Nat). SNatI n => SNat n
snat :: SNat q of
SNat q
SZ -> Neg ((:~:) @Nat ('S p) q) -> Dec ((:~:) @Nat ('S p) q)
forall a. Neg a -> Dec a
No (Neg ((:~:) @Nat ('S p) q) -> Dec ((:~:) @Nat ('S p) q))
-> Neg ((:~:) @Nat ('S p) q) -> Dec ((:~:) @Nat ('S p) q)
forall a b. (a -> b) -> a -> b
$ \(:~:) @Nat ('S p) q
p -> case (:~:) @Nat ('S p) q
p of {}
SNat q
SS -> DiscreteNat p -> Dec ((:~:) @Nat ('S p) ('S n))
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 Dec ((:~:) @Nat p q)
forall (m :: Nat). SNatI m => Dec ((:~:) @Nat p m)
rec :: Dec (p :~: q) of
Yes (:~:) @Nat p q
Refl -> (:~:) @Nat ('S p) ('S q) -> Dec ((:~:) @Nat ('S p) ('S q))
forall a. a -> Dec a
Yes (:~:) @Nat ('S p) ('S p)
(:~:) @Nat ('S p) ('S q)
forall {k} (a :: k). (:~:) @k a a
Refl
No Neg ((:~:) @Nat p q)
np -> Neg ((:~:) @Nat ('S p) ('S q)) -> Dec ((:~:) @Nat ('S p) ('S q))
forall a. Neg a -> Dec a
No (Neg ((:~:) @Nat ('S p) ('S q)) -> Dec ((:~:) @Nat ('S p) ('S q)))
-> Neg ((:~:) @Nat ('S p) ('S q)) -> Dec ((:~:) @Nat ('S p) ('S q))
forall a b. (a -> b) -> a -> b
$ \(:~:) @Nat ('S p) ('S q)
Refl -> Neg ((:~:) @Nat p q)
np (:~:) @Nat p p
(:~:) @Nat p q
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 = (:~:) @Nat a b -> Maybe ((:~:) @Nat a b)
forall a. a -> Maybe a
Just (:~:) @Nat a a
(:~:) @Nat a b
forall {k} (a :: k). (:~:) @k a a
Refl
testEquality SNat a
SZ SNat b
SS = Maybe ((:~:) @Nat a b)
forall a. Maybe a
Nothing
testEquality SNat a
SS SNat b
SZ = Maybe ((:~:) @Nat a b)
forall a. Maybe a
Nothing
testEquality SNat a
SS SNat b
SS = Maybe ((:~:) @Nat a b)
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
instance SNatI n => Boring (SNat n) where
boring :: SNat n
boring = SNat n
forall (n :: Nat). SNatI n => SNat n
snat
instance GShow SNat where
gshowsPrec :: forall (p :: Nat). Int -> SNat p -> ShowS
gshowsPrec = Int -> SNat a -> ShowS
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 = SNat a -> ()
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 = SNat a -> SNat b -> Maybe ((:~:) @Nat a b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality @k f =>
f a -> f b -> Maybe ((:~:) @k a b)
forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> Maybe ((:~:) @Nat 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 = GOrdering @Nat a a
GOrdering @Nat a b
forall {k} (a :: k). GOrdering @k a a
GEQ
gcompare SNat a
SZ SNat b
SS = GOrdering @Nat a b
forall {k} (a :: k) (b :: k). GOrdering @k a b
GLT
gcompare SNat a
SS SNat b
SZ = GOrdering @Nat a b
forall {k} (a :: k) (b :: k). GOrdering @k a b
GGT
gcompare SNat a
SS SNat b
SS = GOrdering @Nat a b
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
instance EqP SNat where eqp :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Bool
eqp = SNat a -> SNat b -> Bool
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 = SNat a -> SNat b -> Ordering
forall {k} (f :: k -> *) (a :: k) (b :: k).
GCompare @k f =>
f a -> f b -> Ordering
defaultCompare
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 = NatCmp n -> forall (m :: Nat). SNatI m => GOrdering @Nat n m
forall (n :: Nat).
NatCmp n -> forall (m :: Nat). SNatI m => GOrdering @Nat n m
getNatCmp (NatCmp n -> forall (m :: Nat). SNatI m => GOrdering @Nat n m)
-> NatCmp n -> forall (m :: Nat). SNatI m => GOrdering @Nat n m
forall a b. (a -> b) -> a -> b
$ NatCmp 'Z
-> (forall (m :: Nat). SNatI m => NatCmp m -> NatCmp ('S m))
-> NatCmp n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction ((forall (m :: Nat). SNatI m => GOrdering @Nat 'Z m) -> NatCmp 'Z
forall (n :: Nat).
(forall (m :: Nat). SNatI m => GOrdering @Nat n m) -> NatCmp n
NatCmp GOrdering @Nat 'Z m
forall (m :: Nat). SNatI m => GOrdering @Nat 'Z m
start) (\NatCmp m
p -> (forall (m :: Nat). SNatI m => GOrdering @Nat ('S m) m)
-> NatCmp ('S m)
forall (n :: Nat).
(forall (m :: Nat). SNatI m => GOrdering @Nat n m) -> NatCmp n
NatCmp (NatCmp m -> GOrdering @Nat ('S m) m
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 (m :: Nat). SNatI m => GOrdering @Nat 'Z m
start = case SNat p
forall (n :: Nat). SNatI n => SNat n
snat :: SNat p of
SNat p
SZ -> GOrdering @Nat 'Z p
GOrdering @Nat 'Z 'Z
forall {k} (a :: k). GOrdering @k a a
GEQ
SNat p
SS -> GOrdering @Nat 'Z p
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 SNat q
forall (n :: Nat). SNatI n => SNat n
snat :: SNat q of
SNat q
SZ -> GOrdering @Nat ('S p) q
forall {k} (a :: k) (b :: k). GOrdering @k a b
GGT
SNat q
SS -> NatCmp p -> GOrdering @Nat ('S p) ('S n)
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 GOrdering @Nat p q
forall (m :: Nat). SNatI m => GOrdering @Nat p m
hind :: GOrdering p q of
GOrdering @Nat p q
GEQ -> GOrdering @Nat ('S p) ('S p)
GOrdering @Nat ('S p) ('S q)
forall {k} (a :: k). GOrdering @k a a
GEQ
GOrdering @Nat p q
GLT -> GOrdering @Nat ('S p) ('S q)
forall {k} (a :: k) (b :: k). GOrdering @k a b
GLT
GOrdering @Nat p q
GGT -> GOrdering @Nat ('S p) ('S q)
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 = (a -> b) -> Konst a n -> Konst b m
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 = Flipped f a n -> f n a
forall (f :: Nat -> * -> *) a (b :: Nat). Flipped f a b -> f b a
unflip (Flipped f a 'Z
-> (forall (m :: Nat).
SNatI m =>
Flipped f a m -> Flipped f a ('S m))
-> Flipped f a n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (f 'Z a -> Flipped f a 'Z
forall (f :: Nat -> * -> *) a (b :: Nat). f b a -> Flipped f a b
Flip f 'Z a
z) (\(Flip f m a
x) -> f ('S m) a -> Flipped f a ('S m)
forall (f :: Nat -> * -> *) a (b :: Nat). f b a -> Flipped f a b
Flip (f m a -> f ('S m) a
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
_ = Fix a n -> (a -> a) -> a
forall a (n :: Nat). Fix a n -> (a -> a) -> a
getFix (Fix a 'Z
-> (forall (m :: Nat). SNatI m => Fix a m -> Fix a ('S m))
-> Fix a n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction Fix a 'Z
start Fix a m -> Fix a ('S m)
forall (m :: Nat). Fix a m -> Fix a ('S m)
forall (m :: Nat). SNatI m => Fix a m -> Fix a ('S m)
step :: Fix a n) where
start :: Fix a 'Z
start :: Fix a 'Z
start = ((a -> a) -> a) -> Fix a 'Z
forall a (n :: Nat). ((a -> a) -> a) -> Fix a n
Fix (a -> a) -> a
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) = ((a -> a) -> a) -> Fix a ('S m)
forall a (n :: Nat). ((a -> a) -> a) -> Fix a n
Fix (((a -> a) -> a) -> Fix a ('S m))
-> ((a -> a) -> a) -> Fix a ('S m)
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 = (:~:) @Nat n n
(:~:) @Nat (Plus 'Z n) n
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 = ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n
forall (n :: Nat). ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n
getProofPlusNZero (ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n)
-> ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n
forall a b. (a -> b) -> a -> b
$ ProofPlusNZero 'Z
-> (forall (m :: Nat).
SNatI m =>
ProofPlusNZero m -> ProofPlusNZero ('S m))
-> ProofPlusNZero n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction ((:~:) @Nat (Plus 'Z 'Z) 'Z -> ProofPlusNZero 'Z
forall (n :: Nat). (:~:) @Nat (Plus n 'Z) n -> ProofPlusNZero n
ProofPlusNZero (:~:) @Nat 'Z 'Z
(:~:) @Nat (Plus 'Z 'Z) 'Z
forall {k} (a :: k). (:~:) @k a a
Refl) ProofPlusNZero m -> ProofPlusNZero ('S m)
forall (m :: Nat). ProofPlusNZero m -> ProofPlusNZero ('S m)
forall (m :: Nat).
SNatI m =>
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) = (:~:) @Nat (Plus ('S m) 'Z) ('S m) -> ProofPlusNZero ('S m)
forall (n :: Nat). (:~:) @Nat (Plus n 'Z) n -> ProofPlusNZero n
ProofPlusNZero (:~:) @Nat ('S m) ('S m)
(:~:) @Nat (Plus ('S m) 'Z) ('S m)
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 = (:~:) @Nat 'Z 'Z
(:~:) @Nat (Mult 'Z n) 'Z
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
_ =
ProofMultNZero n -> (:~:) @Nat (Mult n 'Z) 'Z
forall (n :: Nat). ProofMultNZero n -> (:~:) @Nat (Mult n 'Z) 'Z
getProofMultNZero (ProofMultNZero 'Z
-> (forall (m :: Nat).
SNatI m =>
ProofMultNZero m -> ProofMultNZero ('S m))
-> ProofMultNZero n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction ((:~:) @Nat (Mult 'Z 'Z) 'Z -> ProofMultNZero 'Z
forall (n :: Nat). (:~:) @Nat (Mult n 'Z) 'Z -> ProofMultNZero n
ProofMultNZero (:~:) @Nat 'Z 'Z
(:~:) @Nat (Mult 'Z 'Z) 'Z
forall {k} (a :: k). (:~:) @k a a
Refl) ProofMultNZero m -> ProofMultNZero ('S m)
forall (m :: Nat). ProofMultNZero m -> ProofMultNZero ('S m)
forall (m :: Nat).
SNatI m =>
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) = (:~:) @Nat (Mult ('S m) 'Z) 'Z -> ProofMultNZero ('S m)
forall (n :: Nat). (:~:) @Nat (Mult n 'Z) 'Z -> ProofMultNZero n
ProofMultNZero (:~:) @Nat 'Z 'Z
(:~:) @Nat (Mult ('S m) 'Z) 'Z
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 = (:~:) @Nat (Mult Nat1 n) n
(:~:) @Nat (Plus n 'Z) n
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 = ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n
forall (n :: Nat). ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n
getProofMultNOne (ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n)
-> ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n
forall a b. (a -> b) -> a -> b
$ ProofMultNOne 'Z
-> (forall (m :: Nat).
SNatI m =>
ProofMultNOne m -> ProofMultNOne ('S m))
-> ProofMultNOne n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction ((:~:) @Nat (Mult 'Z Nat1) 'Z -> ProofMultNOne 'Z
forall (n :: Nat). (:~:) @Nat (Mult n Nat1) n -> ProofMultNOne n
ProofMultNOne (:~:) @Nat 'Z 'Z
(:~:) @Nat (Mult 'Z Nat1) 'Z
forall {k} (a :: k). (:~:) @k a a
Refl) ProofMultNOne m -> ProofMultNOne ('S m)
forall (m :: Nat). ProofMultNOne m -> ProofMultNOne ('S m)
forall (m :: Nat).
SNatI m =>
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) = (:~:) @Nat (Mult ('S m) Nat1) ('S m) -> ProofMultNOne ('S m)
forall (n :: Nat). (:~:) @Nat (Mult n Nat1) n -> ProofMultNOne n
ProofMultNOne (:~:) @Nat ('S m) ('S m)
(:~:) @Nat (Mult ('S m) Nat1) ('S m)
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 }