{-# 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 #-}
-- | 'Nat' numbers. @DataKinds@ stuff.
--
-- This module re-exports "Data.Nat", and adds type-level things.
module Data.Type.Nat (
    -- * Natural, Nat numbers
    Nat(..),
    toNatural,
    fromNatural,
    cata,
    -- * Showing
    explicitShow,
    explicitShowsPrec,
    -- * Singleton
    SNat(..),
    snatToNat,
    snatToNatural,
    -- * Implicit
    SNatI(..),
    snat,
    withSNat,
    reify,
    reflect,
    reflectToNum,
    -- * Equality
    eqNat,
    EqNat,
    discreteNat,
    cmpNat,
    -- * Induction
    induction1,
    -- ** Example: unfoldedFix
    unfoldedFix,
    -- * Arithmetic
    Plus,
    Mult,
    Mult2,
    DivMod2,
    -- * Conversion to GHC Nat
    ToGHC,
    FromGHC,
    -- * Aliases
    -- ** Nat
    nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9,
    -- ** promoted Nat
    Nat0, Nat1, Nat2, Nat3, Nat4, Nat5, Nat6, Nat7, Nat8, Nat9,
    -- * Proofs
    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)

import qualified GHC.TypeLits as GHC

import Unsafe.Coerce (unsafeCoerce)

import Data.Nat
import TrustworthyCompat

-- $setup
-- >>> :set -XTypeOperators -XDataKinds
-- >>> import qualified GHC.TypeLits as GHC
-- >>> import Data.Type.Dec (Dec (..), decShow)
-- >>> import Data.Type.Equality
-- >>> import Control.Applicative (Const (..))
-- >>> import Data.Coerce (coerce)
-- >>> import Data.GADT.Compare (GOrdering (..))

-------------------------------------------------------------------------------
-- SNat
-------------------------------------------------------------------------------

-- | Singleton of 'Nat'.
data SNat (n :: Nat) where
    SZ :: SNat 'Z
    SS :: SNatI n => SNat ('S n)
  deriving (Typeable)

deriving instance Show (SNat p)

-- | Implicit 'SNat'.
--
-- In an unorthodox singleton way, it actually provides an induction function.
--
-- The induction should often be fully inlined.
-- See @test/Inspection.hs@.
--
-- >>> :set -XPolyKinds
-- >>> newtype Const a b = Const a deriving (Show)
-- >>> induction (Const 0) (coerce ((+2) :: Int -> Int)) :: Const Int Nat3
-- Const 6
--
class SNatI (n :: Nat) where
    induction
        :: f 'Z                                    -- ^ zero case
        -> (forall m. SNatI m => f m -> f ('S m))  -- ^ induction step
        -> f n

instance SNatI 'Z where
    induction :: 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 :: 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
induction f 'Z
n forall (m :: Nat). SNatI m => f m -> f ('S m)
c)

-- | Construct explicit 'SNat' value.
snat :: SNatI n => SNat n
snat :: 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
induction SNat 'Z
SZ (\SNat m
_ -> SNat ('S m)
forall (n :: Nat). SNatI n => SNat ('S n)
SS)

-- | Constructor 'SNatI' dictionary from 'SNat'.
--
-- @since 0.0.3
withSNat :: SNat n -> (SNatI n => r) -> r
withSNat :: 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 type-level 'Nat' to the term level.
reflect :: forall n proxy. SNatI n => proxy n -> Nat
reflect :: 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
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)

-- | As 'reflect' but with any 'Num'.
reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m
reflectToNum :: 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
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 'Nat'.
--
-- >>> reify nat3 reflect
-- 3
reify :: forall r. Nat -> (forall n. SNatI n => Proxy n -> r) -> r
reify :: 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)))

-- | Convert 'SNat' to 'Nat'.
--
-- >>> snatToNat (snat :: SNat Nat1)
-- 1
--
snatToNat :: forall n. SNat n -> Nat
snatToNat :: 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
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)

-- | Convert 'SNat' to 'Natural'
--
-- >>> snatToNatural (snat :: SNat Nat0)
-- 0
--
-- >>> snatToNatural (snat :: SNat Nat2)
-- 2
--
snatToNatural :: forall n. SNat n -> Natural
snatToNatural :: 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
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)

