module Data.Type.Witness.Specific.Natural
    ( KnownNat
    , type (<=)
    , type (+)
    , type (*)
    , type (^)
    , type (-)
    , CmpNat
    , Div
    , Mod
    , Log2
    , Nat
    , NaturalType(..)
    , zeroNaturalType
    , succNaturalType
    , addNaturalType
    , multiplyNaturalType
    , PeanoToNatural
    , peanoToNaturalType
    ) where

import Data.PeanoNat
import Data.Type.Witness.General.AllConstraint
import Data.Type.Witness.General.Order
import Data.Type.Witness.General.Representative
import Data.Type.Witness.General.WitnessValue
import Data.Type.Witness.Specific.PeanoNat
import GHC.TypeNats
import Import
import Unsafe.Coerce

type NaturalType :: Nat -> Type
type role NaturalType nominal
data NaturalType bn where
    MkNaturalType :: KnownNat bn => NaturalType bn

instance WitnessValue NaturalType where
    type WitnessValueType NaturalType = Natural
    witnessToValue :: forall t. NaturalType t -> Natural
    witnessToValue :: forall (t :: Nat). NaturalType t -> Nat
witnessToValue NaturalType t
MkNaturalType = Proxy t -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t)
    valueToWitness :: forall r.
WitnessValueType NaturalType
-> (forall (t :: Nat). NaturalType t -> r) -> r
valueToWitness WitnessValueType NaturalType
i forall (t :: Nat). NaturalType t -> r
cont =
        case Nat -> SomeNat
someNatVal Nat
WitnessValueType NaturalType
i of
            SomeNat Proxy n
p -> let
                psw :: forall (t :: Nat). KnownNat t
                    => Proxy t
                    -> NaturalType t
                psw :: forall (t :: Nat). KnownNat t => Proxy t -> NaturalType t
psw Proxy t
_ = NaturalType t
forall (bn :: Nat). KnownNat bn => NaturalType bn
MkNaturalType
                in NaturalType n -> r
forall (t :: Nat). NaturalType t -> r
cont (NaturalType n -> r) -> NaturalType n -> r
forall a b. (a -> b) -> a -> b
$ Proxy n -> NaturalType n
forall (t :: Nat). KnownNat t => Proxy t -> NaturalType t
psw Proxy n
p

instance TestEquality NaturalType where
    testEquality :: forall (a :: Nat) (b :: Nat).
NaturalType a -> NaturalType b -> Maybe (a :~: b)
testEquality (NaturalType a
MkNaturalType :: NaturalType a) (NaturalType b
MkNaturalType :: NaturalType b) = Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @a) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)

instance TestOrder NaturalType where
    testCompare :: forall (a :: Nat) (b :: Nat).
NaturalType a -> NaturalType b -> WOrdering a b
testCompare NaturalType a
a NaturalType b
b =
        case NaturalType a -> NaturalType b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat).
NaturalType a -> NaturalType b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NaturalType a
a NaturalType b
b of
            Just a :~: b
Refl -> WOrdering a a
WOrdering a b
forall k (a :: k). WOrdering a a
WEQ
            Maybe (a :~: b)
Nothing ->
                if NaturalType a -> WitnessValueType NaturalType
forall (t :: Nat). NaturalType t -> WitnessValueType NaturalType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue NaturalType a
a Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> NaturalType b -> WitnessValueType NaturalType
forall (t :: Nat). NaturalType t -> WitnessValueType NaturalType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue NaturalType b
b
                    then WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WGT
                    else WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WLT

instance Representative NaturalType where
    getRepWitness :: Subrepresentative NaturalType NaturalType
getRepWitness NaturalType a
MkNaturalType = Dict (Is NaturalType a)
forall (a :: Constraint). a => Dict a
Dict

instance KnownNat bn => Is NaturalType bn where
    representative :: NaturalType bn
representative = NaturalType bn
forall (bn :: Nat). KnownNat bn => NaturalType bn
MkNaturalType

instance Show (NaturalType bn) where
    show :: NaturalType bn -> String
show = Nat -> String
forall a. Show a => a -> String
show (Nat -> String)
-> (NaturalType bn -> Nat) -> NaturalType bn -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. NaturalType bn -> Nat
NaturalType bn -> WitnessValueType NaturalType
forall (t :: Nat). NaturalType t -> WitnessValueType NaturalType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue

instance AllConstraint Show NaturalType where
    allConstraint :: forall (t :: Nat). Dict (Show (NaturalType t))
allConstraint = Dict (Show (NaturalType t))
forall (a :: Constraint). a => Dict a
Dict

