Suppression des library roots, on teste si un nom est absolu autrement

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

4 files changed, 81 insertions, 67 deletions

diff --git a/library/declare.ml b/library/declare.ml
index ca1cea16a..1c9875718 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -82,7 +82,7 @@ let cache_variable (sp,(id,(d,_,_) as vd)) =
     | SectionLocalAssum ty -> Global.push_named_assum (id,ty)
     | SectionLocalDef c -> Global.push_named_def (id,c)
   end;
-  Nametab.push_short_name id (VarRef sp);
+  Nametab.push_short_name sp (VarRef sp);
   vartab := let (m,l) = !vartab in (Spmap.add sp vd m, sp::l)
 
 let (in_variable, out_variable) =
@@ -107,7 +107,7 @@ let cache_parameter (sp,c) =
       [< pr_id (basename sp); 'sTR " already exists" >];
   Global.add_parameter sp c (current_section_context ());
   Nametab.push sp (ConstRef sp);
-  Nametab.push_short_name (basename sp) (ConstRef sp)
+  Nametab.push_short_name sp (ConstRef sp)
 
 let load_parameter (sp,_) =
   if Nametab.exists_cci sp then
@@ -116,7 +116,7 @@ let load_parameter (sp,_) =
   Nametab.push sp (ConstRef sp)
 
 let open_parameter (sp,_) =
-  Nametab.push_short_name (basename sp) (ConstRef sp)
+  Nametab.push_short_name sp (ConstRef sp)
 
 let export_parameter x = Some x
 
@@ -162,7 +162,7 @@ let cache_constant (sp,(cdt,stre,op)) =
     | ConstantRecipe r -> Global.add_discharged_constant sp r sc
   end;
   Nametab.push sp (ConstRef sp);
-  Nametab.push_short_name (basename sp) (ConstRef sp);
+  Nametab.push_short_name sp (ConstRef sp);
   if op then Global.set_opaque sp;
   csttab := Spmap.add sp stre !csttab
 
@@ -174,7 +174,7 @@ let load_constant (sp,(ce,stre,op)) =
   Nametab.push sp (ConstRef sp)
 
 let open_constant (sp,_) =
-  Nametab.push_short_name (basename sp) (ConstRef sp)
+  Nametab.push_short_name sp (ConstRef sp)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = ConstantEntry { 
@@ -234,8 +234,9 @@ let cache_inductive (sp,mie) =
   let names = inductive_names sp mie in
   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
-  (basename sp) ref) names
+  List.iter 
+    (fun (sp, ref) -> Nametab.push sp ref; Nametab.push_short_name sp ref)
+    names
 
 let load_inductive (sp,mie) =
   let names = inductive_names sp mie in
@@ -244,7 +245,7 @@ let load_inductive (sp,mie) =
 
 let open_inductive (sp,mie) =
   let names = inductive_names sp mie in
-  List.iter (fun (sp, ref) -> Nametab.push_short_name (basename sp) ref) names
+  List.iter (fun (sp, ref) -> Nametab.push_short_name sp ref) names
 
 let dummy_one_inductive_entry mie = {
   mind_entry_nparams = 0;
diff --git a/library/library.ml b/library/library.ml
index 5556bf32e..bc95496bc 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -271,7 +271,7 @@ and load_absolute_module_from dir =
       [< 'sTR"Cannot find module "; pr_dirpath dir; 'sTR" in loadpath">]
   | _ -> assert false
 
-let try_locate_qualified_library qid =
+let locate_qualified_library qid =
   (* Look if loaded *)
   try 
     let dir = Nametab.locate_loaded_library qid in
@@ -282,12 +282,9 @@ let try_locate_qualified_library qid =
     let dir, base = repr_qualid qid in 
     let loadpath =
       if dir = [] then get_load_path ()
-      else if is_absolute_dirpath dir then
+      else 
+        (* we assume dir is an absolute dirpath *)
 	load_path_of_logical_path dir
-      else
-	error
-	  ("Not loaded partially qualified library names not implemented: "
-	  ^(string_of_qualid qid))
     in
     if loadpath = [] then raise LibUnmappedDir;
     let name =  (string_of_id base)^".vo" in
@@ -295,9 +292,9 @@ let try_locate_qualified_library qid =
     (LibInPath, find_logical_path path@[base], file)
   with Not_found -> raise LibNotFound
 
-let locate_qualified_library qid =
+let try_locate_qualified_library qid =
   try
-    try_locate_qualified_library qid
+    locate_qualified_library qid
   with
   | LibUnmappedDir ->
       let prefix, id = repr_qualid qid in
@@ -346,10 +343,10 @@ let locate_module qid = function
       locate_by_filename_only (Some id) f
   | None ->
       (* No name, we need to find the file name *)
-      locate_qualified_library qid
+      try_locate_qualified_library qid
 
 let read_module qid =
-  ignore (load_module (locate_qualified_library qid))
+  ignore (load_module (try_locate_qualified_library qid))
 
 let read_module_from_file f =
   let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
diff --git a/library/nametab.ml b/library/nametab.ml
index 3d7ca98f4..a33bb9705 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -32,20 +32,27 @@ let qualid_of_dirpath dir =
   make_qualid l a
 
 exception GlobalizationError of qualid
+exception GlobalizationConstantError of qualid
 
 let error_global_not_found_loc loc q =
   Stdpp.raise_with_loc loc (GlobalizationError q)
 
+let error_global_constant_not_found_loc loc q =
+  Stdpp.raise_with_loc loc (GlobalizationConstantError q)
+
 let error_global_not_found q = raise (GlobalizationError q)
 
 (*s Roots of the space of absolute names *)
 
-let roots = ref []
-let push_library_root s = roots := list_add_set s !roots
-
 let coq_root = id_of_string "Coq"
 let default_root_prefix = []
 
+(* Obsolète
+let roots = ref []
+let push_library_root s = roots := list_add_set s !roots
+*)
+let push_library_root s = ()
+
 (* Constructions and syntactic definitions live in the same space *)
 type extended_global_reference =
   | TrueGlobal of global_reference
@@ -61,6 +68,16 @@ let the_libtab = ref (ModIdmap.empty : dirtab)
 let the_sectab = ref (ModIdmap.empty : dirtab)
 let the_objtab = ref (Idmap.empty : objtab)
 
+let dirpath_of_reference = function
+  | ConstRef sp -> dirpath sp
+  | VarRef sp -> dirpath sp
+  | ConstructRef ((sp,_),_) -> dirpath sp
+  | IndRef (sp,_) -> dirpath sp
+
+let dirpath_of_extended_ref = function
+  | TrueGlobal ref -> dirpath_of_reference ref
+  | SyntacticDef sp -> dirpath sp
+
 (* How necessarily_open works: concretely, roots and directory are
    always open but libraries are open only during their interactive
    construction or on demand if a precompiled one; then for a name
@@ -69,33 +86,41 @@ let the_objtab = ref (Idmap.empty : objtab)
 
 (* 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 tab dir o =
+let push_tree extract_dirpath tab dir o =
   let rec push necessarily_open (current,dirmap) = function
     | modid :: path as dir ->
 	let mc = 
 	  try ModIdmap.find modid dirmap
 	  with Not_found -> (None, ModIdmap.empty)
 	in
-	let this = if necessarily_open then Some o else current in
+	let this =
+          if necessarily_open then
+            if option_app extract_dirpath current = Some dir then
+              (* This is an absolute name, we must keep it otherwise it may
+                 become unaccessible forever *)
+              current
+            else
+              Some o
+          else current in
 	(this, ModIdmap.add modid (push true mc path) dirmap)
     | [] -> (Some o,dirmap) in
   push false tab (List.rev dir)
 
-let push_idtree tab dir id o =
+let push_idtree extract_dirpath tab dir id o =
   let modtab =
     try Idmap.find id !tab
     with Not_found -> (None, ModIdmap.empty) in
-  tab := Idmap.add id (push_tree modtab dir o) !tab
+  tab := Idmap.add id (push_tree extract_dirpath modtab dir o) !tab
 
-let push_long_names_ccipath = push_idtree the_ccitab
-let push_short_name_ccipath = push_idtree the_ccitab
-let push_short_name_objpath = push_idtree the_objtab
+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
+let push_short_name_objpath = push_idtree dirpath the_objtab
 
 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 modtab dir o) !tab
+  tab := ModIdmap.add id (push_tree (fun x -> x) modtab dir o) !tab
 
 let push_long_names_secpath = push_modidtree the_sectab
 let push_long_names_libpath = push_modidtree the_libtab
@@ -113,9 +138,9 @@ let push_cci sp ref =
 
 let push = push_cci
 
-let push_short_name id ref =
+let push_short_name sp ref =
   (* We push a volatile unqualified name *)
-  push_short_name_ccipath [] id (TrueGlobal ref)
+  push_short_name_ccipath [] (basename sp) (TrueGlobal ref)
 
 (* This is for Syntactic Definitions *)
 
@@ -142,7 +167,6 @@ let push_section fulldir =
   push_long_names_secpath [] s fulldir
 
 (* These are entry points to locate names *)
-(* If the name starts with the coq_root name, then it is an absolute name *)
 let locate_in_tree tab dir =
   let dir = List.rev dir in
   let rec search (current,modidtab) = function
@@ -185,8 +209,10 @@ let locate_section qid =
 (* Derived functions *)
 
 let locate_constant qid =
+  (* TODO: restrict to defined constants *)
   match locate_cci qid with
     | TrueGlobal (ConstRef sp) -> sp
+    | TrueGlobal (VarRef sp) -> sp
     | _ -> raise Not_found
 
 let sp_of_id _ id = match locate_cci (make_qualid [] id) with
@@ -200,6 +226,7 @@ let constant_sp_of_id id =
     | TrueGlobal (ConstRef sp) -> sp
     | _ -> raise Not_found
 
+(*
 let check_absoluteness dir =
   match dir with
     | a::_ when List.mem a !roots -> ()
@@ -216,34 +243,19 @@ let absolute_reference sp =
 let locate_in_absolute_module dir id =
   check_absoluteness dir;
   locate (make_qualid dir id)
-
-(*
-(* These are entry points to make the contents of a module/section visible *)
-(* in the current env (does not affect the absolute name space `coq_root') *)
-let open_module_contents qid =
-  let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
-  Idmap.iter push_cci_current ccitab;
-(*  Idmap.iter (fun _ -> Libobject.open_object) objtab;*)
-  Stringmap.iter push_mod_current modtab
-
-let conditional_push ref = push_cci_current ref (* TODO *)
-
-let open_section_contents qid =
-  let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
-  Idmap.iter push_cci_current ccitab;
-(*  Idmap.iter (fun _ -> Libobject.open_object) objtab;*)
-  Stringmap.iter push_mod_current modtab
-
-let rec rec_open_module_contents qid =
-  let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
-  Idmap.iter push_cci_current ccitab;
-(*  Idmap.iter (fun _ -> Libobject.open_object) objtab;*)
-  Stringmap.iter 
-    (fun m (sp,_ as mt) -> 
-       push_mod_current m mt;
-       rec_open_module_contents (qualid_of_sp sp))
-    modtab
 *)
+
+let absolute_reference sp =
+  let a = locate_cci (qualid_of_sp sp) in
+  if not (dirpath_of_extended_ref a = dirpath sp) then
+    anomaly ("Not an absolute path: "^(string_of_path sp));
+  match a with
+    | TrueGlobal ref -> ref
+    | _ -> raise Not_found
+
+let locate_in_absolute_module dir id =
+  absolute_reference (make_path dir id CCI)
+
 let exists_cci sp =
   try let _ = locate_cci (qualid_of_sp sp) in true
   with Not_found -> false
@@ -263,22 +275,22 @@ let init () =
   the_ccitab := Idmap.empty; 
   the_libtab := ModIdmap.empty;
   the_sectab := ModIdmap.empty;
-  the_objtab := Idmap.empty;
-  roots := []
+  the_objtab := Idmap.empty
+(*  ;roots := []*)
 
 let freeze () =
   !the_ccitab, 
   !the_libtab,
   !the_sectab,
-  !the_objtab,
-  !roots
+  !the_objtab
+(*  ,!roots*)
 
-let unfreeze (mc,ml,ms,mo,r) =
+let unfreeze (mc,ml,ms,mo(*,r*)) =
   the_ccitab := mc;
   the_libtab := ml;
   the_sectab := ms;
-  the_objtab := mo;
-  roots := r
+  the_objtab := mo(*;
+  roots := r*)
 
 let _ = 
   Summary.declare_summary "names"
diff --git a/library/nametab.mli b/library/nametab.mli
index 927205dea..6989e6bbf 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -37,17 +37,19 @@ val pr_qualid : qualid -> std_ppcmds
 val qualid_of_sp : section_path -> qualid
 
 exception GlobalizationError of qualid
+exception GlobalizationConstantError of qualid
 
 (* Raises a globalization error *)
 val error_global_not_found_loc : loc -> qualid -> 'a
 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_syntactic_definition : section_path -> unit
 
 (*s Register visibility of absolute paths by short names *)
-val push_short_name : identifier -> global_reference -> unit
+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
 
@@ -99,7 +101,9 @@ val push_library_root : module_ident -> unit
    references inside a block of mutual inductive *)
 val absolute_reference : section_path -> global_reference
 
+(*
 val is_absolute_dirpath : dir_path -> bool
+*)
 
 (* [locate_in_absolute_module dir id] finds [id] in module [dir] or in
    one of its section/subsection *)