open Syntax
open Value

(* 実際の計算をする関数 *)
(* Definitional interpreter for λ-calculus with control and prompt : eval1 *)

(* 初期継続 *)
let idc v t = match t with
    TNil -> v
  | Trail (c) -> c v TNil

(* cons : c -> t -> t *)
let rec cons c t = match t with
    TNil -> Trail (c)
  | Trail (c') -> Trail (fun v t' -> c v (cons c' t'))

(* apnd : t -> t -> t *)
let apnd t0 t1 = match t0 with
    TNil -> t1
  | Trail (c) -> cons c t1

(* f1 : e -> string list -> v list -> c -> t -> v *)
let rec f1 e xs vs c t = match e with
    Num (n) -> c (VNum (n)) t
  | Var (x) -> c (List.nth vs (Env.offset x xs)) t
  | Op (e0, op, e1) ->
    f1 e0 xs vs (fun v0 t0 ->
        f1 e1 xs vs (fun v1 t1 ->
            begin match (v0, v1) with
                (VNum (n0), VNum (n1)) ->
                begin match op with
                    Plus -> c (VNum (n0 + n1)) t1
                  | Minus -> c (VNum (n0 - n1)) t1
                  | Times -> c (VNum (n0 * n1)) t1
                  | Divide ->
                    if n1 = 0 then failwith "Division by zero"
                    else c (VNum (n0 / n1)) t1
                end
              | _ -> failwith "op error"
            end) t0) t
  | Fun (x, e) -> c (VFun (fun v c' t' -> f1 e (x :: xs) (v :: vs) c' t')) t
  | App (e0, e1) ->
    f1 e0 xs vs (fun v0 t0 ->
        f1 e1 xs vs (fun v1 t1 ->
            begin match v0 with
                VFun (f) -> f v1 c t1
              | VCont (c', t') -> c' v1 (apnd t' (cons c t1))
              | _ -> failwith "not app"
            end) t0) t
  | Control (x, e) -> f1 e (x :: xs) (VCont (c, t) :: vs) idc TNil
  | Prompt (e) -> c (f1 e xs vs idc TNil) t

(* f : e -> v *)
let f expr = f1 expr [] [] idc TNil