Merge PR#558: Adding a fold_glob_constr_with_binders combinator

4 files changed, 74 insertions, 207 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 7f11c0a3b..d6749e918 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -131,61 +131,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
 	  if Id.List.mem_assoc id vs then vs
 	  else (id, loc) :: vs
 	else vs
-    | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
-    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
-	let vs' = vars bound vs ty in
-	let bound' = add_name_to_ids bound na in
-	vars bound' vs' c
-    | GLetIn (loc,na,b,ty,c) ->
-	let vs' = vars bound vs b in
-	let vs'' = Option.fold_left (vars bound) vs' ty in
-	let bound' = add_name_to_ids bound na in
-	vars bound' vs'' c
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
-	let vs1 = vars_option bound vs rtntypopt in
-	let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in
-	List.fold_left (vars_pattern bound) vs2 pl
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
-	let vs1 = vars_return_type bound vs rtntyp in
-	let vs2 = vars bound vs1 b in
-	let bound' = List.fold_left add_name_to_ids bound nal in
-	vars bound' vs2 c
-    | GIf (loc,c,rtntyp,b1,b2) ->
-	let vs1 = vars_return_type bound vs rtntyp in
-	let vs2 = vars bound vs1 c in
-	let vs3 = vars bound vs2 b1 in
-	vars bound vs3 b2
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
-	let bound' = Array.fold_right Id.Set.add idl bound in
-	let vars_fix i vs fid =
-	  let vs1,bound1 =
-	    List.fold_left
-	      (fun (vs,bound) (na,k,bbd,bty) ->
-		 let vs' = vars_option bound vs bbd in
-		 let vs'' = vars bound vs' bty in
-		 let bound' = add_name_to_ids bound na in
-		 (vs'',bound')
-	      )
-	      (vs,bound')
-	      bl.(i)
-	  in
-	  let vs2 = vars bound1 vs1 tyl.(i) in
-	  vars bound1 vs2 bv.(i)
-	in
-	Array.fold_left_i vars_fix vs idl
-    | GCast (loc,c,k) -> let v = vars bound vs c in
-	(match k with CastConv t | CastVM t -> vars bound v t | _ -> v)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
-
-  and vars_pattern bound vs (loc,idl,p,c) =
-    let bound' = List.fold_right Id.Set.add idl bound  in
-    vars bound' vs c
-
-  and vars_option bound vs = function None -> vs | Some p -> vars bound vs p
-
-  and vars_return_type bound vs (na,tyopt) =
-    let bound' = add_name_to_ids bound na in
-    vars_option bound' vs tyopt
+    | c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
   in fun rt -> 
     let vars = List.rev (vars bound [] rt) in
       List.iter (fun (id, loc) ->
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index ebbfa195f..080ec5ed1 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -214,55 +214,57 @@ let fold_glob_constr f acc = function
     f acc c
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
 
-let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
+let fold_return_type_with_binders f g v acc (na,tyopt) =
+  Option.fold_left (f (name_fold g na v)) acc tyopt
+
+let fold_glob_constr_with_binders g f v acc = function
+  | GVar _ -> acc
+  | GApp (_,c,args) -> List.fold_left (f v) (f v acc c) args
+  | GLambda (_,na,_,b,c) | GProd (_,na,_,b,c) ->
+    f (name_fold g na v) (f v acc b) c
+  | GLetIn (_,na,b,t,c) ->
+    f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c
+  | GCases (_,_,rtntypopt,tml,pl) ->
+    let fold_pattern acc (_,idl,p,c) = f (List.fold_right g idl v) acc c in
+    let fold_tomatch (v',acc) (tm,(na,onal)) =
+      (Option.fold_left (fun v'' (_,_,nal) -> List.fold_right (name_fold g) nal v'')
+                        (name_fold g na v') onal,
+       f v acc tm) in
+    let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in
+    let acc = Option.fold_left (f v') acc rtntypopt in
+    List.fold_left fold_pattern acc pl
+  | GLetTuple (_,nal,rtntyp,b,c) ->
+    f v (f v (fold_return_type_with_binders f g v acc rtntyp) b) c
+  | GIf (_,c,rtntyp,b1,b2) ->
+    f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2
+  | GRec (_,_,idl,bll,tyl,bv) ->
+    let f' i acc fid =
+      let v,acc =
+	List.fold_left
+	  (fun (v,acc) (na,k,bbd,bty) ->
+            (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty))
+          (v,acc)
+          bll.(i) in
+      f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in
+    Array.fold_left_i f' acc idl
+  | GCast (_,c,k) ->
+    let acc = match k with
+      | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
+    f v acc c
+  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
 
-let same_id na id = match na with
-| Anonymous -> false
-| Name id' -> Id.equal id id'
+let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
 let occur_glob_constr id =
-  let rec occur = function
+  let rec occur barred acc = function
     | GVar (loc,id') -> Id.equal id id'
-    | GApp (loc,f,args) -> (occur f) || (List.exists occur args)
-    | GLambda (loc,na,bk,ty,c) ->
-      (occur ty) || (not (same_id na id) && (occur c))
-    | GProd (loc,na,bk,ty,c) ->
-      (occur ty) || (not (same_id na id) && (occur c))
-    | GLetIn (loc,na,b,t,c) ->
-      (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c))
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
-	(occur_option rtntypopt)
-        || (List.exists (fun (tm,_) -> occur tm) tml)
-	|| (List.exists occur_pattern pl)
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
-	occur_return_type rtntyp id
-        || (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c))
-    | GIf (loc,c,rtntyp,b1,b2) ->
-	occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2)
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
-        not (Array.for_all4 (fun fid bl ty bd ->
-          let rec occur_fix = function
-              [] -> not (occur ty) && (Id.equal fid id || not(occur bd))
-            | (na,k,bbd,bty)::bl ->
-                not (occur bty) &&
-                (match bbd with
-                    Some bd -> not (occur bd)
-                  | _ -> true) &&
-                (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in
-          occur_fix bl)
-          idl bl tyl bv)
-    | GCast (loc,c,k) -> (occur c) || (match k with CastConv t
-      | CastVM t | CastNative t -> occur t | CastCoerce -> false)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false
-
-  and occur_pattern (loc,idl,p,c) = not (Id.List.mem id idl) && (occur c)
-
-  and occur_option = function None -> false | Some p -> occur p
-
-  and occur_return_type (na,tyopt) id = not (same_id na id) && occur_option tyopt
-
-  in occur
-
+    | c ->
+       (* [g] looks if [id] appears in a binding position, in which
+          case, we don't have to look in the corresponding subterm *)
+       let g id' barred = barred || Id.equal id id' in
+       let f barred acc c = acc || not barred && occur false acc c in
+       fold_glob_constr_with_binders g f barred acc c in
+  occur false false
 
 let add_name_to_ids set na =
   match na with
@@ -270,64 +272,9 @@ let add_name_to_ids set na =
     | Name id -> Id.Set.add id set
 
 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)
-    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
-	let vs' = vars bounded vs ty in
-	let bounded' = add_name_to_ids bounded na in
-       vars bounded' vs' c
-    | GLetIn (loc,na,b,ty,c) ->
-	let vs' = vars bounded vs b in
-	let vs'' = Option.fold_left (vars bounded) vs' ty in
-	let bounded' = add_name_to_ids bounded na in
-       vars bounded' vs'' c
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
-	let vs1 = vars_option bounded vs rtntypopt in
-	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
-	List.fold_left (vars_pattern bounded) vs2 pl
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
-	let vs1 = vars_return_type bounded vs rtntyp in
-	let vs2 = vars bounded vs1 b in
-	let bounded' = List.fold_left add_name_to_ids bounded nal in
-	vars bounded' vs2 c
-    | GIf (loc,c,rtntyp,b1,b2) ->
-	let vs1 = vars_return_type bounded vs rtntyp in
-	let vs2 = vars bounded vs1 c in
-	let vs3 = vars bounded vs2 b1 in
-	vars bounded vs3 b2
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
-	let bounded' = Array.fold_right Id.Set.add idl bounded in
-	let vars_fix i vs fid =
-	  let vs1,bounded1 =
-	    List.fold_left
-	      (fun (vs,bounded) (na,k,bbd,bty) ->
-		 let vs' = vars_option bounded vs bbd in
-		 let vs'' = vars bounded vs' bty in
-		 let bounded' = add_name_to_ids bounded na in
-		 (vs'',bounded')
-	      )
-	      (vs,bounded')
-	      bl.(i)
-	  in
-	  let vs2 = vars bounded1 vs1 tyl.(i) in
-	  vars bounded1 vs2 bv.(i)
-	in
-	Array.fold_left_i vars_fix vs idl
-    | GCast (loc,c,k) -> let v = vars bounded vs c in
-	(match k with CastConv t | CastVM t | CastNative t -> vars bounded v t | _ -> v)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
-
-  and vars_pattern bounded vs (loc,idl,p,c) =
-    let bounded' = List.fold_right Id.Set.add idl bounded  in
-    vars bounded' vs c
-
-  and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p
-
-  and vars_return_type bounded vs (na,tyopt) =
-    let bounded' = add_name_to_ids bounded na in
-    vars_option bounded' vs tyopt
-  in
+  let rec vars bound vs = function
+    | GVar (loc,id') -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs
+    | c -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in
   fun rt ->
     let vs = vars Id.Set.empty Id.Set.empty rt in
     Id.Set.elements vs
@@ -353,57 +300,16 @@ let add_and_check_ident id set =
   Id.Set.add id set
 
 let bound_glob_vars =
-  let rec vars bound = function
-    | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c ->
-        let bound = name_fold add_and_check_ident na bound in
-        fold_glob_constr vars bound c
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
-	let bound = vars_option bound rtntypopt in
-	let bound =
-          List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in
-	List.fold_left vars_pattern bound pl
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
-	let bound = vars_return_type bound rtntyp in
-	let bound = vars bound b in
-	let bound = List.fold_right (name_fold add_and_check_ident) nal bound in
-	vars bound c
-    | GIf (loc,c,rtntyp,b1,b2) ->
-	let bound = vars_return_type bound rtntyp in
-	let bound = vars bound c in
-	let bound = vars bound b1 in
-	vars bound b2
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
-	let bound = Array.fold_right Id.Set.add idl bound in
-	let vars_fix i bound fid =
-	  let bound =
-	    List.fold_left
-	      (fun bound (na,k,bbd,bty) ->
-		 let bound = vars_option bound bbd in
-		 let bound = vars bound bty in
-		 name_fold add_and_check_ident na bound
-	      )
-	      bound
-	      bl.(i)
-	  in
-	  let bound = vars bound tyl.(i) in
-	  vars bound bv.(i)
-	in
-	Array.fold_left_i vars_fix bound idl
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound
-    | GApp _ | GCast _ as c -> fold_glob_constr vars bound c
-
-  and vars_pattern bound (loc,idl,p,c) =
-    let bound = List.fold_right add_and_check_ident idl bound in
-    vars bound c
-
-  and vars_option bound = function None -> bound | Some p -> vars bound p
-
-  and vars_return_type bound (na,tyopt) =
-    let bound = name_fold add_and_check_ident na bound in
-    vars_option bound tyopt
+  let rec vars bound =
+    fold_glob_constr_with_binders
+      (fun id () -> bound := add_and_check_ident id !bound)
+      (fun () () -> vars bound)
+      () ()
   in
   fun rt ->
-    vars Id.Set.empty rt
+    let bound = ref Id.Set.empty in
+    vars bound rt;
+    !bound
 
 (** Mapping of names in binders *)
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 55e6b6533..af2834e49 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -37,6 +37,7 @@ val map_glob_constr_left_to_right :
 val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit
 
 val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
+val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : Id.t -> glob_constr -> bool
 val free_glob_vars : glob_constr -> Id.t list
diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v
new file mode 100644
index 000000000..fafe27292
--- /dev/null
+++ b/test-suite/success/boundvars.v
@@ -0,0 +1,14 @@
+(* An example showing a bug in the detection of free variables *)
+(* "x" is not free in the common type of "x" and "y" *)
+
+Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.
+
+(* An example showing a bug in the detection of bound variables *)
+
+Goal forall x, match x return x = x with 0 => eq_refl | _ => eq_refl end = eq_refl.
+intro.
+match goal with
+|- (match x as y in nat return y = y with O => _ | S n => _ end) = _ => assert (forall y, y = 0) end.
+intro.
+Check x0. (* Check that "y" has been bound to "x0" while matching "match x as x0 return x0=x0 with ... end" *)
+Abort.