pieuvre/expr.ml

type id = string

type ty_annot = id * Types.ty

type expr =
  Fun of ty_annot * expr
  | App of expr * expr
  | Var of id
  | Exf of expr * string

(** alpha renaming in a deterministic way *)
let alpha_convert (e : expr) : expr =
  let cpt_ty = ref 0 in (* id cpt for type variables *)
  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 renamed = ref []
  in let rename (cpt : int ref) (var : id) : id = (* checks if a variable already has a new id, or generates one *)
    match List.assoc_opt var !renamed with
      | Some var' -> var'
      | None -> let var' = generator cpt in (
          renamed := (var, var')::!renamed;
          var')

  in let rec alpha_ty (t : Types.ty) : Types.ty = match t with
    Arr (t1, t2) -> Arr (alpha_ty t1, alpha_ty t2)
    | TVar (v) -> TVar (rename cpt_ty v)
    | Bot -> Bot

  
  in let rec alpha_aux (e : expr) : expr = match e with (* actual renaming *)
    Fun ((v, t), e) -> Fun ((rename cpt_var v, alpha_ty t), alpha_aux e)
    | App (e1, e2) -> App (alpha_aux e1, alpha_aux e2)
    | Var v -> Var (rename cpt_var v)
    | Exf (e, s) -> Exf (alpha_aux e, s)
  in alpha_aux e


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