scope.ml

type var = string

module Term = struct
  type t =
    | Int of int
    | Lam of var * t
    | Var of var
    | App of t * t
end

module WellScoped = struct
  type _ index =
    | S : 'a index -> (unit * 'a) index
    | Z : (unit * _) index

  type ('a, _) env =
    | Nil : (_, unit) env
    | Cons : 'a * ('a, 'e) env -> ('a, unit * 'e) env

  let rec partial_lookup env var =
    let rec loop : type t . (_, t) env -> t index = function
      | Nil -> failwith ("unbound: " ^ var)
      | Cons (name, xs) -> if var = name then Z else S (loop xs) in
    loop env

  let rec total_lookup env index =
    let rec loop : type t . ('a, t) env -> t index -> 'a =
      fun e i ->
        match e, i with
        | Cons (_, e'), S i' -> loop e' i'
        | Cons (x, _), Z -> x
        | Nil, _ -> . in
    loop env index

  type 'env t =
    | Int : int -> _ t
    | Lam : (unit * 'env) t -> 'env t
    | Var : 'env index -> 'env t
    | App : 'env t * 'env t -> 'env t

  let rec well_scoped : type a . (var, a) env -> Term.t -> a t =
    fun env term ->
      match term with
      | Term.Int n -> Int n
      | Term.Lam (arg, body) -> Lam (well_scoped (Cons (arg, env)) body)
      | Term.Var name -> Var (partial_lookup env name)
      | Term.App (f, x) -> App (well_scoped env f, well_scoped env x)
end

module W = WellScoped

module Phoas = struct
  type 'a t =
    | Int of int
    | Lam of ('a -> 'a t)
    | Var of 'a
    | App of 'a t * 'a t

  let rec from_scoped : type a . (_, a) W.env -> a W.t -> _ t =
    fun env -> function
      | W.Int n -> Int n
      | W.Lam body -> Lam (fun x -> from_scoped (W.Cons (x, env)) body)
      | W.Var idx -> Var (W.total_lookup env idx)
      | W.App (f, x) -> App (from_scoped env f, from_scoped env x)
end

let to_phoas term =
  Phoas.from_scoped W.Nil (W.well_scoped W.Nil term)

let to_phoas_open term env1 env2 =
  Phoas.from_scoped env1 (W.well_scoped env2 term)