Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le «load» des Remark/Fact

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

10 files changed, 76 insertions, 52 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 7bede5758..9b6466f47 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -25,27 +25,43 @@ open Indrec
 open Nametab
 open Library
 
+(* For [DischargeAt (dir,n)], [dir] is the minimum prefix that a
+   construction keeps in its name (if persistent), or the section name
+   beyond which it is discharged (if volatile); the integer [n]
+   (useful only for persistent constructions), is the length of the section
+   part in [dir] *)
+
 type strength = 
   | NotDeclare
-  | DischargeAt of dir_path
+  | DischargeAt of dir_path * int
   | NeverDischarge
 
-let make_strength = function
-  | [] -> NeverDischarge
-  | l  -> DischargeAt l
+let depth_of_strength = function
+  | DischargeAt (sp',n) -> n
+  | NeverDischarge -> 0
+  | NotDeclare -> assert false
+
+let restrict_path n sp =
+  let dir, s, k = repr_path sp in
+  let dir' = list_lastn n dir in
+  Names.make_path dir' s k
 
-let make_strength_0 () = make_strength (Lib.cwd())
+let make_strength_0 () = 
+  let depth = Lib.sections_depth () in
+  let cwd = Lib.cwd() in
+  if depth > 0 then DischargeAt (cwd, depth) else NeverDischarge
 
 let make_strength_1 () =
+  let depth = Lib.sections_depth () in
   let cwd = Lib.cwd() in
-  let path = try list_firstn (List.length cwd - 1) cwd with Failure _ -> [] in
-  make_strength path
+  if depth > 1 then DischargeAt (list_firstn (List.length cwd -1) cwd, depth-1)
+  else NeverDischarge
 
 let make_strength_2 () =
+  let depth = Lib.sections_depth () in
   let cwd = Lib.cwd() in
-  let path = try list_firstn (List.length cwd - 2) cwd with Failure _ -> [] in
-  make_strength path
-
+  if depth > 2 then DischargeAt (list_firstn (List.length cwd -2) cwd, depth-2)
+  else NeverDischarge
 
 (* Section variables. *)
 
@@ -76,9 +92,6 @@ let _ = Summary.declare_summary "VARIABLE"
 	    Summary.survive_section = false }
 
 let cache_variable (sp,(id,(d,str,sticky))) =
-(*
-  if Nametab.exists_cci sp then
-*)
   (* Constr raisonne sur les noms courts *)
   if List.mem_assoc id (current_section_context ()) then
     errorlabstrm "cache_variable"
@@ -87,7 +100,7 @@ let cache_variable (sp,(id,(d,str,sticky))) =
     | SectionLocalAssum ty -> Global.push_named_assum (id,ty)
     | SectionLocalDef c -> Global.push_named_def (id,c)
   in
-  Nametab.push_short_name sp (VarRef sp);
+  Nametab.push 0 (restrict_path 0 sp) (VarRef sp);
   vartab := let (m,l) = !vartab in (Spmap.add sp (id,(vd,str,sticky)) m, sp::l)
 
 let (in_variable, out_variable) =
