Allègement du noyau

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

4 files changed, 41 insertions, 36 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 47bd656aea..bb22475230 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -479,32 +479,6 @@ let fold_constr f acc c = match kind_of_term c with
       let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in
       Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd
 
-(* [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
-
 (* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
    not specified *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 1867cc4505..2c8e9be3f0 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -453,16 +453,6 @@ val subst_mps : substitution -> constr -> constr
 
 val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
 
-(* [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
-
 (* [map_constr f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
    not specified *)
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 *)