Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de la section; 2 racines officielles pour l'espace des noms : Coq et Scratch

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

2 files changed, 69 insertions, 18 deletions

diff --git a/library/nametab.ml b/library/nametab.ml
index c7afb5bfc..7b92a40cc 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -8,9 +8,15 @@ open Libobject
 open Declarations
 open Term
 
+(*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 = "Coq"
+let default_root = "Scratch"
+
+(* Names tables *)
 type cci_table = global_reference Stringmap.t
 type obj_table = (section_path * obj) Stringmap.t
 type mod_table = (section_path * module_contents) Stringmap.t
@@ -19,7 +25,8 @@ and module_contents = Closed of cci_table * obj_table * mod_table
 let empty =
   Closed (Stringmap.empty, Stringmap.empty, Stringmap.empty)
  
-let nametabs = ref (empty : module_contents)
+let persistent_nametab = ref (empty : module_contents)
+let local_nametab = ref (empty : module_contents)
 
 let push_cci (Closed (ccitab, objtab, modtab)) s ref =
   Closed (Stringmap.add s ref ccitab, objtab, modtab)
@@ -39,14 +46,13 @@ let push_tree push dir id o =
 	  try Stringmap.find id modtab
 	  with Not_found ->
 	    let pref = List.rev pref in
-	    let dir = if pref@[id] = coq_root then [] else pref in
 	    (make_path dir (id_of_string id) CCI, empty)
 	in
 	Closed (ccitab, objtab,
 		Stringmap.add id (sp,search mc (id::pref) dir') modtab)
     | [] ->
-	push tabs id o
-  in nametabs := search !nametabs [] dir
+	push tabs id o in
+  persistent_nametab := search !persistent_nametab [] dir
 
 (* This pushes a name at the current level (for relative qualified use) *)
 let push_cci_current = push_tree push_cci []
@@ -77,6 +83,25 @@ let push_module sp mc =
     warning ("Cannot allow access to "^s^" by relative paths: it is already registered as a root of the Coq library")
   else push_mod_current s (sp,mc)
 
+(* This is an entry point for local declarations at toplevel *)
+(* Do not use with "open" since it pushes an absolute name too *)
+
+let push_cci_local s ref =
+  local_nametab := push_cci !local_nametab s ref
+
+let push_obj_local s o =
+  local_nametab := push_obj !local_nametab s o
+
+let push_local sp ref =
+  let dir, s = repr_qualid (qualid_of_sp sp) in
+  push_cci_absolute dir s ref;
+  push_cci_local s ref
+
+let push_local_object sp obj =
+  let dir, s = repr_qualid (qualid_of_sp sp) in
+  push_obj_absolute dir s (sp,obj);
+  push_obj_local s (sp,obj)
+
 (* These are entry points to locate names *)
 (* If the name starts with the coq_root name, then it is an absolute name *)
 let locate qid =
@@ -84,21 +109,27 @@ let locate qid =
   let rec search (Closed (ccitab,_,modtab)) = function
     | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
     | [] -> Stringmap.find id ccitab
-  in search !nametabs dir
+  in
+  try search !local_nametab dir
+  with Not_found -> search !persistent_nametab dir
 
 let locate_obj qid =
   let (dir,id) = repr_qualid qid in
   let rec search (Closed (_,objtab,modtab)) = function
     | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
     | [] -> Stringmap.find id objtab
-  in search !nametabs dir
+  in
+  try search !local_nametab dir
+  with Not_found -> search !persistent_nametab dir
 
 let locate_module qid =
   let (dir,id) = repr_qualid qid in
   let rec search (Closed (_,_,modtab)) = function
     | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
     | [] -> Stringmap.find id modtab
-  in search !nametabs dir
+  in
+  try search !local_nametab dir
+  with Not_found -> search !persistent_nametab dir
 
 let locate_constant qid =
   match locate qid with
@@ -133,25 +164,33 @@ let rec rec_open_module_contents qid =
 let exists_cci sp =
   try let _ = locate (qualid_of_sp sp) in true with Not_found -> false
 
-(***********************************************)
-(* Registration as a global table and rollback *)
-    
-let init () = nametabs := empty; roots := []
+(********************************************************************)
+(* Registration of persistent tables as a global table and rollback *)
 
 type frozen = module_contents * dir_path list
 
-let freeze () = !nametabs, !roots
-		  
-let unfreeze (mc,r) = nametabs := mc; roots := r
+let init () = persistent_nametab := empty; roots := []
+let freeze () = !persistent_nametab, !roots
+let unfreeze (mc,r) = persistent_nametab := mc; roots := r
 
 let _ = 
-  Summary.declare_summary "names"
+  Summary.declare_summary "persistent-names"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
       Summary.survive_section = true }
 
-let rollback f x =
-  let fs = freeze () in
-  try f x with e -> begin unfreeze fs; raise e end
+(********************************************************************)
+(* Registration of persistent tables as a global table and rollback *)
+
+let init () = local_nametab := empty
+let freeze () = !local_nametab
+let unfreeze mc = local_nametab := mc
+
+let _ = 
+  Summary.declare_summary "local-names"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_section = false }
 
diff --git a/library/nametab.mli b/library/nametab.mli
index 646a2f176..7382b447d 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -19,6 +19,9 @@ val push : section_path -> global_reference -> unit
 val push_object : section_path -> Libobject.obj -> unit
 val push_module : section_path -> module_contents -> unit
 
+val push_local : section_path -> global_reference -> unit
+val push_local_object : section_path -> Libobject.obj -> unit
+
 (* This should eventually disappear *)
 val sp_of_id : path_kind -> identifier -> global_reference
 
@@ -36,5 +39,14 @@ val exists_cci : section_path -> bool
 val open_module_contents : qualid -> unit
 val rec_open_module_contents : qualid -> unit
 
+(*s Roots of the space of absolute names *)
+
+(* This is the root of the standard library of Coq *)
+val coq_root : string
+
+(* This is the default root for developments which doesn't mention a root *)
+val default_root : string
+
+(* This is to declare a new root *)
 val push_library_root : string -> unit