Allègement du noyau

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

2 files changed, 41 insertions, 0 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 43d0e1853a..63b613972c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -286,6 +286,32 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
       then cstr
       else mkCoFix (ln,(lna,tl',bl'))
 
+(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
+   subterms of [c] starting from [acc] and proceeding from left to
+   right according to the usual representation of the constructions as
+   [fold_constr] but it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive *)
+
+let fold_constr_with_binders g f n acc c = match kind_of_term c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> acc
+  | Cast (c,t) -> f n (f n acc c) t
+  | Prod (_,t,c) -> f (g n) (f n acc t) c
+  | Lambda (_,t,c) -> f (g n) (f n acc t) c
+  | LetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
+  | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+  | Evar (_,l) -> Array.fold_left (f n) acc l
+  | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+  | Fix (_,(lna,tl,bl)) -> 
+      let n' = iterate g (Array.length tl) n in
+      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
+  | CoFix (_,(lna,tl,bl)) ->
+      let n' = iterate g (Array.length tl) n in
+      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
+
 (***************************)
 (* occurs check functions  *)                         
 (***************************)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 95d769c43f..0cd757ceda 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -43,6 +43,9 @@ val it_named_context_quantifier :
 val it_mkNamedProd_or_LetIn   : init:types -> named_context -> types
 val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr
 
+(**********************************************************************)
+(* Generic iterators on constr                                        *)
+
 val map_constr_with_named_binders :
   (name -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
@@ -54,6 +57,18 @@ val map_constr_with_full_binders :
   (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
 
+(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
+   subterms of [c] starting from [acc] and proceeding from left to
+   right according to the usual representation of the constructions as
+   [fold_constr] but it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive *)
+
+val fold_constr_with_binders :
+  ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
+
+(**********************************************************************)
+
 val strip_head_cast : constr -> constr
 
 (* occur checks *)