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 Numeric.Natural
import Unsafe.Coerce

type NaturalType :: Nat -> Type
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 = forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal (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 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
_ = forall (bn :: Nat). KnownNat bn => NaturalType bn
MkNaturalType
                in forall (t :: Nat). NaturalType t -> r
cont forall a b. (a -> b) -> a -> b
$ 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) = forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @a) (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 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 -> forall k (a :: k). WOrdering a a
WEQ
            Maybe (a :~: b)
Nothing ->
                if forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue NaturalType a
a forall a. Ord a => a -> a -> Bool
> forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue NaturalType b
b
                    then forall k (a :: k) (b :: k). WOrdering a b
WGT
                    else forall k (a :: k) (b :: k). WOrdering a b
WLT

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

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

instance Show (NaturalType bn) where
    show :: NaturalType bn -> String
show = forall a. Show a => a -> String
show forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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 = forall (a :: Constraint). a => Dict a
Dict

unsafeNaturalType :: forall n. Natural -> NaturalType n
unsafeNaturalType :: forall (n :: Nat). Nat -> NaturalType n
unsafeNaturalType Nat
i = forall k (w :: k -> Type) r.
WitnessValue w =>
WitnessValueType w -> (forall (t :: k). w t -> r) -> r
valueToWitness Nat
i 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 = 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 = forall (n :: Nat). Nat -> NaturalType n
unsafeNaturalType forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a
succ forall a b. (a -> b) -> a -> b
$ 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 = forall (n :: Nat). Nat -> NaturalType n
unsafeNaturalType forall a b. (a -> b) -> a -> b
$ forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue NaturalType a
a forall a. Num a => a -> a -> a
+ 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 = forall (n :: Nat). Nat -> NaturalType n
unsafeNaturalType forall a b. (a -> b) -> a -> b
$ forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue NaturalType a
a forall a. Num a => a -> a -> a
* 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
zeroNaturalType
peanoToNaturalType (SuccType PeanoNatType t1
n) = forall (a :: Nat). NaturalType a -> NaturalType (a + 1)
succNaturalType forall a b. (a -> b) -> a -> b
$ forall (pn :: PeanoNat).
PeanoNatType pn -> NaturalType (PeanoToNatural pn)
peanoToNaturalType PeanoNatType t1
n