Names.make_mbid and co : convert from/to identifier (avoid some String.copy)

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

5 files changed, 10 insertions, 10 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index c65e624c2..c85389434 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -72,8 +72,8 @@ let string_of_dirpath = function
 
 
 let u_number = ref 0
-type uniq_ident = int * string * dir_path
-let make_uid dir s = incr u_number;(!u_number,String.copy s,dir)
+type uniq_ident = int * identifier * dir_path
+let make_uid dir s = incr u_number;(!u_number,s,dir)
  let debug_string_of_uid (i,s,p) =
  "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
 let string_of_uid (i,s,p) =
@@ -347,8 +347,8 @@ module Hdir = Hashcons.Make(
 module Huniqid = Hashcons.Make(
   struct
     type t = uniq_ident
-    type u = (string -> string) * (dir_path -> dir_path)
-    let hash_sub (hstr,hdir) (n,s,dir) = (n,hstr s,hdir dir)
+    type u = (identifier -> identifier) * (dir_path -> dir_path)
+    let hash_sub (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
     let equal (n1,s1,dir1) (n2,s2,dir2) = n1 = n2 && s1 == s2 && dir1 == dir2
     let hash = Hashtbl.hash
   end)
@@ -394,7 +394,7 @@ let hcons_names () =
   let hident = hstring in
   let hname = Hashcons.simple_hcons Hname.f hident in
   let hdir = Hashcons.simple_hcons Hdir.f hident in
-  let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in
+  let huniqid = Hashcons.simple_hcons Huniqid.f (hident,hdir) in
   let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in
   let hmind = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in
   let hcn = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in
diff --git a/kernel/names.mli b/kernel/names.mli
index 62d2040c2..8a2e892ef 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -62,8 +62,8 @@ type mod_bound_id
 (** The first argument is a file name - to prevent conflict between
    different files *)
 
-val make_mbid : dir_path -> string -> mod_bound_id
-val repr_mbid : mod_bound_id -> int * string * dir_path
+val make_mbid : dir_path -> identifier -> mod_bound_id
+val repr_mbid : mod_bound_id -> int * identifier * dir_path
 val id_of_mbid : mod_bound_id -> identifier
 val label_of_mbid : mod_bound_id -> label
 val debug_string_of_mbid : mod_bound_id -> string
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 8753624a9..d4712762a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -545,7 +545,7 @@ let process_module_seb_binding mbid seb =
 let intern_args interp_modtype (idl,(arg,ann)) =
   let inl = inline_annot ann in
   let lib_dir = Lib.library_dp() in
-  let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
+  let mbids = List.map (fun (_,id) -> make_mbid lib_dir id) idl in
   let mty = interp_modtype (Global.env()) arg in
   let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
   let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env())
diff --git a/library/lib.ml b/library/lib.ml
index cfaea3b66..23d334a5d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -728,7 +728,7 @@ let rec split_mp mp =
     | Names.MPdot (prfx, lbl) ->
 	let mprec, dprec = split_mp prfx in
 	  mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
-    | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [Names.id_of_string id]
+    | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [id]
 
 let split_modpath mp =
   let rec aux = function
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index bb20dc7fc..b1ba16b5c 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -260,7 +260,7 @@ let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
   let lib_dir = Lib.library_dp() in
   List.iter (fun (_,id) ->
     Declaremods.process_module_bindings [id]
-      [make_mbid lib_dir (string_of_id id),
+      [make_mbid lib_dir id,
        (Modintern.interp_modtype (Global.env()) mty, inl)]) idl;
   (* Builds the stream *)
   spc() ++