l3-ENSL/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fix alpha renaming

Browse Source
This commit is contained in:
augustin64 2024-04-16 10:40:50 +02:00
parent bc697b30a0
commit 5af7419020
1 changed files with 12 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
lam.ml
View File

@ -10,31 +10,28 @@ type lam =
(** alpha renaming in a deterministic way *) (** alpha renaming in a deterministic way *)
let alpha_convert (e : lam) : lam = let alpha_convert (e : lam) : lam =
let cpt_ty = ref 0 in (* id cpt for type variables *)
let cpt_var = ref 0 in (* id cpt for variables *) let cpt_var = ref 0 in (* id cpt for variables *)
let generator (cpt : int ref) : id = (* id generator *) let generator (cpt : int ref) : id = (* id generator *)
let v = string_of_int !cpt let v = "__"^(string_of_int !cpt)
in incr cpt; v in incr cpt; v
in let renamed = ref [] 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 *) in let new_ren_var (cpt : int ref) (var : id) : id = (* checks if a variable already has a new id, or generates one *)
let var' = generator cpt in (
renamed := (var, var')::!renamed;
var'
)
in let get_ren_var (var : id) : id = (* returns var if not found *)
match List.assoc_opt var !renamed with match List.assoc_opt var !renamed with
| Some var' -> var' | Some var' -> var'
| None -> let var' = generator cpt in ( | None -> var
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 : lam) : lam = match e with (* actual renaming *) in let rec alpha_aux (e : lam) : lam = match e with (* actual renaming *)
Fun ((v, t), e) -> Fun ((rename cpt_var v, alpha_ty t), alpha_aux e) Fun ((v, t), e) -> Fun ((new_ren_var cpt_var v, t), alpha_aux e)
| App (e1, e2) -> App (alpha_aux e1, alpha_aux e2) | App (e1, e2) -> App (alpha_aux e1, alpha_aux e2)
| Var v -> Var (rename cpt_var v) | Var v -> Var (get_ren_var v)
| Exf (e, s) -> Exf (alpha_aux e, s) | Exf (e, t) -> Exf (alpha_aux e, t)
in alpha_aux e in alpha_aux e