(** Delimited dynamic binding in OCaml. Tests and examples.

   Joint work with Chung-chieh Shan and Amr Sabry.

   $Id: vdynvar.ml,v 1.1 2006/04/10 02:25:32 oleg Exp $
*)

open Dynvar

(* First test *)
let testc = 
  let p = dnew () in
   dlet p 0 (fun () -> 
   let f = fun () -> dref p in
   let x = f () in
   let y = dlet p 1 (fun () -> f ()) in
   let z = f () in
   (x,y,z))
(* (0,1,0) *)

(* Demonstration of dref and dset *)
let test12 =
  let p = dnew () in
  dlet p 1 (fun () ->
    let v1 = dref p in
    let v2 = dlet p 2 (fun () ->
      let v3 = dset p 12 in
      let v4 = dref p in
      (v3,v4)) in
    let v5 = dref p in
    (v1,v2,v5))
(* (1, (2, 12), 1) *)


(* Chung-chieh Shan's example: treating the execution context as an
   inductive data structure: a list
*)

let dnil  p body   = dlet p None body
let dcons p v body = dlet p (Some v) body
let rec dmemberp p v = dupp p 
    (function 
      |	None -> false
      | Some y -> v == y || dmemberp p v)

let testa =
  let p = dnew () in
  dnil p (fun () ->
    dcons p 1 (fun () ->
      dcons p 2 (fun () ->
	(dmemberp p 2, dmemberp p 1, dmemberp p 3))))
(* (true,true,false) *)


(* Chung-chieh Shan's nub example *)
(* nub is a function that removes duplicates from the input list,
   while maintaining the order otherwise: if an element occurs
   several times in the input list, only its _first_ occurrence remains
   in the output list.
   Our function below assumes only equality on the elements of the list;
   we do _not_ assume any order relation for the list elements and
   so can't use sort.
*)
let nub lst =
  let p = dnew () in
  let rec nub' = 
    function 
      |	[] -> []
      |	(h::t) -> 
	  if dmemberp p h (* h has been seen before *)
	      then nub' t
	      else dcons p h (fun () -> (h :: nub' t))
  in dnil p (fun () -> nub' lst)

let test_nub = nub [1;1;1;1;1;1;1;1;1;1;3;2;1;1;1;1;1;1;2;1;1;1]
;;
(* [1;3;2] *)


(*------------------------------------------------------------------------*)
(* Demonstrate delimited continuations and cooperative threads.
   The latter are implemented via the delimited continuations.

   The salient feature of the example is a _partial_ inheritance 
   of the dynamic environment. At thread creation time, we can designate
   which dynamic variables are to be private to the thread and which can be
   shared with the parent (and other threads). Any new dynamic variable
   used in a thread is automatically private to the thread.

   Mutation of a `shared' parameter is visible to everyone; mutation to the
   private one is visible only in the corresponding thread. That behavior
   is inherent in the implementation; we don't need to do anything
   special for it. To designate a parameter `private', we merely need to
   add a dummy binding for it: dlet p (dref p) ... No special syntax 
   is needed.

   The example below uses delimited continuations (shift) to create and
   cooperatively run two `threads'
*)


(* We need the caml-shift library Delimcc:
   http://pobox.com/~oleg/ftp/continuations/implementations.html#caml-shift
*)

open Delimcc

(* captured delimited continuations are recursive *)
type ('a,'b) reck = 
    J of ('a -> ('a,'b) reck)
  | R of 'b

let shift p f = take_subcont p (fun sk () ->
  push_prompt p (fun () -> (f (fun v -> 
    push_prompt p (fun () -> push_subcont sk (fun () -> v))))))


let parmp = dnew ()	(* will be private in threads *)
let parms = dnew ()	(* this parameter will be `shared' *)


let tf1 title =		(* Just print the current dynamic environment *)
   Printf.printf "%s: private %d, shared %d\n" title (dref parmp) (dref parms)

let test_thread () =
   let p0 = new_prompt () in
   let yield () = shift p0 (fun f -> J f) in
   let runt thunk = 
     (match thunk () with | J thunk -> thunk
                          | R () -> failwith "thread is finished") in
   dlet parmp 1 (fun () ->
   dlet parms 500 (fun () ->
   let thread1 = runt (fun () ->
     push_prompt p0 (fun () ->
     dlet parmp (dref parmp) (fun () -> (* this line makes parmp private *)
       tf1 "thread1: starting";
       dlet parmp 10 (fun () ->
       yield ();
       tf1 "thread1: continuing...";
       ignore (dset parmp 11);	 (* mutate both parameters *)
       ignore (dset parms 600);
       yield ();
       tf1 "thread1: finishing, after dlet...";
       R ())))) in
   let thread2 = runt (fun () ->
     dlet parmp 2 (fun () ->
     push_prompt p0 (fun () ->
     dlet parmp (dref parmp) (fun () -> (* this line makes parmp private *)
       tf1 "thread2: starting";
       yield ();
       tf1 "thread2: continuing...";
       dlet parmp 22 (fun () ->
       yield ();
       tf1 "thread2: finishing, after dlet...";
       R ()))))) in
   (* main thread *)
   dlet parmp 100 (fun () ->
   dlet parms 501 (fun () ->
   let () = tf1 "main thread" in
   let thread1 = runt thread1 in
   let () = tf1 "main thread" in
   let thread2 = runt thread2 in
   dlet parmp 110 (fun () ->
   dlet parms 510 (fun () ->
   ignore (thread1 ());
   ignore (thread2 ());
   ()
))))))
;;

(*
This example produces the following result:

thread1: starting: private 1, shared 500
thread2: starting: private 2, shared 500
main thread: private 100, shared 501
thread1: continuing...: private 10, shared 501
main thread: private 100, shared 600
thread2: continuing...: private 2, shared 600
thread1: finishing, after dlet...: private 11, shared 510
thread2: finishing, after dlet...: private 22, shared 510

*)