Déplacement de qualid dans Nametab, hors du noyau

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

7 files changed, 60 insertions, 12 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 853a22d12..f0f2790a5 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -15,6 +15,7 @@ open Libobject
 open Lib
 open Impargs
 open Indrec
+open Nametab
 
 type strength = 
   | NotDeclare
diff --git a/library/declare.mli b/library/declare.mli
index 07dc96914..6c47e3a52 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -90,11 +90,11 @@ val extract_instance : global_reference -> constr array -> constr array
 val constr_of_reference :
   'a Evd.evar_map -> Environ.env -> global_reference -> constr
 
-val global_qualified_reference : qualid -> constr
+val global_qualified_reference : Nametab.qualid -> constr
 val global_absolute_reference : section_path -> constr
 val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
-val construct_qualified_reference : Environ.env -> qualid -> constr
+val construct_qualified_reference : Environ.env -> Nametab.qualid -> constr
 val construct_absolute_reference : Environ.env -> section_path -> constr
 
 (* This should eventually disappear *)
diff --git a/library/global.ml b/library/global.ml
index cdc7fdb18..faca388aa 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -57,7 +57,7 @@ let import cenv = global_env := import cenv !global_env
 
 (* Some instanciations of functions from [Environ]. *)
 
-let sp_of_global id = Environ.sp_of_global (env_of_safe_env !global_env) id
+let sp_of_global ref = Environ.sp_of_global (env_of_safe_env !global_env) ref
 
 (* To know how qualified a name should be to be understood in the current env*)
 
@@ -65,14 +65,16 @@ let qualid_of_global ref =
   let sp = sp_of_global ref in
   let id = basename sp in
   let rec find_visible dir qdir =
-    let qid = make_qualid qdir id in
+    let qid = Nametab.make_qualid qdir id in
     if (try Nametab.locate qid = ref with Not_found -> false) then qid
     else match dir with
-      | [] -> qualid_of_sp sp
+      | [] -> Nametab.qualid_of_sp sp
       | a::l -> find_visible l (a::qdir)
   in
   find_visible (List.rev (dirpath sp)) []
 
+let string_of_global ref = Nametab.string_of_qualid (qualid_of_global ref)
+
 (*s Function to get an environment from the constants part of the global
     environment and a given context. *)
 
diff --git a/library/global.mli b/library/global.mli
index 74a7197d4..da0386be1 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -49,7 +49,10 @@ val import : compiled_env -> unit
 (*s Some functions of [Environ] instanciated on the global environment. *)
 
 val sp_of_global : global_reference -> section_path
-val qualid_of_global : global_reference -> qualid
+
+(*s This is for printing purpose *)
+val qualid_of_global : global_reference -> Nametab.qualid
+val string_of_global : global_reference -> string
 
 (*s Function to get an environment from the constants part of the global
     environment and a given context. *)
diff --git a/library/library.ml b/library/library.ml
index 0ec028963..d1e162aff 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -8,6 +8,7 @@ open Names
 open Environ
 open Libobject
 open Lib
+open Nametab
 
 (*s Load path. *)
 
@@ -27,7 +28,7 @@ type module_disk = {
   md_name : string;
   md_compiled_env : compiled_env;
   md_declarations : library_segment;
-  md_nametab : Nametab.module_contents;
+  md_nametab : module_contents;
   md_deps : (string * Digest.t * bool) list }
 
 (*s Modules loaded in memory contain the following informations. They are
@@ -38,7 +39,7 @@ type module_t = {
   module_filename : load_path_entry * string;
   module_compiled_env : compiled_env;
   module_declarations : library_segment;
-  module_nametab : Nametab.module_contents;
+  module_nametab : module_contents;
   mutable module_opened : bool;
   mutable module_exported : bool;
   module_deps : (string * Digest.t * bool) list;
@@ -117,7 +118,7 @@ let rec open_module force s =
   if force or not m.module_opened then begin
     List.iter (fun (m,_,exp) -> if exp then open_module force m) m.module_deps;
     open_objects m.module_declarations;
-    Nametab.open_module_contents (make_qualid [] (id_of_string s)); 
+    open_module_contents (make_qualid [] (id_of_string s)); 
     m.module_opened <- true
   end
 
@@ -155,7 +156,7 @@ let rec load_module_from s f =
     Global.import m.module_compiled_env;
     load_objects m.module_declarations;
     let sp = Names.make_path lpe.coq_dirpath (id_of_string s) CCI in
-    Nametab.push_module sp m.module_nametab;
+    push_module sp m.module_nametab;
     modules_table := Stringmap.add s m !modules_table;
     m
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 046a9518c..253483791 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -8,6 +8,23 @@ open Libobject
 open Declarations
 open Term
 
+(*s qualified names *)
+type qualid = string list * identifier
+
+let make_qualid p id = (p,id)
+let repr_qualid q = q
+
+let string_of_qualid (l,id) = String.concat "." (l@[string_of_id id])
+let pr_qualid (l,id) =
+  prlist_with_sep (fun () -> pr_str ".") pr_str (l@[string_of_id id])
+
+let qualid_of_sp sp = make_qualid (dirpath sp) (basename sp)
+
+exception GlobalizationError of qualid
+
+let error_global_not_found_loc loc q =
+  Stdpp.raise_with_loc loc (GlobalizationError q)
+
 (*s Roots of the space of absolute names *)
 
 let roots = ref []
diff --git a/library/nametab.mli b/library/nametab.mli
index a9a466bb3..a62385bb6 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -3,18 +3,40 @@
 
 (*i*)
 open Util
+open Pp
 open Names
 open Term
 (*i*)
 
-(* This module contains the table for globalization, which associates global
-   names (section paths) to identifiers. *)
+(*s This module contains the table for globalization, which associates global
+   names (section paths) to qualified names. *)
 
+(*s A [qualid] is a partially qualified ident; it includes fully
+    qualified names (= absolute names) and all intermediate partial
+    qualifications of absolute names, including single identifiers *)
+type qualid
+
+val make_qualid : dir_path -> identifier -> qualid
+val repr_qualid : qualid -> dir_path * identifier
+
+val string_of_qualid : qualid -> string
+val pr_qualid : qualid -> std_ppcmds
+
+(* Turns an absolute name into a qualified name denoting the same name *)
+val qualid_of_sp : section_path -> qualid
+
+exception GlobalizationError of qualid
+
+(* Raises a globalization error *)
+val error_global_not_found_loc : loc -> qualid -> 'a
+
+(*s Names tables *)
 type cci_table = global_reference Idmap.t
 type obj_table = (section_path * Libobject.obj) Idmap.t
 type mod_table = (section_path * module_contents) Stringmap.t
 and module_contents = Closed of cci_table * obj_table * mod_table
 
+(*s Registers absolute paths *)
 val push : section_path -> global_reference -> unit
 val push_object : section_path -> Libobject.obj -> unit
 val push_module : section_path -> module_contents -> unit
@@ -25,6 +47,8 @@ val push_local_object : section_path -> Libobject.obj -> unit
 (* This should eventually disappear *)
 val sp_of_id : path_kind -> identifier -> global_reference
 
+(*s The following functions perform globalization of qualified names *)
+
 (* This returns the section path of a constant or fails with [Not_found] *)
 val constant_sp_of_id : identifier -> section_path