unsafeNaturalType :: forall n. Natural -> NaturalType n
unsafeNaturalType :: forall (n :: Nat). Nat -> NaturalType n
unsafeNaturalType Nat
i = WitnessValueType NaturalType
-> (forall {t :: Nat}. NaturalType t -> NaturalType n)
-> NaturalType n
forall r.
WitnessValueType NaturalType
-> (forall (t :: Nat). NaturalType t -> r) -> r
forall k (w :: k -> Type) r.
WitnessValue w =>
WitnessValueType w -> (forall (t :: k). w t -> r) -> r
valueToWitness Nat
WitnessValueType NaturalType
i ((forall {t :: Nat}. NaturalType t -> NaturalType n)
 -> NaturalType n)
-> (forall {t :: Nat}. NaturalType t -> NaturalType n)
-> NaturalType n
forall a b. (a -> b) -> a -> b
$ \(NaturalType t
nt :: NaturalType t) -> forall a b. a -> b
unsafeCoerce @(NaturalType t) @(NaturalType n) NaturalType t
nt

zeroNaturalType :: NaturalType 0
zeroNaturalType :: NaturalType 0
zeroNaturalType = NaturalType 0
forall (bn :: Nat). KnownNat bn => NaturalType bn
MkNaturalType

succNaturalType :: NaturalType a -> NaturalType (a + 1)
succNaturalType :: forall (a :: Nat). NaturalType a -> NaturalType (a + 1)
succNaturalType NaturalType a
a = Nat -> NaturalType (a + 1)
forall (n :: Nat). Nat -> NaturalType n
unsafeNaturalType (Nat -> NaturalType (a + 1)) -> Nat -> NaturalType (a + 1)
forall a b. (a -> b) -> a -> b
$ Nat -> Nat
forall a. Enum a => a -> a
succ (Nat -> Nat) -> Nat -> Nat
forall a b. (a -> b) -> a -> b
$ NaturalType a -> WitnessValueType NaturalType
forall (t :: Nat). NaturalType t -> WitnessValueType NaturalType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue NaturalType a
a

addNaturalType :: NaturalType a -> NaturalType b -> NaturalType (a + b)
addNaturalType :: forall (a :: Nat) (b :: Nat).
NaturalType a -> NaturalType b -> NaturalType (a + b)
addNaturalType NaturalType a
a NaturalType b
b = Nat -> NaturalType (a + b)
forall (n :: Nat). Nat -> NaturalType n
unsafeNaturalType (Nat -> NaturalType (a + b)) -> Nat -> NaturalType (a + b)
forall a b. (a -> b) -> a -> b
$ NaturalType a -> WitnessValueType NaturalType
forall (t :: Nat). NaturalType t -> WitnessValueType NaturalType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue NaturalType a
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ NaturalType b -> WitnessValueType NaturalType
forall (t :: Nat). NaturalType t -> WitnessValueType NaturalType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue NaturalType b
b

multiplyNaturalType :: NaturalType a -> NaturalType b -> NaturalType (a * b)
multiplyNaturalType :: forall (a :: Nat) (b :: Nat).
NaturalType a -> NaturalType b -> NaturalType (a * b)
multiplyNaturalType NaturalType a
a NaturalType b
b = Nat -> NaturalType (a * b)
forall (n :: Nat). Nat -> NaturalType n
unsafeNaturalType (Nat -> NaturalType (a * b)) -> Nat -> NaturalType (a * b)
forall a b. (a -> b) -> a -> b
$ NaturalType a -> WitnessValueType NaturalType
forall (t :: Nat). NaturalType t -> WitnessValueType NaturalType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue NaturalType a
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* NaturalType b -> WitnessValueType NaturalType
forall (t :: Nat). NaturalType t -> WitnessValueType NaturalType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue NaturalType b
b

peanoToNaturalType :: PeanoNatType pn -> NaturalType (PeanoToNatural pn)
peanoToNaturalType :: forall (pn :: PeanoNat).
PeanoNatType pn -> NaturalType (PeanoToNatural pn)
peanoToNaturalType PeanoNatType pn
ZeroType = NaturalType 0
NaturalType (PeanoToNatural pn)
zeroNaturalType
peanoToNaturalType (SuccType PeanoNatType t1
n) = NaturalType (PeanoToNatural t1)
-> NaturalType (PeanoToNatural t1 + 1)
forall (a :: Nat). NaturalType a -> NaturalType (a + 1)
succNaturalType (NaturalType (PeanoToNatural t1)
 -> NaturalType (PeanoToNatural t1 + 1))
-> NaturalType (PeanoToNatural t1)
-> NaturalType (PeanoToNatural t1 + 1)
forall a b. (a -> b) -> a -> b
$ PeanoNatType t1 -> NaturalType (PeanoToNatural t1)
forall (pn :: PeanoNat).
PeanoNatType pn -> NaturalType (PeanoToNatural pn)
peanoToNaturalType PeanoNatType t1
n