{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Primary.Transformer.Continuation where

import Pandora.Core.Functor (type (:.), type (:=), type (::|:.))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category (($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-)))
import Pandora.Pattern.Functor.Monoidal (Monoidal)
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.Algebraic.Exponential ((!.), (%))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:))
import Pandora.Paradigm.Primary.Algebraic (point)

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 :: * -> * -> *) a b. Category m => 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.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((b -> t r) -> (a -> b) -> a -> t r
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> b
f)

instance Covariant (->) (->) t => Bindable (->) (Continuation r t) where
	a -> Continuation r t b
f =<< :: (a -> Continuation r t 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 (m a b) (m a b)
$ \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 :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \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 :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Continuation r t b
f a
y ((((->) ::|:. b) :. t) := r) -> (((->) ::|:. b) :. t) := r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# b -> t r
g

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

instance (forall u . Bindable (->) u) => Liftable (->) (Continuation r) where
	lift :: u a -> Continuation r u a
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.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((a -> u r) -> u a -> u r) -> u a -> (((->) ::|:. a) :. u) := r
forall a b c. (a -> b -> c) -> b -> a -> c
(%) (a -> u r) -> u a -> u r
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (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 (m a b) (m a b)
$ \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.
Semigroupoid 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 (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.
Semigroupoid m =>
m b c -> m a b -> m a c
. t r -> (((->) ::|:. b) :. t) := r
forall a b. a -> b -> a
(!.) (t r -> (((->) ::|:. b) :. t) := r)
-> (a -> t r) -> a -> (((->) ::|:. b) :. t) := r
forall (m :: * -> * -> *) b c a.
Semigroupoid 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) => 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 (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
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.
Semigroupoid 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 r) -> Continuation r t r -> t r
forall a b c. (a -> b -> c) -> b -> a -> c
% r -> t r
forall (t :: * -> *) a.
Monoidal (->) (->) (:*:) (:*:) t =>
a -> t a
point)

-- | Capture the continuation up to the nearest enclosing 'reset' and pass it
shift :: Monoidal (->) (->) (:*:) (:*:) 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 (m a b) (m a b)
$ (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 r) -> Continuation r t r -> t r
forall a b c. (a -> b -> c) -> b -> a -> c
% r -> t r
forall (t :: * -> *) a.
Monoidal (->) (->) (:*:) (:*:) t =>
a -> t a
point) (Continuation r t r -> t r)
-> ((a -> t r) -> Continuation r t r) -> (((->) ::|:. a) :. t) := r
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> t r) -> Continuation r t r
f

interruptable :: Monoidal (->) (->) (:*:) (:*:) 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 a) -> Continuation a t a -> t a
forall a b c. (a -> b -> c) -> b -> a -> c
% a -> t a
forall (t :: * -> *) a.
Monoidal (->) (->) (:*:) (:*:) t =>
a -> t a
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.
Semigroupoid 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