module Data.Type.Witness.Specific.FiniteAllFor where

import Data.Type.Witness.General.Finite
import Data.Type.Witness.Specific.All
import Data.Type.Witness.Specific.Either
import Data.Type.Witness.Specific.Some
import Import

type FiniteAllFor :: forall k. (k -> Type) -> (k -> Type) -> Type
type role FiniteAllFor representational representational
data FiniteAllFor f w = MkFiniteAllFor
    { forall k (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> [Some w]
finiteDomain :: [Some w]
    , forall k (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> forall (t :: k). w t -> f t
finiteGetAllFor :: forall t. w t -> f t
    }

finiteAllFor :: FiniteAllFor f w -> AllFor f w
finiteAllFor :: forall {k} (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> AllFor f w
finiteAllFor (MkFiniteAllFor [Some w]
_ forall (t :: k). w t -> f t
f) = (forall (t :: k). w t -> f t) -> AllFor f w
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor w t -> f t
forall (t :: k). w t -> f t
f

finiteCodomain :: FiniteAllFor f w -> [Some f]
finiteCodomain :: forall {k} (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> [Some f]
finiteCodomain FiniteAllFor f w
sw = (Some w -> Some f) -> [Some w] -> [Some f]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(MkSome w a
st) -> f a -> Some f
forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome (f a -> Some f) -> f a -> Some f
forall a b. (a -> b) -> a -> b
$ FiniteAllFor f w -> forall (t :: k). w t -> f t
forall k (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> forall (t :: k). w t -> f t
finiteGetAllFor FiniteAllFor f w
sw w a
st) ([Some w] -> [Some f]) -> [Some w] -> [Some f]
forall a b. (a -> b) -> a -> b
$ FiniteAllFor f w -> [Some w]
forall k (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> [Some w]
finiteDomain FiniteAllFor f w
sw

mapFiniteAllFor :: (forall t. f1 t -> f2 t) -> FiniteAllFor f1 w -> FiniteAllFor f2 w
mapFiniteAllFor :: forall {k} (f1 :: k -> Type) (f2 :: k -> Type) (w :: k -> Type).
(forall (t :: k). f1 t -> f2 t)
-> FiniteAllFor f1 w -> FiniteAllFor f2 w
mapFiniteAllFor forall (t :: k). f1 t -> f2 t
ff (MkFiniteAllFor [Some w]
ai forall (t :: k). w t -> f1 t
i) = [Some w] -> (forall {t :: k}. w t -> f2 t) -> FiniteAllFor f2 w
forall k (f :: k -> Type) (w :: k -> Type).
[Some w] -> (forall (t :: k). w t -> f t) -> FiniteAllFor f w
MkFiniteAllFor [Some w]
ai ((forall {t :: k}. w t -> f2 t) -> FiniteAllFor f2 w)
-> (forall {t :: k}. w t -> f2 t) -> FiniteAllFor f2 w
forall a b. (a -> b) -> a -> b
$ \w t
s -> f1 t -> f2 t
forall (t :: k). f1 t -> f2 t
ff (f1 t -> f2 t) -> f1 t -> f2 t
forall a b. (a -> b) -> a -> b
$ w t -> f1 t
forall (t :: k). w t -> f1 t
i w t
s

eitherFiniteAllFor :: FiniteAllFor t w1 -> FiniteAllFor t w2 -> FiniteAllFor t (EitherType w1 w2)
eitherFiniteAllFor :: forall {k} (t :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type).
FiniteAllFor t w1
-> FiniteAllFor t w2 -> FiniteAllFor t (EitherType w1 w2)
eitherFiniteAllFor (MkFiniteAllFor [Some w1]
a1 forall (t :: k). w1 t -> t t
i1) (MkFiniteAllFor [Some w2]
a2 forall (t :: k). w2 t -> t t
i2) =
    [Some (EitherType w1 w2)]
-> (forall (t :: k). EitherType w1 w2 t -> t t)
-> FiniteAllFor t (EitherType w1 w2)
forall k (f :: k -> Type) (w :: k -> Type).
[Some w] -> (forall (t :: k). w t -> f t) -> FiniteAllFor f w
MkFiniteAllFor
        (((Some w1 -> Some (EitherType w1 w2))
-> [Some w1] -> [Some (EitherType w1 w2)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall (t :: k). w1 t -> EitherType w1 w2 t)
-> Some w1 -> Some (EitherType w1 w2)
forall k (g :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type).
(forall (t :: k). w1 t -> w2 t) -> SomeFor g w1 -> SomeFor g w2
mapSome w1 t -> EitherType w1 w2 t
forall (t :: k). w1 t -> EitherType w1 w2 t
forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w1 t -> EitherType w1 w2 t
LeftType) [Some w1]
a1) [Some (EitherType w1 w2)]
-> [Some (EitherType w1 w2)] -> [Some (EitherType w1 w2)]
forall a. [a] -> [a] -> [a]
++ ((Some w2 -> Some (EitherType w1 w2))
-> [Some w2] -> [Some (EitherType w1 w2)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall (t :: k). w2 t -> EitherType w1 w2 t)
-> Some w2 -> Some (EitherType w1 w2)
forall k (g :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type).
(forall (t :: k). w1 t -> w2 t) -> SomeFor g w1 -> SomeFor g w2
mapSome w2 t -> EitherType w1 w2 t
forall (t :: k). w2 t -> EitherType w1 w2 t
forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w2 t -> EitherType w1 w2 t
RightType) [Some w2]
a2))
        (AllFor t (EitherType w1 w2)
-> forall (t :: k). EitherType w1 w2 t -> t t
forall k (f :: k -> Type) (w :: k -> Type).
AllFor f w -> forall (t :: k). w t -> f t
unAllFor (AllFor t (EitherType w1 w2)
 -> forall (t :: k). EitherType w1 w2 t -> t t)
-> AllFor t (EitherType w1 w2)
-> forall (t :: k). EitherType w1 w2 t -> t t
forall a b. (a -> b) -> a -> b
$ AllFor t w1 -> AllFor t w2 -> AllFor t (EitherType w1 w2)
forall {k} (f :: k -> Type) (sel1 :: k -> Type)
       (sel2 :: k -> Type).
AllFor f sel1 -> AllFor f sel2 -> AllFor f (EitherType sel1 sel2)
eitherAllFor ((forall (t :: k). w1 t -> t t) -> AllFor t w1
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor w1 t -> t t
forall (t :: k). w1 t -> t t
i1) ((forall (t :: k). w2 t -> t t) -> AllFor t w2
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor w2 t -> t t
forall (t :: k). w2 t -> t t
i2))

mkFiniteAllFor ::
       forall f w. FiniteWitness w
    => (forall t. w t -> f t)
    -> FiniteAllFor f w
mkFiniteAllFor :: forall {k} (f :: k -> Type) (w :: k -> Type).
FiniteWitness w =>
(forall (t :: k). w t -> f t) -> FiniteAllFor f w
mkFiniteAllFor = [Some w] -> (forall {t :: k}. w t -> f t) -> FiniteAllFor f w
forall k (f :: k -> Type) (w :: k -> Type).
[Some w] -> (forall (t :: k). w t -> f t) -> FiniteAllFor f w
MkFiniteAllFor [Some w]
forall {k} (w :: k -> Type). FiniteWitness w => [Some w]
allWitnesses