Suppression capture des variables par lieurs non liés dans Notation; simplification bound_binders

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6314 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 20 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 4ce07815e..c483327b6 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -250,36 +250,33 @@ let discriminate_patterns nl l1 l2 =
 
 let aconstr_and_vars_of_rawconstr a =
   let found = ref [] in
-  let bound_binders = ref [] in
   let rec aux = function
-  | RVar (_,id) -> 
-      if not (List.mem id !bound_binders) then found := id::!found;
-      AVar id
+  | RVar (_,id) -> found := id::!found; AVar id
   | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args 
   | RApp (_,g,args) -> AApp (aux g, List.map aux args)
-  | RLambda (_,na,ty,c) -> add_name bound_binders na; ALambda (na,aux ty,aux c)
-  | RProd (_,na,ty,c) -> add_name bound_binders na; AProd (na,aux ty,aux c)
-  | RLetIn (_,na,b,c) -> add_name bound_binders na; ALetIn (na,aux b,aux c)
+  | RLambda (_,na,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
+  | RProd (_,na,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
+  | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
   | RCases (_,(tyopt,rtntypopt),tml,eqnl) ->
       let f (_,idl,pat,rhs) =
-        bound_binders := idl@(!bound_binders);
+        found := idl@(!found);
         (idl,pat,aux rhs) in
       ACases (option_app aux tyopt,
         option_app aux !rtntypopt,
         List.map (fun (tm,{contents = (na,x)}) ->
-	  add_name bound_binders na;
+	  add_name found na;
 	  option_iter
-	    (fun (_,_,nl) -> List.iter (add_name bound_binders) nl) x;
+	    (fun (_,_,nl) -> List.iter (add_name found) nl) x;
           (aux tm,(na,option_app (fun (_,ind,nal) -> (ind,nal)) x))) tml,
         List.map f eqnl)
   | ROrderedCase (_,b,tyopt,tm,bv,_) ->
       AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
   | RLetTuple (loc,nal,(na,po),b,c) ->
-      add_name bound_binders na;
-      List.iter (add_name bound_binders) nal;
+      add_name found na;
+      List.iter (add_name found) nal;
       ALetTuple (nal,(na,option_app aux po),aux b,aux c)
   | RIf (loc,c,(na,po),b1,b2) ->
-      add_name bound_binders na;
+      add_name found na;
       AIf (aux c,(na,option_app aux po),aux b1,aux b2)
   | RCast (_,c,t) -> ACast (aux c,aux t)
   | RSort (_,s) -> ASort s
@@ -305,7 +302,7 @@ allowed in abbreviatable expressions"
       let x,y,order = match discr with Some z -> z | None -> 
 	error "Both ends of the recursive pattern are the same" in
       List.iter (fun id ->
-        if List.mem id !bound_binders or List.mem id !found 
+        if List.mem id !found
         then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part";
         found := id::!found) [x;y];
       let iter =
@@ -327,12 +324,12 @@ allowed in abbreviatable expressions"
   in
   let t = aux a in
   (* Side effect *)
-  t, !found, !bound_binders
+  t, !found
 
 let aconstr_of_rawconstr vars a =
-  let a,notbindingvars,binders = aconstr_and_vars_of_rawconstr a in
+  let a,foundvars = aconstr_and_vars_of_rawconstr a in
   let check_type x =
-    if not (List.mem x notbindingvars or List.mem x binders) then
+    if not (List.mem x foundvars) then
       error ((string_of_id x)^" is unbound in the right-hand-side") in
   List.iter check_type vars;
   a
@@ -356,12 +353,14 @@ let rec alpha_var id1 id2 = function
 
 let alpha_eq_val (x,y) = x = y
 
-let bind_env sigma var v =
+let bind_env alp sigma var v =
   try
     let vvar = List.assoc var sigma in
     if alpha_eq_val (v,vvar) then sigma
     else raise No_match
   with Not_found ->
+    (* Check that no capture of binding variables occur *)
+    if List.exists (fun (id,_) ->occur_rawconstr id v) alp then raise No_match;
     (* TODO: handle the case of multiple occs in different scopes *)
     (var,v)::sigma
 
@@ -372,13 +371,13 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
 
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (Name id1,Name id2) when List.mem id2 metas ->
-      alp, bind_env sigma id2 (RVar (dummy_loc,id1))
+      alp, bind_env alp sigma id2 (RVar (dummy_loc,id1))
   | (Name id1,Name id2) -> (id1,id2)::alp,sigma
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
 
 let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
-  | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
+  | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
   | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
   | RRef (_,r1), ARef r2 when r1 = r2 -> sigma
   | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma