module Data.Type.Witness.Specific.PeanoNat where

import Data.PeanoNat
import Data.Type.Witness.General.Order
import Data.Type.Witness.General.Representative
import Data.Type.Witness.General.WitnessValue
import Import

type PeanoNatType :: PeanoNat -> Type
data PeanoNatType t where
    ZeroType :: PeanoNatType 'Zero
    SuccType :: PeanoNatType t -> PeanoNatType ('Succ t)

instance TestEquality PeanoNatType where
    testEquality :: forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> Maybe (a :~: b)
testEquality PeanoNatType a
ZeroType PeanoNatType b
ZeroType = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
    testEquality (SuccType PeanoNatType t
a) (SuccType PeanoNatType t
b) = do
        t :~: t
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality PeanoNatType t
a PeanoNatType t
b
        forall (m :: Type -> Type) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
    testEquality PeanoNatType a
_ PeanoNatType b
_ = forall a. Maybe a
Nothing

instance TestOrder PeanoNatType where
    testCompare :: forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> WOrdering a b
testCompare PeanoNatType a
ZeroType PeanoNatType b
ZeroType = forall k (a :: k). WOrdering a a
WEQ
    testCompare (SuccType PeanoNatType t
a) (SuccType PeanoNatType t
b) =
        case forall k (w :: k -> Type) (a :: k) (b :: k).
TestOrder w =>
w a -> w b -> WOrdering a b
testCompare PeanoNatType t
a PeanoNatType t
b of
            WOrdering t t
WLT -> forall k (a :: k) (b :: k). WOrdering a b
WLT
            WOrdering t t
WGT -> forall k (a :: k) (b :: k). WOrdering a b
WGT
            WOrdering t t
WEQ -> forall k (a :: k). WOrdering a a
WEQ
    testCompare (SuccType PeanoNatType t
_) PeanoNatType b
ZeroType = forall k (a :: k) (b :: k). WOrdering a b
WGT
    testCompare PeanoNatType a
ZeroType (SuccType PeanoNatType t
_) = forall k (a :: k) (b :: k). WOrdering a b
WLT

instance Representative PeanoNatType where
    getRepWitness :: Subrepresentative PeanoNatType PeanoNatType
getRepWitness PeanoNatType a
ZeroType = forall (a :: Constraint). a => Dict a
Dict
    getRepWitness (SuccType PeanoNatType t
n) =
        case forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness PeanoNatType t
n of
            Dict (Is PeanoNatType t)
Dict -> forall (a :: Constraint). a => Dict a
Dict

instance Is PeanoNatType 'Zero where
    representative :: PeanoNatType 'Zero
representative = PeanoNatType 'Zero
ZeroType

instance Is PeanoNatType n => Is PeanoNatType ('Succ n) where
    representative :: PeanoNatType ('Succ n)
representative = forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a)
SuccType forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative

instance WitnessValue PeanoNatType where
    type WitnessValueType PeanoNatType = PeanoNat
    witnessToValue :: forall t. PeanoNatType t -> PeanoNat
    witnessToValue :: forall (t :: PeanoNat). PeanoNatType t -> PeanoNat
witnessToValue PeanoNatType t
ZeroType = PeanoNat
Zero
    witnessToValue (SuccType PeanoNatType t
n) = PeanoNat -> PeanoNat
Succ forall a b. (a -> b) -> a -> b
$ forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue PeanoNatType t
n
    valueToWitness :: forall r.
WitnessValueType PeanoNatType
-> (forall (t :: PeanoNat). PeanoNatType t -> r) -> r
valueToWitness WitnessValueType PeanoNatType
PeanoNat
Zero forall (t :: PeanoNat). PeanoNatType t -> r
cont = forall (t :: PeanoNat). PeanoNatType t -> r
cont PeanoNatType 'Zero
ZeroType
    valueToWitness (Succ PeanoNat
n) forall (t :: PeanoNat). PeanoNatType t -> r
cont = forall k (w :: k -> Type) r.
WitnessValue w =>
WitnessValueType w -> (forall (t :: k). w t -> r) -> r
valueToWitness PeanoNat
n forall a b. (a -> b) -> a -> b
$ \PeanoNatType t
t -> forall (t :: PeanoNat). PeanoNatType t -> r
cont forall a b. (a -> b) -> a -> b
$ forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a)
SuccType PeanoNatType t
t

type GreaterEqual :: PeanoNat -> PeanoNat -> Type
data GreaterEqual a b where
    ZeroGreaterEqual :: GreaterEqual a 'Zero
    SuccGreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)

greaterEqualIndex :: GreaterEqual a b -> PeanoNatType b
greaterEqualIndex :: forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> PeanoNatType b
greaterEqualIndex GreaterEqual a b
ZeroGreaterEqual = PeanoNatType 'Zero
ZeroType
greaterEqualIndex (SuccGreaterEqual GreaterEqual a b
n) = forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a)
SuccType forall a b. (a -> b) -> a -> b
$ forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> PeanoNatType b
greaterEqualIndex GreaterEqual a b
n

samePeanoGreaterEqual :: PeanoNatType a -> GreaterEqual a a
samePeanoGreaterEqual :: forall (a :: PeanoNat). PeanoNatType a -> GreaterEqual a a
samePeanoGreaterEqual PeanoNatType a
ZeroType = forall (a :: PeanoNat). GreaterEqual a 'Zero
ZeroGreaterEqual
samePeanoGreaterEqual (SuccType PeanoNatType t
a) = forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)
SuccGreaterEqual forall a b. (a -> b) -> a -> b
$ forall (a :: PeanoNat). PeanoNatType a -> GreaterEqual a a
samePeanoGreaterEqual PeanoNatType t
a

diff1GreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) b
diff1GreaterEqual :: forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> GreaterEqual ('Succ a) b
diff1GreaterEqual GreaterEqual a b
ZeroGreaterEqual = forall (a :: PeanoNat). GreaterEqual a 'Zero
ZeroGreaterEqual
diff1GreaterEqual (SuccGreaterEqual GreaterEqual a b
ge) = forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)
SuccGreaterEqual forall a b. (a -> b) -> a -> b
$ forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> GreaterEqual ('Succ a) b
diff1GreaterEqual GreaterEqual a b
ge

peanoGreaterEqual :: PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b)
peanoGreaterEqual :: forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b)
peanoGreaterEqual PeanoNatType a
_ PeanoNatType b
ZeroType = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall (a :: PeanoNat). GreaterEqual a 'Zero
ZeroGreaterEqual
peanoGreaterEqual PeanoNatType a
ZeroType PeanoNatType b
_ = forall a. Maybe a
Nothing
peanoGreaterEqual (SuccType PeanoNatType t
a) (SuccType PeanoNatType t
b) = do
    GreaterEqual t t
al <- forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b)
peanoGreaterEqual PeanoNatType t
a PeanoNatType t
b
    forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)
SuccGreaterEqual GreaterEqual t t
al

addPeanoNatType :: PeanoNatType a -> PeanoNatType b -> PeanoNatType (Add a b)
addPeanoNatType :: forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> PeanoNatType (Add a b)
addPeanoNatType PeanoNatType a
ZeroType PeanoNatType b
b = PeanoNatType b
b
addPeanoNatType (SuccType PeanoNatType t
a) PeanoNatType b
b = forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a)
SuccType forall a b. (a -> b) -> a -> b
$ forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> PeanoNatType (Add a b)
addPeanoNatType PeanoNatType t
a PeanoNatType b
b

addZeroPeanoNatTypeEqual :: PeanoNatType a -> Add a 'Zero :~: a
addZeroPeanoNatTypeEqual :: forall (a :: PeanoNat). PeanoNatType a -> Add a 'Zero :~: a
addZeroPeanoNatTypeEqual PeanoNatType a
ZeroType = forall {k} (a :: k). a :~: a
Refl
addZeroPeanoNatTypeEqual (SuccType PeanoNatType t
a) =
    case forall (a :: PeanoNat). PeanoNatType a -> Add a 'Zero :~: a
addZeroPeanoNatTypeEqual PeanoNatType t
a of
        Add t 'Zero :~: t
Refl -> forall {k} (a :: k). a :~: a
Refl

succAddPeanoNatTypeEqual' :: forall a b. PeanoNatType a -> 'Succ (Add a b) :~: Add a ('Succ b)
succAddPeanoNatTypeEqual' :: forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> 'Succ (Add a b) :~: Add a ('Succ b)
succAddPeanoNatTypeEqual' PeanoNatType a
ZeroType = forall {k} (a :: k). a :~: a
Refl
succAddPeanoNatTypeEqual' (SuccType PeanoNatType t
a) =
    case forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> 'Succ (Add a b) :~: Add a ('Succ b)
succAddPeanoNatTypeEqual' @_ @b PeanoNatType t
a of
        'Succ (Add t b) :~: Add t ('Succ b)
