Merge pull request #9216 from gasche/lambda-duplicate
extend Lambda.subst on bound variables, add Lambda.duplicatemaster
Gabriel Scherer
GitHub
commit
50806ced7f
3
Changes
3
Changes
|
|
@ -183,6 +183,9 @@ Working version
|
|||
|
||||
### Internal/compiler-libs changes:
|
||||
|
||||
- #9216: add Lambda.duplicate which refreshes bound identifiers
|
||||
(Gabriel Scherer, review by Pierre Chambart and Vincent Laviron)
|
||||
|
||||
- #9493, #9520, #9563, #9599, #9608: refactor the pattern-matching compiler
|
||||
(Thomas Refis and Gabriel Scherer, review by Florian Angeletti)
|
||||
|
||||
|
|
|
|||
156
lambda/lambda.ml
156
lambda/lambda.ml
|
|
@ -684,79 +684,120 @@ let rec make_sequence fn = function
|
|||
Assumes that the image of the substitution is out of reach
|
||||
of the bound variables of the lambda-term (no capture). *)
|
||||
|
||||
let subst update_env s lam =
|
||||
let rec subst s lam =
|
||||
let remove_list l s =
|
||||
List.fold_left (fun s (id, _kind) -> Ident.Map.remove id s) s l
|
||||
in
|
||||
let subst update_env ?(freshen_bound_variables = false) s input_lam =
|
||||
(* [s] contains a partial substitution for the free variables of the
|
||||
input term [input_lam].
|
||||
|
||||
During our traversal of the term we maintain a second environment
|
||||
[l] with all the bound variables of [input_lam] in the current
|
||||
scope, mapped to either themselves or freshened versions of
|
||||
themselves when [freshen_bound_variables] is set. *)
|
||||
let bind id l =
|
||||
let id' = if not freshen_bound_variables then id else Ident.rename id in
|
||||
id', Ident.Map.add id id' l
|
||||
in
|
||||
let bind_many ids l =
|
||||
List.fold_right (fun (id, rhs) (ids', l) ->
|
||||
let id', l = bind id l in
|
||||
((id', rhs) :: ids' , l)
|
||||
) ids ([], l)
|
||||
in
|
||||
let rec subst s l lam =
|
||||
match lam with
|
||||
| Lvar id as l ->
|
||||
begin try Ident.Map.find id s with Not_found -> l end
|
||||
| Lvar id as lam ->
|
||||
begin match Ident.Map.find id l with
|
||||
| id' -> Lvar id'
|
||||
| exception Not_found ->
|
||||
(* note: as this point we know [id] is not a bound
|
||||
variable of the input term, otherwise it would belong
|
||||
to [l]; it is a free variable of the input term. *)
|
||||
begin try Ident.Map.find id s with Not_found -> lam end
|
||||
end
|
||||
| Lconst _ as l -> l
|
||||
| Lapply ap ->
|
||||
Lapply{ap with ap_func = subst s ap.ap_func;
|
||||
ap_args = subst_list s ap.ap_args}
|
||||
Lapply{ap with ap_func = subst s l ap.ap_func;
|
||||
ap_args = subst_list s l ap.ap_args}
|
||||
| Lfunction lf ->
|
||||
let s =
|
||||
List.fold_right
|
||||
(fun (id, _) s -> Ident.Map.remove id s)
|
||||
lf.params s
|
||||
in
|
||||
Lfunction {lf with body = subst s lf.body}
|
||||
let params, l' = bind_many lf.params l in
|
||||
Lfunction {lf with params; body = subst s l' lf.body}
|
||||
| Llet(str, k, id, arg, body) ->
|
||||
Llet(str, k, id, subst s arg, subst (Ident.Map.remove id s) body)
|
||||
let id, l' = bind id l in
|
||||
Llet(str, k, id, subst s l arg, subst s l' body)
|
||||
| Lletrec(decl, body) ->
|
||||
let s =
|
||||
List.fold_left (fun s (id, _) -> Ident.Map.remove id s)
|
||||
s decl
|
||||
in
|
||||
Lletrec(List.map (subst_decl s) decl, subst s body)
|
||||
| Lprim(p, args, loc) -> Lprim(p, subst_list s args, loc)
|
||||
let decl, l' = bind_many decl l in
|
||||
Lletrec(List.map (subst_decl s l') decl, subst s l' body)
|
||||
| Lprim(p, args, loc) -> Lprim(p, subst_list s l args, loc)
|
||||
| Lswitch(arg, sw, loc) ->
|
||||
Lswitch(subst s arg,
|
||||
{sw with sw_consts = List.map (subst_case s) sw.sw_consts;
|
||||
sw_blocks = List.map (subst_case s) sw.sw_blocks;
|
||||
sw_failaction = subst_opt s sw.sw_failaction; },
|
||||
Lswitch(subst s l arg,
|
||||
{sw with sw_consts = List.map (subst_case s l) sw.sw_consts;
|
||||
sw_blocks = List.map (subst_case s l) sw.sw_blocks;
|
||||
sw_failaction = subst_opt s l sw.sw_failaction; },
|
||||
loc)
|
||||
| Lstringswitch (arg,cases,default,loc) ->
|
||||
Lstringswitch
|
||||
(subst s arg,List.map (subst_strcase s) cases,subst_opt s default,loc)
|
||||
| Lstaticraise (i,args) -> Lstaticraise (i, subst_list s args)
|
||||
(subst s l arg,
|
||||
List.map (subst_strcase s l) cases,
|
||||
subst_opt s l default,
|
||||
loc)
|
||||
| Lstaticraise (i,args) -> Lstaticraise (i, subst_list s l args)
|
||||
| Lstaticcatch(body, (id, params), handler) ->
|
||||
Lstaticcatch(subst s body, (id, params),
|
||||
subst (remove_list params s) handler)
|
||||
let params, l' = bind_many params l in
|
||||
Lstaticcatch(subst s l body, (id, params),
|
||||
subst s l' handler)
|
||||
| Ltrywith(body, exn, handler) ->
|
||||
Ltrywith(subst s body, exn, subst (Ident.Map.remove exn s) handler)
|
||||
| Lifthenelse(e1, e2, e3) -> Lifthenelse(subst s e1, subst s e2, subst s e3)
|
||||
| Lsequence(e1, e2) -> Lsequence(subst s e1, subst s e2)
|
||||
| Lwhile(e1, e2) -> Lwhile(subst s e1, subst s e2)
|
||||
let exn, l' = bind exn l in
|
||||
Ltrywith(subst s l body, exn, subst s l' handler)
|
||||
| Lifthenelse(e1, e2, e3) ->
|
||||
Lifthenelse(subst s l e1, subst s l e2, subst s l e3)
|
||||
| Lsequence(e1, e2) -> Lsequence(subst s l e1, subst s l e2)
|
||||
| Lwhile(e1, e2) -> Lwhile(subst s l e1, subst s l e2)
|
||||
| Lfor(v, lo, hi, dir, body) ->
|
||||
Lfor(v, subst s lo, subst s hi, dir,
|
||||
subst (Ident.Map.remove v s) body)
|
||||
let v, l' = bind v l in
|
||||
Lfor(v, subst s l lo, subst s l hi, dir, subst s l' body)
|
||||
| Lassign(id, e) ->
|
||||
assert(not (Ident.Map.mem id s));
|
||||
Lassign(id, subst s e)
|
||||
assert (not (Ident.Map.mem id s));
|
||||
let id = try Ident.Map.find id l with Not_found -> id in
|
||||
Lassign(id, subst s l e)
|
||||
| Lsend (k, met, obj, args, loc) ->
|
||||
Lsend (k, subst s met, subst s obj, subst_list s args, loc)
|
||||
Lsend (k, subst s l met, subst s l obj, subst_list s l args, loc)
|
||||
| Levent (lam, evt) ->
|
||||
let lev_env =
|
||||
Ident.Map.fold (fun id _ env ->
|
||||
match Env.find_value (Path.Pident id) evt.lev_env with
|
||||
| exception Not_found -> env
|
||||
| vd -> update_env id vd env
|
||||
) s evt.lev_env
|
||||
let old_env = evt.lev_env in
|
||||
let env_updates =
|
||||
let find_in_old id = Env.find_value (Path.Pident id) old_env in
|
||||
let rebind id id' new_env =
|
||||
match find_in_old id with
|
||||
| exception Not_found -> new_env
|
||||
| vd -> Env.add_value id' vd new_env
|
||||
in
|
||||
let update_free id new_env =
|
||||
match find_in_old id with
|
||||
| exception Not_found -> new_env
|
||||
| vd -> update_env id vd new_env
|
||||
in
|
||||
Ident.Map.merge (fun id bound free ->
|
||||
match bound, free with
|
||||
| Some id', _ ->
|
||||
if Ident.equal id id' then None else Some (rebind id id')
|
||||
| None, Some _ -> Some (update_free id)
|
||||
| None, None -> None
|
||||
) l s
|
||||
in
|
||||
Levent (subst s lam, { evt with lev_env })
|
||||
| Lifused (v, e) -> Lifused (v, subst s e)
|
||||
and subst_list s l = List.map (subst s) l
|
||||
and subst_decl s (id, exp) = (id, subst s exp)
|
||||
and subst_case s (key, case) = (key, subst s case)
|
||||
and subst_strcase s (key, case) = (key, subst s case)
|
||||
and subst_opt s = function
|
||||
let new_env =
|
||||
Ident.Map.fold (fun _id update env -> update env) env_updates old_env
|
||||
in
|
||||
Levent (subst s l lam, { evt with lev_env = new_env })
|
||||
| Lifused (id, e) ->
|
||||
let id = try Ident.Map.find id l with Not_found -> id in
|
||||
Lifused (id, subst s l e)
|
||||
and subst_list s l li = List.map (subst s l) li
|
||||
and subst_decl s l (id, exp) = (id, subst s l exp)
|
||||
and subst_case s l (key, case) = (key, subst s l case)
|
||||
and subst_strcase s l (key, case) = (key, subst s l case)
|
||||
and subst_opt s l = function
|
||||
| None -> None
|
||||
| Some e -> Some (subst s e)
|
||||
| Some e -> Some (subst s l e)
|
||||
in
|
||||
subst s lam
|
||||
subst s Ident.Map.empty input_lam
|
||||
|
||||
let rename idmap lam =
|
||||
let update_env oldid vd env =
|
||||
|
|
@ -766,6 +807,13 @@ let rename idmap lam =
|
|||
let s = Ident.Map.map (fun new_id -> Lvar new_id) idmap in
|
||||
subst update_env s lam
|
||||
|
||||
let duplicate lam =
|
||||
subst
|
||||
(fun _ _ env -> env)
|
||||
~freshen_bound_variables:true
|
||||
Ident.Map.empty
|
||||
lam
|
||||
|
||||
let shallow_map f = function
|
||||
| Lvar _
|
||||
| Lconst _ as lam -> lam
|
||||
|
|
|
|||
|
|
@ -379,21 +379,30 @@ val transl_class_path: scoped_location -> Env.t -> Path.t -> lambda
|
|||
|
||||
val make_sequence: ('a -> lambda) -> 'a list -> lambda
|
||||
|
||||
val subst: (Ident.t -> Types.value_description -> Env.t -> Env.t) ->
|
||||
val subst:
|
||||
(Ident.t -> Types.value_description -> Env.t -> Env.t) ->
|
||||
?freshen_bound_variables:bool ->
|
||||
lambda Ident.Map.t -> lambda -> lambda
|
||||
(** [subst env_update_fun s lt] applies a substitution [s] to the lambda-term
|
||||
[lt].
|
||||
(** [subst update_env ?freshen_bound_variables s lt]
|
||||
applies a substitution [s] to the lambda-term [lt].
|
||||
|
||||
Assumes that the image of the substitution is out of reach
|
||||
of the bound variables of the lambda-term (no capture).
|
||||
|
||||
[env_update_fun] is used to refresh the environment contained in debug
|
||||
events. *)
|
||||
[update_env] is used to refresh the environment contained in debug
|
||||
events.
|
||||
|
||||
[freshen_bound_variables], which defaults to [false], freshens
|
||||
the bound variables within [lt].
|
||||
*)
|
||||
|
||||
val rename : Ident.t Ident.Map.t -> lambda -> lambda
|
||||
(** A version of [subst] specialized for the case where we're just renaming
|
||||
idents. *)
|
||||
|
||||
val duplicate : lambda -> lambda
|
||||
(** Duplicate a term, freshening all locally-bound identifiers. *)
|
||||
|
||||
val map : (lambda -> lambda) -> lambda -> lambda
|
||||
(** Bottom-up rewriting, applying the function on
|
||||
each node from the leaves to the root. *)
|
||||
|
|
|
|||
Loading…
Reference in New Issue