pieuvre/lam.ml

type id = string

type ty_annot = id * Types.ty

type lam =
  Fun of ty_annot * lam
  | App of lam * lam
  | Var of id
  | Exf of lam * Types.ty


(** alpha renaming in a deterministic way *)
let alpha_convert (e : lam) : lam =
  let cpt_var = ref 0 in (* id cpt for variables *)
  let generator (cpt : int ref) : id = (* id generator *)
    let v = "__"^(string_of_int !cpt)
    in incr cpt; v

    in let get_ren_var (var : id) (g : (id * id) list): id = (* returns var if not found *)
    match List.assoc_opt var g with
      | Some var' -> var'
      | None -> var

  in let rec alpha_aux (e : lam) (g : (id * id) list): lam = match e with (* actual renaming *)
    Fun ((v, t), e) ->
      let v' = generator cpt_var in
      Fun ((v', t), alpha_aux e ((v, v')::g))
    | App (e1, e2) -> App (alpha_aux e1 g, alpha_aux e2 g)
    | Var v -> Var (get_ren_var v g)
    | Exf (e, t) -> Exf (alpha_aux e g, t)
  in alpha_aux e []


(** alpha equivalence *)
let (=~) (e1 : lam) (e2 : lam) : bool =
  alpha_convert e1 = alpha_convert e2

(** beta-reduction *)