open Syntax open Value (* delinearlize continuation *) (* initial continuation : c *) let idc = C0 (* cons : (v -> t -> m -> v) -> t -> t *) let rec cons k1 t2 = match t2 with | TNil -> Trail k1 | Trail k2 -> Trail (fun v t m -> k1 v (cons k2 t) m) (* apnd : t -> t -> t *) let apnd t1 t2 = match t1 with | TNil -> t2 | Trail k1 -> cons k1 t2 (* f1 : e -> string list -> v list -> c -> s -> t -> m -> v *) let rec f1 e xs vs c s t m = match e with | Num n -> run_c c (VNum n) s t m | Var x -> run_c c (List.nth vs (Env.offset x xs)) s t m | Op (e1, op, e2) -> f1 e1 xs vs (COp1 (e2, xs, op, c)) (VEnv (vs) :: s) t m | Fun (x, e) -> run_c c (VFun (fun v c' s' t' m' -> f1 e (x :: xs) (v :: vs) c' s' t' m')) s t m | App (e1, e2) -> f1 e1 xs vs (CApp1 (e2, xs, c)) (VEnv (vs) :: s) t m | Try (e1, x, k, e2) -> let rec h = fun v c1 s1 t1 c0 s0 t0 m0 -> let vc = VFun (fun v2 c2 s2 t2 m2 -> run_c c1 v2 s1 t1 (MCons ((c2, h, s2, t2), m2))) in f1 e2 (x :: k :: xs) (v :: vc :: vs) c0 s0 t0 m0 in f1 e1 xs vs idc [] TNil (MCons ((c, h, s, t), m)) | TryShallow (e1, x, k, e2) -> let h = fun v c1 s1 t1 c0 s0 t0 m0 -> let vc = VFun (fun v2 c2 s2 t2 m2 -> let c2 = fun v t m -> run_c c2 v s2 t m in run_c c1 v2 s1 (apnd t1 (cons c2 t2)) m2) in f1 e2 (x :: k :: xs) (v :: vc :: vs) c0 s0 t0 m0 in f1 e1 xs vs idc [] TNil (MCons ((c, h, s, t), m)) | Perform e -> f1 e xs vs (CPerform (c)) s t m (* run_c : c -> v -> s -> t -> m -> v *) and run_c c v s t m = match (c, s) with | (C0, []) -> begin match t with | TNil -> begin match m with | MNil -> v | MCons ((c0, h0, s0, t0), m0) -> run_c c0 v s0 t0 m0 end | Trail k -> k v TNil m end | (COp1 (e2, xs, op, c), VEnv (vs) :: s) -> f1 e2 xs vs (COp2 (op, c)) (v :: s) t m | (COp2 (op, c), v1 :: s) -> begin match (v1, v) with | (VNum n1, VNum n2) -> begin match op with | Plus -> run_c c (VNum (n1 + n2)) s t m | Minus -> run_c c (VNum (n1 - n2)) s t m | Times -> run_c c (VNum (n1 * n2)) s t m | Divide -> if n2 = 0 then failwith "Division by zero" else run_c c (VNum (n1 / n2)) s t m end | _ -> failwith (to_string v1 ^ " or " ^ to_string v ^ " are not numbers") end | (CApp1 (e2, xs, c), VEnv (vs) :: s) -> f1 e2 xs vs (CApp2 (c)) (v :: s) t m | (CApp2 (c), v1 :: s) -> apply1 v1 v c s t m | (CPerform (c), s) -> begin match m with | MNil -> failwith "empty metacontinuation in CPerform" | MCons ((c0, h0, s0, t0), m0) -> h0 v c s t c0 s0 t0 m0 end (* apply1 : v -> v -> c -> s -> t -> m -> v *) and apply1 v1 v2 c s t m = match v1 with | VFun f -> f v2 c s t m | _ -> failwith (to_string v1 ^ " is not a function; it can not be applied.") (* f : e -> v *) let f expr = f1 expr [] [] idc [] TNil MNil