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
type role PeanoNatType nominal
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 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    testEquality (SuccType PeanoNatType t
a) (SuccType PeanoNatType t
b) = do
        t :~: t
Refl <- PeanoNatType t -> PeanoNatType t -> Maybe (t :~: t)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> Maybe (a :~: b)
testEquality PeanoNatType t
a PeanoNatType t
b
        (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    testEquality PeanoNatType a
_ PeanoNatType b
_ = Maybe (a :~: 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 = WOrdering a a
WOrdering a b
forall k (a :: k). WOrdering a a
WEQ
    testCompare (SuccType PeanoNatType t
a) (SuccType PeanoNatType t
b) =
        case PeanoNatType t -> PeanoNatType t -> WOrdering t t
forall k (w :: k -> Type) (a :: k) (b :: k).
TestOrder w =>
w a -> w b -> WOrdering a b
forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> WOrdering a b
testCompare PeanoNatType t
a PeanoNatType t
b of
            WOrdering t t
WLT -> WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WLT
            WOrdering t t
WGT -> WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WGT
            WOrdering t t
WEQ -> WOrdering a a
WOrdering a b
forall k (a :: k). WOrdering a a
WEQ
    testCompare (SuccType PeanoNatType t
_) PeanoNatType b
ZeroType = WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WGT
    testCompare PeanoNatType a
ZeroType (SuccType PeanoNatType t
_) = WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WLT

instance Representative PeanoNatType where
    getRepWitness :: Subrepresentative PeanoNatType PeanoNatType
getRepWitness PeanoNatType a
ZeroType = Dict (Is PeanoNatType a)
forall (a :: Constraint). a => Dict a
Dict
    getRepWitness (SuccType PeanoNatType t
n) =
        case PeanoNatType t -> Dict (Is PeanoNatType t)
forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
Subrepresentative PeanoNatType PeanoNatType
getRepWitness PeanoNatType t
n of
            Dict (Is PeanoNatType t)
Dict -> Dict (Is PeanoNatType a)
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 = PeanoNatType n -> PeanoNatType ('Succ n)
forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a)
SuccType PeanoNatType n
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 (PeanoNat -> PeanoNat) -> PeanoNat -> PeanoNat
forall a b. (a -> b) -> a -> b
$ PeanoNatType t -> WitnessValueType PeanoNatType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
forall (t :: PeanoNat).
PeanoNatType t -> WitnessValueType PeanoNatType
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 = PeanoNatType 'Zero -> r
forall (t :: PeanoNat). PeanoNatType t -> r
cont PeanoNatType 'Zero
ZeroType
    valueToWitness (Succ PeanoNat
n) forall (t :: PeanoNat). PeanoNatType t -> r
cont = WitnessValueType PeanoNatType
-> (forall (t :: PeanoNat). PeanoNatType t -> r) -> r
forall r.
WitnessValueType PeanoNatType
-> (forall (t :: PeanoNat). PeanoNatType t -> r) -> r
forall k (w :: k -> Type) r.
WitnessValue w =>
WitnessValueType w -> (forall (t :: k). w t -> r) -> r
valueToWitness WitnessValueType PeanoNatType
PeanoNat
n ((forall (t :: PeanoNat). PeanoNatType t -> r) -> r)
-> (forall (t :: PeanoNat). PeanoNatType t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \PeanoNatType t
t -> PeanoNatType ('Succ t) -> r
forall (t :: PeanoNat). PeanoNatType t -> r
cont (PeanoNatType ('Succ t) -> r) -> PeanoNatType ('Succ t) -> r
forall a b. (a -> b) -> a -> b
$ PeanoNatType t -> PeanoNatType ('Succ t)
forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a)
SuccType PeanoNatType t
t

type GreaterEqual :: PeanoNat -> PeanoNat -> Type
type role GreaterEqual nominal nominal
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 b
PeanoNatType 'Zero
ZeroType
greaterEqualIndex (SuccGreaterEqual GreaterEqual a b
n) = PeanoNatType b -> PeanoNatType ('Succ b)
forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a)
SuccType (PeanoNatType b -> PeanoNatType ('Succ b))
-> PeanoNatType b -> PeanoNatType ('Succ b)
forall a b. (a -> b) -> a -> b
$ GreaterEqual a b -> PeanoNatType 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 = GreaterEqual a a
GreaterEqual a 'Zero
forall (a :: PeanoNat). GreaterEqual a 'Zero
ZeroGreaterEqual
samePeanoGreaterEqual (SuccType PeanoNatType t
a) = GreaterEqual t t -> GreaterEqual ('Succ t) ('Succ t)
forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)
SuccGreaterEqual (GreaterEqual t t -> GreaterEqual ('Succ t) ('Succ t))
-> GreaterEqual t t -> GreaterEqual ('Succ t) ('Succ t)
forall a b. (a -> b) -> a -> b
$ PeanoNatType t -> GreaterEqual t t
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 = GreaterEqual ('Succ a) b
GreaterEqual ('Succ a) 'Zero
forall (a :: PeanoNat). GreaterEqual a 'Zero
ZeroGreaterEqual
diff1GreaterEqual (SuccGreaterEqual GreaterEqual a b
ge) = GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)
forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)
SuccGreaterEqual (GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b))
-> GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)
forall a b. (a -> b) -> a -> b
$ GreaterEqual a b -> GreaterEqual ('Succ 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 = GreaterEqual a b -> Maybe (GreaterEqual a b)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return GreaterEqual a b
GreaterEqual a 'Zero
forall (a :: PeanoNat). GreaterEqual a 'Zero
ZeroGreaterEqual
peanoGreaterEqual PeanoNatType a
ZeroType PeanoNatType b
_ = Maybe (GreaterEqual a b)
forall a. Maybe a
Nothing
peanoGreaterEqual (SuccType PeanoNatType t
a) (SuccType PeanoNatType t
b) = do
    GreaterEqual t t
al <- PeanoNatType t -> PeanoNatType t -> Maybe (GreaterEqual t t)
forall (a :: PeanoNat) (b :: PeanoNat).
PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b)
peanoGreaterEqual PeanoNatType t
a PeanoNatType t
b
    GreaterEqual a b -> Maybe (GreaterEqual a b)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GreaterEqual a b -> Maybe (GreaterEqual a b))
-> GreaterEqual a b -> Maybe (GreaterEqual a b)
forall a b. (a -> b) -> a -> b
$ GreaterEqual t t -> GreaterEqual ('Succ t) ('Succ t)
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
PeanoNatType (Add a b)
b
addPeanoNatType (SuccType PeanoNatType t
a) PeanoNatType b
b = PeanoNatType (Add t b) -> PeanoNatType ('Succ (Add t b))
forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a)
SuccType (PeanoNatType (Add t b) -> PeanoNatType ('Succ (Add t b)))
-> PeanoNatType (Add t b) -> PeanoNatType ('Succ (Add t b))
forall a b. (a -> b) -> a -> b
$ PeanoNatType t -> PeanoNatType b -> PeanoNatType (Add t 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 = a :~: a
Add a 'Zero :~: a
forall {k} (a :: k). a :~: a
Refl
addZeroPeanoNatTypeEqual (SuccType PeanoNatType t
a) =
    case PeanoNatType t -> Add t 'Zero :~: t
forall (a :: PeanoNat). PeanoNatType a -> Add a 'Zero :~: a
addZeroPeanoNatTypeEqual PeanoNatType t
a of
        Add t 'Zero :~: t
Refl -> a :~: a
Add a 'Zero :~: a
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 = 'Succ b :~: 'Succ b
'Succ (Add a b) :~: Add a ('Succ b)
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 -> 'Succ (Add a b) :~: Add a ('Succ b)
'Succ ('Succ (Add t b)) :~: 'Succ ('Succ (Add t b))
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 PeanoNatType a -> Add a 'Zero :~: a
forall (a :: PeanoNat). PeanoNatType a -> Add a 'Zero :~: a
addZeroPeanoNatTypeEqual PeanoNatType a
a of
        Add a 'Zero :~: a
Refl -> PeanoNatType a -> GreaterEqual a a
forall (a :: PeanoNat). PeanoNatType a -> GreaterEqual a a
samePeanoGreaterEqual PeanoNatType a
a
addPeanoNatTypeGE PeanoNatType a
a (SuccType PeanoNatType t
b) =
    case PeanoNatType a
-> PeanoNatType t -> 'Succ (Add a t) :~: Add a ('Succ t)
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 -> GreaterEqual (Add a t) a -> GreaterEqual ('Succ (Add a t)) a
forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> GreaterEqual ('Succ a) b
diff1GreaterEqual (GreaterEqual (Add a t) a -> GreaterEqual ('Succ (Add a t)) a)
-> GreaterEqual (Add a t) a -> GreaterEqual ('Succ (Add a t)) a
forall a b. (a -> b) -> a -> b
$ PeanoNatType a -> PeanoNatType t -> GreaterEqual (Add a t) a
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
type role Greater nominal nominal
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) = GreaterEqual a b -> PeanoNatType b
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 = (GreaterEqual t b -> Greater a b)
-> Maybe (GreaterEqual t b) -> Maybe (Greater a b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap GreaterEqual t b -> Greater a b
GreaterEqual t b -> Greater ('Succ t) b
forall (a :: PeanoNat) (b :: PeanoNat).
GreaterEqual a b -> Greater ('Succ a) b
MkGreater (Maybe (GreaterEqual t b) -> Maybe (Greater a b))
-> Maybe (GreaterEqual t b) -> Maybe (Greater a b)
forall a b. (a -> b) -> a -> b
$ PeanoNatType t -> PeanoNatType b -> Maybe (GreaterEqual t 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
_ = Maybe (Greater a b)
forall a. Maybe a
Nothing

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

instance Searchable (Greater 'Zero b) where
    search :: forall b. (Greater 'Zero b -> Maybe b) -> Maybe b
search = (Greater 'Zero b -> Maybe b) -> Maybe b
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 = Greater 'Zero b -> Maybe (Greater 'Zero b)
forall n a. Empty n => n -> a
forall a. Greater 'Zero b -> a
never
    countMaybeNext :: Maybe (Greater 'Zero b) -> Maybe (Greater 'Zero b)
countMaybeNext Maybe (Greater 'Zero b)
Nothing = Maybe (Greater 'Zero b)
forall a. Maybe a
Nothing
    countMaybeNext (Just Greater 'Zero b
n) = Greater 'Zero b -> Maybe (Greater 'Zero b)
forall n a. Empty n => n -> a
forall a. Greater 'Zero b -> 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
_ = (Greater 'Zero b -> b) -> f (Greater 'Zero b -> b)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Greater 'Zero b -> b
forall n a. Empty n => n -> a
forall a. Greater 'Zero b -> 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 {}