module Pandora.Paradigm.Primary.Transformer.Continuation where

import Pandora.Core.Functor (type (:.), type (:=), type (::|:.))
import Pandora.Pattern.Category ((.), ($), (/))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Applicative (Applicative ((<*>)))
import Pandora.Pattern.Functor.Traversable (Traversable)
import Pandora.Pattern.Functor.Bindable (Bindable ((>>=)))
import Pandora.Pattern.Functor.Monad (Monad)
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))
import Pandora.Paradigm.Primary.Functor.Function ((!), (%))

newtype Continuation r t a = Continuation ((->) ::|:. a :. t := r)

instance Interpreted (Continuation r t) where
	type Primary (Continuation r t) a = (->) ::|:. a :. t := r
	run :: Continuation r t a -> Primary (Continuation r t) a
run ~(Continuation (((->) ::|:. a) :. t) := r
x) = Primary (Continuation r t) a
(((->) ::|:. a) :. t) := r
x
	unite :: Primary (Continuation r t) a -> Continuation r t a
unite = Primary (Continuation r t) a -> Continuation r t a
forall k (r :: k) (t :: k -> *) a.
((((->) ::|:. a) :. t) := r) -> Continuation r t a
Continuation

instance Covariant t => Covariant (Continuation r t) where
	a -> b
f <$> :: (a -> b) -> Continuation r t a -> Continuation r t b
<$> Continuation (((->) ::|:. a) :. t) := r
continuation = ((((->) ::|:. b) :. t) := r) -> Continuation r t b
forall k (r :: k) (t :: k -> *) a.
((((->) ::|:. a) :. t) := r) -> Continuation r t a
Continuation (((((->) ::|:. b) :. t) := r) -> Continuation r t b)
-> ((((->) ::|:. b) :. t) := r) -> Continuation r t b
forall (m :: * -> * -> *). Category m => m ~~> m
$ (((->) ::|:. a) :. t) := r
continuation ((((->) ::|:. a) :. t) := r)
-> ((b -> t r) -> a -> t r) -> (((->) ::|:. b) :. t) := r
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((b -> t r) -> (a -> b) -> a -> t r
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> b
f)

instance Covariant t => Pointable (Continuation r t) where
	point :: a :=> Continuation r t
point a
x = ((((->) ::|:. a) :. t) := r) -> Continuation r t a
forall k (r :: k) (t :: k -> *) a.
((((->) ::|:. a) :. t) := r) -> Continuation r t a
Continuation ((a -> t r) -> a -> t r
forall (m :: * -> * -> *). Category m => m ~~> m
$ a
x)

instance Covariant t => Applicative (Continuation r t) where
	Continuation r t (a -> b)
f <*> :: Continuation r t (a -> b)
-> Continuation r t a -> Continuation r t b
<*> Continuation r t a
x = ((((->) ::|:. b) :. t) := r) -> Continuation r t b
forall k (r :: k) (t :: k -> *) a.
((((->) ::|:. a) :. t) := r) -> Continuation r t a
Continuation (((((->) ::|:. b) :. t) := r) -> Continuation r t b)
-> ((((->) ::|:. b) :. t) := r) -> Continuation r t b
forall (m :: * -> * -> *). Category m => m ~~> m
$ \b -> t r
h -> Continuation r t (a -> b) -> Primary (Continuation r t) (a -> b)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Continuation r t (a -> b)
f ((((->) ::|:. (a -> b)) :. t) := r)
-> (((->) ::|:. (a -> b)) :. t) := r
forall (m :: * -> * -> *). Category m => m ~~> m
$ \a -> b
g -> Continuation r t a -> Primary (Continuation r t) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Continuation r t a
x ((((->) ::|:. a) :. t) := r) -> (((->) ::|:. a) :. t) := r
forall (m :: * -> * -> *). Category m => m ~~> m
/ b -> t r
h (b -> t r) -> (a -> b) -> a -> t r
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> b
g

instance Covariant t => Bindable (Continuation r t) where
	Continuation r t a
x >>= :: Continuation r t a
-> (a -> Continuation r t b) -> Continuation r t b
>>= a -> Continuation r t b
f = ((((->) ::|:. b) :. t) := r) -> Continuation r t b
forall k (r :: k) (t :: k -> *) a.
((((->) ::|:. a) :. t) := r) -> Continuation r t a
Continuation (((((->) ::|:. b) :. t) := r) -> Continuation r t b)
-> ((((->) ::|:. b) :. t) := r) -> Continuation r t b
forall (m :: * -> * -> *). Category m => m ~~> m
$ \b -> t r
g -> Continuation r t a -> Primary (Continuation r t) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Continuation r t a
x ((((->) ::|:. a) :. t) := r) -> (((->) ::|:. a) :. t) := r
forall (m :: * -> * -> *). Category m => m ~~> m
$ \a
y -> Continuation r t b -> (((->) ::|:. b) :. t) := r
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Continuation r t b -> (((->) ::|:. b) :. t) := r)
-> Continuation r t b -> (((->) ::|:. b) :. t) := r
forall (m :: * -> * -> *). Category m => m ~~> m
/ a -> Continuation r t b
f a
y ((((->) ::|:. b) :. t) := r) -> (((->) ::|:. b) :. t) := r
forall (m :: * -> * -> *). Category m => m ~~> m
/ b -> t r
g

