From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 pretyping/glob_ops.ml | 94 ++++++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 90 insertions(+), 4 deletions(-)

(limited to 'pretyping/glob_ops.ml')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index c9860864..51660818 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -266,7 +266,7 @@ let add_name_to_ids set na =
     | Anonymous -> set
     | Name id -> Id.Set.add id set
 
-let free_glob_vars  =
+let free_glob_vars =
   let rec vars bounded vs = function
     | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
     | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
@@ -324,10 +324,24 @@ let free_glob_vars  =
     let vs = vars Id.Set.empty Id.Set.empty rt in
     Id.Set.elements vs
 
+let glob_visible_short_qualid c =
+  let rec aux acc = function
+    | GRef (_,c,_) ->
+        let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in
+        let dir,id = Libnames.repr_qualid  qualid in
+        if DirPath.is_empty dir then id :: acc else acc
+    | c ->
+        fold_glob_constr aux acc c
+  in aux [] c
+
+let warn_variable_collision =
+  let open Pp in
+  CWarnings.create ~name:"variable-collision" ~category:"ltac"
+         (fun name ->
+          strbrk "Collision between bound variables of name " ++ pr_id name)
+
 let add_and_check_ident id set =
-  if Id.Set.mem id set then
-    Pp.(msg_warning
-      (str "Collision between bound variables of name " ++ Id.print id));
+  if Id.Set.mem id set then warn_variable_collision id;
   Id.Set.add id set
 
 let bound_glob_vars =
@@ -455,6 +469,78 @@ let loc_of_glob_constr = function
   | GHole (loc,_,_,_) -> loc
   | GCast (loc,_,_) -> loc
 
+(**********************************************************************)
+(* Alpha-renaming                                                     *)
+
+let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l
+let test_id l id = if collide_id l id then raise Not_found
+let test_na l na = name_iter (test_id l) na
+
+let update_subst na l =
+  let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in
+  let l' = name_fold Id.List.remove_assoc na l in
+  name_fold
+    (fun id _ ->
+     if in_range id l' then
+       let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in
+       Name id', (id,id')::l
+     else na,l)
+    na (na,l)
+
+exception UnsoundRenaming
+
+let rename_var l id =
+  try
+    let id' = Id.List.assoc id l in
+    (* Check that no other earlier binding hide the one found *)
+    let _,(id'',_) = List.extract_first (fun (_,id) -> Id.equal id id') l in
+    if Id.equal id id'' then id' else raise UnsoundRenaming
+  with Not_found ->
+    if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
+    else id
+
+let rec rename_glob_vars l = function
+  | GVar (loc,id) as r ->
+      let id' = rename_var l id in
+      if id == id' then r else GVar (loc,id')
+  | GRef (_,VarRef id,_) as r ->
+      if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
+      else r
+  | GProd (loc,na,bk,t,c) ->
+      let na',l' = update_subst na l in
+      GProd (loc,na,bk,rename_glob_vars l t,rename_glob_vars l' c)
+  | GLambda (loc,na,bk,t,c) ->
+      let na',l' = update_subst na l in
+      GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c)
+  | GLetIn (loc,na,b,c) ->
+      let na',l' = update_subst na l in
+      GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c)
+  (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *)
+  | GCases (loc,ci,po,tomatchl,cls) ->
+      let test_pred_pat (na,ino) =
+        test_na l na; Option.iter (fun (_,_,nal) -> List.iter (test_na l) nal) ino in
+      let test_clause idl = List.iter (test_id l) idl in
+      let po = Option.map (rename_glob_vars l) po in
+      let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in
+      let cls = Util.List.map_left (fun (loc,idl,p,c) -> test_clause idl; (loc,idl,p,rename_glob_vars l c)) cls in
+      GCases (loc,ci,po,tomatchl,cls)
+  | GLetTuple (loc,nal,(na,po),c,b) ->
+     List.iter (test_na l) (na::nal);
+     GLetTuple (loc,nal,(na,Option.map (rename_glob_vars l) po),
+                rename_glob_vars l c,rename_glob_vars l b)
+  | GIf (loc,c,(na,po),b1,b2) ->
+     test_na l na;
+     GIf (loc,rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po),
+          rename_glob_vars l b1,rename_glob_vars l b2)
+  | GRec (loc,k,idl,decls,bs,ts) ->
+     Array.iter (test_id l) idl;
+     GRec (loc,k,idl,
+           Array.map (List.map (fun (na,k,bbd,bty) ->
+             test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls,
+           Array.map (rename_glob_vars l) bs,
+           Array.map (rename_glob_vars l) ts)
+  | r -> map_glob_constr (rename_glob_vars l) r
+
 (**********************************************************************)
 (* Conversion from glob_constr to cases pattern, if possible            *)
 
-- 
cgit v1.2.3