{-# LANGUAGE GADTs #-}

{- | This module contains the instances and definitions
   supporting 'Control.Multiwalk' module, along with
   the combinators for writing 'MultiSub' instances.
-}
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

-- | Modify (only) substructures by applying functions from 'FList'.
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)

-- | Query (only) substructures by applying functions from 'QList'.
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 :?:

-- | Heterogeneous list of queries
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 :.:

-- | Heterogeneous list of monadic-valued functions
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

{- | Auxiliary class that keeps track of how retrieve queries and walks from their
   lists and apply them according to the combinators.
-}
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

-- Useful combinators

-- | Use this for matching with a type inside a traversable functor.
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

{- | Use this for matching with another type that is coercible to the type you
   want.
-}
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

{- | Use this for matching a subcomponent nested inside another type. Useful if
   you don't want to add the middle type to the list of walkable types.
-}
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