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