-------------------------------------------------------------------------------
-- Equality
-------------------------------------------------------------------------------

-- | Decide equality of type-level numbers.
--
-- >>> eqNat :: Maybe (Nat3 :~: Plus Nat1 Nat2)
-- Just Refl
--
-- >>> eqNat :: Maybe (Nat3 :~: Mult Nat2 Nat2)
-- Nothing
--
eqNat :: forall n m. (SNatI n, SNatI m) => Maybe (n :~: m)
eqNat :: 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
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 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 :: Maybe ((:~:) @Nat 'Z p)
start = case SNat p
forall (n :: Nat). SNatI n => SNat n
snat :: SNat p of
        SNat p
SZ -> (:~:) @Nat 'Z 'Z -> Maybe ((:~:) @Nat 'Z 'Z)
forall a. a -> Maybe a
Just (:~:) @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 :: 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' :: 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 p) -> Maybe ((:~:) @Nat ('S p) ('S p))
forall (m :: * -> *) a. Monad m => a -> m a
return (:~:) @Nat ('S p) ('S p)
forall k (a :: k). (:~:) @k a a
Refl

newtype NatEq n = NatEq { NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)
getNatEq :: forall m. SNatI m => Maybe (n :~: m) }

-- | Decide equality of type-level numbers.
--
-- >>> decShow (discreteNat :: Dec (Nat3 :~: Plus Nat1 Nat2))
-- "Yes Refl"
--
-- @since 0.0.3
discreteNat :: forall n m. (SNatI n, SNatI m) => Dec (n :~: m)
discreteNat :: 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
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 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 :: Dec ((:~:) @Nat 'Z p)
start = case SNat p
forall (n :: Nat). SNatI n => SNat n
snat :: SNat p of
        SNat p
SZ -> (:~:) @Nat 'Z 'Z -> Dec ((:~:) @Nat 'Z 'Z)
forall a. a -> Dec a
Yes (:~:) @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 :: 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' :: 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 p) -> Dec ((:~:) @Nat ('S p) ('S p))
forall a. a -> Dec a
Yes (:~:) @Nat ('S p) ('S p)
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 q
forall k (a :: k). (:~:) @k a a
Refl

newtype DiscreteNat n = DiscreteNat { DiscreteNat n -> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m)
getDiscreteNat :: forall m. SNatI m => Dec (n :~: m) }

instance TestEquality SNat where
    testEquality :: SNat a -> SNat b -> Maybe ((:~:) @Nat a b)
testEquality SNat a
SZ SNat b
SZ = (:~:) @Nat a a -> Maybe ((:~:) @Nat a a)
forall a. a -> Maybe a
Just (:~:) @Nat a a
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 used to implement 'Data.Type.Equality.==' from "Data.Type.Equality" module.
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

-- | @since 0.2.1
instance SNatI n => Boring (SNat n) where
    boring :: SNat n
boring = SNat n
forall (n :: Nat). SNatI n => SNat n
snat

-- | @since 0.2.1
instance GShow SNat where
    gshowsPrec :: Int -> SNat a -> ShowS
gshowsPrec = Int -> SNat a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

-- | @since 0.2.1
instance NFData (SNat n) where
    rnf :: SNat n -> ()
rnf SNat n
SZ = ()
    rnf SNat n
SS = ()

-- | @since 0.2.1
instance GNFData SNat where
    grnf :: SNat a -> ()
grnf = SNat a -> ()
forall a. NFData a => a -> ()
rnf

-- | @since 0.2.1
instance GEq SNat where
    geq :: 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)
testEquality

-- | @since 0.2.1
instance GCompare SNat where
    gcompare :: SNat a -> SNat b -> GOrdering @Nat a b
gcompare SNat a
SZ SNat b
SZ = 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

