(* Translating De Bruijn notation to nominal notation. This code
   snippet is particularly easy in terms of proof obligations. *)

(* De Bruijn indices, expressed in unary notation, since we have
   no primitive integers yet. *)

type dbindex =
  | IZero
  | ISucc of dbindex

(* De Bruijn style lambda-terms. *)

type dbterm =
  | DBVar of dbindex
  | DBLambda of dbterm
  | DBApp of dbterm * dbterm

(* Nominal style lambda-terms. *)

type term =
  | Var of atom
  | Lambda of < atom * inner term >
  | App of term * term

(* Environments for translating De Bruijn terms to nominal
   terms. *)

type env =
  | ENil
  | ECons of env * atom

(* The translation code. *)

fun find accepts env, index produces a =
  case env, index of
  | ECons (_, x), IZero ->
      x
  | ECons (env, _), ISucc (index) ->
      find (env, index)
  end

fun import accepts env, dbterm produces term =
  case dbterm of
  | DBVar (index) ->
      Var (find (env, index))
  | DBLambda (dbterm) ->
      fresh x in Lambda (x, import (ECons (env, x), dbterm))
  | DBApp (dbterm1, dbterm2) ->
      App (import (env, dbterm1), import (env, dbterm2))
  end

fun main accepts dbterm produces term
where free(term) == empty (* postcondition not required, but we can prove that it holds *)
=
  import (ENil, dbterm)

(* The reverse translation. *)

fun lookup accepts env, a where free(a) <= free(env) produces index =
  case env of
  | ENil ->
      absurd
  | ECons (env, b) ->
      if a == b then
        IZero
      else
        ISucc (lookup (env, a))
      end
  end

fun export accepts env, t where free(t) <= free(env) produces dbterm =
  case t of
  | Var (x) ->
      DBVar (lookup (env, x))
  | Lambda (x, t) ->
      DBLambda (export (ECons (env, x), t))
  | App (t1, t2) ->
      DBApp (export (env, t1), export (env, t2))
  end

fun malabar accepts t where free(t) == empty produces dbterm =
  export (ENil, t)