Refl -> forall {k} (a :: k). a :~: a
Refl

succAddPeanoNatTypeEqual :: forall a b. PeanoNatType a -> PeanoNatType b -> 'Succ (Add a b) :~: Add a ('Succ b)
succAddPeanoNatTypeEqual :: forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a
-> PeanoNatType b -> 'Succ (Add a b) :~: Add a ('Succ b)
succAddPeanoNatTypeEqual PeanoNatType a
a PeanoNatType b
_ = forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> 'Succ (Add a b) :~: Add a ('Succ b)
succAddPeanoNatTypeEqual' @a @b PeanoNatType a
a

addPeanoNatTypeGE :: PeanoNatType a -> PeanoNatType b -> GreaterEqual (Add a b) a
addPeanoNatTypeGE :: forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> GreaterEqual (Add a b) a
addPeanoNatTypeGE PeanoNatType a
a PeanoNatType b
ZeroType =
    case forall (a :: PeanoNat). PeanoNatType a -> Add a 'Zero :~: a
addZeroPeanoNatTypeEqual PeanoNatType a
a of
        Add a 'Zero :~: a
Refl -> forall (a :: PeanoNat). PeanoNatType a -> GreaterEqual a a
samePeanoGreaterEqual PeanoNatType a
a
addPeanoNatTypeGE PeanoNatType a
a (SuccType PeanoNatType t
b) =
    case forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a
-> PeanoNatType b -> 'Succ (Add a b) :~: Add a ('Succ b)
succAddPeanoNatTypeEqual PeanoNatType a
a PeanoNatType t
b of
        'Succ (Add a t) :~: Add a ('Succ t)
Refl -> forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> GreaterEqual ('Succ a) b
diff1GreaterEqual forall a b. (a -> b) -> a -> b
$ forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> GreaterEqual (Add a b) a
addPeanoNatTypeGE PeanoNatType a
a PeanoNatType t
b

type Greater :: PeanoNat -> PeanoNat -> Type
data Greater a b where
    MkGreater :: GreaterEqual a b -> Greater ('Succ a) b

greaterIndex :: Greater a b -> PeanoNatType b
greaterIndex :: forall (a :: PeanoNat) (b :: PeanoNat).
Greater a b -> PeanoNatType b
greaterIndex (MkGreater GreaterEqual a b
n) = forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> PeanoNatType b
greaterEqualIndex GreaterEqual a b
n

peanoGreater :: PeanoNatType a -> PeanoNatType b -> Maybe (Greater a b)
peanoGreater :: forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> Maybe (Greater a b)
peanoGreater (SuccType PeanoNatType t
a) PeanoNatType b
b = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> Greater ('Succ a) b
MkGreater forall a b. (a -> b) -> a -> b
$ forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b)
peanoGreaterEqual PeanoNatType t
a PeanoNatType b
b
peanoGreater PeanoNatType a
ZeroType PeanoNatType b
_ = forall a. Maybe a
Nothing

instance Eq (Greater 'Zero b) where
    == :: Greater 'Zero b -> Greater 'Zero b -> Bool
(==) = forall n a. Empty n => n -> a
never

instance Searchable (Greater 'Zero b) where
    search :: forall b. (Greater 'Zero b -> Maybe b) -> Maybe b
search = forall a b. Finite a => (a -> Maybe b) -> Maybe b
finiteSearch

instance Countable (Greater 'Zero b) where
    countPrevious :: Greater 'Zero b -> Maybe (Greater 'Zero b)
countPrevious = forall n a. Empty n => n -> a
never
    countMaybeNext :: Maybe (Greater 'Zero b) -> Maybe (Greater 'Zero b)
countMaybeNext Maybe (Greater 'Zero b)
Nothing = forall a. Maybe a
Nothing
    countMaybeNext (Just Greater 'Zero b
n) = forall n a. Empty n => n -> a
never Greater 'Zero b
n

instance Finite (Greater 'Zero b) where
    allValues :: [Greater 'Zero b]
allValues = []
    assemble :: forall b (f :: Type -> Type).
Applicative f =>
(Greater 'Zero b -> f b) -> f (Greater 'Zero b -> b)
assemble Greater 'Zero b -> f b
_ = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall n a. Empty n => n -> a
never

instance Empty (Greater 'Zero b) where
    never :: forall a. Greater 'Zero b -> a
never Greater 'Zero b
n = case Greater 'Zero b
n of {}