{-# LANGUAGE RebindableSyntax, NoMonomorphismRestriction #-}

-- A simple EDSL with answer-type modifying shift/reset
-- emulate direct-style shift-reset. We can implement the examples
-- from Kenichi Asai's tutorial like list append that do require 
-- answer-type modification.

-- We rely RebindableSyntax to make the Haskell code look like
-- OChaCaml code. It is up to the reader to determine how well
-- we succeeded.

-- This code is the veneer over ShiftResetGenuine, which is
-- an implementation of the calculus lambda-sr-let
--   Polymorphic delimited continuations
--   Asai and Kameyama, APLAS 2007
--   http://logic.cs.tsukuba.ac.jp/~kam/paper/aplas07.pdf
--   hereafter, AK07
-- We try to hide the Monadish plumbing.

module SRTest where

import ShiftResetGenuine

import Prelude (Int, Show(..), (.))
import qualified Prelude

-- ------------------------------------------------------------------------
-- The examples

-- OchaCaml:
-- let f x = reset (fun () -> 3 + shift (fun k -> k) - 1) x ;;

f = reset (3 + shift (\k -> return k) - 1)

-- pure function application
tf = run (f $: 10)
-- 12


-- OchaCaml:
-- let f2 x = reset (fun () -> if shift (fun k -> k) then 1 else 2) x;;
f2 = reset (if shift (\k -> return k) then 1 else 2)
f2r = run (f2 $: true)
-- 1

-- in Haskell, we don't need eta-expand the definitions to avoid
-- the value restriction

{-
bad = reset (3 + shift (\k -> true)) - 1

    Couldn't match expected type `Int' with actual type `Prelude.Bool'
    Expected type: C Int Int Int
      Actual type: C Int Int Prelude.Bool
    In the expression: true
    In the first argument of `shift', namely `(\ k -> true)'
-}

-- The list-append example, which requires pattern-matching
-- Pattern-matching in our EDSL is a bit ungainly

-- OchaCaml:
{-
let rec id lst = match lst with
     [] -> shift (fun k -> k)
   | first :: rest -> first :: id rest ;;
 (* id : 'a list => 'a list = <fun> *)
 (* id : 'a list / 'b -> 'a list / ('a list -> 'b) = <fun> *)
-}

idl ls = ls >>= check 
 where
 check []           = shift (\k -> return k)
 check (first:rest) = return first `cons` (idl (return rest))

-- Inferred type:
-- idl :: C ([sigma] -> b) ([sigma] -> b) [sigma]
--      -> C b ([sigma] -> b) [sigma]

-- OchaCaml:
{-
 let append lst = reset (fun () -> id [1; 2; 3]) lst ;;
 (* append : int list -> int list = <fun> *)
-}
append = reset (idl (1 `cons` 2 `cons` 3 `cons` nil))
-- append :: Prelude.Num sigma => C a a ([sigma] -> [sigma])

tapp = run (append $: (4 `cons` 5 `cons` nil))
-- [1,2,3,4,5]


-- ------------------------------------------------------------------------
-- The implementation: hiding the Monadish plumbing

true, false :: (Monadish m) => m a a (Prelude.Bool)
true  = return Prelude.True
false = return Prelude.False

-- Standard arithmetic
infixl 6 +,-
infixl 7 *

(+),(-),(*) :: (Monadish m) => m b1 b Int -> m b g Int -> m b1 g Int

x + y = ((Prelude.+) `appure` x ) $: y
x - y = ((Prelude.-) `appure` x ) $: y
x * y = ((Prelude.*) `appure` x ) $: y

fromInteger = return . Prelude.fromInteger

ifThenElse e1 e2 e3 = e1 >>= \x -> case x of {Prelude.True -> e2; _ -> e3}

-- define the standard `monadic' operations
-- to be monadish instead
m >>= f = m >== f
return x = ret x
fail x = Prelude.error x
f =<< m = m >>= f

infixr 5 `cons`
cons x y = ((:) `appure` x) $: y

nil = return []

appure f m = m >>= \x -> return (f x)
infixr 0 $:
f $: m = do
	 xv <- m
	 fv <- f
	 return (fv xv)