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

10 files changed, 140 insertions, 98 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 64c64c4eee..075e98a7d1 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -745,7 +745,7 @@ and frterm =
 
 and frreference =
   (* only vars as args of FConst ... exploited for caching *)
-  | FConst of constant
+  | FConst of section_path * freeze array
   | FEvar of (existential * freeze subs)
   | FVar of identifier
   | FFarRel of int (* index in the rel_context part of _initial_ environment *)
@@ -827,10 +827,9 @@ let rec traverse_term env t =
         { norm = false; term = FInd (sp, Array.map (traverse_term env) v) }
     | IsMutConstruct (sp,v) ->
         { norm = false; term = FConstruct (sp,Array.map (traverse_term env) v)}
-    | IsConst (_,v as cst) ->
-	assert (array_for_all isVar v);
+    | IsConst (sp,v) ->
         { norm = false;
-	  term = FFlex (FConst cst) }
+	  term = FFlex (FConst (sp,Array.map (traverse_term env) v)) }
     | IsEvar (_,v as ev) ->
 	assert (array_for_all (fun a -> isVar a or isRel a) v);
         { norm = false;
@@ -880,8 +879,8 @@ let rec lift_term_of_freeze lfts v =
     | FAtom c -> c
     | FCast (a,b) ->
         mkCast (lift_term_of_freeze lfts a, lift_term_of_freeze lfts b)
-    | FFlex (FConst cst) ->
-	mkConst cst
+    | FFlex (FConst (op, ve)) ->
+	mkConst (op, Array.map (lift_term_of_freeze lfts) ve) 
     | FFlex (FEvar ((n,args), env)) ->
 	let f a = lift_term_of_freeze lfts (traverse_term env a) in
 	mkEvar (n, Array.map f args)
@@ -938,7 +937,7 @@ let rec fstrong unfreeze_fun lfts v =
     | FCast (a,b) ->
         mkCast (fstrong unfreeze_fun lfts a, fstrong unfreeze_fun lfts b)
     | FFlex (FConst (op,ve)) ->
-	mkConst (op, ve)
+	mkConst (op, Array.map (fstrong unfreeze_fun lfts) ve)
     | FFlex (FEvar ((n,args),env)) ->
 	let f a = fstrong unfreeze_fun lfts (freeze env a) in
 	mkEvar (n, Array.map f args)
@@ -1077,7 +1076,8 @@ and whnf_frterm info ft =
           { norm = uf.norm; term = FLIFT(k, uf) }
       | FCast (f,_) -> whnf_frterm info f  (* remove outer casts *)
       | FApp (f,appl) -> whnf_apply info f appl
-      | FFlex (FConst (sp,vars as cst)) ->
+      | FFlex (FConst (sp,vars)) ->
+	  let cst = (sp, Array.map term_of_freeze vars) in
 	  if red_under info.i_flags (CONST [sp]) then
             (match ref_value_cache info (ConstBinding cst) with
                | Some def ->
@@ -1188,8 +1188,9 @@ and whnf_term info env t =
     | IsApp (f,ve) ->
       	whnf_frterm info
 	  { norm = false; term = FApp (freeze env f, freeze_vect env ve)}
-    | IsConst cst ->
-      	whnf_frterm info { norm = false; term = FFlex (FConst cst) }
+    | IsConst (op,v) ->
+      	whnf_frterm info 
+	  { norm = false; term = FFlex (FConst (op, freeze_vect env v)) }
     | IsEvar ev ->
       	whnf_frterm info { norm = false; term = FFlex (FEvar (ev, env)) }
     | IsMutCase (ci,p,c,ve) ->
@@ -1239,7 +1240,9 @@ let whd_val info v =
 let inject = freeze (ESID 0)
 
 let search_frozen_value info = function
-  | FConst cst -> ref_value_cache info (ConstBinding cst)
+  | FConst (op,v) -> 
+      let cst = (op, Array.map (norm_val info) v) in
+      ref_value_cache info (ConstBinding cst)
   | FEvar ev -> ref_value_cache info (EvarBinding ev)
   | FVar id -> ref_value_cache info (VarBinding id)
   | FFarRel p -> ref_value_cache info (FarRelBinding p)
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 0ebf97a7bd..bf855b2624 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -154,7 +154,7 @@ and frterm =
   | FFROZEN of constr * freeze subs
 
 and frreference =
-  | FConst of constant
+  | FConst of section_path * freeze array
   | FEvar of (existential * freeze subs)
   | FVar of identifier
   | FFarRel of int
diff --git a/library/declare.ml b/library/declare.ml
index e1884ed5fc..1fa7236cb9 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 9b5ba27b7f..4dd0a36f20 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 397e5a53b4..35d8cf2acf 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 70cf895e53..30fba46ecd 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 de5c22c09e..d13e378e81 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 9a90a70b89..54c4bc67be 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
 
 
 
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index c89ec4a534..b4880f6fbc 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -496,7 +496,7 @@ let ast_of_qualid loc sp =
   try
     let ref = Nametab.locate sp in
     let c = Declare.constr_of_reference Evd.empty (Global.env()) ref in
-    match kind_of_term c with
+    match kind_of_term (snd (decompose_lam c)) with
       | IsConst (sp, _) -> Node (loc, "CONST", [path_section loc sp])
       | IsEvar (ev, _) -> Node (loc, "EVAR", [Num (loc, ev)])
       | IsMutConstruct (((sp, i), j), _) ->
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 2b552fffc0..48056f79cc 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -256,6 +256,26 @@ let push_inductive_names ccitab sp mie =
       mie.mind_entry_inds
   in ccitab
 
+(*s Operations performed at section closing. *)
+
+let cache_end_section (_,(s,mc)) =
+  Nametab.push_module s mc;
+  Nametab.open_module_contents s
+
+let load_end_section (_,(s,mc)) =
+  Nametab.push_module s mc
+
+let open_end_section (_,(s,_)) =
+  Nametab.rec_open_module_contents s
+
+let (in_end_section, out_end_section) =
+  declare_object
+    ("END-SECTION",
+     { cache_function = cache_end_section;
+       load_function = load_end_section;
+       open_function = open_end_section;
+       export_function = (fun x -> Some x) })
+
 let rec process_object (ccitab, objtab, modtab as tabs) = function
   | sp,Leaf obj -> 
       begin match object_tag obj with
@@ -267,6 +287,9 @@ let rec process_object (ccitab, objtab, modtab as tabs) = function
 	    (push_inductive_names ccitab sp mie, objtab, modtab)
         (* Variables are never visible *)
 	| "VARIABLE" -> tabs
+	| "END-SECTION" ->
+	    let (id,mc) = out_end_section obj in
+	    (ccitab, objtab, Stringmap.add id mc modtab)
         (* All the rest is visible only at toplevel ??? *)
         (* Actually it is unsafe, it should be visible only in empty context *)
         (* ou quelque chose comme cela *)
@@ -276,34 +299,31 @@ let rec process_object (ccitab, objtab, modtab as tabs) = function
 	     Stringmap.add (string_of_id (basename sp)) (sp,obj) objtab,
 	     modtab)
       end 
-  | sp,ClosedSection (export,_,seg,contents) ->
-      let id = string_of_id (basename sp) in
-      (ccitab, objtab, Stringmap.add id contents modtab)
-  | _,(OpenedSection _ | FrozenState _ | Module _) ->  tabs
+  | _,(ClosedSection _ | OpenedSection _ | FrozenState _ | Module _) ->  tabs
 
-and module_contents seg =
+and segment_contents seg =
   let ccitab, objtab, modtab =
     List.fold_left process_object
       (Stringmap.empty, Stringmap.empty, Stringmap.empty)
       seg
-  in Nametab.Closed (ccitab, objtab, modtab)
+  in 
+  Nametab.Closed (ccitab, objtab, modtab)
 
 let close_section _ s = 
   let oldenv = Global.env() in
-  let process_segment fs sec_sp decls =
-    let newdir = dirpath sec_sp in
-    let olddir = wd_of_sp sec_sp in
-    let (ops,ids,_) = 
-      List.fold_left 
-	(process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
-    in 
-    Summary.unfreeze_lost_summaries fs;
-    Global.pop_named_decls ids;
-    List.iter process_operation (List.rev ops);
-    module_contents decls 
-  in
-  close_section false process_segment s
+  let sec_sp,decls,fs = close_section false s in
+  let newdir = dirpath sec_sp in
+  let olddir = wd_of_sp sec_sp in
+  let (ops,ids,_) = 
+    List.fold_left 
+      (process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
+  in 
+  Global.pop_named_decls ids;
+  Summary.unfreeze_lost_summaries fs;
+  let mc = segment_contents decls in
+  add_anonymous_leaf (in_end_section (s,mc));
+  List.iter process_operation (List.rev ops)
 
 let save_module_to s f =
-  Library.save_module_to module_contents s f
+  Library.save_module_to segment_contents s f