diff options
| author | Pierre-Marie Pédrot | 2019-05-06 17:05:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-28 13:07:51 +0200 |
| commit | eabcd5cfe9d96192747d40776668489f9c5e545c (patch) | |
| tree | 1278cf64bce8ec6aa682ca4c4fb8512272d4cdaf /engine/evarutil.ml | |
| parent | aa52ef99b90ada505d86fea4f4e7d500b9be2433 (diff) | |
Tentative alternative fix for #9992.
We crawl the context in the other direction, preventing the allocation of
the return boolean and enhancing sharing. This fast-path is assuming the
heuristic that the variable being renamed always appears in the context,
otherwise we would be renaming for nothing. It seems to always be the
case, due to the way we pick the set of names to be avoided.
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 25 |
1 files changed, 10 insertions, 15 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 4bff98c0c2..42b9fa4714 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -331,21 +331,16 @@ let push_rel_decl_to_named_context let map_decl f d = NamedDecl.map_constr f d in - let replace_var_named_declaration id0 id nc = - let rec replace = function - | [] -> false, [] - | decl :: nc -> - let seen, nc = replace nc in - if seen then - let vsubst = [id0 , mkVar id] in - true, (map_decl (fun c -> replace_vars vsubst c) decl) :: nc - else if Id.equal id0 (NamedDecl.get_id decl) then - true, (NamedDecl.set_id id decl) :: nc - else - false, decl :: nc - in - let (_, nc) = replace nc in - nc + let rec replace_var_named_declaration id0 id = function + | [] -> [] + | decl :: nc -> + if Id.equal id0 (NamedDecl.get_id decl) then + (* Stop here, the variable cannot occur before its definition *) + (NamedDecl.set_id id decl) :: nc + else + let nc = replace_var_named_declaration id0 id nc in + let vsubst = [id0 , mkVar id] in + map_decl (fun c -> replace_vars vsubst c) decl :: nc in let extract_if_neq id = function | Anonymous -> None |