module Data.Type.Witness.Specific.Either where

import Data.Type.Witness.General.AllConstraint
import Data.Type.Witness.General.Finite
import Data.Type.Witness.General.ListElement
import Data.Type.Witness.General.WitnessConstraint
import Data.Type.Witness.Specific.All
import Data.Type.Witness.Specific.List.Element
import Data.Type.Witness.Specific.Single
import Import

type EitherType :: forall k. (k -> Type) -> (k -> Type) -> (k -> Type)
type role EitherType representational representational nominal
data EitherType w1 w2 t
    = LeftType (w1 t)
    | RightType (w2 t)

instance (TestEquality w1, TestEquality w2) => TestEquality (EitherType w1 w2) where
    testEquality :: forall (a :: k) (b :: k).
EitherType w1 w2 a -> EitherType w1 w2 b -> Maybe (a :~: b)
testEquality (LeftType w1 a
s1) (LeftType w1 b
s2) = do
        a :~: b
Refl <- w1 a -> w1 b -> Maybe (a :~: b)
forall (a :: k) (b :: k). w1 a -> w1 b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w1 a
s1 w1 b
s2
        (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 (RightType w2 a
s1) (RightType w2 b
s2) = do
        a :~: b
Refl <- w2 a -> w2 b -> Maybe (a :~: b)
forall (a :: k) (b :: k). w2 a -> w2 b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w2 a
s1 w2 b
s2
        (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 EitherType w1 w2 a
_ EitherType w1 w2 b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance (FiniteWitness p, FiniteWitness q) => FiniteWitness (EitherType p q) where
    assembleAllFor :: forall (m :: Type -> Type) (f :: k -> Type).
Applicative m =>
(forall (t :: k). EitherType p q t -> m (f t))
-> m (AllFor f (EitherType p q))
assembleAllFor forall (t :: k). EitherType p q t -> m (f t)
getsel =
        (\(MkAllFor forall (t :: k). p t -> f t
p) (MkAllFor forall (t :: k). q t -> f t
q) ->
             (forall (t :: k). EitherType p q t -> f t)
-> AllFor f (EitherType p q)
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor ((forall (t :: k). EitherType p q t -> f t)
 -> AllFor f (EitherType p q))
-> (forall (t :: k). EitherType p q t -> f t)
-> AllFor f (EitherType p q)
forall a b. (a -> b) -> a -> b
$ \EitherType p q t
wt ->
                 case EitherType p q t
wt of
                     LeftType p t
rt -> p t -> f t
forall (t :: k). p t -> f t
p p t
rt
                     RightType q t
rt -> q t -> f t
forall (t :: k). q t -> f t
q q t
rt) (AllFor f p -> AllFor f q -> AllFor f (EitherType p q))
-> m (AllFor f p) -> m (AllFor f q -> AllFor f (EitherType p q))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
        (forall (t :: k). p t -> m (f t)) -> m (AllFor f p)
forall k (w :: k -> Type) (m :: Type -> Type) (f :: k -> Type).
(FiniteWitness w, Applicative m) =>
(forall (t :: k). w t -> m (f t)) -> m (AllFor f w)
forall (m :: Type -> Type) (f :: k -> Type).
Applicative m =>
(forall (t :: k). p t -> m (f t)) -> m (AllFor f p)
assembleAllFor (EitherType p q t -> m (f t)
forall (t :: k). EitherType p q t -> m (f t)
getsel (EitherType p q t -> m (f t))
-> (p t -> EitherType p q t) -> p t -> m (f t)
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
. p t -> EitherType p q t
forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w1 t -> EitherType w1 w2 t
LeftType) m (AllFor f q -> AllFor f (EitherType p q))
-> m (AllFor f q) -> m (AllFor f (EitherType p q))
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*>
        (forall (t :: k). q t -> m (f t)) -> m (AllFor f q)
forall k (w :: k -> Type) (m :: Type -> Type) (f :: k -> Type).
(FiniteWitness w, Applicative m) =>
(forall (t :: k). w t -> m (f t)) -> m (AllFor f w)
forall (m :: Type -> Type) (f :: k -> Type).
Applicative m =>
(forall (t :: k). q t -> m (f t)) -> m (AllFor f q)
assembleAllFor (EitherType p q t -> m (f t)
forall (t :: k). EitherType p q t -> m (f t)
getsel (EitherType p q t -> m (f t))
-> (q t -> EitherType p q t) -> q t -> m (f t)
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
. q t -> EitherType p q t
forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w2 t -> EitherType w1 w2 t
RightType)

instance (WitnessConstraint c p, WitnessConstraint c q) => WitnessConstraint c (EitherType p q) where
    witnessConstraint :: forall (t :: k). EitherType p q t -> Dict (c t)
witnessConstraint (LeftType p t
rt) =
        case forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k).
WitnessConstraint c w =>
w t -> Dict (c t)
witnessConstraint @_ @c p t
rt of
            Dict (c t)
Dict -> Dict (c t)
forall (a :: Constraint). a => Dict a
Dict
    witnessConstraint (RightType q t
rt) =
        case forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k).