instance Monad t => Monad (Continuation r t) where

instance (forall u . Bindable u) => Liftable (Continuation r) where
	lift :: u ~> Continuation r u
lift = ((((->) ::|:. a) :. u) := r) -> Continuation r u a
forall k (r :: k) (t :: k -> *) a.
((((->) ::|:. a) :. t) := r) -> Continuation r t a
Continuation (((((->) ::|:. a) :. u) := r) -> Continuation r u a)
-> (u a -> (((->) ::|:. a) :. u) := r) -> u a -> Continuation r u a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. u a -> (((->) ::|:. a) :. u) := r
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
(>>=)

-- | Call with current continuation
cwcc :: ((a -> Continuation r t b) -> Continuation r t a) -> Continuation r t a
cwcc :: ((a -> Continuation r t b) -> Continuation r t a)
-> Continuation r t a
cwcc (a -> Continuation r t b) -> Continuation r t a
f = ((((->) ::|:. a) :. t) := r) -> Continuation r t a
forall k (r :: k) (t :: k -> *) a.
((((->) ::|:. a) :. t) := r) -> Continuation r t a
Continuation (((((->) ::|:. a) :. t) := r) -> Continuation r t a)
-> ((((->) ::|:. a) :. t) := r) -> Continuation r t a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \a -> t r
g -> Continuation r t a -> (((->) ::|:. a) :. t) := r
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Continuation r t a -> (((->) ::|:. a) :. t) := r)
-> (a -> t r) -> Continuation r t a -> t r
forall a b c. (a -> b -> c) -> b -> a -> c
% a -> t r
g (Continuation r t a -> t r)
-> ((a -> Continuation r t b) -> Continuation r t a)
-> (a -> Continuation r t b)
-> t r
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> Continuation r t b) -> Continuation r t a
f ((a -> Continuation r t b) -> t r)
-> (a -> Continuation r t b) -> t r
forall (m :: * -> * -> *). Category m => m ~~> m
$ ((((->) ::|:. b) :. t) := r) -> Continuation r t b
forall k (r :: k) (t :: k -> *) a.
((((->) ::|:. a) :. t) := r) -> Continuation r t a
Continuation (((((->) ::|:. b) :. t) := r) -> Continuation r t b)
-> (a -> (((->) ::|:. b) :. t) := r) -> a -> Continuation r t b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (!) (t r -> (((->) ::|:. b) :. t) := r)
-> (a -> t r) -> a -> (((->) ::|:. b) :. t) := r
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> t r
g

-- | Delimit the continuation of any 'shift'
reset :: (forall u . Bindable u, Monad t, Traversable t) => Continuation r t r -> Continuation s t r
reset :: Continuation r t r -> Continuation s t r
reset = t r -> Continuation s t r
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (t r -> Continuation s t r)
-> (Continuation r t r -> t r)
-> Continuation r t r
-> Continuation s t r
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Continuation r t r -> (((->) ::|:. r) :. t) := r
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Continuation r t r -> (((->) ::|:. r) :. t) := r)
-> (r :=> t) -> Continuation r t r -> t r
forall a b c. (a -> b -> c) -> b -> a -> c
% r :=> t
forall (t :: * -> *) a. Pointable t => a :=> t
point

-- | Capture the continuation up to the nearest enclosing 'reset' and pass it
shift :: Pointable t => ((a -> t r) -> Continuation r t r) -> Continuation r t a
shift :: ((a -> t r) -> Continuation r t r) -> Continuation r t a
shift (a -> t r) -> Continuation r t r
f = ((((->) ::|:. a) :. t) := r) -> Continuation r t a
forall k (r :: k) (t :: k -> *) a.
((((->) ::|:. a) :. t) := r) -> Continuation r t a
Continuation (((((->) ::|:. a) :. t) := r) -> Continuation r t a)
-> ((((->) ::|:. a) :. t) := r) -> Continuation r t a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Continuation r t r -> (((->) ::|:. r) :. t) := r
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Continuation r t r -> (((->) ::|:. r) :. t) := r)
-> (r :=> t) -> Continuation r t r -> t r
forall a b c. (a -> b -> c) -> b -> a -> c
% r :=> t
forall (t :: * -> *) a. Pointable t => a :=> t
point (Continuation r t r -> t r)
-> ((a -> t r) -> Continuation r t r) -> (((->) ::|:. a) :. t) := r
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> t r) -> Continuation r t r
f

interruptable :: Pointable t => ((a -> Continuation a t a) -> Continuation a t a) -> t a
interruptable :: ((a -> Continuation a t a) -> Continuation a t a) -> t a
interruptable = Continuation a t a -> (((->) ::|:. a) :. t) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Continuation a t a -> (((->) ::|:. a) :. t) := a)
-> (a :=> t) -> Continuation a t a -> t a
forall a b c. (a -> b -> c) -> b -> a -> c
% a :=> t
forall (t :: * -> *) a. Pointable t => a :=> t
point (Continuation a t a -> t a)
-> (((a -> Continuation a t a) -> Continuation a t a)
    -> Continuation a t a)
-> ((a -> Continuation a t a) -> Continuation a t a)
-> t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((a -> Continuation a t a) -> Continuation a t a)
-> Continuation a t a
forall k a (r :: k) (t :: k -> *) b.
((a -> Continuation r t b) -> Continuation r t a)
-> Continuation r t a
cwcc