interp2.ml

(* A tagless-final embedding of the language with shift/reset
   operators and fully supported answer-type modification (ATM).

   This implementation is based on the prompt-passing translation
   described in the paper "ATM without tears: prompt-passing style
   transformation for typed delimited-control operators"
   http://ebooks.au.dk/index.php/aul/catalog/view/4/4/31-1
 *)

open Delimcc;;

(*
  The Symantics of Source Calculi
 *)
module type Sym = sig
    type 't pure               (* pure expression *)
    type ('t, 'a, 'b) eff      (* effectful expression *)
    type ('s, 't, 'a, 'b) efun (* effectful function *)
    type ('s, 't) pfun         (* pure function *)

    val const : 't -> 't pure

    val lam : ('s pure -> ('t, 'a, 'b) eff) -> ('s, 't, 'a, 'b) efun pure
    val app : (('s, 't, 'a, 'b) efun, 'b, 'c) eff -> ('s, 'c, 'd) eff -> ('t, 'a, 'd) eff

    val appP : ('s, 't) pfun pure -> 's pure -> 't pure

    val shift : (('t, 'a) pfun pure -> 'b pure) -> ('t, 'a, 'b) eff
    val reset : ('s, 's, 't) eff -> 't pure

    val exp : 't pure -> ('t, 'a, 'a) eff
    val run : 't pure -> 't
  end

(*
   Interpretation with Prompt-Passing Style Transformation
 *)
module R = struct
  (* Translation for types and typings *)
  type 't pure = unit -> 't
  type ('t, 'a, 'b) eff = 'b prompt -> 'a prompt -> 't
  type ('s, 't, 'a, 'b) efun = 's pure -> ('t, 'a, 'b) eff
  type ('s, 't) pfun = 's pure -> 't pure

  (* lambda v. Omega *)
  let coerce _ = failwith "unreachable"

  let wrap x : 'a pure = fun () -> x
  let unwrap : 'a pure -> 'a = fun x -> x ()

  let const x = wrap x

  let lam f = wrap f

  let app e1 (e2: ('s, 'c, 'd ) eff) : ('t, 'a, 'd) eff =
    fun p q ->
    let r, s = new_prompt (), new_prompt () in
    let v2 = wrap @@ e2 p r in
    let v1 = e1 r s in
    v1 v2 s q

  let appP e1 e2 : 't pure =
    fun () ->
    let v2 = unwrap e2 in
    let v1 = unwrap e1 in
    v1 (wrap v2) ()

  let shift f : ('t, 'a, 'b) eff =
    fun p q ->
    Delimcc.shift p
      (fun k' ->
       unwrap @@ f @@ wrap (fun y ->
			    wrap @@ push_prompt q (fun () -> coerce (k' @@ unwrap y ))))

  let reset e =
    fun () ->
    let p, q = new_prompt (), new_prompt () in
    push_prompt p (fun () -> abort q @@ e p q)
		    
  let exp e =
    fun p q -> Delimcc.shift p (fun k -> push_prompt q (fun () -> k @@ unwrap e))

  let run (x: 't pure) : 't = x ()
end

module T1 (S: Sym) = struct
  open S
  let res1 = run (const 10)
  let res2' = reset (shift (fun k -> appP k (appP k (const 1))))
  let res2 = run res2'
  let res3 = run @@ reset @@ app (exp @@ lam @@ fun x -> exp @@ x) (exp @@ const 10)
end
let _ = let module M = T1(R) in M.res1 (* => 10 *)
let _ = let module M = T1(R) in M.res2 (* => 1 *)
let _ = let module M = T1(R) in M.res3 (* => 10 *)

(*
  Symantics for the Extended Language
 *)
module type SymP = sig
    include Sym

    (* 2-arg primitive *)
    val p2E : ('s -> 't -> 'u) -> ('s, 'a, 'b) eff -> ('t, 'b, 'c) eff -> ('u, 'a, 'c) eff
    (* 1-arg primitive *)
    val pE: ('t -> 'u) -> ('t, 'a, 'a) eff -> ('u, 'a, 'a) eff

    (* if *)
    val ifE : (bool, 'b, 'c) eff -> ('t, 'a, 'b) eff -> ('t, 'a, 'b) eff -> ('t, 'a, 'c) eff
    (* fixpoint operator *)
    val fixE : (('s, 't, 'a, 'b) efun pure -> 's pure -> ('t, 'a, 'b) eff) -> ('s, 't, 'a, 'b) efun pure
  end

module RP = struct
  include R

  let p2E f e1 e2 = fun p q ->
    let r = new_prompt () in
    let v2 = e2 p r in
    let v1 = e1 r q in
    f v1 v2

  let pE f x = fun p q -> f (x p q)

  let ifE b e e' = fun p q ->
    let r = new_prompt () in
    if b p r then e r q else e' r q

  let rec fixE (f: ('s, 't, 'a, 'b) efun pure -> 's pure -> (('t, 'a, 'b) eff)) : ('s, 't, 'a, 'b) efun pure =
    lam (fun x -> f (fun x -> fixE f x) x)
end

(*
  Examples for List Operations

  These examples are taken form [AK07]
 *)
module LIST (S: SymP) = struct
  open S

  (* List Operatoins *)
  let list x = const x
  let (@*) x y = p2E (fun x y -> x :: y) x y
  let head x = pE List.hd x
  let tail x = pE List.tl x
  let null x = pE (fun x -> x = []) @@ exp x

  (* Turn pure functions (continuations) to effectful functions *)
  let exp2 f = exp @@ lam (fun x -> exp @@ appP f x)

  let append = fixE (fun f x ->
		     ifE (null x)
			 (shift (fun k -> k))
			 (head (exp x) @* app (exp f) (tail @@ exp x)))

  let res1 = run @@ reset @@ app (exp2 @@ reset (app (exp append) (exp @@ list [1;2;3])))
				 (exp @@ list [4;5;6])

  let prefix = fixE (fun f x ->
		     ifE (null x)
			 (shift (fun k -> list []))
			 (head (exp x) @* shift (fun k -> reset @@
					   (exp (appP k (list [])))
					   @* (exp (reset @@ app (exp2 k)
								 (app (exp f) (tail @@ exp x)))))))
  let res2 = run @@ reset @@ app (exp prefix) (exp @@ list [1;2;3])
end
let _ = let module M = LIST(RP) in M.res1 (* => [1; 2; 3; 4; 5; 6] *)
let _ = let module M = LIST(RP) in M.res2 (* => [[1]; [1; 2]; [1; 2; 3]] *)

(*
  The sprintf example taken from [As09]

  In this implementation, embedded functions are restricted to monomorphic.
 *)
module SPRINTF (S: SymP) = struct
  open S

  let s_int = lam (fun x -> pE string_of_int (exp x))
  let fmt = exp @@ lam (fun to_str ->
			shift (fun k ->
			       lam (fun x -> exp @@ appP k (reset @@ app (exp to_str) (exp x)))))
  let lit = exp @@ lam (fun str -> exp str)
  let (^^) = p2E (^)

  let res = run @@ reset @@
	       app (exp @@ reset ((app lit (exp @@ const "Hello")) ^^ (app fmt (exp @@ s_int))))
		   (exp @@ const 100)
end
let _ = let module M = SPRINTF(RP) in M.res (* => "Hello100" *)