module Data.Type.Witness.Specific.All where

import Data.Type.Witness.General.WitnessConstraint
import Data.Type.Witness.Specific.Some
import Import

type AllFor :: forall k. (k -> Type) -> (k -> Type) -> Type
newtype AllFor f w = MkAllFor
    { forall k (f :: k -> Type) (w :: k -> Type).
AllFor f w -> forall (t :: k). w t -> f t
unAllFor :: forall t. w t -> f t
    }

type AllOf :: (Type -> Type) -> Type
newtype AllOf w = MkAllOf
    { forall (w :: Type -> Type). AllOf w -> forall t. w t -> t
unAllOf :: forall t. w t -> t
    }

setAllOf ::
       forall (w :: Type -> Type) (a :: Type). TestEquality w
    => w a
    -> a
    -> AllOf w
    -> AllOf w
setAllOf :: forall (w :: Type -> Type) a.
TestEquality w =>
w a -> a -> AllOf w -> AllOf w
setAllOf w a
wa a
a (MkAllOf forall t. w t -> t
wtt) =
    forall (w :: Type -> Type). (forall t. w t -> t) -> AllOf w
MkAllOf forall a b. (a -> b) -> a -> b
$ \w t
wa' ->
        case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w a
wa w t
wa' of
            Just a :~: t
Refl -> a
a
            Maybe (a :~: t)
Nothing -> forall t. w t -> t
wtt w t
wa'

allForToAllOf :: forall (w :: Type -> Type). AllFor Identity w -> AllOf w
allForToAllOf :: forall (w :: Type -> Type). AllFor Identity w -> AllOf w
allForToAllOf (MkAllFor forall t. w t -> Identity t
wtit) = forall (w :: Type -> Type). (forall t. w t -> t) -> AllOf w
MkAllOf forall a b. (a -> b) -> a -> b
$ \w t
wt -> forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall t. w t -> Identity t
wtit w t
wt

allOfToAllFor :: forall (w :: Type -> Type). AllOf w -> AllFor Identity w
allOfToAllFor :: forall (w :: Type -> Type). AllOf w -> AllFor Identity w
allOfToAllFor (MkAllOf forall t. w t -> t
wtt) = 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
$ \w t
wt -> forall a. a -> Identity a
Identity forall a b. (a -> b) -> a -> b
$ forall t. w t -> t
wtt w t
wt

allMapSome :: AllFor f w -> SomeFor g w -> SomeFor g f
allMapSome :: forall {k} (f :: k -> Type) (w :: k -> Type) (g :: k -> Type).
AllFor f w -> SomeFor g w -> SomeFor g f
allMapSome (MkAllFor forall (t :: k). w t -> f t
f) = 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 forall (t :: k). w t -> f t
f

type UnAllOf :: Type -> Type -> Type
type family UnAllOf aw where
    UnAllOf (AllOf w) = w

splitSomeOfList ::
       forall (w :: Type -> Type). TestEquality w
    => [SomeOf w]
    -> AllFor [] w
splitSomeOfList :: forall (w :: Type -> Type).
TestEquality w =>
[SomeOf w] -> AllFor [] w
splitSomeOfList [] = 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
$ \w t
_ -> []
splitSomeOfList ((MkSomeOf w a
wt a
t):[SomeOf w]
rr) =
    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
$ \w t
wt' ->
        case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w a
wt w t
wt' of
            Just a :~: t
Refl -> a
t forall a. a -> [a] -> [a]
: (forall k (f :: k -> Type) (w :: k -> Type).
AllFor f w -> forall (t :: k). w t -> f t
unAllFor (forall (w :: Type -> Type).
TestEquality w =>
[SomeOf w] -> AllFor [] w
splitSomeOfList [SomeOf w]
rr) w t
wt')
            Maybe (a :~: t)
Nothing -> forall k (f :: k -> Type) (w :: k -> Type).
AllFor f w -> forall (t :: k). w t -> f t
unAllFor (forall (w :: Type -> Type).
TestEquality w =>
[SomeOf w] -> AllFor [] w
splitSomeOfList [SomeOf w]
rr) w t
wt'

allForWitnessConstraint ::
       forall k (c :: k -> Constraint) (w :: k -> Type). WitnessConstraint c w
    => AllFor (Compose Dict c) w
allForWitnessConstraint :: forall k (c :: k -> Constraint) (w :: k -> Type).
WitnessConstraint c w =>
AllFor (Compose Dict c) w
allForWitnessConstraint = 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
$ \w t
wt -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall a b. (a -> b) -> a -> b
$ forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k).
WitnessConstraint c w =>
w t -> Dict (c t)
witnessConstraint w t
wt