Prise en compte de noms absolus dans la nametab

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

6 files changed, 139 insertions, 63 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index c8eb17ca95..ae80915b74 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -136,10 +136,14 @@ let repr_qualid q = q
 let string_of_qualid (l,s) = String.concat "." (l@[s])
 let pr_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s])
 
-(*s Section paths *)
-
+(*s Directory paths = section names paths *)
 type dir_path = string list
 
+(* The root of absolute names *)
+let coq_root = ["Coq"]
+
+(*s Section paths are absolute names *)
+
 type section_path = {
   dirpath : dir_path ;
   basename : identifier ;
@@ -152,13 +156,16 @@ let kind_of_path sp = sp.kind
 let basename sp = sp.basename
 let dirpath sp = sp.dirpath
 
+let qualid_of_sp sp =
+  make_qualid (coq_root @ dirpath sp) (string_of_id (basename sp))
+
 (* parsing and printing of section paths *)
-let string_of_dirpath sl = String.concat "#" (""::sl)
+let string_of_dirpath sl = String.concat "." (coq_root@sl)
 
 let string_of_path sp =
   let (sl,id,k) = repr_path sp in
   String.concat ""
-    ("#"::(List.flatten (List.map (fun s -> [s;"."]) sl))
+    (List.flatten (List.map (fun s -> [s;"."]) (coq_root@sl))
      @ [ string_of_id id ])
     
 let path_of_string s =
diff --git a/kernel/names.mli b/kernel/names.mli
index 070e7917fa..a5ae56da46 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -46,21 +46,21 @@ val kind_of_string : string -> path_kind
 (*s Directory paths = section names paths *)
 type dir_path = string list
 
-(* Printing of directory paths as ["#module#submodule"] *)
-val string_of_dirpath : dir_path -> string
-
+val coq_root : dir_path
 
-(*s Section paths *)
+(* Printing of directory paths as ["coq_root.module.submodule"] *)
+val string_of_dirpath : dir_path -> string
 
+(*s Qualified idents are names relative to the current visilibity of names *)
 type qualid
 
-val make_qualid : string list -> string -> qualid
-val repr_qualid : qualid -> string list * string
+val make_qualid : dir_path -> string -> qualid
+val repr_qualid : qualid -> dir_path * string
 
 val string_of_qualid : qualid -> string
 val pr_qualid : qualid -> std_ppcmds
 
-(*s Section paths *)
+(*s Section paths are {\em absolute} names *)
 type section_path
 
 (* Constructors of [section_path] *)
@@ -75,7 +75,10 @@ val kind_of_path : section_path -> path_kind
 val sp_of_wd : string list -> section_path
 val wd_of_sp : section_path -> string list
 
-(* Parsing and printing of section path as ["#module#id#kind"] *)
+(* Turns an absolute name into a qualified name denoting the same name *)
+val qualid_of_sp : section_path -> qualid
+
+(* Parsing and printing of section path as ["coq_root.module.id"] *)
 val path_of_string : string -> section_path
 val string_of_path : section_path -> string
 val pr_sp : section_path -> std_ppcmds
diff --git a/library/library.ml b/library/library.ml
index 30fba46ecd..54e1d394b8 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -123,7 +123,7 @@ let rec open_module s =
   if not m.module_opened then begin
     List.iter (fun (m,_,exp) -> if exp then open_module m) m.module_deps;
     open_objects m.module_declarations;
-    Nametab.open_module_contents s; 
+    Nametab.open_module_contents (make_qualid [] s); 
     m.module_opened <- true
   end
 
@@ -157,7 +157,8 @@ let rec load_module_from s f =
     List.iter (load_mandatory_module s) m.module_deps;
     Global.import m.module_compiled_env;
     load_objects m.module_declarations;
-    Nametab.push_module s m.module_nametab;
+    let sp = Names.make_path [] (id_of_string s) CCI in
+    Nametab.push_module sp m.module_nametab;
     modules_table := Stringmap.add s m !modules_table
   end
 
diff --git a/library/nametab.ml b/library/nametab.ml
index d13e378e81..595f3b58a1 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 open Util
+open Pp
 open Names
 open Libobject
 open Declarations
@@ -9,76 +10,136 @@ open Term
 
 type cci_table = global_reference Stringmap.t
 type obj_table = (section_path * obj) Stringmap.t
-type mod_table = module_contents Stringmap.t
+type mod_table = (section_path * module_contents) Stringmap.t
 and module_contents = Closed of cci_table * obj_table * mod_table
 
-let mod_tab = ref (Stringmap.empty : mod_table)
-let cci_tab = ref (Stringmap.empty : cci_table)
-let obj_tab = ref (Stringmap.empty : obj_table)
+let empty =
+  Closed (Stringmap.empty, Stringmap.empty, Stringmap.empty)
+ 
+let nametabs = ref (empty : module_contents)
 
-let sp_of_id _ id = Stringmap.find (string_of_id id) !cci_tab
+let push_cci (Closed (ccitab, objtab, modtab)) s ref =
+  Closed (Stringmap.add s ref ccitab, objtab, modtab)
 
-let constant_sp_of_id id =
-  match Stringmap.find (string_of_id id) !cci_tab with
-    | ConstRef sp -> sp
-    | _ -> raise Not_found
-
-let push_cci s sp = cci_tab := Stringmap.add s sp !cci_tab
-let push_obj s sp = obj_tab := Stringmap.add s sp !obj_tab
-let push_module s mc = mod_tab := Stringmap.add s mc !mod_tab
+let push_obj (Closed (ccitab, objtab, modtab)) s obj =
+  Closed (ccitab, Stringmap.add s obj objtab, modtab)
 
-let push_object id = push_obj (string_of_id id)
-let push id = push_cci (string_of_id id) 
+let push_mod (Closed (ccitab, objtab, modtab)) s mc =
+  (* devrait pas mais ca plante en décommentant la ligne ci-dessous *)
+ (* assert (not (Stringmap.mem s modtab)); *)
+  Closed (ccitab, objtab, Stringmap.add s mc modtab)
 
+let push_tree push dir id o =
+  let rec search (Closed (ccitab, objtab, modtab) as tabs) pref = function
+    | id :: dir' ->
+	let sp, mc = 
+	  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
+
+(* This pushes a name at the current level (for relative qualified use) *)
+let push_cci_current = push_tree push_cci []
+let push_obj_current = push_tree push_obj []
+let push_mod_current = push_tree push_mod []
+
+(* This pushes a name at the root level (for absolute access) *)
+let push_cci_absolute = push_tree push_cci
+let push_obj_absolute = push_tree push_obj
+let push_mod_absolute = push_tree push_mod
+
+(* These are entry points for new declarations at toplevel *)
+(* Do not use with "open" since it pushes an absolute name too *)
+let push sp ref =
+  let dir, s = repr_qualid (qualid_of_sp sp) in
+  push_cci_absolute dir s ref;
+  push_cci_current s ref
+
+let push_object sp obj =
+  let dir, s = repr_qualid (qualid_of_sp sp) in
+  push_obj_absolute dir s (sp,obj);
+  push_obj_current s (sp,obj)
+
+let push_module sp mc =
+  let dir, s = repr_qualid (qualid_of_sp sp) in
+  push_mod_absolute dir s (sp,mc);
+  if s = List.hd coq_root then 
+    warning ("Cannot allow access to "^s^" by relative paths: it conflicts with the \nroot of Coq library")
+  else push_mod_current s (sp,mc)
+
+(* 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 =
   let (dir,id) = repr_qualid qid in
-  let rec search (ccitab,modtab) = function
-    | id :: dir' ->
-	let (Closed (ccitab, _, modtab)) = Stringmap.find id modtab in
-	search (ccitab,modtab) dir'
+  let rec search (Closed (ccitab,_,modtab)) = function
+    | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
     | [] -> Stringmap.find id ccitab
-  in search (!cci_tab,!mod_tab) dir
+  in search !nametabs dir
 
 let locate_obj qid =
   let (dir,id) = repr_qualid qid in
-  let rec search (objtab,modtab) = function
-    | id :: dir' ->
-	let (Closed (_, objtab, modtab)) = Stringmap.find id modtab in
-	search (objtab,modtab) dir'
+  let rec search (Closed (_,objtab,modtab)) = function
+    | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
     | [] -> Stringmap.find id objtab
-  in search (!obj_tab,!mod_tab) dir
+  in search !nametabs 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
 
 let locate_constant qid =
   match locate qid with
     | ConstRef sp -> sp
     | _ -> raise Not_found
 
-let open_module_contents s =
-  let (Closed (ccitab,objtab,modtab)) = Stringmap.find s !mod_tab in
-  Stringmap.iter push_cci ccitab;
+let sp_of_id _ id = locate (make_qualid [] (string_of_id id))
+
+let constant_sp_of_id id =
+  match locate (make_qualid [] (string_of_id id)) with
+    | ConstRef sp -> sp
+    | _ -> raise Not_found
+
+(* 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
+  Stringmap.iter push_cci_current ccitab;
 (*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
-  Stringmap.iter push_module modtab
+  Stringmap.iter push_mod_current modtab
 
-let rec rec_open_module_contents id =
-  let (Closed (ccitab,objtab,modtab)) = Stringmap.find id !mod_tab in
-  Stringmap.iter push_cci ccitab;
+let rec rec_open_module_contents qid =
+  let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
+  Stringmap.iter push_cci_current ccitab;
 (*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
   Stringmap.iter 
-    (fun m mt -> push_module m mt; rec_open_module_contents m) modtab
+    (fun m (sp,_ as mt) -> 
+       push_mod_current m mt;
+       rec_open_module_contents (qualid_of_sp sp))
+    modtab
+
+let exists_cci sp =
+  try let _ = locate (qualid_of_sp sp) in true with Not_found -> false
 
-(* Registration as a global table and rollback. *)
+(***********************************************)
+(* Registration as a global table and rollback *)
     
-let init () =
-  cci_tab := Stringmap.empty;
-  obj_tab := Stringmap.empty;
-  mod_tab := Stringmap.empty;
+let init () = nametabs := empty
 
-type frozen = cci_table Stringmap.t * obj_table Stringmap.t * mod_table Stringmap.t
+type frozen = module_contents
 
-let freeze () = (!cci_tab, !obj_tab, !mod_tab)
+let freeze () = !nametabs
 		  
-let unfreeze (ccitab,objtab,modtab) =
-  cci_tab := ccitab; obj_tab := objtab; mod_tab := modtab
+let unfreeze mc = nametabs := mc
 
 let _ = 
   Summary.declare_summary "names"
diff --git a/library/nametab.mli b/library/nametab.mli
index 54c4bc67be..1d39eb3107 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -12,12 +12,12 @@ open Term
 
 type cci_table = global_reference Stringmap.t
 type obj_table = (section_path * Libobject.obj) Stringmap.t
-type mod_table = module_contents Stringmap.t
+type mod_table = (section_path * module_contents) Stringmap.t
 and module_contents = Closed of cci_table * obj_table * mod_table
 
-val push : identifier -> global_reference -> unit
-val push_object : identifier -> (section_path * Libobject.obj) -> unit
-val push_module : string -> module_contents -> unit
+val push : section_path -> global_reference -> unit
+val push_object : section_path -> Libobject.obj -> unit
+val push_module : section_path -> module_contents -> unit
 
 val sp_of_id : path_kind -> identifier -> global_reference
 
@@ -27,9 +27,13 @@ val constant_sp_of_id : identifier -> section_path
 val locate : qualid -> global_reference
 val locate_obj : qualid -> (section_path * Libobject.obj)
 val locate_constant : qualid -> constant_path
+val locate_module : qualid -> section_path * module_contents
 
-val open_module_contents : string -> unit
-val rec_open_module_contents : string -> unit
+(* [exists sp] tells if [sp] is already bound to a cci term *)
+val exists_cci : section_path -> bool
+
+val open_module_contents : qualid -> unit
+val rec_open_module_contents : qualid -> unit
 
 
 
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index 4801d017e7..1e63907a49 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -36,7 +36,7 @@ let (in_syntax_constant, out_syntax_constant) =
 let _ =
   cache_syntax_constant := fun (sp,c) ->
     add_syntax_constant sp c;
-    Nametab.push_object (basename sp) (sp, in_syntax_constant c)
+    Nametab.push_object sp (in_syntax_constant c)
 
 let declare_syntactic_definition id c =
   let _ = add_leaf id CCI (in_syntax_constant c) in ()