<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(* See: Kenichi Asai and Arisa Kitani "Functional Derivation of a
   Virtual Machine for Delimited Continuations," PPDP 2010, pp. 87-97 *)

(* exceptions *)
exception UnboundVariable
exception TypeError
exception CannotHappen

(* Figure 0 *)

type t = Var of string                  (* term *)
       | Lam of string * t | App of t * t
       | Shift of string * t | Reset of t
       | Int of int
       | Plus of t * t | Times of t * t

type xs = string list          (* argument list *)

(* offset : string -> xs -> int *)
let offset x xs =
  let rec loop xs n = match xs with
      [] -> raise UnboundVariable
    | a::rest ->
        if x = a then n else loop rest (n + 1)
  in loop xs 0

(* some helper functions for testing *)

let rec to_string term lam app = match term with
    Var(x) -> x
  | Lam(x,t) ->
      if lam
      then "(¦Ë" ^ x ^ "." ^ to_string t false false ^ ")"
      else "¦Ë" ^ x ^ "." ^ to_string t false false ^ ""
  | App(t0,t1) ->
      if app
      then "(" ^ to_string t0 true false ^ " " ^ to_string t1 false true ^ ")"
      else to_string t0 true false ^ " " ^ to_string t1 false true
  | Shift(x,t) ->
      if lam
      then "(¦Î" ^ x ^ "." ^ to_string t false false ^ ")"
      else "¦Î" ^ x ^ "." ^ to_string t false false ^ ""
  | Reset(t) ->
      "<" ^ to_string t false false ^ ">"
  | Int(n) -> string_of_int n
  | Plus(t0,t1) ->
      if app
      then "(" ^ to_string t0 true true ^ " + "
               ^ to_string t1 false true ^ ")"
      else to_string t0 true true ^ " + " ^ to_string t1 false true
  | Times(t0,t1) ->
      if app
      then "(" ^ to_string t0 true true ^ " * "
               ^ to_string t1 false true ^ ")"
      else to_string t0 true true ^ " * " ^ to_string t1 false true

let term_to_string term = to_string term false false

(* example terms : a list of pairs of terms and expected results *)
let test_cases = [
 (Int 1
 ,1);
 (App(Lam("x",Var "x"),Int 3)
 ,3);
 (App(App(Lam("x",Lam("y",Var "x")),Int 3),Int 2)
 ,3);
 (Plus(Int 1,Int 2)
 ,3);
 (Reset(Int 3)
 ,3);
 (Reset(Shift("k",App(Var "k",Int 3)))
 ,3);
 (Reset(Shift("k",Int 3))
 ,3);
 (Reset(Plus(Int 1,Shift("k",App(Var "k",Int 2))))
 ,3);
 (Reset(Plus(Int 1,Shift("k",Times(Int 3,App(Var "k",Int 2)))))
 ,9);
 (Plus(Int 1,Reset(Plus(Int 4,Shift("k",Times(Int 3,App(Var "k",Int 2))))))
 ,19);
 (Reset(Plus(Int 1,Shift("k",App(Var "k",App(Var "k",Int 2)))))
 ,4);
 (Reset(Plus(Int 1,Times(Shift("k",App(Var "k",App(Var "k",Int 2))),Int 3)))
 ,22);
 (Plus(Int 1,Reset(Times(Shift("k",App(Var "k",App(Var "k",Int 2))),Int 3)))
 ,19);
 (Plus(Int 1,
       Plus(Reset(Times(Shift("k",App(Var "k",App(Var "k",Int 2))),Int 3)),
            Int 4))
 ,23);
 (Reset(Plus(Int 1,
             App(Shift("k",Times(Int 2,
                                 App(Var "k",Lam("l",Times(Var "l",Int 3))))),
                 Int 4)))
 ,26);
 (Reset(Plus(Int 1,
             App(Shift("k",Times(Int 3,
                                 Shift("l",App(Var "k",Var "l")))), Int 2)))
 ,7);
 (Reset(Plus(Int 1,
             App(Shift("k",App(Var "k",Lam("l",Plus(Var "l",Times(Int 3,
               Shift("m",App(Var "k",Var "m"))))))),Int 2)))
 ,10);
 (App(Reset(Plus(Int 1,Shift("k",Var "k"))),Int 3)
 ,4);
 (Plus(Int 1,Reset(Plus(Int 2,Shift("k",Plus(App(Var "k",Int 3),
    Shift("l",Plus(Int 4,App(Var "l",App(Var "k",Int 5)))))))))
 ,17);
 (Reset(Plus(Shift("k",(App(Var "k",App(Var "k",Int 1)))),
             Shift("l",(App(Var "l",App(Var "l",Int 2))))))
 ,10);
]

(* run_test *)
let run_test f unint =
  let rec loop lst = match lst with
      [] -> true
    | (t,n)::rest ->
        print_string (term_to_string t);
        print_newline ();
        print_string "should be: ";
        print_string (string_of_int n);
        print_string " produces: ";
        print_string (string_of_int (unint (f t)));
        print_newline ();
        assert (unint (f t) = n);
        loop rest
  in loop test_cases

(* Figure 1 *)

type v = VFun of (v -> c -> v)         (* value *)
       | VCont of c
       | VInt of int
and  c = v -> v                 (* continuation *)

(* f1 : t -> xs -> v list -> c -> v *)
let rec f1 t xs vs c = match t with
    Var(x) -> c (List.nth vs (offset x xs))
  | Lam(x,t) ->
      c (VFun(fun v c' ->
                f1 t (x::xs) (v::vs) c'))
  | App(t0,t1) ->
      f1 t0 xs vs (fun v0 ->
      f1 t1 xs vs (fun v1 ->
      match v0 with
          VFun(f) -> f v1 c
        | VCont(c') -> c (c' v1)
        | VInt(_) -> raise TypeError))
  | Shift(x,t) ->
      f1 t (x::xs) (VCont(c)::vs) (fun v -> v)
  | Reset(t) -> c (f1 t xs vs (fun v -> v))
  | Int(n) -> c (VInt(n))
  | Plus(t0,t1) ->
      f1 t0 xs vs (fun v0 ->
      f1 t1 xs vs (fun v1 ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> c (VInt(n0 + n1))
        | (_, _) -> raise TypeError))
  | Times(t0,t1) ->
      f1 t0 xs vs (fun v0 ->
      f1 t1 xs vs (fun v1 ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> c (VInt(n0 * n1))
        | (_, _) -> raise TypeError))

(* eval1 : t -> v *)
let eval1 t = f1 t [] [] (fun v -> v)

(* test *)
let test1 = run_test eval1 (fun (VInt(n)) -> n)

(* Figure 2 *)

type v = VFun of (v -> c -> v)         (* value *)
       | VCont of c
       | VInt of int
and  c = C0                     (* continuation *)
       | CApp0 of t * xs * v list * c
       | CApp1 of v * c
       | CPlus0 of t * xs * v list * c
       | CPlus1 of v * c
       | CTimes0 of t * xs * v list * c
       | CTimes1 of v * c

(* run_c2 : c -> v -> v *)
let rec run_c2 c v = match c with
    C0 -> v
  | CApp0(t1,xs,vs,c) -> f2 t1 xs vs (CApp1(v,c))
  | CApp1(v0,c) ->
      (match v0 with
           VFun(f) -> f v c
         | VCont(c') -> run_c2 c (run_c2 c' v)
         | VInt(_) -> raise TypeError)
  | CPlus0(t1,xs,vs,c) ->
      f2 t1 xs vs (CPlus1(v,c))
  | CPlus1(v0,c) ->
      (match (v0, v) with
           (VInt(n0), VInt(n1)) -> run_c2 c (VInt(n0 + n1))
         | (_, _) -> raise TypeError)
  | CTimes0(t1,xs,vs,c) ->
      f2 t1 xs vs (CTimes1(v,c))
  | CTimes1(v0,c) ->
      (match (v0, v) with
           (VInt(n0), VInt(n1)) -> run_c2 c (VInt(n0 * n1))
         | (_, _) -> raise TypeError)

(* f2 : t -> xs -> v list -> c -> v *)
and f2 t xs vs c = match t with
    Var(x) -> run_c2 c (List.nth vs (offset x xs))
  | Lam(x,t) ->
      run_c2 c (VFun(fun v c' ->
                       f2 t (x::xs) (v::vs) c'))
  | App(t0,t1) -> f2 t0 xs vs (CApp0(t1,xs,vs,c))
  | Shift(x,t) -> f2 t (x::xs) (VCont(c)::vs) C0
  | Reset(t) -> run_c2 c (f2 t xs vs C0)
  | Int(n) -> run_c2 c (VInt(n))
  | Plus(t0,t1) ->
      f2 t0 xs vs (CPlus0(t1,xs,vs,c))
  | Times(t0,t1) ->
      f2 t0 xs vs (CTimes0(t1,xs,vs,c))

(* eval2 : t -> v *)
let eval2 t = f2 t [] [] C0

(* test *)
let test2 = run_test eval2 (fun (VInt(n)) -> n)

(* Figure 3 *)

type v = VFun of (v -> c -> v)         (* value *)
       | VCont of c
       | VInt of int
and  f = CApp0 of t * xs * v list      (* frame *)
       | CApp1 of v
       | CPlus0 of t * xs * v list
       | CPlus1 of v
       | CTimes0 of t * xs * v list
       | CTimes1 of v
and  c = f list                 (* continuation *)

(* run_c3 : c -> v -> v *)
let rec run_c3 c v = match c with
    [] -> v
  | CApp0(t1,xs,vs)::c ->
      f3 t1 xs vs (CApp1(v)::c)
  | CApp1(v0)::c ->
      (match v0 with
           VFun(f) -> f v c
         | VCont(c') -> run_c3 c (run_c3 c' v)
         | VInt(_) -> raise TypeError)
  | CPlus0(t1,xs,vs)::c ->
      f3 t1 xs vs (CPlus1(v)::c)
  | CPlus1(v0)::c ->
      (match (v0, v) with
           (VInt(n0), VInt(n1)) -> run_c3 c (VInt(n0 + n1))
         | (_, _) -> raise TypeError)
  | CTimes0(t1,xs,vs)::c ->
      f3 t1 xs vs (CTimes1(v)::c)
  | CTimes1(v0)::c ->
      (match (v0, v) with
           (VInt(n0), VInt(n1)) -> run_c3 c (VInt(n0 * n1))
         | (_, _) -> raise TypeError)

(* f3 : t -> xs -> v list -> c -> v *)
and f3 t xs vs c = match t with
    Var(x) -> run_c3 c (List.nth vs (offset x xs))
  | Lam(x,t) ->
      run_c3 c (VFun(fun v c' ->
                       f3 t (x::xs) (v::vs) c'))
  | App(t0,t1) -> f3 t0 xs vs (CApp0(t1,xs,vs)::c)
  | Shift(x,t) -> f3 t (x::xs) (VCont(c)::vs) []
  | Reset(t) -> run_c3 c (f3 t xs vs [])
  | Int(n) -> run_c3 c (VInt n)
  | Plus(t0,t1) ->
      f3 t0 xs vs (CPlus0(t1,xs,vs)::c)
  | Times(t0,t1) ->
      f3 t0 xs vs (CTimes0(t1,xs,vs)::c)

(* eval3 : t -> v *)
let eval3 t = f3 t [] [] []

(* test *)
let test3 = run_test eval3 (fun (VInt(n)) -> n)

(* Figure 4 *)

type v = VFun of (v -> s -> c -> v)    (* value *)
       | VCont of c * s
       | VEnv of v list
       | VInt of int
and  f = CApp0 of t * xs               (* frame *)
       | CApp1
       | CPlus0 of t * xs
       | CPlus1
       | CTimes0 of t * xs
       | CTimes1
and  c = f list                 (* continuation *)
and  s = v list                   (* data stack *)

(* run_c4 : c -> v -> s -> v *)
let rec run_c4 c v s = match (c, s) with
    ([], []) -> v
  | (CApp0(t1,xs)::c, VEnv(vs)::s) ->
      f4 t1 xs vs (v::s) (CApp1::c)
  | (CApp1::c, v0::s) ->
      (match v0 with
           VFun(f) -> f v s c
         | VCont(c',s') ->
             run_c4 c (run_c4 c' v s') s
	 | VEnv(_) -> raise CannotHappen
         | VInt(_) -> raise TypeError)
  | (CPlus0(t1,xs)::c, VEnv(vs)::s) ->
      f4 t1 xs vs (v::s) (CPlus1::c)
  | (CPlus1::c, v0::s) ->
      (match (v0, v) with
           (VInt(n0), VInt(n1)) -> run_c4 c (VInt(n0 + n1)) s
         | (_, _) -> raise TypeError)
  | (CTimes0(t1,xs)::c, VEnv(vs)::s) ->
      f4 t1 xs vs (v::s) (CTimes1::c)
  | (CTimes1::c, v0::s) ->
      (match (v0, v) with
           (VInt(n0), VInt(n1)) -> run_c4 c (VInt(n0 * n1)) s
         | (_, _) -> raise TypeError)
  | (_, _) -> raise CannotHappen

(* f4 : t -> xs -> v list -> s -> c -> v *)
and f4 t xs vs s c = match t with
    Var(x) ->
      run_c4 c (List.nth vs (offset x xs)) s
  | Lam(x,t) ->
      run_c4 c
             (VFun(fun v s' c' ->
                     f4 t (x::xs) (v::vs) s' c'))
             s
  | App(t0,t1) ->
      f4 t0 xs vs (VEnv(vs)::s) (CApp0(t1,xs)::c)
  | Shift(x,t) ->
      f4 t (x::xs) (VCont(c,s)::vs) [] []
  | Reset(t) -> run_c4 c (f4 t xs vs [] []) s
  | Int(n) -> run_c4 c (VInt(n)) s
  | Plus(t0,t1) ->
      f4 t0 xs vs (VEnv(vs)::s) (CPlus0(t1,xs)::c)
  | Times(t0,t1) ->
      f4 t0 xs vs (VEnv(vs)::s) (CTimes0(t1,xs)::c)

(* eval4 : t -> v *)
let eval4 t = f4 t [] [] [] []

(* test *)
let test4 = run_test eval4 (fun (VInt(n)) -> n)

(* Figure 5 *)

type v = VFun of (v -> s -> c -> v)    (* value *)
       | VCont of c * s
       | VEnv of v list
       | VInt of int
and  c = C0                     (* continuation *)
       | CApp0 of t * xs * c
       | CApp1 of c
       | CPlus0 of t * xs * c
       | CPlus1 of c
       | CTimes0 of t * xs * c
       | CTimes1 of c
and  s = v list                   (* data stack *)

(* run_c5 : c -> v -> s -> v *)
let rec run_c5 c v s = match (c, s) with
    (C0, []) -> v
  | (CApp0(t1,xs,c), VEnv(vs)::s) ->
      f5 t1 xs vs (v::s) (CApp1(c))
  | (CApp1(c), v0::s) ->
      (match v0 with
           VFun(f) -> f v s c
         | VCont(c',s') ->
             run_c5 c (run_c5 c' v s') s
	 | VEnv(_) -> raise CannotHappen
         | VInt(_) -> raise TypeError)
  | (CPlus0(t1,xs,c), VEnv(vs)::s) ->
      f5 t1 xs vs (v::s) (CPlus1(c))
  | (CPlus1(c), v0::s) ->
      (match (v0, v) with
           (VInt(n0), VInt(n1)) -> run_c5 c (VInt(n0 + n1)) s
         | (_,_) -> raise TypeError)
  | (CTimes0(t1,xs,c), VEnv(vs)::s) ->
      f5 t1 xs vs (v::s) (CTimes1(c))
  | (CTimes1(c), v0::s) ->
      (match (v0, v) with
           (VInt(n0), VInt(n1)) -> run_c5 c (VInt(n0 * n1)) s
         | (_,_) -> raise TypeError)
  | (_, _) -> raise CannotHappen

(* f5 : t -> xs -> v list -> s -> c -> v *)
and f5 t xs vs s c = match t with
    Var(x) ->
      run_c5 c (List.nth vs (offset x xs)) s
  | Lam(x,t) ->
      run_c5 c
             (VFun(fun v s' c' ->
                     f5 t (x::xs) (v::vs) s' c'))
             s
  | App(t0,t1) ->
      f5 t0 xs vs (VEnv(vs)::s) (CApp0(t1,xs,c))
  | Shift(x,t) ->
      f5 t (x::xs) (VCont(c,s)::vs) [] C0
  | Reset(t) -> run_c5 c (f5 t xs vs [] C0) s
  | Int(n) -> run_c5 c (VInt(n)) s
  | Plus(t0,t1) ->
      f5 t0 xs vs (VEnv(vs)::s) (CPlus0(t1,xs,c))
  | Times(t0,t1) ->
      f5 t0 xs vs (VEnv(vs)::s) (CTimes0(t1,xs,c))

(* eval5 : t -> v *)
let eval5 t = f5 t [] [] [] C0

(* test *)
let test5 = run_test eval5 (fun (VInt(n)) -> n)

(* Figure 6 *)

type v = VFun of (v -> s -> c -> v)    (* value *)
       | VCont of c * s
       | VEnv of v list
       | VInt of int
and  c = v -> s -> v            (* continuation *)
and  s = v list                   (* data stack *)

(* f6 : t -> xs -> v list -> s -> c -> v *)
let rec f6 t xs vs s c = match t with
    Var(x) -> c (List.nth vs (offset x xs)) s
  | Lam(x,t) ->
      c (VFun(fun v s' c' ->
                f6 t (x::xs) (v::vs) s' c'))
        s
  | App(t0,t1) ->
      f6 t0 xs vs (VEnv(vs)::s)
                          (fun v0 (VEnv(vs)::s) ->
      f6 t1 xs vs (v0::s) (fun v1 (v0::s) ->
      match v0 with
          VFun(f) -> f v1 s c
        | VCont(c',s') -> c (c' v1 s') s
	| VEnv(_) -> raise CannotHappen
	| VInt(_) -> raise TypeError))
  | Shift(x,t) ->
      f6 t (x::xs) (VCont(c,s)::vs) []
         (fun v [] -> v)
  | Reset(t) ->
      c (f6 t xs vs [] (fun v [] -> v)) s
  | Int(n) -> c (VInt(n)) s
  | Plus(t0,t1) ->
      f6 t0 xs vs (VEnv(vs)::s) (fun v0 (VEnv(vs)::s) ->
      f6 t1 xs vs (v0::s) (fun v1 (v0::s) ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> c (VInt(n0 + n1)) s
        | (_, _) -> raise TypeError))
  | Times(t0,t1) ->
      f6 t0 xs vs (VEnv(vs)::s) (fun v0 (VEnv(vs)::s) ->
      f6 t1 xs vs (v0::s) (fun v1 (v0::s) ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> c (VInt(n0 * n1)) s
        | (_, _) -> raise TypeError))

(* eval6 : t -> v *)
let eval6 t = f6 t [] [] [] (fun v [] -> v)

(* test *)
let test6 = run_test eval6 (fun (VInt(n)) -> n)

(* Figure 7 *)

type v = VFun of (s -> c -> v)         (* value *)
       | VCont of c * s
       | VEnv of v list
       | VInt of int
and  c = s -> v                 (* continuation *)
and  s = v list                   (* data stack *)

(* f7 : t -> xs -> s -> c -> v *)
let rec f7 t xs (VEnv(vs)::s) c = match t with
    Var(x) -> c ((List.nth vs (offset x xs))::s)
  | Lam(x,t) ->
      c (VFun(fun (v::s') c' ->
                f7 t (x::xs) (VEnv(v::vs)::s') c')
         ::s)
  | App(t0,t1) ->
      f7 t0 xs (VEnv(vs)::VEnv(vs)::s)
                         (fun (v0::VEnv(vs)::s) ->
      f7 t1 xs (VEnv(vs)::v0::s)
                               (fun (v1::v0::s) ->
      match v0 with
          VFun(f) -> f (v1::s) c
        | VCont(c',s') -> c ((c' (v1::s'))::s)
	| VEnv(_) -> raise CannotHappen
        | VInt(_) -> raise TypeError))
  | Shift(x,t) ->
      f7 t (x::xs) [VEnv(VCont(c,s)::vs)]
         (fun [v] -> v)
  | Reset(t) ->
      c ((f7 t xs [VEnv(vs)] (fun [v] -> v))::s)
  | Int(n) -> c (VInt(n)::s)
  | Plus(t0,t1) ->
      f7 t0 xs (VEnv(vs)::VEnv(vs)::s) (fun (v0::VEnv(vs)::s) ->
      f7 t1 xs (VEnv(vs)::v0::s) (fun (v1::v0::s) ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> c (VInt(n0 + n1)::s)
        | (_, _) -> raise TypeError))
  | Times(t0,t1) ->
      f7 t0 xs (VEnv(vs)::VEnv(vs)::s) (fun (v0::VEnv(vs)::s) ->
      f7 t1 xs (VEnv(vs)::v0::s) (fun (v1::v0::s) ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> c (VInt(n0 * n1)::s)
        | (_, _) -> raise TypeError))

(* eval7 : t -> v *)
let eval7 t = f7 t [] [VEnv([])] (fun [v] -> v)

(* test *)
let test7 = run_test eval7 (fun (VInt(n)) -> n)

(* Figure 8 *)

type v = VFun of (s -> c -> v)         (* value *)
       | VCont of c * s
       | VEnv of v list
       | VK of c
       | VInt of int
and  c = s -> v                 (* continuation *)
and  s = v list                   (* data stack *)

type i = s -> c -> v             (* instruction *)

(* (>>) : i -> i -> i *)
let (>>) i1 i2 = fun s c ->
  i1 s (fun s' -> i2 s' c)

(* access : int -> i *)
let access n = fun (VEnv(vs)::s) c ->
  c ((List.nth vs n)::s)

(* push_closure : i -> i *)
let push_closure code = fun (VEnv(vs)::s) c ->
  c (VFun(fun (v::s') c' ->
            code (VEnv(v::vs)::s') c')
     ::s)

(* return : i *)
let return = fun (v::VK(c')::s) _ ->
  c' (v::s)

(* push_env : i *)
let push_env = fun (VEnv(vs)::s) c ->
  c (VEnv(vs)::VEnv(vs)::s)

(* pop_env : i *)
let pop_env = fun (v0::VEnv(vs)::s) c ->
  c (VEnv(vs)::v0::s)

(* call : i *)
let call = fun (v1::v0::s) c ->
  match v0 with                   (* dummy *)
      VFun(f) -> f (v1::VK(c)::s) (fun [v] -> v)
    | VCont(c',s') -> c ((c' (v1::s'))::s)
    | VEnv(_) -> raise CannotHappen
    | VK(_) -> raise CannotHappen
    | VInt(_) -> raise TypeError

(* shift : i -> i *)
let shift code = fun (VEnv(vs)::s) c ->
  code [VEnv(VCont(c,s)::vs)] (fun [v] -> v)

(* reset : i -> i *)
let reset code = fun (VEnv(vs)::s) c ->
  c ((code [VEnv(vs)] (fun [v] -> v))::s)

(* push_int : int -> i *)
let push_int n = fun (VEnv(vs)::s) c ->
  c (VInt(n)::s)

(* plus : i *)
let plus = fun (v1::v0::s) c -> match (v0, v1) with
    (VInt(n0), VInt(n1)) -> c (VInt(n0 + n1)::s)
  | (_, _) -> raise TypeError

(* times : i *)
let times = fun (v1::v0::s) c -> match (v0, v1) with
    (VInt(n0), VInt(n1)) -> c (VInt(n0 * n1)::s)
  | (_, _) -> raise TypeError

(* f8 : t -> xs -> i *)
let rec f8 t xs = match t with
    Var(x) -> access (offset x xs)
  | Lam(x,t) ->
      push_closure (f8 t (x::xs) >> return)
  | App(t0,t1) ->
      push_env >> f8 t0 xs >> pop_env >> f8 t1 xs
      >> call
  | Shift(x,t) -> shift (f8 t (x::xs))
  | Reset(t) -> reset (f8 t xs)
  | Int(n) -> push_int n
  | Plus(t0,t1) ->
      push_env >> f8 t0 xs >> pop_env >> f8 t1 xs >> plus
  | Times(t0,t1) ->
      push_env >> f8 t0 xs >> pop_env >> f8 t1 xs >> times

(* eval8 : t -> v *)
let eval8 t = f8 t [] [VEnv([])] (fun [v] -> v)

(* test *)
let test8 = run_test eval8 (fun (VInt(n)) -> n)

(* Figure 9 *)

type v = VFun of (s -> c -> d -> v)    (* value *)
       | VCont of c * s
       | VEnv of v list
       | VK of c
       | VInt of int
and  c = s -> d -> v            (* continuation *)
and  d = v -> v      (* dump (metacontinuation) *)
and  s = v list                   (* data stack *)

type i = s -> c -> d -> v        (* instruction *)
(* instruction : s -> c -> d -> v *)

(* (>>) : i -> i -> i *)
let (>>) i1 i2 = fun s c ->
  i1 s (fun s' -> i2 s' c)

(* access : int -> i *)
let access n = fun (VEnv(vs)::s) c ->
  c ((List.nth vs n)::s)

(* push_closure : i -> i *)
let push_closure code = fun (VEnv(vs)::s) c ->
  c (VFun(fun (v::s') c' ->
            code (VEnv(v::vs)::s') c')
     ::s)

(* return : i *)
let return = fun (v::VK(c')::s) _ ->
  c' (v::s)

(* push_env : i *)
let push_env = fun (VEnv(vs)::s) c ->
  c (VEnv(vs)::VEnv(vs)::s)

(* pop_env : i *)
let pop_env = fun (v0::VEnv(vs)::s) c ->
  c (VEnv(vs)::v0::s)

(* push_int : int -> i *)
let push_int n = fun (VEnv(vs)::s) c ->
  c (VInt(n)::s)

(* plus : i *)
let plus = fun (v1::v0::s) c -> match (v0, v1) with
    (VInt(n0), VInt(n1)) -> c (VInt(n0 + n1)::s)
  | (_, _) -> raise TypeError

(* times : i *)
let times = fun (v1::v0::s) c -> match (v0, v1) with
    (VInt(n0), VInt(n1)) -> c (VInt(n0 * n1)::s)
  | (_, _) -> raise TypeError

(* instructions same as Figure 8 up to here *)

(* call : i *)
let call = fun (v1::v0::s) c d -> match v0 with
    VFun(f) ->         (* dummy *)
      f (v1::VK(c)::s) (fun [v] d -> d v) d
  | VCont(c',s') ->
      c' (v1::s') (fun v -> c (v::s) d)
  | VEnv(_) -> raise CannotHappen
  | VK(_) -> raise CannotHappen
  | VInt(_) -> raise TypeError

(* shift : i -> i *)
let shift code = fun (VEnv(vs)::s) c ->
  code [VEnv(VCont(c,s)::vs)] (fun [v] d -> d v)

(* reset : i -> i *)
let reset code = fun (VEnv(vs)::s) c d ->
  code [VEnv(vs)] (fun [v] d -> d v)
       (fun v -> c (v::s) d)

(* f9 : t -> xs -> i *)
let rec f9 t xs = match t with
    Var(x) -> access (offset x xs)
  | Lam(x,t) ->
      push_closure (f9 t (x::xs) >> return)
  | App(t0,t1) ->
      push_env >> f9 t0 xs >> pop_env >> f9 t1 xs
      >> call
  | Shift(x,t) -> shift (f9 t (x::xs))
  | Reset(t) -> reset (f9 t xs)
  | Int(n) -> push_int n
  | Plus(t0,t1) ->
      push_env >> f9 t0 xs >> pop_env >> f9 t1 xs >> plus
  | Times(t0,t1) ->
      push_env >> f9 t0 xs >> pop_env >> f9 t1 xs >> times

(* eval9 : t -> v *)
let eval9 t =
  f9 t [] [VEnv([])] (fun [v] d -> d v)
     (fun v -> v)

(* test *)
let test9 = run_test eval9 (fun (VInt(n)) -> n)

(* Figure 10 *)

type i = IAccess of int          (* instruction *)
       | IPush_closure of i | IReturn
       | IPush_env | IPop_env | ICall
       | IShift of i | IReset of i
       | ISeq of i * i
       | IPush_int of int | IPlus | ITimes

type v = VFun of (s -> c -> d -> v)    (* value *)
       | VCont of c * s
       | VEnv of v list
       | VK of c
       | VInt of int
and  c = i list                 (* continuation *)
and  d = (c * s) list                   (* dump *)
and  s = v list                   (* data stack *)

(* run_d10 : d -> v -> v *)
let rec run_d10 d v = match d with
    [] -> v
  | (c,s)::d' -> run_c10 c (v::s) d'

(* run_c10 : c -> s -> d -> v *)
and run_c10 c s d = match c with
    [] -> (match s with [v] -> run_d10 d v)
  | g::c -> run_i10 g s c d

(* run_i10 : i -> s -> c -> d -> v *)
and run_i10 i s c d = match i with
    IAccess(n) -> (match s with (VEnv(vs)::s) ->
      run_c10 c ((List.nth vs n)::s) d)
  | IPush_closure(code) ->
     (match s with (VEnv(vs)::s) ->
        run_c10 c
                (VFun(fun (v::s') c' d' ->
                   run_i10 code (VEnv(v::vs)::s')
                           c' d')
                 ::s) d)
  | IReturn -> (match s with (v::VK(c')::s) ->
      run_c10 c' (v::s) d)
  | IPush_env -> (match s with (VEnv(vs)::s) ->
      run_c10 c (VEnv(vs)::VEnv(vs)::s) d)
  | IPop_env -> (match s with (v0::VEnv(vs)::s) ->
      run_c10 c (VEnv(vs)::v0::s) d)
  | ICall -> (match s with (v1::v0::s) ->
      match v0 with                   (* dummy *)
          VFun(f) -> f (v1::VK(c)::s) [] d
        | VCont(c',s') ->
            run_c10 c' (v1::s') ((c,s)::d)
        | VEnv(_) -> raise CannotHappen
        | VK(_) -> raise CannotHappen
        | VInt(_) -> raise TypeError)
  | IShift(code) -> (match s with (VEnv(vs)::s) ->
      run_i10 code [VEnv(VCont(c,s)::vs)] [] d)
  | IReset(code) -> (match s with (VEnv(vs)::s) ->
      run_i10 code [VEnv(vs)] [] ((c,s)::d))
  | ISeq(f,g) -> run_i10 f s (g::c) d
  | IPush_int(n) -> (match s with (VEnv(vs)::s) ->
      run_c10 c (VInt(n)::s) d)
  | IPlus -> (match s with (v1::v0::s) ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> run_c10 c (VInt(n0 + n1)::s) d
        | (_, _) -> raise TypeError)
  | ITimes -> (match s with (v1::v0::s) ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> run_c10 c (VInt(n0 * n1)::s) d
        | (_, _) -> raise TypeError)

(* (>>) : i -> i -> i *)
let (>>) f g = ISeq(f,g)

(* f10 : t -> xs -> i *)
let rec f10 t xs = match t with
    Var(x) -> IAccess(offset x xs)
  | Lam(x,t) ->
      IPush_closure(f10 t (x::xs) >> IReturn)
  | App(t0,t1) ->
      IPush_env >> f10 t0 xs >> IPop_env
      >> f10 t1 xs >> ICall
  | Shift(x,t) -> IShift(f10 t (x::xs))
  | Reset(t) -> IReset(f10 t xs)
  | Int(n) -> IPush_int(n)
  | Plus(t0,t1) ->
      IPush_env >> f10 t0 xs >> IPop_env >> f10 t1 xs >> IPlus
  | Times(t0,t1) ->
      IPush_env >> f10 t0 xs >> IPop_env >> f10 t1 xs >> ITimes

(* eval10 : t -> v *)
let eval10 t =
  run_i10 (f10 t []) [VEnv([])] [] []

(* test *)
let test10 = run_test eval10 (fun (VInt(n)) -> n)

(* Figure 11 *)

type i = IAccess of int          (* instruction *)
       | IPush_closure of i list | IReturn
       | IPush_env | IPop_env | ICall
       | IShift of i list | IReset of i list
       | IPush_int of int | IPlus | ITimes

type v = VFun of (s -> c -> d -> v)    (* value *)
       | VCont of c * s
       | VEnv of v list
       | VK of c
       | VInt of int
and  c = i list                 (* continuation *)
and  d = (c * s) list                   (* dump *)
and  s = v list                   (* data stack *)

(* run_d11 : d -> v -> v *)
let rec run_d11 d v = match d with
    [] -> v
  | (c,s)::d' -> run_c11 c (v::s) d'

(* run_c11 : i list -> s -> d -> v *)
and run_c11 c s d = match c with
    [] -> (match s with [v] -> run_d11 d v)
  | IAccess(n)::c ->
     (match s with (VEnv(vs)::s) ->
        run_c11 c ((List.nth vs n)::s) d)
  | IPush_closure(code)::c ->
     (match s with (VEnv(vs)::s) ->
       run_c11 c
         (VFun(fun (v::s') c' d' ->
           run_c11 (code@c') (VEnv(v::vs)::s') d')
          ::s) d)
  | IReturn::c -> (match s with (v::VK(c')::s) ->
      run_c11 c' (v::s) d)
  | IPush_env::c -> (match s with (VEnv(vs)::s) ->
      run_c11 c (VEnv(vs)::VEnv(vs)::s) d)
  | IPop_env::c ->
     (match s with (v0::VEnv(vs)::s) ->
        run_c11 c (VEnv(vs)::v0::s) d)
  | ICall::c -> (match s with (v1::v0::s) ->
      match v0 with                    (* dummy *)
          VFun(f) -> f (v1::VK(c)::s) [] d
        | VCont(c',s') ->
            run_c11 c' (v1::s') ((c,s)::d)
        | VEnv(_) -> raise CannotHappen
        | VK(_) -> raise CannotHappen
        | VInt(_) -> raise TypeError)
  | IShift(code)::c ->
     (match s with (VEnv(vs)::s) ->
        run_c11 code [VEnv(VCont(c,s)::vs)] d)
  | IReset(code)::c ->
     (match s with (VEnv(vs)::s) ->
        run_c11 code [VEnv(vs)] ((c,s)::d))
  | IPush_int(n)::c -> (match s with (VEnv(vs)::s) ->
      run_c11 c (VInt(n)::s) d)
  | IPlus::c -> (match s with (v1::v0::s) ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> run_c11 c (VInt(n0 + n1)::s) d
        | (_, _) -> raise TypeError)
  | ITimes::c -> (match s with (v1::v0::s) ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> run_c11 c (VInt(n0 * n1)::s) d
        | (_, _) -> raise TypeError)

(* f11 : t -> xs -> i list *)
let rec f11 t xs = match t with
    Var(x) -> [IAccess (offset x xs)]
  | Lam(x,t) ->
      [IPush_closure((f11 t (x::xs))@[IReturn])]
  | App(t0,t1) ->
      [IPush_env]@(f11 t0 xs)@[IPop_env]
      @(f11 t1 xs)@[ICall]
  | Shift(x,t) -> [IShift(f11 t (x::xs))]
  | Reset(t) -> [IReset(f11 t xs)]
  | Int(n) -> [IPush_int(n)]
  | Plus(t0,t1) ->
      [IPush_env]@(f11 t0 xs)@[IPop_env]@(f11 t1 xs)@[IPlus]
  | Times(t0,t1) ->
      [IPush_env]@(f11 t0 xs)@[IPop_env]@(f11 t1 xs)@[ITimes]

(* eval11 : t -> v *)
let eval11 t = run_c11 (f11 t []) [VEnv([])] []

(* test *)
let test11 = run_test eval11 (fun (VInt(n)) -> n)

(* Section 5.4 *)

type i = IAccess of int          (* instruction *)
       | IPush_closure of i list | IReturn
       | IPush_env | IPop_env | ICall
       | IShift of i list | IReset of i list
       | IPush_int of int | IPlus | ITimes

type v = VFun of c * v list            (* value *)
       | VCont of c * s
       | VEnv of v list
       | VK of c
       | VInt of int
and  c = i list                 (* continuation *)
and  d = (c * s) list                   (* dump *)
and  s = v list                   (* data stack *)

(* run_d12 : d -> v -> v *)
let rec run_d12 d v = match d with
    [] -> v
  | (c,s)::d' -> run_c12 c (v::s) d'

(* run_c12 : i list -> s -> d -> v *)
and run_c12 c s d = match c with
    [] -> (match s with [v] -> run_d12 d v)
  | IAccess(n)::c ->
     (match s with (VEnv(vs)::s) ->
        run_c12 c ((List.nth vs n)::s) d)
  | IPush_closure(code)::c ->
     (match s with (VEnv(vs)::s) ->
        run_c12 c (VFun(code,vs)::s) d)
  | IReturn::c -> (match s with (v::VK(c')::s) ->
      run_c12 c' (v::s) d)
  | IPush_env::c -> (match s with (VEnv(vs)::s) ->
      run_c12 c (VEnv(vs)::VEnv(vs)::s) d)
  | IPop_env::c ->
     (match s with (v0::VEnv(vs)::s) ->
        run_c12 c (VEnv(vs)::v0::s) d)
  | ICall::c -> (match s with (v1::v0::s) ->
      match v0 with
          VFun(code,vs) ->
            run_c12 code (VEnv(v1::vs)::VK(c)::s) d
        | VCont(c',s') ->
            run_c12 c' (v1::s') ((c,s)::d)
        | VEnv(_) -> raise CannotHappen
        | VK(_) -> raise CannotHappen
        | VInt(_) -> raise TypeError)
  | IShift(code)::c ->
     (match s with (VEnv(vs)::s) ->
        run_c12 code [VEnv(VCont(c,s)::vs)] d)
  | IReset(code)::c ->
     (match s with (VEnv(vs)::s) ->
        run_c12 code [VEnv(vs)] ((c,s)::d))
  | IPush_int(n)::c -> (match s with (VEnv(vs)::s) ->
      run_c12 c (VInt(n)::s) d)
  | IPlus::c -> (match s with (v1::v0::s) ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> run_c12 c (VInt(n0 + n1)::s) d
        | (_, _) -> raise TypeError)
  | ITimes::c -> (match s with (v1::v0::s) ->
      match (v0, v1) with
          (VInt(n0), VInt(n1)) -> run_c12 c (VInt(n0 * n1)::s) d
        | (_, _) -> raise TypeError)

(* f12 : t -> xs -> i list *)
let rec f12 t xs = match t with
    Var(x) -> [IAccess (offset x xs)]
  | Lam(x,t) ->
      [IPush_closure((f12 t (x::xs))@[IReturn])]
  | App(t0,t1) ->
      [IPush_env]@(f12 t0 xs)@[IPop_env]
      @(f12 t1 xs)@[ICall]
  | Shift(x,t) -> [IShift(f12 t (x::xs))]
  | Reset(t) -> [IReset(f12 t xs)]
  | Int(n) -> [IPush_int(n)]
  | Plus(t0,t1) ->
      [IPush_env]@(f12 t0 xs)@[IPop_env]@(f12 t1 xs)@[IPlus]
  | Times(t0,t1) ->
      [IPush_env]@(f12 t0 xs)@[IPop_env]@(f12 t1 xs)@[ITimes]

(* eval12 : t -> v *)
let eval12 t = run_c12 (f12 t []) [VEnv([])] []

(* test *)
let test12 = run_test eval12 (fun (VInt(n)) -> n)