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.Primary.Functor.Function ((!), (%))

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

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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ (((->) ::|:. 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ \b -> t r
h -> Continuation r t (a -> b) -> (((->) ::|:. (a -> b)) :. t) := r
forall k (r :: k) (t :: k -> *) a.
Continuation r t a -> (((->) ::|:. a) :. t) := r
continue Continuation r t (a -> b)
f ((((->) ::|:. (a -> b)) :. t) := r)
-> (((->) ::|:. (a -> b)) :. t) := r
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ \a -> b
g -> Continuation r t a -> (((->) ::|:. a) :. t) := r
forall k (r :: k) (t :: k -> *) a.
Continuation r t a -> (((->) ::|:. a) :. t) := r
continue Continuation r t a
x (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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ \b -> t r
g -> Continuation r t a -> (((->) ::|:. a) :. t) := r
forall k (r :: k) (t :: k -> *) a.
Continuation r t a -> (((->) ::|:. a) :. t) := r
continue Continuation r t a
x ((((->) ::|:. a) :. t) := r) -> (((->) ::|:. a) :. t) := r
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ \a
y -> Continuation r t b -> (((->) ::|:. b) :. t) := r
forall k (r :: k) (t :: k -> *) a.
Continuation r t a -> (((->) ::|:. a) :. t) := r
continue (a -> Continuation r t b
f a
y) 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ \a -> t r
g -> Continuation r t a -> (((->) ::|:. a) :. t) := r
forall k (r :: k) (t :: k -> *) a.
Continuation r t a -> (((->) ::|:. a) :. t) := r
continue (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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ ((((->) ::|:. 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 k (r :: k) (t :: k -> *) a.
Continuation r t a -> (((->) ::|:. a) :. t) := r
continue (Continuation r t r -> (((->) ::|:. r) :. t) := r)
-> (r -> t r) -> Continuation r t r -> t r
forall a b c. (a -> b -> c) -> b -> a -> c
% r -> t r
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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ Continuation r t r -> (((->) ::|:. r) :. t) := r
forall k (r :: k) (t :: k -> *) a.
Continuation r t a -> (((->) ::|:. a) :. t) := r
continue (Continuation r t r -> (((->) ::|:. r) :. t) := r)
-> (r -> t r) -> Continuation r t r -> t r
forall a b c. (a -> b -> c) -> b -> a -> c
% r -> t r
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 k (r :: k) (t :: k -> *) a.
Continuation r t a -> (((->) ::|:. a) :. t) := r
continue (Continuation a t a -> (((->) ::|:. a) :. t) := a)
-> (a -> t a) -> Continuation a t a -> t a
forall a b c. (a -> b -> c) -> b -> a -> c
% a -> t a
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