-- | Decide equality of type-level numbers.
--
-- >>> cmpNat :: GOrdering Nat3 (Plus Nat1 Nat2)
-- GEQ
--
-- >>> cmpNat :: GOrdering Nat3 (Mult Nat2 Nat2)
-- GLT
--
-- >>> cmpNat :: GOrdering Nat5 (Mult Nat2 Nat2)
-- GGT
--
cmpNat :: forall n m. (SNatI n, SNatI m) => GOrdering n m
cmpNat :: 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
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 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 :: GOrdering @Nat 'Z p
start = case SNat p
forall (n :: Nat). SNatI n => SNat n
snat :: SNat p of
        SNat p
SZ -> GOrdering @Nat 'Z p
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 :: 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' :: 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 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 { NatCmp n -> forall (m :: Nat). SNatI m => GOrdering @Nat n m
getNatCmp :: forall m. SNatI m => GOrdering n m }

-------------------------------------------------------------------------------
-- Induction
-------------------------------------------------------------------------------

newtype Konst a (n :: Nat) = Konst { Konst a n -> a
unKonst :: a }

kmap :: (a -> b) -> Konst a n -> Konst b m
kmap :: (a -> b) -> Konst a n -> Konst b m
kmap = (a -> b) -> Konst a n -> Konst b m
coerce

newtype Flipped f a (b :: Nat) = Flip { Flipped f a b -> f b a
unflip :: f b a }

-- | Induction on 'Nat', functor form. Useful for computation.
--
induction1
    :: forall n f a. SNatI n
    => f 'Z a                                      -- ^ zero case
    -> (forall m. SNatI m => f m a -> f ('S m) a)  -- ^ induction step
    -> f n a
induction1 :: 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
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 #-}

-- | Unfold @n@ steps of a general recursion.
--
-- /Note:/ Always __benchmark__. This function may give you both /bad/ properties:
-- a lot of code (increased binary size), and worse performance.
--
-- For known @n@ 'unfoldedFix' will unfold recursion, for example
--
-- @
-- 'unfoldedFix' ('Proxy' :: 'Proxy' 'Nat3') f = f (f (f (fix f)))
-- @
--
unfoldedFix :: forall n a proxy. SNatI n => proxy n -> (a -> a) -> a
unfoldedFix :: 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
induction Fix a 'Z
start 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 :: 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 { Fix a n -> (a -> a) -> a
getFix :: (a -> a) -> a }

-------------------------------------------------------------------------------
-- Conversion to GHC Nat
-------------------------------------------------------------------------------

-- | Convert to GHC 'GHC.Nat'.
--
-- >>> :kind! ToGHC Nat5
-- ToGHC Nat5 :: GHC.Nat...
-- = 5
--
type family ToGHC (n :: Nat) :: GHC.Nat where
    ToGHC 'Z     = 0
    ToGHC ('S n) = 1 GHC.+ ToGHC n

-- | Convert from GHC 'GHC.Nat'.
--
-- >>> :kind! FromGHC 7
-- FromGHC 7 :: Nat
-- = 'S ('S ('S ('S ('S ('S ('S 'Z))))))
--
type family FromGHC (n :: GHC.Nat) :: Nat where
    FromGHC 0 = 'Z
    FromGHC n = 'S (FromGHC (n GHC.- 1))

-------------------------------------------------------------------------------
-- Arithmetic
-------------------------------------------------------------------------------