@@ -111,17 +124,16 @@ let cache_parameter (sp,c) =
     errorlabstrm "cache_parameter"
       [< pr_id (basename sp); 'sTR " already exists" >];
   Global.add_parameter sp c (current_section_context ());
-  Nametab.push sp (ConstRef sp);
-  Nametab.push_short_name sp (ConstRef sp)
+  Nametab.push 0 sp (ConstRef sp)
 
 let load_parameter (sp,_) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_parameter"
       [< pr_id (basename sp); 'sTR " already exists" >];
-  Nametab.push sp (ConstRef sp)
+  Nametab.push 1 sp (ConstRef sp)
 
 let open_parameter (sp,_) =
-  Nametab.push_short_name sp (ConstRef sp)
+  Nametab.push 0 (restrict_path 0 sp) (ConstRef sp)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_parameter_entry = mkProp
@@ -169,25 +181,31 @@ let cache_constant (sp,(cdt,stre,op)) =
     | ConstantEntry ce -> Global.add_constant sp ce sc
     | ConstantRecipe r -> Global.add_discharged_constant sp r sc
   end;
-  Nametab.push sp (ConstRef sp);
   (match stre with
-    (* Remark & Fact outside their scope aren't visible without qualif *)
-    | DischargeAt sp' when not (is_dirpath_prefix_of sp' (Lib.cwd ())) -> ()
-    (* Theorem, Lemma & Definition are accessible from the base name *)
-    | NeverDischarge| DischargeAt _ -> Nametab.push_short_name sp (ConstRef sp)
+    | DischargeAt (sp',n) when not (is_dirpath_prefix_of sp' (Lib.cwd ())) ->
+        (* Only qualifications including the sections segment from the current
+           section to the discharge section is available for Remark & Fact *)
+        Nametab.push (n-Lib.sections_depth()) sp (ConstRef sp)
+    | (NeverDischarge| DischargeAt _) -> 
+        (* All qualifications of Theorem, Lemma & Definition are visible *)
+        Nametab.push 0 sp (ConstRef sp)
     | NotDeclare -> assert false);
   if op then Global.set_opaque sp;
   csttab := Spmap.add sp stre !csttab
 
+(* At load-time, the segment starting from the module name to the discharge *)
+(* section (if Remark or Fact) is needed to access a construction *)
 let load_constant (sp,(ce,stre,op)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_constant"
       [< pr_id (basename sp); 'sTR " already exists" >] ;
   csttab := Spmap.add sp stre !csttab;
-  Nametab.push sp (ConstRef sp)
+  Nametab.push (depth_of_strength stre + 1) sp (ConstRef sp)
 
-let open_constant (sp,_) =
-  Nametab.push_short_name sp (ConstRef sp)
+(* Opening means making the name without its module qualification available *)
+let open_constant (sp,(_,stre,_)) =
+  let n = depth_of_strength stre in
+  Nametab.push n (restrict_path n sp) (ConstRef sp)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = ConstantEntry { 
@@ -252,17 +270,17 @@ let cache_inductive (sp,mie) =
   List.iter check_exists_inductive names;
   Global.add_mind sp mie (current_section_context ());
   List.iter 
-    (fun (sp, ref) -> Nametab.push sp ref; Nametab.push_short_name sp ref)
+    (fun (sp, ref) -> Nametab.push 0 sp ref)
     names
 
 let load_inductive (sp,mie) =
   let names = inductive_names sp mie in
   List.iter check_exists_inductive names;
-  List.iter (fun (sp, ref) -> Nametab.push sp ref) names
+  List.iter (fun (sp, ref) -> Nametab.push 1 sp ref) names
 
 let open_inductive (sp,mie) =
   let names = inductive_names sp mie in
-  List.iter (fun (sp, ref) -> Nametab.push_short_name sp ref) names
+  List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names
 
 let dummy_one_inductive_entry mie = {
   mind_entry_nparams = 0;
diff --git a/library/declare.mli b/library/declare.mli
index 08c45f462..b347456ce 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -26,7 +26,7 @@ open Library
 
 type strength = 
   | NotDeclare
-  | DischargeAt of dir_path
+  | DischargeAt of dir_path * int
   | NeverDischarge
 
 type section_variable_entry =
@@ -67,7 +67,7 @@ val declare_eliminations : mutual_inductive_path -> unit
 
 val out_inductive : Libobject.obj -> mutual_inductive_entry 
 
-val make_strength : dir_path -> strength
+(*val make_strength : dir_path -> strength*)
 val make_strength_0 : unit -> strength
 val make_strength_1 : unit -> strength
 val make_strength_2 : unit -> strength
diff --git a/library/lib.ml b/library/lib.ml
index 94cba5e0c..c6ebfa000 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -64,6 +64,8 @@ let pop_path_prefix () =
 
 let make_path id k = Names.make_path !path_prefix id k
 
+let sections_depth () = List.length !path_prefix - List.length (module_sp ())
+
 let cwd () = !path_prefix
 
 let find_entry_p p = 
diff --git a/library/lib.mli b/library/lib.mli
index 27fec78bf..0421f0812 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -55,6 +55,7 @@ val sections_are_opened : unit -> bool
 
 val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> dir_path
+val sections_depth : unit -> int
 val is_section_p : dir_path -> bool
 
 (* This is to declare the interactive toplevel default module name as a root*)
diff --git a/library/nametab.ml b/library/nametab.ml
index 1fadea6ae..979c9f2dc 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -90,11 +90,9 @@ let dirpath_of_extended_ref = function
    "Root.Rep.Lib.name", but not "name" are pushed; which means, visibility is
    always 1 *)
 
-let visibility = 1
-
 (* We add a binding of [[modid1;...;modidn;id]] to [o] in the name tab *)
 (* We proceed in the reverse way, looking first to [id] *)
-let push_tree extract_dirpath tab dir o =
+let push_tree extract_dirpath tab visibility dir o =
   let rec push level (current,dirmap) = function
     | modid :: path as dir ->
 	let mc = 
@@ -114,11 +112,11 @@ let push_tree extract_dirpath tab dir o =
     | [] -> (Some o,dirmap) in
   push 0 tab (List.rev dir)
 
-let push_idtree extract_dirpath tab dir id o =
+let push_idtree extract_dirpath tab n dir id o =
   let modtab =
     try Idmap.find id !tab
     with Not_found -> (None, ModIdmap.empty) in
-  tab := Idmap.add id (push_tree extract_dirpath modtab dir o) !tab
+  tab := Idmap.add id (push_tree extract_dirpath modtab n dir o) !tab
 
 let push_long_names_ccipath = push_idtree dirpath_of_extended_ref the_ccitab
 let push_short_name_ccipath = push_idtree dirpath_of_extended_ref the_ccitab
@@ -128,7 +126,7 @@ let push_modidtree tab dir id o =
   let modtab =
     try ModIdmap.find id !tab
     with Not_found -> (None, ModIdmap.empty) in
-  tab := ModIdmap.add id (push_tree (fun x -> x) modtab dir o) !tab
+  tab := ModIdmap.add id (push_tree (fun x -> x) modtab 0 dir o) !tab
 
 let push_long_names_secpath = push_modidtree the_sectab
 let push_long_names_libpath = push_modidtree the_libtab
@@ -139,32 +137,35 @@ let push_long_names_libpath = push_modidtree the_libtab
    possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom,
    Parameter but also Remark and Fact) *)
 
-let push_cci sp ref =
+let push_cci n sp ref =
   let dir, s = repr_qualid (qualid_of_sp sp) in
   (* We push partially qualified name (with at least one prefix) *)
-  push_long_names_ccipath dir s (TrueGlobal ref)
+  push_long_names_ccipath n dir s (TrueGlobal ref)
 
 let push = push_cci
 
+(*
 let push_short_name sp ref =
   (* We push a volatile unqualified name *)
-  push_short_name_ccipath [] (basename sp) (TrueGlobal ref)
+  push_short_name_ccipath 0 [] (basename sp) (TrueGlobal ref)
+*)
 
 (* This is for Syntactic Definitions *)
 
 let push_syntactic_definition sp =
   let dir, s = repr_qualid (qualid_of_sp sp) in
-  push_long_names_ccipath dir s (SyntacticDef sp)
+  push_long_names_ccipath 0 dir s (SyntacticDef sp)
 
 let push_short_name_syntactic_definition sp =
   let _, s = repr_qualid (qualid_of_sp sp) in
-  push_short_name_ccipath [] s (SyntacticDef sp)
+  push_short_name_ccipath Pervasives.max_int [] s (SyntacticDef sp)
 
 (* This is for dischargeable non-cci objects (removed at the end of the
    section -- i.e. Hints, Grammar ...) *) (* --> Unused *)
 
 let push_short_name_object sp =
-  push_short_name_objpath [] (basename sp) sp
+  let _, s = repr_qualid (qualid_of_sp sp) in
+  push_short_name_objpath 0 [] s sp
 
 (* This is to remember absolute Section/Module names and to avoid redundancy *)
 
diff --git a/library/nametab.mli b/library/nametab.mli
index 6989e6bbf..f525d49c7 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -45,11 +45,13 @@ val error_global_not_found     : qualid -> 'a
 val error_global_constant_not_found_loc : loc -> qualid -> 'a
 
 (*s Register visibility of absolute paths by qualified names *)
-val push : section_path -> global_reference -> unit
+val push : visibility:int -> section_path -> global_reference -> unit
 val push_syntactic_definition : section_path -> unit
 
 (*s Register visibility of absolute paths by short names *)
+(*
 val push_short_name : section_path -> global_reference -> unit
+*)
 val push_short_name_syntactic_definition : section_path -> unit
 val push_short_name_object : section_path -> unit
 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 93751cf5d..322a61af7 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -532,7 +532,7 @@ open Classops
 let string_of_strength = function
   | NotDeclare -> "(temp)"
   | NeverDischarge -> "(global)"
-  | DischargeAt sp -> "(disch@"^(string_of_dirpath sp)
+  | DischargeAt (sp,_) -> "(disch@"^(string_of_dirpath sp)
 
 let print_coercion_value v = prterm (get_coercion_value v)
 
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 667e12706..3fb0f67a5 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -36,7 +36,7 @@ let stre_gt = function
   | (NotDeclare,_) -> false
   | (_,NeverDischarge) -> true
   | (_,NotDeclare) -> true
-  | (DischargeAt sp1,DischargeAt sp2) ->
+  | (DischargeAt (sp1,_),DischargeAt (sp2,_)) ->
       is_dirpath_prefix_of sp1 sp2
 	(* was sp_gt but don't understand why - HH *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f53f26b8d..f290d684b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -75,7 +75,7 @@ let definition_body_red red_option ident (local,n) com comtypeopt =
   let ce' = red_constant_entry ce red_option in
   match n with
     | NeverDischarge -> declare_global_definition ident ce' n local
-    | DischargeAt disch_sp ->
+    | DischargeAt (disch_sp,_) ->
         if Lib.is_section_p disch_sp then begin
 	  let c = constr_of_constr_entry ce' in
           let sp = declare_variable ident (SectionLocalDef c,n,false) in
@@ -115,7 +115,7 @@ let declare_global_assumption ident c =
 let hypothesis_def_var is_refining ident n c =
   match n with
     | NeverDischarge -> declare_global_assumption ident c
-    | DischargeAt disch_sp ->
+    | DischargeAt (disch_sp,_) ->
         if Lib.is_section_p disch_sp then begin
 	  let t = interp_type Evd.empty (Global.env()) c in
           let sp = declare_variable ident (SectionLocalAssum t,n,false) in
@@ -437,7 +437,7 @@ let apply_tac_not_declare id pft = function
 let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
   strength =
   begin match strength with
-    | DischargeAt disch_sp when Lib.is_section_p disch_sp && not opacity ->
+    | DischargeAt (disch_sp,_) when Lib.is_section_p disch_sp && not opacity ->
 	let c = constr_of_constr_entry const in
 	let _ = declare_variable id (SectionLocalDef c,strength,opacity) in ()
     | NeverDischarge | DischargeAt _ ->
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 730817bf3..819df64e0 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -218,7 +218,7 @@ let process_object oldenv dir sec_sp
 	  let cb = Environ.lookup_constant sp oldenv in
 	  let imp = is_implicit_constant sp in
 	  let newsp = match stre with
-	    | DischargeAt d when not (is_dirpath_prefix_of d dir) -> sp
+	    | DischargeAt (d,_) when not (is_dirpath_prefix_of d dir) -> sp
 	    | _ -> recalc_sp dir sp in
 	  let mods = 
 	    let modl = build_abstract_list cb.const_hyps ids_to_discard in
@@ -241,7 +241,7 @@ let process_object oldenv dir sec_sp
 
     | "CLASS" -> 
 	let ((cl,clinfo) as x) = outClass lobj in
-	if clinfo.cl_strength = (DischargeAt sec_sp) then 
+	if (match clinfo.cl_strength with DischargeAt (sp,_) -> sp = sec_sp | _ -> false) then 
 	  (ops,ids_to_discard,work_alist)
 	else
 	  let (y1,y2) = process_class sec_sp ids_to_discard x in
@@ -249,7 +249,7 @@ let process_object oldenv dir sec_sp
 	  
     | "COERCION" -> 
 	let (((_,coeinfo),_,_)as x) = outCoercion lobj in
-        if coercion_strength coeinfo = (DischargeAt sec_sp) then 
+	if (match coercion_strength coeinfo with DischargeAt (sp,_) -> sp = sec_sp | _ -> false) then 
 	  (ops,ids_to_discard,work_alist)
         else
 	  let y = process_coercion sec_sp ids_to_discard x in