diff --git a/lam.ml b/lam.ml index 71f2341..12caae1 100644 --- a/lam.ml +++ b/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) diff --git a/main.ml b/main.ml index 2e175e0..c8b95d2 100644 --- a/main.ml +++ b/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) diff --git a/tests/alpha_equiv/throwaway1.lam b/tests/alpha_equiv/throwaway1.lam new file mode 100644 index 0000000..4db31c6 --- /dev/null +++ b/tests/alpha_equiv/throwaway1.lam @@ -0,0 +1 @@ +fun (x : A) => fun (x : A) => x & fun (y : A) => fun (x : A) => x diff --git a/tests/alpha_equiv/throwaway2.lam b/tests/alpha_equiv/throwaway2.lam new file mode 100644 index 0000000..a392ed3 --- /dev/null +++ b/tests/alpha_equiv/throwaway2.lam @@ -0,0 +1 @@ +fun (x : A) => fun (x : A) => x & fun (x : A) => fun (y : A) => x