{-# LANGUAGE AllowAmbiguousTypes #-}
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 #-}