EduardoRFS · September 1, 2025 19:48
diff --git a/simple-optimal.ml b/simple-optimal.ml
 (*
  Start with an environment based interpreter that does
    all the reductions, including under lambdas.

  Then make everything not on the head path lazy.
  When you go to evaluate everything on the side,
    you force the head producing a potentially stuck value
    and then apply the new environment, progressing further.

  Lazy acts like graph sharing for reductions on the side.
  Everything on the head is shared by the environment.
  
  The env captured by lazy makes a form of environment sharing,
    which seems to be a fundamental requirement for optimality.
 *)

 type var = int

 type term =
  | T_var of var
  | T_let of var * term lazy_t * term
  | T_lambda of var * term lazy_t
  | T_apply of term * term lazy_t

 and env = E_hole | E_let of env * var * term lazy_t

 let rec lookup env var =
  match env with
  | E_hole -> None
  | E_let (env, env_var, arg) -> (
      match Int.equal var env_var with
      | true -> Some arg
      | false -> lookup env var)

 let rec eval_head env term =
  match term with
  | T_var var -> (
      match lookup env var with Some arg -> Lazy.force arg | None -> T_var var)
  | T_let (var, arg, body) ->
      let arg = eval_lazy env arg in
      let env = E_let (env, var, arg) in
      eval_head env body
  | T_lambda (var, body) ->
      let body = eval_lazy env body in
      T_lambda (var, body)
  | T_apply (funct, arg) -> (
      let funct = eval_head env funct in
      let arg = eval_lazy env arg in
      match funct with
      | T_lambda (var, body) ->
          let env = E_let (E_hole, var, arg) in
          let body = Lazy.force body in
          eval_head env body
      | T_var _ | T_let _ | T_apply _ -> T_apply (funct, arg))

 and eval_lazy env term =
  lazy
    (let term = Lazy.force term in
     eval_head env term)
	(*
	Start with an environment based interpreter that does
	all the reductions, including under lambdas.

	Then make everything not on the head path lazy.
	When you go to evaluate everything on the side,
	you force the head producing a potentially stuck value
	and then apply the new environment, progressing further.

	Lazy acts like graph sharing for reductions on the side.
	Everything on the head is shared by the environment.

	The env captured by lazy makes a form of environment sharing,
	which seems to be a fundamental requirement for optimality.
	*)

	type var = int

	type term =
	\| T_var of var
	\| T_let of var * term lazy_t * term
	\| T_lambda of var * term lazy_t
	\| T_apply of term * term lazy_t

	and env = E_hole \| E_let of env * var * term lazy_t

	let rec lookup env var =
	match env with
	\| E_hole -> None
	\| E_let (env, env_var, arg) -> (
	match Int.equal var env_var with
	\| true -> Some arg
	\| false -> lookup env var)

	let rec eval_head env term =
	match term with
	\| T_var var -> (
	match lookup env var with Some arg -> Lazy.force arg \| None -> T_var var)
	\| T_let (var, arg, body) ->
	let arg = eval_lazy env arg in
	let env = E_let (env, var, arg) in
	eval_head env body
	\| T_lambda (var, body) ->
	let body = eval_lazy env body in
	T_lambda (var, body)
	\| T_apply (funct, arg) -> (
	let funct = eval_head env funct in
	let arg = eval_lazy env arg in
	match funct with
	\| T_lambda (var, body) ->
	let env = E_let (E_hole, var, arg) in
	let body = Lazy.force body in
	eval_head env body
	\| T_var _ \| T_let _ \| T_apply _ -> T_apply (funct, arg))

	and eval_lazy env term =
	lazy
	(let term = Lazy.force term in
	eval_head env term)