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)
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 <- 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
        forall (m :: Type -> Type) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
    testEquality (RightType w2 a
s1) (RightType w2 b
s2) = do
        a :~: b
Refl <- 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
        forall (m :: Type -> Type) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
    testEquality EitherType w1 w2 a
_ EitherType w1 w2 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 k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor forall a b. (a -> b) -> a -> b
$ \EitherType p q t
wt ->
                 case EitherType p q t
wt of
                     LeftType p t
rt -> forall (t :: k). p t -> f t
p p t
rt
                     RightType q t
rt -> forall (t :: k). q t -> f t
q q t
rt) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
        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)
assembleAllFor (forall (t :: k). EitherType p q t -> m (f t)
getsel 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 (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w1 t -> EitherType w1 w2 t
LeftType) forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*>
        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)
assembleAllFor (forall (t :: k). EitherType p q t -> m (f t)
getsel 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 (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 -> 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 -> 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) = forall a. Show a => a -> String
show p t
rt
    show (RightType q t
rt) = 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 -> 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 (w :: Type -> Type). (forall t. w t -> t) -> AllOf w
MkAllOf forall a b. (a -> b) -> a -> b
$ \EitherType sel1 sel2 t
esel ->
        case EitherType sel1 sel2 t
esel of
            LeftType sel1 t
sel -> forall t. sel1 t -> t
tup1 sel1 t
sel
            RightType sel2 t
sel -> 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 k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor forall a b. (a -> b) -> a -> b
$ \EitherType sel1 sel2 t
esel ->
        case EitherType sel1 sel2 t
esel of
            LeftType sel1 t
sel -> forall (t :: k). sel1 t -> f t
tup1 sel1 t
sel
            RightType sel2 t
sel -> 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) = forall {k} (t :: k) (tt :: [k]). ListElementType (t : tt) t
FirstElementType
    toListElementWitness (RightType lt t
sel) = forall {k} (aa :: [k]) (t :: k) (a :: k).
ListElementType aa t -> ListElementType (a : aa) t
RestElementType forall a b. (a -> b) -> a -> b
$ 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 = forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w1 t -> EitherType w1 w2 t
LeftType forall {k} (a :: k). a :~: a
Refl
    fromListElementWitness (RestElementType ListElementType aa t
lt) = forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w2 t -> EitherType w1 w2 t
RightType forall a b. (a -> b) -> a -> b
$ forall k (w :: k -> Type) (t :: k).
ListElementWitness w =>
ListElementType (WitnessTypeList w) t -> w t
fromListElementWitness ListElementType aa t
lt