(* 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)