WitnessConstraint c w =>
w t -> Dict (c t)
witnessConstraint @_ @c q t
rt of
            Dict (c t)
Dict -> Dict (c t)
forall (a :: Constraint). a => Dict a
Dict

instance (Show (p t), Show (q t)) => Show (EitherType p q t) where
    show :: EitherType p q t -> String
show (LeftType p t
rt) = p t -> String
forall a. Show a => a -> String
show p t
rt
    show (RightType q t
rt) = q t -> String
forall a. Show a => a -> String
show q t
rt

instance (AllConstraint Show p, AllConstraint Show q) => AllConstraint Show (EitherType p q) where
    allConstraint :: forall t. Dict (Show (EitherType p q t))
    allConstraint :: forall (t :: kt). Dict (Show (EitherType p q t))
allConstraint =
        case forall kw kt (c :: kw -> Constraint) (w :: kt -> kw) (t :: kt).
AllConstraint c w =>
Dict (c (w t))
allConstraint @_ @_ @Show @p @t of
            Dict (Show (p t))
Dict ->
                case forall kw kt (c :: kw -> Constraint) (w :: kt -> kw) (t :: kt).
AllConstraint c w =>
Dict (c (w t))
allConstraint @_ @_ @Show @q @t of
                    Dict (Show (q t))
Dict -> Dict (Show (EitherType p q t))
forall (a :: Constraint). a => Dict a
Dict

eitherAllOf :: AllOf sel1 -> AllOf sel2 -> AllOf (EitherType sel1 sel2)
eitherAllOf :: forall (sel1 :: Type -> Type) (sel2 :: Type -> Type).
AllOf sel1 -> AllOf sel2 -> AllOf (EitherType sel1 sel2)
eitherAllOf (MkAllOf forall t. sel1 t -> t
tup1) (MkAllOf forall t. sel2 t -> t
tup2) =
    (forall t. EitherType sel1 sel2 t -> t)
-> AllOf (EitherType sel1 sel2)
forall (w :: Type -> Type). (forall t. w t -> t) -> AllOf w
MkAllOf ((forall t. EitherType sel1 sel2 t -> t)
 -> AllOf (EitherType sel1 sel2))
-> (forall t. EitherType sel1 sel2 t -> t)
-> AllOf (EitherType sel1 sel2)
forall a b. (a -> b) -> a -> b
$ \EitherType sel1 sel2 t
esel ->
        case EitherType sel1 sel2 t
esel of
            LeftType sel1 t
sel -> sel1 t -> t
forall t. sel1 t -> t
tup1 sel1 t
sel
            RightType sel2 t
sel -> sel2 t -> t
forall t. sel2 t -> t
tup2 sel2 t
sel

eitherAllFor :: AllFor f sel1 -> AllFor f sel2 -> AllFor f (EitherType sel1 sel2)
eitherAllFor :: forall {k} (f :: k -> Type) (sel1 :: k -> Type)
       (sel2 :: k -> Type).
