open Syntax
open Value

(* defunctionalize VFun, trail, handler, and metacontinuation *)

(* 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 (Append (k1, k2))

(* 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 (e, x, xs, vs)) 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 h = (e2, x, k, xs, vs)
      in f1 e1 xs vs idc [] TNil ((c, h, s, t) :: m)
  | Perform e -> f1 e xs vs (CPerform (c)) s t m
  | PerformShallow e -> f1 e xs vs (CPerformShallow (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
                    | [] -> v
                    | (c0, h0, s0, t0) :: m0 -> run_c c0 v s0 t0 m0
                    end
          | Trail k -> run_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
      | [] -> failwith "empty metacontinuation in CPerform"
      | (c0, h0, s0, t0) :: m0 ->
          let vc = VContS (c, s, t, h0) in
          run_h h0 v vc c0 s0 t0 m0
    end
  | (CPerformShallow (c), s) -> begin match m with
      | [] -> failwith "empty metacontinuation in CPerformShallow"
      | (c0, h0, s0, t0) :: m0 ->
          let vc = VContC (c, s, t) in
          run_h h0 v vc c0 s0 t0 m0
    end

(* run_k : k -> v -> t -> m -> v *)
and run_k k v t m = match k with
  | Hold (c, s) -> run_c c v s t m
  | Append (k, k') -> run_k k v (cons k' t) m

(* run_h : h -> v -> v -> c -> s -> t -> m -> v *)
and run_h (e2, x, k, xs, vs) v vc c s t m =
  f1 e2 (x :: k :: xs) (v :: vc :: vs) c s t m

(* apply1 : v -> v -> c -> s -> t -> m -> v *)
and apply1 v1 v2 c s t m = match v1 with
  | VFun (e, x, xs, vs) -> f1 e (x :: xs) (v2 :: vs) c s t m
  | VContS (c', s', t', h) -> run_c c' v2 s' t' ((c, h, s, t) :: m)
  | VContC (c', s', t') -> run_c c' v2 s' (apnd t' (cons (Hold (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 []