{-# LANGUAGE DerivingVia #-}

module Bluefin.Internal.GadtEffect where

import Bluefin.Internal
  ( Eff,
    Effects,
    Handle,
    HandleReader,
    OneWayCoercibleHandle (..),
    localHandle,
    mapHandle,
    oneWayCoercibleTrustMe,
    useImplIn,
    useImplUnder,
    (:&),
    (:>),
  )
import Bluefin.Internal.OneWayCoercible (OneWayCoercible (oneWayCoercibleImpl), OneWayCoercibleD)
import Data.Kind (Type)

type Send :: Effect -> Effects -> Type
-- | Bring a 'Send' into scope with 'interpret'.
newtype Send f e = MkSend (EffectHandler f e)
  deriving (HandleD (Send f)
HandleD (Send f) -> Handle (Send f)
forall (h :: Effects -> *). HandleD h -> Handle h
forall (f :: Effect). HandleD (Send f)
$chandleImpl :: forall (f :: Effect). HandleD (Send f)
handleImpl :: HandleD (Send f)
Handle) via OneWayCoercibleHandle (Send f)

-- | A convenient type synoynm matching
-- [@effectful@](https://hackage-content.haskell.org/package/effectful-core/docs/Effectful.html#t:Effect)
-- and
-- [@polysemy@](https://hackage.haskell.org/package/polysemy/docs/Polysemy.html#t:Effect)'s
-- usages provided for people who are migrating from those libraries.
type Effect = (Type -> Type) -> Type -> Type

instance (e :> es) => OneWayCoercible (Send f e) (Send f es) where
  oneWayCoercibleImpl :: OneWayCoercibleD (Send f e) (Send f es)
oneWayCoercibleImpl =
    (forall (e' :: Effects) (es' :: Effects).
 (e' :> es') =>
 Send f e' -> Send f es')
-> OneWayCoercibleD (Send f e) (Send f es)
forall (e :: Effects) (es :: Effects) (h :: Effects -> *).
(e :> es) =>
(forall (e' :: Effects) (es' :: Effects).
 (e' :> es') =>
 h e' -> h es')
-> OneWayCoercibleD (h e) (h es)
oneWayCoercibleTrustMe (\(MkSend EffectHandler f e'
g) -> EffectHandler f es' -> Send f es'
forall (f :: Effect) (e :: Effects). EffectHandler f e -> Send f e
MkSend (Eff (e :& e') r -> Eff (e :& es') r
forall (e :: Effects) (es :: Effects) (e1 :: Effects) r.
(e :> es) =>
Eff (e1 :& e) r -> Eff (e1 :& es) r
useImplUnder (Eff (e :& e') r -> Eff (e :& es') r)
-> (f (Eff e) r -> Eff (e :& e') r)
-> f (Eff e) r
-> Eff (e :& es') r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Eff e) r -> Eff (e :& e') r
EffectHandler f e'
g))

-- | Send a primitive operation to the handler for interpretation.
-- This is the Bluefin analog of @effectful@'s
-- [@send@](https://hackage.haskell.org/package/effectful-core/docs/Effectful-Dispatch-Dynamic.html#v:send)
-- and @polysemy@'s
-- [@send@](https://hackage.haskell.org/package/polysemy/docs/Polysemy.html#v:send).
send ::
  (e1 :> es) =>
  Send f e1 ->
  -- | Handle this operation using the effect handler currently in
  -- scope for the @Send f@ handle.
  f (Eff es) r ->
  Eff es r
send :: forall (e1 :: Effects) (es :: Effects) (f :: Effect) r.
(e1 :> es) =>
Send f e1 -> f (Eff es) r -> Eff es r
send (MkSend EffectHandler f e1
g) = (f (Eff es) r -> Eff (es :& e1) r) -> f (Eff es) r -> Eff es r
forall (e :: Effects) (es :: Effects) t r.
(e :> es) =>
(t -> Eff (es :& e) r) -> t -> Eff es r
useImplIn f (Eff es) r -> Eff (es :& e1) r
EffectHandler f e1
g

-- | A convenient type synonym.  This is like @effectful@'s
-- [@EffectHandler@](https://hackage-content.haskell.org/package/effectful-core-2.6.1.0/docs/Effectful-Dispatch-Dynamic.html#t:EffectHandler).
-- A similar type also appears in @polysemy@ as the argument to
-- functions like
-- [@intercept@](https://hackage.haskell.org/package/polysemy-1.9.2.0/docs/Polysemy.html#v:intercept).
type EffectHandler f es =
  forall e r.
  f (Eff e) r ->
  -- | ͘
  Eff (e :& es) r

-- |
-- @
-- import System.IO qualified as IO
--
-- runFileSystem ::
--   forall es e1 e2 r.
--   (e1 :> es, e2 :> es) =>
--   t'Bluefin.IO.IOE' e1 ->
--   t'Bluefin.Exception.Exception' t'Control.Exception.IOException' e2 ->
--   (forall e. 'Send' FileSystem e -> Eff (e :& es) r) ->
--   Eff es r
-- runFileSystem io ex = 'interpret' $ \\case
--   ReadFile path ->
--     adapt (IO.'System.IO.readFile' path)
--   WriteFile path contents ->
--     adapt (IO.'System.IO.writeFile' path contents)
--   Trace msg body -> do
--     'Bluefin.IO.effIO' io (putStrLn ("Start: " <> msg))
--     r <- 'Bluefin.Compound.useImpl' body
--     effIO io (putStrLn ("End: " <> msg))
--     pure r
--   where
--     -- If you don't want to write this signature you can use
--     -- {-# LANGUAGE NoMonoLocalBinds #-}
--     adapt :: (e1 :> es', e2 :> es') => IO r' -> Eff es' r'
--     adapt m = 'Bluefin.IO.rethrowIO' io ex (effIO io m)
-- @
interpret ::
  -- | Implementation of effect handler for @Send f@
  EffectHandler f es ->
  -- | Within this block, @send@ has the implementation given above.
  (forall e. Send f e -> Eff (e :& es) r) ->
  Eff es r
interpret :: forall (f :: Effect) (es :: Effects) r.
EffectHandler f es
-> (forall (e :: Effects). Send f e -> Eff (e :& es) r) -> Eff es r
interpret EffectHandler f es
g forall (e :: Effects). Send f e -> Eff (e :& es) r
k = (Send f es -> Eff (es :& es) r) -> Send f es -> Eff es r
forall (e :: Effects) (es :: Effects) t r.
(e :> es) =>
(t -> Eff (es :& e) r) -> t -> Eff es r
useImplIn Send f es -> Eff (es :& es) r
forall (e :: Effects). Send f e -> Eff (e :& es) r
k (EffectHandler f es -> Send f es
forall (f :: Effect) (e :: Effects). EffectHandler f e -> Send f e
MkSend f (Eff e) r -> Eff (e :& es) r
EffectHandler f es
g)

type GadtEffect :: ((Type -> Type) -> Type -> Type) -> Type -> Effects -> Type
newtype GadtEffect f a e = MkGadtEffect {forall (f :: Effect) a (e :: Effects).
GadtEffect f a e -> f (Eff e) a
unGadtEffect :: f (Eff e) a}

mapGadtEffect ::
  (f1 (Eff e1) r1 -> f2 (Eff e2) r2) ->
  GadtEffect f1 r1 e1 ->
  GadtEffect f2 r2 e2
mapGadtEffect :: forall (f1 :: Effect) (e1 :: Effects) r1 (f2 :: Effect)
       (e2 :: Effects) r2.
(f1 (Eff e1) r1 -> f2 (Eff e2) r2)
-> GadtEffect f1 r1 e1 -> GadtEffect f2 r2 e2
mapGadtEffect f1 (Eff e1) r1 -> f2 (Eff e2) r2
f = f2 (Eff e2) r2 -> GadtEffect f2 r2 e2
forall (f :: Effect) a (e :: Effects).
f (Eff e) a -> GadtEffect f a e
MkGadtEffect (f2 (Eff e2) r2 -> GadtEffect f2 r2 e2)
-> (GadtEffect f1 r1 e1 -> f2 (Eff e2) r2)
-> GadtEffect f1 r1 e1
-> GadtEffect f2 r2 e2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f1 (Eff e1) r1 -> f2 (Eff e2) r2
f (f1 (Eff e1) r1 -> f2 (Eff e2) r2)
-> (GadtEffect f1 r1 e1 -> f1 (Eff e1) r1)
-> GadtEffect f1 r1 e1
-> f2 (Eff e2) r2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GadtEffect f1 r1 e1 -> f1 (Eff e1) r1
forall (f :: Effect) a (e :: Effects).
GadtEffect f a e -> f (Eff e) a
unGadtEffect

-- |
-- @
-- instance
--   (e :> es) =>
--   t'Bluefin.Compound.OneWayCoercible' ('GadtEffect' FileSystem r e) (GadtEffect FileSystem r es)
--   where
--   'Bluefin.Compound.oneWayCoercibleImpl' = 'oneWayCoercibleGadtEffectTrustMe' $ \\case
--     ReadFile path -> ReadFile path
--     WriteFile path contents -> WriteFile path contents
--     Trace msg body -> Trace msg (useImpl body)
-- @
oneWayCoercibleGadtEffectTrustMe ::
  (e :> es) =>
  (forall e' es'. (e' :> es') => f (Eff e') r -> f (Eff es') r) ->
  -- | ͘
  OneWayCoercibleD (GadtEffect f r e) (GadtEffect f r es)
oneWayCoercibleGadtEffectTrustMe :: forall (e :: Effects) (es :: Effects) (f :: Effect) r.
(e :> es) =>
(forall (e' :: Effects) (es' :: Effects).
 (e' :> es') =>
 f (Eff e') r -> f (Eff es') r)
-> OneWayCoercibleD (GadtEffect f r e) (GadtEffect f r es)
oneWayCoercibleGadtEffectTrustMe forall (e' :: Effects) (es' :: Effects).
(e' :> es') =>
f (Eff e') r -> f (Eff es') r
k = (forall (e' :: Effects) (es' :: Effects).
 (e' :> es') =>
 GadtEffect f r e' -> GadtEffect f r es')
-> OneWayCoercibleD (GadtEffect f r e) (GadtEffect f r es)
forall (e :: Effects) (es :: Effects) (h :: Effects -> *).
(e :> es) =>
(forall (e' :: Effects) (es' :: Effects).
 (e' :> es') =>
 h e' -> h es')
-> OneWayCoercibleD (h e) (h es)
oneWayCoercibleTrustMe ((f (Eff e') r -> f (Eff es') r)
-> GadtEffect f r e' -> GadtEffect f r es'
forall (f1 :: Effect) (e1 :: Effects) r1 (f2 :: Effect)
       (e2 :: Effects) r2.
(f1 (Eff e1) r1 -> f2 (Eff e2) r2)
-> GadtEffect f1 r1 e1 -> GadtEffect f2 r2 e2
mapGadtEffect f (Eff e') r -> f (Eff es') r
forall (e' :: Effects) (es' :: Effects).
(e' :> es') =>
f (Eff e') r -> f (Eff es') r
k)

-- | Version of 'send' for use when pattern matching in 'interpose'
--
-- @
-- augmentOp2Interpose ::
--   (e1 :> es, e2 :> es) =>
--   IOE e2 ->
--   t'Bluefin.HandleReader.HandleReader' (Send E) e1 ->
--   Eff es r ->
--   Eff es r
-- augmentOp2Interpose io = 'interpose' $ \\fc -> \\case
--   Op2 -> effIO io (putStrLn "augmented op2") >> send fc Op2
--   op -> 'passthrough' fc op
-- @
passthrough ::
  (Handle (GadtEffect f r), e1 :> es, e2 :> es) =>
  Send f e1 ->
  f (Eff e2) r ->
  -- | ͘
  Eff es r
passthrough :: forall (f :: Effect) r (e1 :: Effects) (es :: Effects)
       (e2 :: Effects).
(Handle (GadtEffect f r), e1 :> es, e2 :> es) =>
Send f e1 -> f (Eff e2) r -> Eff es r
passthrough Send f e1
fc = Send f e1 -> f (Eff es) r -> Eff es r
forall (e1 :: Effects) (es :: Effects) (f :: Effect) r.
(e1 :> es) =>
Send f e1 -> f (Eff es) r -> Eff es r
send Send f e1
fc (f (Eff es) r -> Eff es r)
-> (f (Eff e2) r -> f (Eff es) r) -> f (Eff e2) r -> Eff es r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GadtEffect f r es -> f (Eff es) r
forall (f :: Effect) a (e :: Effects).
GadtEffect f a e -> f (Eff e) a
unGadtEffect (GadtEffect f r es -> f (Eff es) r)
-> (f (Eff e2) r -> GadtEffect f r es)
-> f (Eff e2) r
-> f (Eff es) r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GadtEffect f r e2 -> GadtEffect f r es
forall (h :: Effects -> *) (e :: Effects) (es :: Effects).
(Handle h, e :> es) =>
h e -> h es
mapHandle (GadtEffect f r e2 -> GadtEffect f r es)
-> (f (Eff e2) r -> GadtEffect f r e2)
-> f (Eff e2) r
-> GadtEffect f r es
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Eff e2) r -> GadtEffect f r e2
forall (f :: Effect) a (e :: Effects).
f (Eff e) a -> GadtEffect f a e
MkGadtEffect

-- |
-- @
-- augmentOp2Interpose ::
--   (e1 :> es, e2 :> es) =>
--   IOE e2 ->
--   t'Bluefin.HandleReader.HandleReader' (Send E) e1 ->
--   Eff es r ->
--   Eff es r
-- augmentOp2Interpose io = 'interpose' $ \\fc -> \\case
--   Op2 -> effIO io (putStrLn "augmented op2") >> send fc Op2
--   op -> 'passthrough' fc op
-- @
interpose ::
  (e1 :> es) =>
  -- | Reimplementation of effect handler for @Send f@ in terms of the
  -- the original effect handler, which is passed as the argument
  (Send f es -> EffectHandler f es) ->
  -- | Original effect handler
  HandleReader (Send f) e1 ->
  -- | Within this block, @send@ has the implementation given above.
  Eff es r ->
  Eff es r
interpose :: forall (e1 :: Effects) (es :: Effects) (f :: Effect) r.
(e1 :> es) =>
(Send f es -> EffectHandler f es)
-> HandleReader (Send f) e1 -> Eff es r -> Eff es r
interpose Send f es -> EffectHandler f es
h HandleReader (Send f) e1
hr = HandleReader (Send f) e1
-> (Send f es -> Send f es) -> Eff es r -> Eff es r
forall (e :: Effects) (es :: Effects) (h :: Effects -> *) r.
(e :> es, Handle h) =>
HandleReader h e -> (h es -> h es) -> Eff es r -> Eff es r
localHandle HandleReader (Send f) e1
hr (\Send f es
fcOrig -> EffectHandler f es -> Send f es
forall (f :: Effect) (e :: Effects). EffectHandler f e -> Send f e
MkSend (Send f es -> EffectHandler f es
h Send f es
fcOrig))