Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab

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

6 files changed, 84 insertions, 65 deletions

diff --git a/library/declare.ml b/library/declare.ml
index e1884ed5f..1fa7236cb 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -275,16 +275,6 @@ let occur_decl env (id,c,t) hyps =
   with Not_found -> false
 
 (*
-let rec find_common_hyps_then_abstract c env hyps' = function
-  | (id,_,_ as d) :: hyps when occur_decl env d hyps' ->
-      find_common_hyps_then_abstract c (Environ.push_named_decl d env) hyps' hyps
-  | hyps ->
-      Environ.it_mkNamedLambda_or_LetIn c hyps
-
-let find_common_hyps_then_abstract c env hyps' hyps =
-  find_common_hyps_then_abstract c env hyps' (List.rev hyps)
-*)
-
 let find_common_hyps_then_abstract c env hyps' hyps = 
   snd (fold_named_context_both_sides
 	 (fun
@@ -292,13 +282,30 @@ let find_common_hyps_then_abstract c env hyps' hyps =
 	      if occur_decl env d hyps' then 
 		(Environ.push_named_decl d env,c)
 	      else
-		(env, Environ.it_mkNamedLambda_or_LetIn c hyps))
+		let hyps'' = List.rev (d :: hyps) in
+		(env, Environ.it_mkNamedLambda_or_LetIn c hyps''))
 	 hyps
 	 (env,c))
+*)
+
+let rec find_common_hyps_then_abstract c env hyps' = function
+  | (id,_,_ as d) :: hyps when occur_decl env d hyps' ->
+      find_common_hyps_then_abstract c (Environ.push_named_decl d env) hyps' hyps
+  | hyps ->
+      Environ.it_mkNamedLambda_or_LetIn c (List.rev hyps)
+
+let find_common_hyps_then_abstract c env hyps' hyps =
+  find_common_hyps_then_abstract c env hyps' (List.rev hyps)
+
+let current_section_context () =
+  List.fold_right
+    (fun (id,_,_ as d) hyps ->
+       if Spmap.mem (Lib.make_path id CCI) !vartab then d::hyps else hyps)
+    (Global.named_context ()) []
 
 let extract_instance ref args =
   let hyps = context_of_global_reference Evd.empty (Global.env ()) ref in
-  let hyps0 = Global.named_context () in
+  let hyps0 = current_section_context () in
   let na = Array.length args in
   let rec peel n acc = function
     | d::hyps ->
@@ -309,7 +316,7 @@ let extract_instance ref args =
 
 let constr_of_reference sigma env ref =
   let hyps = context_of_global_reference sigma env ref in
-  let hyps0 = Global.named_context () in
+  let hyps0 = current_section_context () in
   let env0 = Environ.reset_context env in
   let args = List.map mkVar (ids_of_named_context hyps) in
   let body = match ref with
diff --git a/library/lib.ml b/library/lib.ml
index 9b5ba27b7..4dd0a36f2 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -11,7 +11,7 @@ type node =
   | Module of string
   | OpenedSection of string * Summary.frozen
   (* bool is to tell if the section must be opened automatically *)
-  | ClosedSection of bool * string * library_segment * Nametab.module_contents
+  | ClosedSection of bool * string * library_segment
   | FrozenState of Summary.frozen
 
 and library_entry = section_path * node
@@ -137,7 +137,7 @@ let export_segment seg =
   in
   clean [] seg
 
