deplacement poly_args; iterateurs sur les segments

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

3 files changed, 74 insertions, 0 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index cf2d09d610..6ef403f59d 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Util
 open Names
 open Term
 open Reduction
@@ -10,6 +11,40 @@ open Inductive
 open Libobject
 open Lib
 
+(* calcul des arguments implicites *)
+
+(* la seconde liste est ordonne'e *)
+
+let ord_add x l =
+  let rec aux l = match l with 
+    | []    -> [x]
+    | y::l' -> if y > x then x::l else if x = y then l else y::(aux l')
+  in 
+  aux l
+    
+let add_free_rels_until bound m acc =
+  let rec frec depth acc c = match kind_of_term c with
+    | IsRel n when (n < bound+depth) & (n >= depth) ->
+	Intset.add (bound+depth-n) acc
+    | _ -> fold_constr_with_binders succ frec depth acc c
+  in 
+  frec 1 acc m 
+
+(* calcule la liste des arguments implicites *)
+
+let poly_args env sigma t =
+  let rec aux env n t =
+    match kind_of_term (whd_betadeltaiota env sigma t) with
+      | IsProd (x,a,b) ->
+	  add_free_rels_until n a
+	    (aux (push_rel_assum (x,a) env) (n+1) b)
+      | _ -> Intset.empty
+  in 
+  match kind_of_term (whd_betadeltaiota env sigma t) with 
+    | IsProd (x,a,b) ->
+	Intset.elements (aux (push_rel_assum (x,a) env) 1 b)
+    | _ -> []
+
 type implicits =
   | Impl_auto of int list
   | Impl_manual of int list
diff --git a/library/library.ml b/library/library.ml
index 55c8aca0fe..558052a115 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -204,6 +204,31 @@ let save_module_to process s f =
   System.marshal_out ch di;
   close_out ch
 
+(*s Iterators. *)
+
+let fold_all_segments insec f x =
+  let rec apply acc = function
+    | sp, Leaf o -> f acc sp o
+    | _, ClosedSection (_,_,seg,_) -> 
+	if insec then List.fold_left apply acc seg else acc
+    | _ -> acc
+  in
+  let acc' = 
+    Stringmap.fold 
+      (fun _ m acc -> List.fold_left apply acc (fst m.module_declarations)) 
+      !modules_table x
+  in
+  List.fold_left apply acc' (Lib.contents_after None)
+
+let iter_all_segments insec f =
+  let rec apply = function
+    | sp, Leaf o -> f sp o
+    | _, ClosedSection (_,_,seg,_) -> if insec then List.iter apply seg
+    | _ -> ()
+  in
+  Stringmap.iter 
+    (fun _ m -> List.iter apply (fst m.module_declarations)) !modules_table;
+  List.iter apply (Lib.contents_after None)
 
 (*s Pretty-printing of modules state. *)
 
diff --git a/library/library.mli b/library/library.mli
index 6d4bb1ed5f..4ff27b4cd6 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -1,6 +1,11 @@
 
 (* $Id$ *)
 
+(*i*)
+open Names
+open Libobject
+(*i*)
+
 (*s This module is the heart of the library. It provides low level functions to
    load, open and save modules. Modules are saved onto the disk with checksums
    (obtained with the [Digest] module), which are checked at loading time to
@@ -41,6 +46,15 @@ val save_module_to : (Lib.library_segment -> Nametab.module_contents) ->
 val module_segment : string option -> Lib.library_segment
 val module_filename : string -> System.load_path_entry * string
 
+(*s [fold_all_segments] and [iter_all_segments] iterate over all
+    segments, the modules' segments first and then the current
+    segment. Modules are presented in an arbitrary order. The given
+    function is applied to all leaves (together with their section
+    path). The boolean indicates if we must enter closed sections. *)
+
+val fold_all_segments : bool -> ('a -> section_path -> obj -> 'a) -> 'a -> 'a
+val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit
+
 (*s Global load path *)
 val get_load_path : unit -> System.load_path
 val add_load_path_entry : System.load_path_entry -> unit