Deplacement de iter_constr_with_full_binders dans Termops

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

2 files changed, 28 insertions, 0 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index a36be94fc..23f9a7ffc 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -314,6 +314,30 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with
       let fd = array_map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd
 
+(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
+   subterms of [c]; it carries an extra data [acc] which is processed by [g] at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
+let iter_constr_with_full_binders g f l c = match kind_of_term c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> ()
+  | Cast (c,t) -> f l c; f l t
+  | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c
+  | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c
+  | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c
+  | App (c,args) -> f l c; Array.iter (f l) args
+  | Evar (_,args) -> Array.iter (f l) args
+  | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
+  | Fix (_,(lna,tl,bl)) -> 
+      let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      Array.iter (f l) tl;
+      Array.iter (f l') bl
+  | CoFix (_,(lna,tl,bl)) ->
+      let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      Array.iter (f l) tl;
+      Array.iter (f l') bl
+
 (***************************)
 (* occurs check functions  *)                         
 (***************************)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index ca5e5139d..af75cfd2d 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -67,6 +67,10 @@ val map_constr_with_full_binders :
 val fold_constr_with_binders :
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
+val iter_constr_with_full_binders :
+  (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> 
+    constr -> unit
+
 (**********************************************************************)
 
 val strip_head_cast : constr -> constr