structure LambdaCalcDelConts = struct
  (* Lambda term (encoded using de bruijn indices),
     booleans and delimited continuations *)
  datatype term =
      Bool of bool
    | Int of Int64.int
    | Branch of term * term * term
    | Var of int
    | Lambda of term
    | App of term * term
    | BuiltinApp of builtin_op * term * term
    | Fix of term
    | Shift of term
    | Reset of term
  and builtin_op = Sum | Sub | LessThan | Equal

  (* Value, the result of a computation *)
  datatype value =
      Closure of env * term
    | Continuation of value -> value
    | BoolV of bool
    | IntV of Int64.int
    | Loop

  (* Why a ref? Because of Fix! We want to update this value post-hoc *)
  and env = Env of value ref list
 

  fun pretty_print_value (Closure _) = "<closure>"
    | pretty_print_value (Continuation _) = "<cont>"
    | pretty_print_value (BoolV b) = Bool.toString b
    | pretty_print_value (IntV n) = Int64.toString n
    | pretty_print_value Loop = "<loop>"


  val empty_env = Env []

  fun env_push_ref (r, Env e) = Env (r :: e)
  fun env_push_value (v, e) = env_push_ref (ref v, e)

  exception UnboundVar

  fun env_lookup (idx, Env e) = !(List.nth (e, idx))
    handle Subscript => raise UnboundVar

  exception Stuck of string

  (* Handle a possibly recursion record *)
  fun unpack_recursion Loop = raise Stuck "<infinite loop>"
    | unpack_recursion x = x

  fun identity x = x

  (* To interpret continuations, we define a continuation
     passing style evaluator. This makes them very straightforward to implement.
     Although WARNING: performances are degraded.
     A first solution is defunctionalization. But it is not enough! *)

  fun eval env (Bool b) k = k (BoolV b)
    | eval env (Int n) k = k (IntV n)
    | eval env (Branch (cond, trueb, falseb)) k = eval env cond (branch_cont env trueb falseb k)
    | eval env (Var idx) k = k (unpack_recursion (env_lookup (idx, env)))
    | eval env (Lambda t) k = k (Closure (env, t))
    | eval env (App (lhs, rhs)) k = eval env lhs (app_cont env rhs k)
    | eval env (BuiltinApp (oper, lhs, rhs)) k = eval env lhs (builtin_app_cont env oper rhs k)
    | eval env (Fix body) k =
        let val self = ref Loop
        in eval (env_push_ref (self, env)) body (fix_cont self k)
        end

    | eval env (Reset body) k =
        (* The identity is what makes the continuation delimited!
           We don't capture the full program continuation, but just the chunk
           inside the reset block
        *)
        k (eval env body identity)

    | eval env (Shift body) k = app_cont2 env body k (Continuation k)

  and branch_cont env trueb _ k (BoolV true) = eval env trueb k
    | branch_cont env _ falseb k (BoolV false) = eval env falseb k
    | branch_cont _ _ _ _ _ = raise Stuck "If conditional is not a boolean"

  and app_cont env rhs k (Closure (benv, body)) = eval env rhs (app_cont2 benv body k)
    (* Observe how in this clause the continuation k is discarded! We are following a different path! *)
    | app_cont env rhs _ (Continuation capt_k) = eval env rhs (invoke_continuation capt_k)
    | app_cont _ _ _ _ = raise Stuck "Left hand side of application is not a function nor continuation"

  and app_cont2 env body k arg = eval (env_push_value (arg, env)) body k
  and invoke_continuation capt_k arg = capt_k arg

  and builtin_app_cont env oper rhs k (IntV n1) = eval env rhs (builtin_app_cont2 n1 oper k)
    | builtin_app_cont _ _ _ _ _ = raise Stuck "Builtin op left argument is not an int"
  and builtin_app_cont2 n1 Sum k (IntV n2) = k (IntV (n1 + n2))
    | builtin_app_cont2 n1 Sub k (IntV n2) = k (IntV (n1 - n2))
    | builtin_app_cont2 n1 LessThan k (IntV n2) = k (BoolV (n1 < n2))
    | builtin_app_cont2 n1 Equal k (IntV n2) = k (BoolV (n1 = n2))
    | builtin_app_cont2 _ _ _ _ = raise Stuck "Builtin op riht argument is not an int"

  and fix_cont self k v =
        let val _ = self := v
        in k v
        end

  fun evaluate term = eval empty_env term identity
end