{-# LANGUAGE AllowAmbiguousTypes #-}

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

module Data.Effect.ShiftReset where

import Control.Monad ((>=>))
import Data.Effect.Key (KeyH (KeyH))
import Data.Functor (void)

data Shift' (ans :: Type) n m a where
    Shift
        :: forall ans n m a
         . ((a -> n ans) -> (forall x. m x -> n x) -> n ans)
        -> Shift' ans n m a
makeKeyedEffect [] [''Shift']

callCC
    :: forall a m ans n
     . (SendHOEBy ShiftKey (Shift' ans n) m, Monad m, Monad n)
    => ((a -> n ans) -> m a)
    -> m a
callCC :: forall a (m :: * -> *) ans (n :: * -> *).
(SendHOEBy ShiftKey (Shift' ans n) m, Monad m, Monad n) =>
((a -> n ans) -> m a) -> m a
callCC (a -> n ans) -> m a
f = ((a -> n ans) -> (forall x. m x -> n x) -> n ans) -> m a
forall ans (n :: * -> *) a (m :: * -> *).
SendHOEBy ShiftKey (Shift' ans n) m =>
((a -> n ans) -> (forall x. m x -> n x) -> n ans) -> m a
shift \a -> n ans
k forall x. m x -> n x
run -> m a -> n a
forall x. m x -> n x
run ((a -> n ans) -> m a
f ((a -> n ans) -> m a) -> (a -> n ans) -> m a
forall a b. (a -> b) -> a -> b
$ a -> n ans
k (a -> n ans) -> (ans -> n ans) -> a -> n ans
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> m ans -> n ans
forall x. m x -> n x
run (m ans -> n ans) -> (ans -> m ans) -> ans -> n ans
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ans -> m ans
forall a (m :: * -> *) ans (n :: * -> *).
(SendHOEBy ShiftKey (Shift' ans n) m, Applicative n) =>
ans -> m a
exit) n a -> (a -> n ans) -> n ans
forall a b. n a -> (a -> n b) -> n b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> n ans
k

exit
    :: forall a m ans n
     . (SendHOEBy ShiftKey (Shift' ans n) m, Applicative n)
    => ans
    -> m a
exit :: forall a (m :: * -> *) ans (n :: * -> *).
(SendHOEBy ShiftKey (Shift' ans n) m, Applicative n) =>
ans -> m a
exit ans
ans = ((a -> n ans) -> (forall x. m x -> n x) -> n ans) -> m a
forall ans (n :: * -> *) a (m :: * -> *).
SendHOEBy ShiftKey (Shift' ans n) m =>
((a -> n ans) -> (forall x. m x -> n x) -> n ans) -> m a
shift \a -> n ans
_ forall x. m x -> n x
_ -> ans -> n ans
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ans
ans
{-# INLINE exit #-}

getCC
    :: forall m ans n
     . (SendHOEBy ShiftKey (Shift' ans n) m, Monad m, Monad n)
    => m (n ans)
getCC :: forall (m :: * -> *) ans (n :: * -> *).
(SendHOEBy ShiftKey (Shift' ans n) m, Monad m, Monad n) =>
m (n ans)
getCC = ((n ans -> n ans) -> m (n ans)) -> m (n ans)
forall a (m :: * -> *) ans (n :: * -> *).
(SendHOEBy ShiftKey (Shift' ans n) m, Monad m, Monad n) =>
((a -> n ans) -> m a) -> m a
callCC \n ans -> n ans
exit' -> let a :: n ans
a = n ans -> n ans
exit' n ans
a in n ans -> m (n ans)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure n ans
a

embed :: forall m ans n. (SendHOEBy ShiftKey (Shift' ans n) m, Monad n) => n ~> m
embed :: forall (m :: * -> *) ans (n :: * -> *).
(SendHOEBy ShiftKey (Shift' ans n) m, Monad n) =>
n ~> m
embed n x
m = ((x -> n ans) -> (forall x. m x -> n x) -> n ans) -> m x
forall ans (n :: * -> *) a (m :: * -> *).
SendHOEBy ShiftKey (Shift' ans n) m =>
((a -> n ans) -> (forall x. m x -> n x) -> n ans) -> m a
shift \x -> n ans
k forall x. m x -> n x
_ -> n x
m n x -> (x -> n ans) -> n ans
forall a b. n a -> (a -> n b) -> n b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= x -> n ans
k
{-# INLINE embed #-}

data Shift_' n m a where
    Shift_'
        :: (forall (ans :: Type). (a -> n ans) -> (forall x. m x -> n x) -> n ans)
        -> Shift_' n m a
makeKeyedEffect [] [''Shift_']

getCC_ :: forall m n. (SendHOEBy Shift_Key (Shift_' n) m, Functor n) => m (n ())
getCC_ :: forall (m :: * -> *) (n :: * -> *).
(SendHOEBy Shift_Key (Shift_' n) m, Functor n) =>
m (n ())
getCC_ = (forall ans. (n () -> n ans) -> (forall x. m x -> n x) -> n ans)
-> m (n ())
forall a (n :: * -> *) (m :: * -> *).
SendHOEBy Shift_Key (Shift_' n) m =>
(forall ans. (a -> n ans) -> (forall x. m x -> n x) -> n ans)
-> m a
shift_' \n () -> n ans
k forall x. m x -> n x
_ -> let k' :: n ans
k' = n () -> n ans
k (n () -> n ans) -> n () -> n ans
forall a b. (a -> b) -> a -> b
$ n ans -> n ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void n ans
k' in n ans
k'

data Reset m (a :: Type) where
    Reset :: m a -> Reset m a
makeEffectH [''Reset]

data ShiftF ans a where
    ShiftF :: forall ans a. ((a -> ans) -> ans) -> ShiftF ans a
makeEffectF [''ShiftF]

fromShiftF :: ShiftF (n ans) ~> Shift ans n m
fromShiftF :: forall (n :: * -> *) ans (m :: * -> *) x.
ShiftF (n ans) x -> Shift ans n m x
fromShiftF (ShiftF (x -> n ans) -> n ans
f) = Shift' ans n m x -> KeyH ShiftKey (Shift' ans n) m x
forall {k} (key :: k) (sig :: (* -> *) -> * -> *) (f :: * -> *) a.
sig f a -> KeyH key sig f a
KeyH (Shift' ans n m x -> KeyH ShiftKey (Shift' ans n) m x)
-> Shift' ans n m x -> KeyH ShiftKey (Shift' ans n) m x
forall a b. (a -> b) -> a -> b
$ ((x -> n ans) -> (forall x. m x -> n x) -> n ans)
-> Shift' ans n m x
forall ans (n :: * -> *) (m :: * -> *) a.
((a -> n ans) -> (forall x. m x -> n x) -> n ans)
-> Shift' ans n m a
Shift \x -> n ans
k forall x. m x -> n x
_ -> (x -> n ans) -> n ans
f x -> n ans
k
{-# INLINE fromShiftF #-}

exitF :: forall ans m a. (ShiftF ans <: m) => ans -> m a
exitF :: forall ans (m :: * -> *) a. (ShiftF ans <: m) => ans -> m a
exitF ans
ans = forall ans a (f :: * -> *).
SendFOE (ShiftF ans) f =>
((a -> ans) -> ans) -> f a
shiftF @ans (((a -> ans) -> ans) -> m a) -> ((a -> ans) -> ans) -> m a
forall a b. (a -> b) -> a -> b
$ ans -> (a -> ans) -> ans
forall a b. a -> b -> a
const ans
ans
{-# INLINE exitF #-}

embedF :: forall ans n m. (ShiftF (n ans) <: m, Monad n) => n ~> m
embedF :: forall ans (n :: * -> *) (m :: * -> *).
(ShiftF (n ans) <: m, Monad n) =>
n ~> m
embedF n x
m = forall ans a (f :: * -> *).
SendFOE (ShiftF ans) f =>
((a -> ans) -> ans) -> f a
shiftF @(n ans) (n x
m >>=)
{-# INLINE embedF #-}