Evaluator for a lambda calculus with de Bruijn indices, levels, and defunctionalised closures. For more, check out the language garden: https://github.com/brendanzab/language-garden/

lambda_nbe.ml

type index = int
type level = int


type expr =
  | Var of index
  | Let of string * expr * expr
  | Fun_lit of string * expr
  | Fun_app of expr * expr


type value =
  | Neu of neu
  | Fun_lit of string * clos
and neu =
  | Var of level
  | Fun_app of neu * value

and clos = env * expr
and env = value list


let rec eval (vs : env) (e : expr) : value =
  match e with
  | Var index -> List.nth vs index
  | Let (_, def, body) -> eval (eval vs def :: vs) body
  | Fun_lit (x, body) -> Fun_lit (x, (vs, body))
  | Fun_app (head, arg) -> fun_app (eval vs head) (eval vs arg)

and fun_app (head : value) (arg : value) =
  match head with
  | Fun_lit (_, body) -> clos_app body arg
  | Neu nv -> Neu (Fun_app (nv, arg))

and clos_app (vs, e : clos) (arg : value) : value =
  eval (arg :: vs) e


let rec quote (size : int) (v : value) : expr =
  match v with
  | Neu nv -> quote_neu size nv
  | Fun_lit (x, body) -> 
      Fun_lit (x, quote (size + 1) (clos_app body (Neu (Var size))))
and quote_neu (size : int) (nv : neu) : expr =
  match nv with
  | Var level -> Var (size - level - 1)
  | Fun_app (head, arg) -> 
      Fun_app (quote_neu size head, quote size arg)


let normalise (vs : env) (e : expr) : expr =
  quote (List.length vs) (eval vs e)