{-# LANGUAGE GADTs #-}
module Control.MultiWalk.Contains (
module Control.MultiWalk.HasSub,
module Control.MultiWalk.Contains,
) where
import Control.MultiWalk.HasSub hiding (Carrier, HasSub (..), ToSpec, ToSpecSel)
import qualified Control.MultiWalk.HasSub as HS
import Data.Coerce (Coercible, coerce)
import Data.Kind (Type)
import Data.Proxy (Proxy (..))
data MWCTag
type family ContainsCarrier (a :: Type) :: Type where
ContainsCarrier (Under b s a) = b
ContainsCarrier (MatchWith s a) = s
ContainsCarrier (Trav f a) = f (Carrier a)
ContainsCarrier a = a
type instance HS.Carrier MWCTag a = ContainsCarrier a
type instance HS.Carrier MWCTag a = ContainsCarrier a
type HasSub tag ls t = HS.HasSub MWCTag tag ls t
type Carrier a = HS.Carrier MWCTag a
type ToSpec a = HS.ToSpec MWCTag a
type ToSpecSel s a = HS.ToSpecSel MWCTag s a
modSubWithFList ::
forall tag ls t fs m.
(HasSub tag ls t, Applicative m, AllMods (TContains fs) ls) =>
FList m fs ->
t ->
m t
modSubWithFList :: forall tag (ls :: Spec) t (fs :: [*]) (m :: * -> *).
(HasSub tag ls t, Applicative m, AllMods (TContains fs) ls) =>
FList m fs -> t -> m t
modSubWithFList FList m fs
fs =
forall {k} ctag (tag :: k) (ls :: Spec) t (c :: * -> Constraint)
(m :: * -> *).
(HasSub ctag tag ls t, Applicative m, AllMods c ls) =>
Proxy c
-> (forall s.
c s =>
Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> t
-> m t
HS.modSub @MWCTag @tag @ls @t (forall {k} (t :: k). Proxy t
Proxy @(TContains fs)) (\(Proxy s
_ :: Proxy s) -> forall (fs :: [*]) t (m :: * -> *).
(TContains fs t, Applicative m) =>
FList m fs -> ContainsCarrier t -> m (ContainsCarrier t)
tGetW @fs @s FList m fs
fs)
getSubWithQList ::
forall tag ls t fs m.
(HasSub tag ls t, Monoid m, AllMods (TContains fs) ls) =>
QList m fs ->
t ->
m
getSubWithQList :: forall tag (ls :: Spec) t (fs :: [*]) m.
(HasSub tag ls t, Monoid m, AllMods (TContains fs) ls) =>
QList m fs -> t -> m
getSubWithQList QList m fs
fs =
forall {k} ctag (tag :: k) (ls :: Spec) t (c :: * -> Constraint) m.
(HasSub ctag tag ls t, Monoid m, AllMods c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> t -> m
HS.getSub @MWCTag @tag @ls @t (forall {k} (t :: k). Proxy t
Proxy @(TContains fs)) (\(Proxy s
_ :: Proxy s) -> forall (fs :: [*]) t m.
(TContains fs t, Monoid m) =>
QList m fs -> ContainsCarrier t -> m
tGetQ @fs @s QList m fs
fs)
infixr 8 :?:
data QList :: Type -> [Type] -> Type where
QNil :: QList m '[]
(:?:) :: (x -> m) -> QList m xs -> QList m (x : xs)
class QContains (l :: [Type]) (t :: Type) where
qGet :: QList m l -> t -> m
qSet :: QList m l -> (t -> m) -> QList m l
instance {-# OVERLAPS #-} QContains (t : xs) t where
qGet :: forall m. QList m (t : xs) -> t -> m
qGet (x -> m
f :?: QList m xs
_) = x -> m
f
qSet :: forall m. QList m (t : xs) -> (t -> m) -> QList m (t : xs)
qSet (x -> m
_ :?: QList m xs
y) t -> m
z = t -> m
z forall x m (xs :: [*]). (x -> m) -> QList m xs -> QList m (x : xs)
:?: QList m xs
y
instance QContains xs t => QContains (x : xs) t where
qGet :: forall m. QList m (x : xs) -> t -> m
qGet (x -> m
_ :?: QList m xs
y) = forall (l :: [*]) t m. QContains l t => QList m l -> t -> m
qGet QList m xs
y
qSet :: forall m. QList m (x : xs) -> (t -> m) -> QList m (x : xs)
qSet (x -> m
x :?: QList m xs
y) t -> m
z = x -> m
x forall x m (xs :: [*]). (x -> m) -> QList m xs -> QList m (x : xs)
:?: forall (l :: [*]) t m.
QContains l t =>
QList m l -> (t -> m) -> QList m l
qSet QList m xs
y t -> m
z
infixr 8 :.:
data FList :: (Type -> Type) -> [Type] -> Type where
FNil :: FList m '[]
(:.:) :: (x -> m x) -> FList m xs -> FList m (x : xs)
class FContains (l :: [Type]) (t :: Type) where
fGet :: FList m l -> t -> m t
fSet :: FList m l -> (t -> m t) -> FList m l
instance {-# OVERLAPS #-} FContains (t : xs) t where
fGet :: forall (m :: * -> *). FList m (t : xs) -> t -> m t
fGet (x -> m x
f :.: FList m xs
_) = x -> m x
f
fSet :: forall (m :: * -> *).
FList m (t : xs) -> (t -> m t) -> FList m (t : xs)
fSet (x -> m x
_ :.: FList m xs
y) t -> m t
z = t -> m t
z forall x (m :: * -> *) (xs :: [*]).
(x -> m x) -> FList m xs -> FList m (x : xs)
:.: FList m xs
y
instance FContains xs t => FContains (x : xs) t where
fGet :: forall (m :: * -> *). FList m (x : xs) -> t -> m t
fGet (x -> m x
_ :.: FList m xs
y) = forall (l :: [*]) t (m :: * -> *).
FContains l t =>
FList m l -> t -> m t
fGet FList m xs
y
fSet :: forall (m :: * -> *).
FList m (x : xs) -> (t -> m t) -> FList m (x : xs)
fSet (x -> m x
x :.: FList m xs
y) t -> m t
z = x -> m x
x forall x (m :: * -> *) (xs :: [*]).
(x -> m x) -> FList m xs -> FList m (x : xs)
:.: forall (l :: [*]) t (m :: * -> *).
FContains l t =>
FList m l -> (t -> m t) -> FList m l
fSet FList m xs
y t -> m t
z
class TContains (fs :: [Type]) (t :: Type) where
tGetW :: Applicative m => FList m fs -> ContainsCarrier t -> m (ContainsCarrier t)
tGetQ :: Monoid m => QList m fs -> ContainsCarrier t -> m
instance
{-# OVERLAPPABLE #-}
( FContains fs (Carrier a)
, QContains fs (Carrier a)
) =>
TContains fs a
where
tGetW :: forall (m :: * -> *).
Applicative m =>
FList m fs -> ContainsCarrier a -> m (ContainsCarrier a)
tGetW = forall (l :: [*]) t (m :: * -> *).
FContains l t =>
FList m l -> t -> m t
fGet
tGetQ :: forall m. Monoid m => QList m fs -> ContainsCarrier a -> m
tGetQ = forall (l :: [*]) t m. QContains l t => QList m l -> t -> m
qGet
data Trav (k :: Type -> Type) (a :: Type)
instance
( Traversable f
, TContains fs a
) =>
TContains fs (Trav f a)
where
tGetW :: forall (m :: * -> *).
Applicative m =>
FList m fs
-> ContainsCarrier (Trav f a) -> m (ContainsCarrier (Trav f a))
tGetW = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fs :: [*]) t (m :: * -> *).
(TContains fs t, Applicative m) =>
FList m fs -> ContainsCarrier t -> m (ContainsCarrier t)
tGetW @fs @a
tGetQ :: forall m. Monoid m => QList m fs -> ContainsCarrier (Trav f a) -> m
tGetQ = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fs :: [*]) t m.
(TContains fs t, Monoid m) =>
QList m fs -> ContainsCarrier t -> m
tGetQ @fs @a
data MatchWith (s :: Type) (a :: Type)
instance
( TContains fs a
, Coercible (Carrier a) s
) =>
TContains fs (MatchWith s a)
where
tGetW :: forall (m :: * -> *).
Applicative m =>
FList m fs
-> ContainsCarrier (MatchWith s a)
-> m (ContainsCarrier (MatchWith s a))
tGetW FList m fs
fs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fs :: [*]) t (m :: * -> *).
(TContains fs t, Applicative m) =>
FList m fs -> ContainsCarrier t -> m (ContainsCarrier t)
tGetW @fs @a FList m fs
fs forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce
tGetQ :: forall m.
Monoid m =>
QList m fs -> ContainsCarrier (MatchWith s a) -> m
tGetQ QList m fs
fs = forall (fs :: [*]) t m.
(TContains fs t, Monoid m) =>
QList m fs -> ContainsCarrier t -> m
tGetQ @fs @a QList m fs
fs forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce
data Under (b :: Type) (s :: SelSpec) (a :: Type)
instance
( TContains fs a
, HasSub GSubTag ('SpecList '[ 'SubSpec s a (Carrier a)]) b
) =>
TContains fs (Under b s a)
where
tGetW :: forall (m :: * -> *).
Applicative m =>
FList m fs
-> ContainsCarrier (Under b s a)
-> m (ContainsCarrier (Under b s a))
tGetW = forall tag (ls :: Spec) t (fs :: [*]) (m :: * -> *).
(HasSub tag ls t, Applicative m, AllMods (TContains fs) ls) =>
FList m fs -> t -> m t
modSubWithFList @GSubTag @('SpecList '[ 'SubSpec s a (Carrier a)]) @b @fs
tGetQ :: forall m.
Monoid m =>
QList m fs -> ContainsCarrier (Under b s a) -> m
tGetQ = forall tag (ls :: Spec) t (fs :: [*]) m.
(HasSub tag ls t, Monoid m, AllMods (TContains fs) ls) =>
QList m fs -> t -> m
getSubWithQList @GSubTag @('SpecList '[ 'SubSpec s a (Carrier a)]) @b @fs