{-|
Copyright   : (c) Hisaket VioletRed, 2022
License     : AGPL-3.0-or-later
Maintainer  : hisaket@outlook.jp
Stability   : experimental

This module provides methods that allow for isolating effects inside or outside the scope locally.

It will be useful when using the effects for virtualization or containerization such as libvirt or Docker safely.
-}

{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use camelCase" #-}

module Polysemy.Scoped.Path.Isolation where
import Polysemy ( Member, Sem, InterpretersFor, Members, rewrite )
import Polysemy.Scoped.Path ( ScopedP, scopedP )
import Polysemy.Input ( Input )
import Polysemy.Bundle ( subsumeBundle, Bundle )
import Control.Category ( (>>>) )
import Polysemy.Scoped.Path.Internal
    ( bundle, subsumeBundleUsing, unbundle )
import Polysemy.Tagged ( tag, untag, Tagged )
import Polysemy.Membership ( ElemOf )

-- | Variant of 'scopedP' that can isolate effects inside or outside the scope locally.
isolatingScopedP
    ::  Member (ScopedP path resource effect) r
    =>  path -> InterpretersFor '[Tagged 'Inner effect, Input path, Tagged 'Outer (Bundle r)] r
isolatingScopedP :: path
-> InterpretersFor
     '[Tagged 'Inner effect, Input path, Tagged 'Outer (Bundle r)] r
isolatingScopedP = (forall (e :: (* -> *) -> * -> *). ElemOf e r -> ElemOf e r)
-> path
-> InterpretersFor
     '[Tagged 'Inner effect, Input path, Tagged 'Outer (Bundle r)] r
forall (es :: [(* -> *) -> * -> *]) path resource
       (effect :: (* -> *) -> * -> *) (r :: [(* -> *) -> * -> *]).
Member (ScopedP path resource effect) r =>
(forall (e :: (* -> *) -> * -> *). ElemOf e es -> ElemOf e r)
-> path
-> InterpretersFor
     '[Tagged 'Inner effect, Input path, Tagged 'Outer (Bundle es)] r
isolatingScopedPSubUsing forall a. a -> a
forall (e :: (* -> *) -> * -> *). ElemOf e r -> ElemOf e r
id

-- | Variant of 'scopedP' that can isolate effects inside or outside the scope locally.
-- A version that can isolate only a subset of effects in regards to outside the scope.
isolatingScopedPSub
    ::  ∀es path resource effect r
    .   (Member (ScopedP path resource effect) r, Members es r)
    =>  path -> InterpretersFor '[Tagged 'Inner effect, Input path, Tagged 'Outer (Bundle es)] r
isolatingScopedPSub :: path
-> InterpretersFor
     '[Tagged 'Inner effect, Input path, Tagged 'Outer (Bundle es)] r
isolatingScopedPSub path
path = Sem
  (Tagged 'Inner effect : Input path : Tagged 'Outer (Bundle es) : r)
  a
-> Sem (effect : Input path : Tagged 'Outer (Bundle es) : r) a
forall k1 (k2 :: k1) (e :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
Sem (Tagged k2 e : r) a -> Sem (e : r) a
untag (Sem
   (Tagged 'Inner effect : Input path : Tagged 'Outer (Bundle es) : r)
   a
 -> Sem (effect : Input path : Tagged 'Outer (Bundle es) : r) a)
-> (Sem (effect : Input path : Tagged 'Outer (Bundle es) : r) a
    -> Sem r a)
-> Sem
     (Tagged 'Inner effect : Input path : Tagged 'Outer (Bundle es) : r)
     a
-> Sem r a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> path
-> InterpretersFor
     '[effect, Input path] (Tagged 'Outer (Bundle es) : r)
forall path resource (effect :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]).
Member (ScopedP path resource effect) r =>
path -> InterpretersFor '[effect, Input path] r
scopedP path
path (Sem (effect : Input path : Tagged 'Outer (Bundle es) : r) a
 -> Sem (Tagged 'Outer (Bundle es) : r) a)
-> (Sem (Tagged 'Outer (Bundle es) : r) a -> Sem r a)
-> Sem (effect : Input path : Tagged 'Outer (Bundle es) : r) a
-> Sem r a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (Tagged 'Outer (Bundle es) : r) a -> Sem (Bundle es : r) a
forall k1 (k2 :: k1) (e :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
Sem (Tagged k2 e : r) a -> Sem (e : r) a
untag (Sem (Tagged 'Outer (Bundle es) : r) a -> Sem (Bundle es : r) a)
-> (Sem (Bundle es : r) a -> Sem r a)
-> Sem (Tagged 'Outer (Bundle es) : r) a
-> Sem r a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (Bundle es : r) a -> Sem r a
forall (r' :: [(* -> *) -> * -> *]) (r :: [(* -> *) -> * -> *]) a.
Members r' r =>
Sem (Bundle r' : r) a -> Sem r a
subsumeBundle

-- | Variant of 'scopedP' that can isolate effects inside or outside the scope locally.
isolatingScopedPSubUsing
    ::  ∀es path resource effect r
    .   Member (ScopedP path resource effect) r
    =>  (∀e. ElemOf e es -> ElemOf e r)
    ->  path -> InterpretersFor '[Tagged 'Inner effect, Input path, Tagged 'Outer (Bundle es)] r
isolatingScopedPSubUsing :: (forall (e :: (* -> *) -> * -> *). ElemOf e es -> ElemOf e r)
-> path
-> InterpretersFor
     '[Tagged 'Inner effect, Input path, Tagged 'Outer (Bundle es)] r
isolatingScopedPSubUsing forall (e :: (* -> *) -> * -> *). ElemOf e es -> ElemOf e r
f path
path = Sem
  (Tagged 'Inner effect : Input path : Tagged 'Outer (Bundle es) : r)
  a
-> Sem (effect : Input path : Tagged 'Outer (Bundle es) : r) a
forall k1 (k2 :: k1) (e :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
Sem (Tagged k2 e : r) a -> Sem (e : r) a
untag (Sem
   (Tagged 'Inner effect : Input path : Tagged 'Outer (Bundle es) : r)
   a
 -> Sem (effect : Input path : Tagged 'Outer (Bundle es) : r) a)
-> (Sem (effect : Input path : Tagged 'Outer (Bundle es) : r) a
    -> Sem r a)
-> Sem
     (Tagged 'Inner effect : Input path : Tagged 'Outer (Bundle es) : r)
     a
-> Sem r a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> path
-> InterpretersFor
     '[effect, Input path] (Tagged 'Outer (Bundle es) : r)
forall path resource (effect :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]).
Member (ScopedP path resource effect) r =>
path -> InterpretersFor '[effect, Input path] r
scopedP path
path (Sem (effect : Input path : Tagged 'Outer (Bundle es) : r) a
 -> Sem (Tagged 'Outer (Bundle es) : r) a)
-> (Sem (Tagged 'Outer (Bundle es) : r) a -> Sem r a)
-> Sem (effect : Input path : Tagged 'Outer (Bundle es) : r) a
-> Sem r a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (Tagged 'Outer (Bundle es) : r) a -> Sem (Bundle es : r) a
forall k1 (k2 :: k1) (e :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
Sem (Tagged k2 e : r) a -> Sem (e : r) a
untag (Sem (Tagged 'Outer (Bundle es) : r) a -> Sem (Bundle es : r) a)
-> (Sem (Bundle es : r) a -> Sem r a)
-> Sem (Tagged 'Outer (Bundle es) : r) a
-> Sem r a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (forall (e :: (* -> *) -> * -> *). ElemOf e es -> ElemOf e r)
-> Sem (Bundle es : r) a -> Sem r a
forall (es :: [(* -> *) -> * -> *]) (r :: [(* -> *) -> * -> *]) a.
(forall (e :: (* -> *) -> * -> *). ElemOf e es -> ElemOf e r)
-> Sem (Bundle es : r) a -> Sem r a
subsumeBundleUsing forall (e :: (* -> *) -> * -> *). ElemOf e es -> ElemOf e r
f

data ScopeSide =
      Inner -- ^ A tag type that represents effects inside the scope.
    | Outer -- ^ A tag type that represents effects outside the scope.

-- | Isolate only effects inside the scope.
inScope :: Member (Tagged Inner (Bundle es)) r => Sem es a -> Sem r a
inScope :: Sem es a -> Sem r a
inScope = Sem es a -> Sem (Bundle es : r) a
forall (es :: [(* -> *) -> * -> *]) a (r :: [(* -> *) -> * -> *]).
Sem es a -> Sem (Bundle es : r) a
bundle (Sem es a -> Sem (Bundle es : r) a)
-> (Sem (Bundle es : r) a -> Sem r a) -> Sem es a -> Sem r a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (Bundle es : r) a -> Sem r a
forall k1 (k2 :: k1) (e :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
Member (Tagged k2 e) r =>
Sem (e : r) a -> Sem r a
tag

-- | Isolate only effects inside the scope.
-- No bundle version.
inScope_single :: Member (Tagged Inner eff) r => Sem '[eff] a -> Sem r a
inScope_single :: Sem '[eff] a -> Sem r a
inScope_single = Sem '[eff] a -> Sem (Bundle '[eff] : r) a
forall (es :: [(* -> *) -> * -> *]) a (r :: [(* -> *) -> * -> *]).
Sem es a -> Sem (Bundle es : r) a
bundle (Sem '[eff] a -> Sem (Bundle '[eff] : r) a)
-> (Sem (Bundle '[eff] : r) a -> Sem r a)
-> Sem '[eff] a
-> Sem r a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (forall (rInitial :: [(* -> *) -> * -> *]) x.
 Bundle '[eff] (Sem rInitial) x -> eff (Sem rInitial) x)
-> Sem (Bundle '[eff] : r) a -> Sem (eff : r) a
forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
(forall (rInitial :: [(* -> *) -> * -> *]) x.
 e1 (Sem rInitial) x -> e2 (Sem rInitial) x)
-> Sem (e1 : r) a -> Sem (e2 : r) a
rewrite forall (rInitial :: [(* -> *) -> * -> *]) x.
Bundle '[eff] (Sem rInitial) x -> eff (Sem rInitial) x
forall k k1 (e :: k -> k1 -> *) (m :: k) (a :: k1).
Bundle '[e] m a -> e m a
unbundle (Sem (Bundle '[eff] : r) a -> Sem (eff : r) a)
-> (Sem (eff : r) a -> Sem r a)
-> Sem (Bundle '[eff] : r) a
-> Sem r a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (eff : r) a -> Sem r a
forall k1 (k2 :: k1) (e :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
Member (Tagged k2 e) r =>
Sem (e : r) a -> Sem r a
tag

-- | Isolate only effects outside the scope.
outScope :: Member (Tagged Outer (Bundle es)) r => Sem es a -> Sem r a
outScope :: Sem es a -> Sem r a
outScope = Sem es a -> Sem (Bundle es : r) a
forall (es :: [(* -> *) -> * -> *]) a (r :: [(* -> *) -> * -> *]).
Sem es a -> Sem (Bundle es : r) a
bundle (Sem es a -> Sem (Bundle es : r) a)
-> (Sem (Bundle es : r) a -> Sem r a) -> Sem es a -> Sem r a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (Bundle es : r) a -> Sem r a
forall k1 (k2 :: k1) (e :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
Member (Tagged k2 e) r =>
Sem (e : r) a -> Sem r a
tag