AllFor f sel1 -> AllFor f sel2 -> AllFor f (EitherType sel1 sel2)
eitherAllFor (MkAllFor forall (t :: k). sel1 t -> f t
tup1) (MkAllFor forall (t :: k). sel2 t -> f t
tup2) =
    (forall (t :: k). EitherType sel1 sel2 t -> f t)
-> AllFor f (EitherType sel1 sel2)
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor ((forall (t :: k). EitherType sel1 sel2 t -> f t)
 -> AllFor f (EitherType sel1 sel2))
-> (forall (t :: k). EitherType sel1 sel2 t -> f t)
-> AllFor f (EitherType sel1 sel2)
forall a b. (a -> b) -> a -> b
$ \EitherType sel1 sel2 t
esel ->
        case EitherType sel1 sel2 t
esel of
            LeftType sel1 t
sel -> sel1 t -> f t
forall (t :: k). sel1 t -> f t
tup1 sel1 t
sel
            RightType sel2 t
sel -> sel2 t -> f t
forall (t :: k). sel2 t -> f t
tup2 sel2 t
sel

type ConsType :: forall k. k -> (k -> Type) -> k -> Type
type ConsType a = EitherType (SingleType a)

instance ListElementWitness lt => ListElementWitness (ConsType a lt) where
    type WitnessTypeList (ConsType a lt) = a ': (WitnessTypeList lt)
    toListElementWitness :: forall (t :: k).
ConsType a lt t
-> ListElementType (WitnessTypeList (ConsType a lt)) t
toListElementWitness (LeftType a :~: t
Refl) = ListElementType (t : WitnessTypeList lt) t
ListElementType (WitnessTypeList (ConsType a lt)) t
forall {k} (t :: k) (tt :: [k]). ListElementType (t : tt) t
FirstElementType
    toListElementWitness (RightType lt t
sel) = ListElementType (WitnessTypeList lt) t
-> ListElementType (a : WitnessTypeList lt) t
forall {k} (aa :: [k]) (t :: k) (a :: k).
ListElementType aa t -> ListElementType (a : aa) t
RestElementType (ListElementType (WitnessTypeList lt) t
 -> ListElementType (a : WitnessTypeList lt) t)
-> ListElementType (WitnessTypeList lt) t
-> ListElementType (a : WitnessTypeList lt) t
forall a b. (a -> b) -> a -> b
$ lt t -> ListElementType (WitnessTypeList lt) t
forall (t :: k). lt t -> ListElementType (WitnessTypeList lt) t
forall k (w :: k -> Type) (t :: k).
ListElementWitness w =>
w t -> ListElementType (WitnessTypeList w) t
toListElementWitness lt t
sel
    fromListElementWitness :: forall (t :: k).
ListElementType (WitnessTypeList (ConsType a lt)) t
-> ConsType a lt t
fromListElementWitness ListElementType (WitnessTypeList (ConsType a lt)) t
FirstElementType = SingleType a t -> EitherType (SingleType a) lt t
forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w1 t -> EitherType w1 w2 t
LeftType SingleType a t
t :~: t
forall {k} (a :: k). a :~: a
Refl
    fromListElementWitness (RestElementType ListElementType aa t
lt) = lt t -> EitherType (SingleType a) lt t
forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w2 t -> EitherType w1 w2 t
RightType (lt t -> EitherType (SingleType a) lt t)
-> lt t -> EitherType (SingleType a) lt t
forall a b. (a -> b) -> a -> b
$ ListElementType (WitnessTypeList lt) t -> lt t
forall (t :: k). ListElementType (WitnessTypeList lt) t -> lt t
forall k (w :: k -> Type) (t :: k).
ListElementWitness w =>
ListElementType (WitnessTypeList w) t -> w t
fromListElementWitness ListElementType aa t
ListElementType (WitnessTypeList lt) t
lt