-let close_section export f s =
+let close_section export s =
   let sp,fs = 
     try match find_entry_p is_opened_section with
       | sp,OpenedSection (s',fs) -> 
@@ -150,12 +150,10 @@ let close_section export f s =
   lib_stk := before;
   let after' = export_segment after in
   pop_path_prefix ();
-  let contents = f fs sp after in
-  add_entry (make_path (id_of_string s) OBJ)
-    (ClosedSection (export, s,after',contents));
-  Nametab.push_module s contents;
-  if export then Nametab.open_module_contents s;
-  add_frozen_state ()
+  add_entry 
+    (make_path (id_of_string s) OBJ) (ClosedSection (export, s,after'));
+  add_frozen_state ();
+  (sp,after,fs)
 
 (* The following function exports the whole library segment, that will be 
    saved as a module. Objects are presented in chronological order, and
diff --git a/library/lib.mli b/library/lib.mli
index 397e5a53b..35d8cf2ac 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -15,7 +15,7 @@ type node =
   | Leaf of obj
   | Module of string
   | OpenedSection of string * Summary.frozen
-  | ClosedSection of bool * string * library_segment * Nametab.module_contents
+  | ClosedSection of bool * string * library_segment
   | FrozenState of Summary.frozen
 
 and library_entry = section_path * node
@@ -40,10 +40,8 @@ val contents_after : section_path option -> library_segment
 (*s Opening and closing a section. *)
 
 val open_section : string -> section_path
-val close_section : export:bool ->
-  (Summary.frozen -> section_path -> library_segment 
-     -> Nametab.module_contents) 
-  -> string -> unit
+val close_section : 
+  export:bool -> string -> section_path * library_segment * Summary.frozen
 
 val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> dir_path
diff --git a/library/library.ml b/library/library.ml
index 70cf895e5..30fba46ec 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -32,7 +32,8 @@ let rec_add_path dir =
 type module_disk = { 
   md_name : string;
   md_compiled_env : compiled_env;
-  md_declarations : library_segment * Nametab.module_contents;
+  md_declarations : library_segment;
+  md_nametab : Nametab.module_contents;
   md_deps : (string * Digest.t * bool) list }
 
 (*s Modules loaded in memory contain the following informations. They are
@@ -42,7 +43,8 @@ type module_t = {
   module_name : string;
   module_filename : load_path_entry * string;
   module_compiled_env : compiled_env;
-  module_declarations : library_segment * Nametab.module_contents;
+  module_declarations : library_segment;
+  module_nametab : Nametab.module_contents;
   mutable module_opened : bool;
   mutable module_exported : bool;
   module_deps : (string * Digest.t * bool) list;
@@ -78,7 +80,7 @@ let opened_modules () =
 
 let module_segment = function
   | None -> contents_after None
-  | Some m -> fst (find_module m).module_declarations
+  | Some m -> (find_module m).module_declarations
 
 let module_filename m = (find_module m).module_filename
 
@@ -91,7 +93,7 @@ let segment_rec_iter f =
   let rec apply = function
     | sp,Leaf obj -> f (sp,obj)
     | _,OpenedSection _ -> assert false
-    | _,ClosedSection (_,_,seg,_) -> iter seg
+    | _,ClosedSection (_,_,seg) -> iter seg
     | _,(FrozenState _ | Module _) -> ()
   and iter seg =
     List.iter apply seg
@@ -102,7 +104,7 @@ let segment_iter f =
   let rec apply = function
     | sp,Leaf obj -> f (sp,obj)
     | _,OpenedSection _ -> assert false
-    | _,ClosedSection (export,_,seg,_) -> if export then iter seg
+    | _,ClosedSection (export,s,seg) -> if export then iter seg
     | _,(FrozenState _ | Module _) -> ()
   and iter seg =
     List.iter apply seg
@@ -120,8 +122,8 @@ let rec open_module s =
   let m = find_module s in
   if not m.module_opened then begin
     List.iter (fun (m,_,exp) -> if exp then open_module m) m.module_deps;
-    (* open_objects m.module_declarations; *)
-    Nametab.open_module_contents s;
+    open_objects m.module_declarations;
+    Nametab.open_module_contents s; 
     m.module_opened <- true
   end
 
@@ -136,26 +138,28 @@ let load_objects decls =
   segment_rec_iter load_object decls
 
 let rec load_module_from s f =
-  let (lpe,fname,ch) = raw_intern_module (get_load_path ()) f in
-  let md = System.marshal_in ch in
-  let digest = System.marshal_in ch in
-  close_in ch;
-  let m = { module_name = md.md_name;
-	    module_filename = (lpe,fname);
-	    module_compiled_env = md.md_compiled_env;
-	    module_declarations = md.md_declarations;
-	    module_opened = false;
-	    module_exported = false;
-	    module_deps = md.md_deps;
-	    module_digest = digest } in
-  if s <> md.md_name then
-    error ("The file " ^ fname ^ " does not contain module " ^ s);
-  List.iter (load_mandatory_module s) m.module_deps;
-  Global.import m.module_compiled_env;
-  load_objects (fst m.module_declarations);
-  Nametab.push_module s (snd m.module_declarations);
-  modules_table := Stringmap.add s m !modules_table;
-  m
+  if not (module_is_loaded s) then begin
+    let (lpe,fname,ch) = raw_intern_module (get_load_path ()) f in
+    let md = System.marshal_in ch in
+    let digest = System.marshal_in ch in
+    close_in ch;
+    let m = { module_name = md.md_name;
+	      module_filename = (lpe,fname);
+	      module_compiled_env = md.md_compiled_env;
+	      module_declarations = md.md_declarations;
+	      module_nametab = md.md_nametab;
+	      module_opened = false;
+	      module_exported = false;
+	      module_deps = md.md_deps;
+	      module_digest = digest } in
+    if s <> md.md_name then
+      error ("The file " ^ fname ^ " does not contain module " ^ s);
+    List.iter (load_mandatory_module s) m.module_deps;
+    Global.import m.module_compiled_env;
+    load_objects m.module_declarations;
+    Nametab.push_module s m.module_nametab;
+    modules_table := Stringmap.add s m !modules_table
+  end
 
 and load_mandatory_module caller (s,d,_) =
   let m = find_module s s in
@@ -166,20 +170,23 @@ and find_module s f =
   try 
     Stringmap.find s !modules_table 
   with Not_found -> 
-    load_module_from s f
+    load_module_from s f;
+    Stringmap.find s !modules_table 
 
 let load_module s = function
-  | None -> let _ = load_module_from s s in ()
-  | Some f -> let _ = load_module_from s f in ()
+  | None -> load_module_from s s
+  | Some f -> load_module_from s f
 
 
 (*s [require_module] loads and opens a module. This is a synchronized
     operation. *)
 
 let cache_require (_,(name,file,export)) =
-  let m = load_module_from name file in
+  load_module_from name file;
   open_module name;
-  if export then m.module_exported <- true
+  if export then 
+    let m = Stringmap.find name !modules_table in
+    m.module_exported <- true
 
 let (in_require, _) =
   declare_object
@@ -208,7 +215,8 @@ let save_module_to process s f =
   let md = { 
     md_name = s;
     md_compiled_env = Global.export s;
-    md_declarations = seg, process seg;
+    md_declarations = seg;
+    md_nametab = process seg;
     md_deps = current_imports () } in
   let (f',ch) = raw_extern_module f in
   System.marshal_out ch md;
@@ -222,13 +230,13 @@ let save_module_to process s f =
 let fold_all_segments insec f x =
   let rec apply acc = function
     | sp, Leaf o -> f acc sp o
-    | _, ClosedSection (_,_,seg,_) -> 
+    | _, 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)) 
+      (fun _ m acc -> List.fold_left apply acc m.module_declarations) 
       !modules_table x
   in
   List.fold_left apply acc' (Lib.contents_after None)
@@ -236,11 +244,11 @@ let fold_all_segments insec f x =
 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
+    | _, ClosedSection (_,_,seg) -> if insec then List.iter apply seg
     | _ -> ()
   in
   Stringmap.iter 
-    (fun _ m -> List.iter apply (fst m.module_declarations)) !modules_table;
+    (fun _ m -> List.iter apply m.module_declarations) !modules_table;
   List.iter apply (Lib.contents_after None)
 
 (*s Pretty-printing of modules state. *)
diff --git a/library/nametab.ml b/library/nametab.ml
index de5c22c09..d13e378e8 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -56,10 +56,17 @@ let locate_constant qid =
 let open_module_contents s =
   let (Closed (ccitab,objtab,modtab)) = Stringmap.find s !mod_tab in
   Stringmap.iter push_cci ccitab;
-  Stringmap.iter (fun _ -> Libobject.open_object) objtab;
+(*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
   Stringmap.iter push_module modtab
 
-(* Registration as a global table and roolback. *)
+let rec rec_open_module_contents id =
+  let (Closed (ccitab,objtab,modtab)) = Stringmap.find id !mod_tab in
+  Stringmap.iter push_cci ccitab;
+(*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
+  Stringmap.iter 
+    (fun m mt -> push_module m mt; rec_open_module_contents m) modtab
+
+(* Registration as a global table and rollback. *)
     
 let init () =
   cci_tab := Stringmap.empty;
diff --git a/library/nametab.mli b/library/nametab.mli
index 9a90a70b8..54c4bc67b 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -29,6 +29,7 @@ val locate_obj : qualid -> (section_path * Libobject.obj)
 val locate_constant : qualid -> constant_path
 
 val open_module_contents : string -> unit
+val rec_open_module_contents : string -> unit