-- | Addition.
--
-- >>> reflect (snat :: SNat (Plus Nat1 Nat2))
-- 3
type family Plus (n :: Nat) (m :: Nat) :: Nat where
    Plus 'Z     m = m
    Plus ('S n) m = 'S (Plus n m)

-- | Multiplication.
--
-- >>> reflect (snat :: SNat (Mult Nat2 Nat3))
-- 6
type family Mult (n :: Nat) (m :: Nat) :: Nat where
    Mult 'Z     m = 'Z
    Mult ('S n) m = Plus m (Mult n m)

-- | Multiplication by two. Doubling.
--
-- >>> reflect (snat :: SNat (Mult2 Nat4))
-- 8
--
type family Mult2 (n :: Nat) :: Nat where
    Mult2 'Z     = 'Z
    Mult2 ('S n) = 'S ('S (Mult2 n))

-- | Division by two. 'False' is 0 and 'True' is 1 as a remainder.
--
-- >>> :kind! DivMod2 Nat7 == '(Nat3, True)
-- DivMod2 Nat7 == '(Nat3, True) :: Bool
-- = 'True
--
-- >>> :kind! DivMod2 Nat4 == '(Nat2, False)
-- DivMod2 Nat4 == '(Nat2, False) :: Bool
-- = 'True
--
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)

-------------------------------------------------------------------------------
-- Aliases
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- proofs
-------------------------------------------------------------------------------

-- | @0 + n = n@
proofPlusZeroN :: Plus Nat0 n :~: n
proofPlusZeroN :: (:~:) @Nat (Plus 'Z n) n
proofPlusZeroN = (:~:) @Nat (Plus 'Z n) n
forall k (a :: k). (:~:) @k a a
Refl

-- | @n + 0 = n@
proofPlusNZero :: SNatI n => Plus n Nat0 :~: n
proofPlusNZero :: (:~:) @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
induction ((:~:) @Nat (Plus 'Z 'Z) 'Z -> ProofPlusNZero 'Z
forall (n :: Nat). (:~:) @Nat (Plus n 'Z) n -> ProofPlusNZero n
ProofPlusNZero (:~:) @Nat (Plus 'Z 'Z) 'Z
forall k (a :: k). (:~:) @k a a
Refl) 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 :: 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 (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 { ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n
getProofPlusNZero :: Plus n Nat0 :~: n }

-- TODO: plusAssoc

-- | @0 * n = 0@
proofMultZeroN :: Mult Nat0 n :~: Nat0
proofMultZeroN :: (:~:) @Nat (Mult 'Z n) 'Z
proofMultZeroN = (:~:) @Nat (Mult 'Z n) 'Z
forall k (a :: k). (:~:) @k a a
Refl

-- | @n * 0 = 0@
proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0
proofMultNZero :: 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
induction ((:~:) @Nat (Mult 'Z 'Z) 'Z -> ProofMultNZero 'Z
forall (n :: Nat). (:~:) @Nat (Mult n 'Z) 'Z -> ProofMultNZero n
ProofMultNZero (:~:) @Nat (Mult 'Z 'Z) 'Z
forall k (a :: k). (:~:) @k a a
Refl) 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 :: 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 (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 { ProofMultNZero n -> (:~:) @Nat (Mult n 'Z) 'Z
getProofMultNZero :: Mult n Nat0 :~: Nat0 }

-- | @1 * n = n@
proofMultOneN :: SNatI n => Mult Nat1 n :~: n
proofMultOneN :: (:~:) @Nat (Mult Nat1 n) n
proofMultOneN = (:~:) @Nat (Mult Nat1 n) n
forall (n :: Nat). SNatI n => (:~:) @Nat (Plus n 'Z) n
proofPlusNZero

{-# NOINLINE [1] proofMultOneN #-}
{-# RULES "Nat: 1 * n = n" proofMultOneN = unsafeCoerce (Refl :: () :~: ()) #-}

-- | @n * 1 = n@
proofMultNOne :: SNatI n => Mult n Nat1 :~: n
proofMultNOne :: (:~:) @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
induction ((:~:) @Nat (Mult 'Z Nat1) 'Z -> ProofMultNOne 'Z
forall (n :: Nat). (:~:) @Nat (Mult n Nat1) n -> ProofMultNOne n
ProofMultNOne (:~:) @Nat (Mult 'Z Nat1) 'Z
forall k (a :: k). (:~:) @k a a
Refl) 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 :: 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 (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 { ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n
getProofMultNOne :: Mult n Nat1 :~: n }

-- TODO: multAssoc