eval_lc_secd_deconstruction.ml

(** Interpreters based on the SECD machine from “A Rational Deconstruction of Landin's SECD Machine”

    - Olivier Danvy. 2003. A Rational Deconstruction of Landin’s SECD Machine.
      BRICS Report Series 33 (October 2003). https://doi.org/10.7146/brics.v10i33.21801
*)

module Source = struct

  type ident = string

  type term =
    | Lit of int
    | Var of ident
    | Lam of ident * term
    | App of term * term

  type program = term

end

module type Env = sig

  type 'a env

  val empty : 'a env
  val extend : Source.ident -> 'a -> 'a env -> 'a env
  val lookup : Source.ident -> 'a env -> 'a

end

exception Eval_error

(** Section 2.1 *)
module Original (Env : Env) = struct

  type value =
    | Int of int
    | Succ
    | Clos of value Env.env * Source.ident * Source.term

  let e_init =
    Env.empty
    |> Env.extend "succ" Succ

  type directive =
    | Term of Source.term
    | Apply

  type stack = value list
  type env = value Env.env
  type control = directive list
  type dump = (stack * env * control) list

  let rec run : stack * env * control * dump -> value =
    function
    (* termination *)
    | [v], _, [], [] -> v
    (* function return *)
    | [v], _, [], (s, e, c) :: d -> run (v :: s, e, c, d)

    (* evaluate a literal *)
    | s, e, Term (Lit n) :: c, d -> run (Int n :: s, e, c, d)
    (* evaluate an identifier *)
    | s, e, Term (Var x) :: c, d -> run (Env.lookup x e :: s, e, c, d)
    (* evaluate a lambda abstraction *)
    | s, e, Term (Lam (x, t)) :: c, d -> run (Clos (e, x, t) :: s, e, c, d)
    (* evaluate an application *)
    | s, e, Term (App (t0, t1)) :: c, d -> run (s, e, Term t1 :: Term t0 :: Apply :: c, d)

    (* apply the successor function *)
    | Succ :: Int n :: s, e, Apply :: c, d -> run (Int (n + 1) :: s, e, c, d)
    (* apply an argument to a closure in tail position (OPTIONAL: section 3.3) *)
    | Clos (e', x, t) :: v' :: [], _, [], d ->
        run ([], Env.extend x v' e', [Term t], d)
    (* apply an argument to a closure *)
    | Clos (e', x, t) :: v' :: s, e, Apply :: c, d ->
        run ([], Env.extend x v' e', [Term t], (s, e, c) :: d)
    | _, _, _, _ -> raise Eval_error

  let evaluate : Source.program -> value =
    fun t ->
      run ([], e_init, [Term t], [])

end

(** Section 2.2 *)
module Structured (Env : Env) = struct

  type value =
    | Int of int
    | Succ
    | Clos of value Env.env * Source.ident * Source.term

  let e_init =
    Env.empty
    |> Env.extend "succ" Succ

  type directive =
    | Term of Source.term
    | Apply

  type stack = value list
  type env = value Env.env
  type control = directive list
  type dump = (stack * env * control) list

  (** Interpret the list of control directives *)
  let rec run_c (s : stack) (e : env) (c : control) (d : dump) : value =
    match c with
    | [] -> run_d s d
    | Term t :: c -> run_t t s e c d
    | Apply :: c -> run_a s e c d

  (** Interpret the dump *)
  and run_d (s : stack) (d : dump) : value =
    match s, d with
    | [v], [] -> v
    | [v], (s, e, c) :: d -> run_c (v :: s) e c d
    | _, _ -> raise Eval_error

  (** Interpret the top term in the list of control directives *)
  and run_t (t : Source.term) (s : stack) (e : env) (c : control) (d : dump) : value =
    match t with
    | Lit n -> run_c (Int n :: s) e c d
    | Var x -> run_c (Env.lookup x e :: s) e c d
    | Lam (x, t) -> run_c (Clos (e, x, t) :: s) e c d
    | App (t0, t1) -> run_c s e (Term t1 :: Term t0 :: Apply :: c) d

  (** Run the top value in the current stack *)
  and run_a (s : stack) (e : env) (c : control) (d : dump) : value =
    match s with
    | Succ :: Int n :: s -> run_c (Int (n + 1) :: s) e c d
    | Clos (e', x, t) :: v' :: s -> run_t t [] (Env.extend x v' e') [] ((s, e, c) :: d)
    | _ -> raise Eval_error

  let evaluate (t : Source.program) : value =
    run_t t [] e_init [] []

end

(** Section 2.3 *)
module Higher_order (Env : Env) = struct

  type value =
    | Int of int
    | Succ
    | Clos of value Env.env * Source.ident * Source.term

  let e_init =
    Env.empty
    |> Env.extend "succ" Succ

  type stack = value list
  type env = value Env.env
  type dump = stack -> value
  type control = stack -> env -> dump -> value

  let rec run_t (t : Source.term) (s : stack) (e : env) (c : control) (d : dump) : value =
    match t with
    | Lit n -> c (Int n :: s) e d
    | Var x -> c (Env.lookup x e :: s) e d
    | Lam (x, t) -> c (Clos (e, x, t) :: s) e d
    | App (t0, t1) ->
        run_t t1 s e
          (fun s e d ->
            run_t t0 s e
              (fun s e d -> run_a s e c d)
              d)
          d

  and run_a (s : stack) (e : env) (c : control) (d : dump) : value =
    match s with
    | Succ :: Int n :: s -> c (Int (n + 1) :: s) e d
    | Clos (e', x, t) :: v' :: s ->
        run_t t [] (Env.extend x v' e')
          (fun s _ d -> d s)
          (function [v] -> c (v :: s) e d | _ -> raise Eval_error)
    | _ -> raise Eval_error

  let evaluate (t : Source.program) : value =
    run_t t [] e_init
      (fun s _ d -> d s)
      (function [v] -> v | _ -> raise Eval_error)

end

(** Section 2.4 *)
module Dump_less (Env : Env) = struct

  type value =
    | Int of int
    | Succ
    | Clos of value Env.env * Source.ident * Source.term

  let e_init =
    Env.empty
    |> Env.extend "succ" Succ

  type stack = value list
  type env = value Env.env
  type control = stack -> env -> stack

  let rec eval (t : Source.term) (s : stack) (e : env) (c : control) : stack =
    match t with
    | Lit n -> c (Int n :: s) e
    | Var x -> c (Env.lookup x e :: s) e
    | Lam (x, t) -> c (Clos (e, x, t) :: s) e
    | App (t0, t1) ->
        (eval [@tailcall]) t1 s e
          (fun s e ->
            (eval [@tailcall]) t0 s e
              (fun s e -> apply s e c))

  and apply (s : stack) (e : env) (c : control) : stack =
    match s with
    | Succ :: Int n :: s -> c (Int (n + 1) :: s) e
    | Clos (e', x, t) :: v' :: s ->
        begin match eval t [] (Env.extend x v' e') (fun s _ -> s) with
        | [v] -> c (v :: s) e
        | _ -> raise Eval_error
        end
    | _ -> raise Eval_error

  let evaluate (t : Source.program) : value =
    match eval t [] e_init (fun s _ -> s) with
    | [v] -> v
    | _ -> raise Eval_error

end

(** Section 2.5 *)
module Control_less (Env : Env) = struct

  type value =
    | Int of int
    | Succ
    | Clos of value Env.env * Source.ident * Source.term

  let e_init =
    Env.empty
    |> Env.extend "succ" Succ

  (* mock-up??? *)
  let reset : type a. (unit -> a) -> a =
    fun thunk -> thunk ()

  type stack = value list
  type env = value Env.env

  let rec eval (t : Source.term) (s : stack) (e : env) : stack * env =
    match t with
    | Lit n -> Int n :: s, e
    | Var x -> Env.lookup x e :: s, e
    | Lam (x, t) -> Clos (e, x, t) :: s, e
    | App (t0, t1) ->
        let s, e = eval t1 s e in
        let s, e = eval t0 s e in
        apply s e

  and apply (s : stack) (e : env) :  stack * env =
    match s with
    | Succ :: Int n :: s -> Int (n + 1) :: s, e
    | Clos (e', x, t) :: v' :: s ->
        begin match reset (fun () -> eval t [] (Env.extend x v' e')) with
        | [v], _ -> v :: s, e
        | _, _ -> raise Eval_error
        end
    | _ -> raise Eval_error

  let evaluate : Source.program -> value =
    fun t ->
      match reset (fun () -> eval t [] e_init) with
      | [v], _ -> v
      | _, _ -> raise Eval_error

end

(** Section 2.6 *)
module Stack_less (Env : Env) = struct

  type value =
    | Int of int
    | Succ
    | Clos of value Env.env * Source.ident * Source.term

  let e_init =
    Env.empty
    |> Env.extend "succ" Succ

  (* mock-up??? *)
  let reset : type a. (unit -> a) -> a =
    fun thunk -> thunk ()

  type env = value Env.env

  let rec eval(t : Source.term) (e : env) : value * env =
    match t with
    | Lit n -> Int n, e
    | Var x -> Env.lookup x e, e
    | Lam (x, t) -> Clos (e, x, t), e
    | App (t0, t1) ->
        let v1, e = eval t1 e in
        let v0, e = eval t0 e in
        apply v0 v1 e

  and apply (v0 : value) (v1 : value) (e : env) : value * env =
    match v0, v1 with
    | Succ, Int n -> Int (n + 1), e
    | Clos (e', x, t), v' ->
        let v, _ = reset (fun () -> eval t (Env.extend x v' e')) in
        v, e
    | _, _ -> raise Eval_error

  let evaluate (t : Source.program) : value =
    let v, _ = reset (fun () -> eval t e_init) in
    v

end

(** Section 2.7 *)
module Compositional (Env : Env) = struct

  type value =
    | Int of int
    | Succ
    | Fun of (value -> value)

  let e_init =
    Env.empty
    |> Env.extend "succ" Succ

  (* mock-up??? *)
  let reset : type a. (unit -> a) -> a =
    fun thunk -> thunk ()

  type env = value Env.env

  let rec eval(t : Source.term) (e : env) : value * env =
    match t with
    | Lit n -> Int n, e
    | Var x -> Env.lookup x e, e
    | Lam (x, t) ->
        Fun (fun v ->
          reset (fun () ->
            let v', _ = eval t (Env.extend x v e) in
            v')),
        e
    | App (t0, t1) ->
        let v1, e = eval t1 e in
        let v0, e = eval t0 e in
        apply v0 v1 e

  and apply (v0 : value) (v1 : value) (e : env) : value * env =
    match v0, v1 with
    | Succ, Int n -> Int (n + 1), e
    | Fun f, v -> f v, e
    | _, _ -> raise Eval_error

  let evaluate (t : Source.program) : value =
    let v, _ = reset (fun () -> eval t e_init) in
    v

end