{-# LANGUAGE
  BangPatterns,
  DeriveAnyClass,
  GADTs,
  RankNTypes,
  ScopedTypeVariables,
  StandaloneKindSignatures,
  TypeOperators #-}

-- | = Algebraic effects and named handlers
--
-- Variant of "Bluefin.Algae" using dynamic exceptions to cancel continuations.
module Bluefin.Algae.DynExn
  ( AEffect
  , HandlerBody
  , Handler
  , handle
  , call
  , continue
  , discontinue
  , discontinueIO
  , cancel
  , CancelContinuation(..)
  ) where

import Control.Exception (Exception)
import Data.Kind (Type)
import Data.Functor (void)
import Bluefin.Internal (Eff, Effects, type (:&), type (:>), IOE)
import Bluefin.Algae.DelCont (PromptTag, Continuation, reset, shift0, resume, continue)
import Bluefin.Exception.Dynamic
import Bluefin.Algae (AEffect)

-- | Interpretation of an algebraic effect @f@: a function to handle the operations of @f@
-- with cancellable continuations.
type HandlerBody :: Effects -> AEffect -> Effects -> Type -> Type
type HandlerBody ex f ss a = (forall x ss0. ex :> ss0 => f x -> Continuation ss0 ss x a -> Eff ss a)

-- | Handler to call operations of the effect @f@ with cancellable continuations.
type Handler :: Effects -> AEffect -> Effects -> Type
data Handler ex f s where
  MkHandler :: !(PromptTag ss a s) -> HandlerBody ex f ss a -> Handler ex f s

-- | Handle operations of @f@ with cancellable continuations.
--
-- The handle for exceptions (first argument) is only there to guide type inference.
-- it can be either 'IOE' or 'DynExn'.
handle ::
  h ex ->
  HandlerBody ex f ss a ->
  (forall s. Handler ex f s -> Eff (s :& ss) a) ->
  Eff ss a
handle :: forall (h :: Effects -> *) (ex :: Effects) (f :: AEffect)
       (ss :: Effects) a.
h ex
-> HandlerBody ex f ss a
-> (forall (s :: Effects). Handler ex f s -> Eff (s :& ss) a)
-> Eff ss a
handle h ex
_ HandlerBody ex f ss a
h forall (s :: Effects). Handler ex f s -> Eff (s :& ss) a
act = (forall (s :: Effects). PromptTag ss a s -> Eff (s :& ss) a)
-> Eff ss a
forall a (ss :: Effects).
(forall (s :: Effects). PromptTag ss a s -> Eff (s :& ss) a)
-> Eff ss a
reset (\PromptTag ss a s
p -> Handler ex f s -> Eff (s :& ss) a
forall (s :: Effects). Handler ex f s -> Eff (s :& ss) a
act (PromptTag ss a s -> HandlerBody ex f ss a -> Handler ex f s
forall (ss :: Effects) a (s :: Effects) (ex :: Effects)
       (f :: AEffect).
PromptTag ss a s -> HandlerBody ex f ss a -> Handler ex f s
MkHandler PromptTag ss a s
p f x -> Continuation ss0 ss x a -> Eff ss a
HandlerBody ex f ss a
h))

-- | Call an operation of @f@ with cancellable continuations.
call :: (ex :> es, s :> es) => Handler ex f s -> f a -> Eff es a
call :: forall (ex :: Effects) (es :: Effects) (s :: Effects)
       (f :: AEffect) a.
(ex :> es, s :> es) =>
Handler ex f s -> f a -> Eff es a
call (MkHandler PromptTag ss a s
p HandlerBody ex f ss a
h) f a
op = PromptTag ss a s
-> (Continuation es ss a a -> Eff ss a) -> Eff es a
forall (s :: Effects) a b (ss :: Effects) (ss0 :: Effects).
(s :> ss0) =>
PromptTag ss a s
-> (Continuation ss0 ss b a -> Eff ss a) -> Eff ss0 b
shift0 PromptTag ss a s
p (\Continuation es ss a a
k -> f a -> Continuation es ss a a -> Eff ss a
HandlerBody ex f ss a
h f a
op Continuation es ss a a
k)

-- | Resume by throwing a dynamic exception.
--
-- Note that different outcomes are possible depending on your handled computation.
-- Be sure to handle them appropriately.
--
-- - A common situation is that the continuation will rethrow the initial exception,
--   then you can just catch it (or use 'cancel').
-- - The continuation may throw a different exception, so you should be
--   careful to catch the right exception.
-- - The continuation may also catch your exception and terminate normally
--   with a result of type @a@.
discontinue :: (Exception e, ex :> es0) => DynExn ex -> Continuation es0 es b a -> e -> Eff es a
discontinue :: forall e (ex :: Effects) (es0 :: Effects) (es :: Effects) b a.
(Exception e, ex :> es0) =>
DynExn ex -> Continuation es0 es b a -> e -> Eff es a
discontinue DynExn ex
ex Continuation es0 es b a
k e
e = Continuation es0 es b a -> Eff es0 b -> Eff es a
forall (t :: Effects) (s :: Effects) b a.
Continuation t s b a -> Eff t b -> Eff s a
resume Continuation es0 es b a
k (DynExn ex -> e -> Eff es0 b
forall e (ex :: Effects) (es :: Effects) a.
(Exception e, ex :> es) =>
DynExn ex -> e -> Eff es a
throw DynExn ex
ex e
e)

-- | Specialization of 'discontinue' to 'IOE'.
discontinueIO :: (Exception e, io :> es0) => IOE io -> Continuation es0 es b a -> e -> Eff es a
discontinueIO :: forall e (io :: Effects) (es0 :: Effects) (es :: Effects) b a.
(Exception e, io :> es0) =>
IOE io -> Continuation es0 es b a -> e -> Eff es a
discontinueIO IOE io
io = DynExn io -> Continuation es0 es b a -> e -> Eff es a
forall e (ex :: Effects) (es0 :: Effects) (es :: Effects) b a.
(Exception e, ex :> es0) =>
DynExn ex -> Continuation es0 es b a -> e -> Eff es a
discontinue (IOE io -> DynExn io
forall (io :: Effects). IOE io -> DynExn io
ioeToDynExn IOE io
io)

-- | 'discontinue' a continuation with the v'CancelContinuation' exception and catch it when it
-- is re-thrown by the continuation.
--
-- The continuation SHOULD re-throw v'CancelContinuation' if it catches it.
cancel :: (ex :> es0, ex :> es) => DynExn ex -> Continuation es0 es b a -> Eff es ()
cancel :: forall (ex :: Effects) (es0 :: Effects) (es :: Effects) b a.
(ex :> es0, ex :> es) =>
DynExn ex -> Continuation es0 es b a -> Eff es ()
cancel DynExn ex
ex Continuation es0 es b a
k = DynExn ex
-> Eff es () -> (CancelContinuation -> Eff es ()) -> Eff es ()
forall e (ex :: Effects) (es :: Effects) a.
(Exception e, ex :> es) =>
DynExn ex -> Eff es a -> (e -> Eff es a) -> Eff es a
catch DynExn ex
ex (Eff es a -> Eff es ()
forall (f :: AEffect) a. Functor f => f a -> f ()
void (DynExn ex
-> Continuation es0 es b a -> CancelContinuation -> Eff es a
forall e (ex :: Effects) (es0 :: Effects) (es :: Effects) b a.
(Exception e, ex :> es0) =>
DynExn ex -> Continuation es0 es b a -> e -> Eff es a
discontinue DynExn ex
ex Continuation es0 es b a
k CancelContinuation
CancelContinuation)) (\CancelContinuation
CancelContinuation -> () -> Eff es ()
forall a. a -> Eff es a
forall (f :: AEffect) a. Applicative f => a -> f a
pure ())

-- | Exception thrown by 'cancel'.
data CancelContinuation = CancelContinuation
  deriving (Int -> CancelContinuation -> ShowS
[CancelContinuation] -> ShowS
CancelContinuation -> String
(Int -> CancelContinuation -> ShowS)
-> (CancelContinuation -> String)
-> ([CancelContinuation] -> ShowS)
-> Show CancelContinuation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CancelContinuation -> ShowS
showsPrec :: Int -> CancelContinuation -> ShowS
$cshow :: CancelContinuation -> String
show :: CancelContinuation -> String
$cshowList :: [CancelContinuation] -> ShowS
showList :: [CancelContinuation] -> ShowS
Show, Show CancelContinuation
Typeable CancelContinuation
(Typeable CancelContinuation, Show CancelContinuation) =>
(CancelContinuation -> SomeException)
-> (SomeException -> Maybe CancelContinuation)
-> (CancelContinuation -> String)
-> Exception CancelContinuation
SomeException -> Maybe CancelContinuation
CancelContinuation -> String
CancelContinuation -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e) -> (e -> String) -> Exception e
$ctoException :: CancelContinuation -> SomeException
toException :: CancelContinuation -> SomeException
$cfromException :: SomeException -> Maybe CancelContinuation
fromException :: SomeException -> Maybe CancelContinuation
$cdisplayException :: CancelContinuation -> String
displayException :: CancelContinuation -> String
Exception)