Nouvelle structure arborescente à la Nametab pour prendre en compte les noms qualifiés

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

2 files changed, 80 insertions, 22 deletions

diff --git a/library/nametab.ml b/library/nametab.ml
index 911a381eb..8e15870e0 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -1,37 +1,76 @@
 
 (* $Id$ *)
 
+open Util
 open Names
+open Libobject
+open Declarations
+open Term
 
-let cci_tab = ref Idmap.empty
-let fw_tab = ref Idmap.empty
+type cci_table = global_reference Idmap.t
+type obj_table = (section_path * obj) Idmap.t
+type mod_table = module_contents Stringmap.t
+and module_contents = Closed of cci_table * obj_table * mod_table
 
-let fw_sp_of_id id =
-  Idmap.find id !fw_tab
+let mod_tab = ref (Stringmap.empty : mod_table)
+let cci_tab = ref (Idmap.empty : cci_table)
+let obj_tab = ref (Idmap.empty : obj_table)
 
-let sp_of_id kind id =
-  match kind with
-    | FW -> Idmap.find id !fw_tab
-    | CCI -> Idmap.find id !cci_tab
-    | OBJ -> invalid_arg "Nametab.sp_of_id"
-	  
-let push id sp =
-  match kind_of_path sp with
-    | FW -> fw_tab := Idmap.add id sp !fw_tab
-    | CCI -> cci_tab := Idmap.add id sp !cci_tab
-    | OBJ -> invalid_arg "Nametab.push"
+let sp_of_id _ id = Idmap.find id !cci_tab
+
+let constant_sp_of_id id =
+  match Idmap.find id !cci_tab with
+    | ConstRef sp -> sp
+    | _ -> raise Not_found
+
+let push_cci id sp = cci_tab := Idmap.add id sp !cci_tab
+let push_obj id sp = obj_tab := Idmap.add id sp !obj_tab
+let push_module id mc = mod_tab := Stringmap.add id mc !mod_tab
+
+let push = push_cci
+
+let locate sp =
+  let (dir,id,_) = repr_path sp in
+  let rec search (ccitab,modtab) = function
+    | id :: dir' ->
+	let (Closed (ccitab, _, modtab)) = Stringmap.find id modtab in
+	search (ccitab,modtab) dir'
+    | [] -> Idmap.find id ccitab
+  in search (!cci_tab,!mod_tab) dir
+
+let locate_obj sp =
+  let (dir,id,_) = repr_path sp in
+  let rec search (objtab,modtab) = function
+    | id :: dir' ->
+	let (Closed (_, objtab, modtab)) = Stringmap.find id modtab in
+	search (objtab,modtab) dir'
+    | [] -> Idmap.find id objtab
+  in search (!obj_tab,!mod_tab) dir
+
+let locate_constant sp =
+  match locate sp with
+    | ConstRef sp -> sp
+    | _ -> raise Not_found
+
+let open_module_contents id =
+  let (Closed (ccitab,objtab,modtab)) = Stringmap.find id !mod_tab in
+  Idmap.iter push_cci ccitab;
+  Idmap.iter (fun _ -> Libobject.open_object) objtab;
+  Stringmap.iter push_module modtab
 
 (* Registration as a global table and roolback. *)
     
 let init () =
   cci_tab := Idmap.empty;
-  fw_tab := Idmap.empty
+  obj_tab := Idmap.empty;
+  mod_tab := Stringmap.empty;
 
-type frozen = section_path Idmap.t * section_path Idmap.t
+type frozen = cci_table Idmap.t * obj_table Idmap.t * mod_table Stringmap.t
 
-let freeze () = (!cci_tab, !fw_tab)
+let freeze () = (!cci_tab, !obj_tab, !mod_tab)
 		  
-let unfreeze (cci,fw) = cci_tab := cci; fw_tab := fw
+let unfreeze (ccitab,objtab,modtab) =
+  cci_tab := ccitab; obj_tab := objtab; mod_tab := modtab
 
 let _ = 
   Summary.declare_summary "names"
@@ -42,3 +81,4 @@ let _ =
 let rollback f x =
   let fs = freeze () in
   try f x with e -> begin unfreeze fs; raise e end
+
diff --git a/library/nametab.mli b/library/nametab.mli
index 463dc63de..2b0e4dd52 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -2,13 +2,31 @@
 (* $Id$ *)
 
 (*i*)
+open Util
 open Names
+open Term
 (*i*)
 
 (* This module contains the table for globalization, which associates global
    names (section paths) to identifiers. *)
 
-val push : identifier -> section_path -> unit
+type cci_table = global_reference Idmap.t
+type obj_table = (section_path * Libobject.obj) Idmap.t
+type mod_table = module_contents Stringmap.t
+and module_contents = Closed of cci_table * obj_table * mod_table
+
+val push : identifier -> global_reference -> unit
+val push_obj : identifier -> (section_path * Libobject.obj) -> unit
+val push_module : string -> module_contents -> unit
+
+val sp_of_id : path_kind -> identifier -> global_reference
+
+(* This returns the section_path of a constant or fails with Not_found *)
+val constant_sp_of_id : identifier -> section_path
+
+val locate : section_path -> global_reference
+val locate_obj : section_path -> (section_path * Libobject.obj)
+val locate_constant : section_path -> constant_path
+
+val open_module_contents : string -> unit
 
-val sp_of_id : path_kind -> identifier -> section_path
-val fw_sp_of_id : identifier -> section_path