on rend l'alpha conversion lisible en gardant les noms de variables

lam.ml

@@ -8,21 +8,23 @@ type lam =
   | Var of id
   | Exf of lam * Types.ty
 
-(** alpha renaming in a deterministic way *)
-let alpha_convert (e : lam) : lam =
+(** alpha renaming in a deterministic way
+    if readable is set to true, original variable's names are used to rename *)
+let alpha_convert ?(readable=false) (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
+  let generator (v : id) (cpt : int ref) : id = (* id generator *)
+    let start = if readable then v else "" in
+    let v = start ^ "__"^(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 *)
+  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
+      let v' = generator v 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)

main.ml

@@ -16,7 +16,7 @@ let beta_reduce e =
     | None -> ()
   in print_expr e;
   print_newline ();
-  let e = Lam.alpha_convert e in
+  let e = Lam.alpha_convert ~readable:true e in
   print_expr e;
   print_newline ();
   aux (Lam.betastep e)

tests/alpha_equiv/throwaway1.lam

@@ -0,0 +1 @@
+fun (x : A) => fun (x : A) => x & fun (y : A) => fun (x : A) => x

tests/alpha_equiv/throwaway2.lam

@@ -0,0 +1 @@
+fun (x : A) => fun (x : A) => x & fun (x : A) => fun (y : A) => x