diff options
| -rw-r--r-- | dev/top_printers.ml | 1 | ||||
| -rw-r--r-- | kernel/names.ml | 10 | ||||
| -rw-r--r-- | kernel/names.mli | 45 | ||||
| -rw-r--r-- | plugins/xml/cic2acic.ml | 32 |
4 files changed, 17 insertions, 71 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 1a1d03a61..daf599d8a 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -38,7 +38,6 @@ let pppp x = pp x (* name printers *) let ppid id = pp (pr_id id) let pplab l = pp (pr_lab l) -let ppmsid msid = pp (str (debug_string_of_msid msid)) let ppmbid mbid = pp (str (debug_string_of_mbid mbid)) let ppdir dir = pp (pr_dirpath dir) let ppmp mp = pp(str (string_of_mp mp)) diff --git a/kernel/names.ml b/kernel/names.ml index d5f301f2f..aef0039e1 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -88,15 +88,6 @@ module Umap = Map.Make(struct type label = string -type mod_self_id = uniq_ident -let make_msid = make_uid -let repr_msid (n, id, dp) = (n, id, dp) -let debug_string_of_msid = debug_string_of_uid -let refresh_msid (_,s,dir) = make_uid dir s -let string_of_msid = string_of_uid -let id_of_msid (_,s,_) = s -let label_of_msid (_,s,_) = s - type mod_bound_id = uniq_ident let make_mbid = make_uid let repr_mbid (n, id, dp) = (n, id, dp) @@ -230,7 +221,6 @@ let default_module_name = "If you see this, it's a bug" let initial_dir = make_dirpath [default_module_name] -let initial_msid = (make_msid initial_dir "If you see this, it's a bug") let initial_path = MPfile initial_dir type variable = identifier diff --git a/kernel/names.mli b/kernel/names.mli index b441bf00a..d64dbe1ca 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -38,26 +38,26 @@ val empty_dirpath : dir_path (** Printing of directory paths as ["coq_root.module.submodule"] *) val string_of_dirpath : dir_path -> string +(** {6 Names of structure elements } *) -(** {6 ... } *) -(** Unique identifier to be used as "self" in structures and - signatures - invisible for users *) type label -type mod_self_id -(** The first argument is a file name - to prevent conflict between - different files *) -val make_msid : dir_path -> string -> mod_self_id -val repr_msid : mod_self_id -> int * string * dir_path -val id_of_msid : mod_self_id -> identifier -val label_of_msid : mod_self_id -> label -val refresh_msid : mod_self_id -> mod_self_id -val debug_string_of_msid : mod_self_id -> string -val string_of_msid : mod_self_id -> string +val mk_label : string -> label +val string_of_label : label -> string + +val label_of_id : identifier -> label +val id_of_label : label -> identifier + +module Labset : Set.S with type elt = label +module Labmap : Map.S with type key = label (** {6 Unique names for bound modules } *) + 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 id_of_mbid : mod_bound_id -> identifier @@ -65,18 +65,8 @@ val label_of_mbid : mod_bound_id -> label val debug_string_of_mbid : mod_bound_id -> string val string_of_mbid : mod_bound_id -> string -(** {6 Names of structure elements } *) - -val mk_label : string -> label -val string_of_label : label -> string - -val label_of_id : identifier -> label -val id_of_label : label -> identifier - -module Labset : Set.S with type elt = label -module Labmap : Map.S with type key = label - (** {6 The module part of the kernel name } *) + type module_path = | MPfile of dir_path | MPbound of mod_bound_id @@ -91,13 +81,12 @@ val string_of_mp : module_path -> string module MPset : Set.S with type elt = module_path module MPmap : Map.S with type key = module_path -(** Name of the toplevel structure *) -val initial_msid : mod_self_id -val initial_path : module_path (** [= MPself initial_msid] *) - (** Initial "seed" of the unique identifier generator *) val initial_dir : dir_path +(** Name of the toplevel structure *) +val initial_path : module_path (** [= MPfile initial_dir] *) + (** {6 The absolute names of objects seen by kernel } *) type kernel_name diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 7f7bf5bf3..a80ceb0ff 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -117,38 +117,6 @@ let subtract l1 l2 = Names.make_dirpath (List.rev (aux l1')) ;; -(*CSC: Dead code to be removed -let token_list_of_kernel_name ~keep_sections kn tag = - let module N = Names in - let (modpath,dirpath,label) = Names.repr_kn kn in - let token_list_of_dirpath dirpath = - List.rev_map N.string_of_id (N.repr_dirpath dirpath) in - let rec token_list_of_modpath = - function - N.MPdot (path,label) -> - token_list_of_modpath path @ [N.string_of_label label] - | N.MPfile dirpath -> token_list_of_dirpath dirpath - | N.MPself self -> - if self = Names.initial_msid then - [ "Top" ] - else - let module_path = - let f = N.string_of_id (N.id_of_msid self) in - let _,longf = - System.find_file_in_path (Library.get_load_path ()) (f^".v") in - let ldir0 = Library.find_logical_path (Filename.dirname longf) in - let id = Names.id_of_string (Filename.basename f) in - Libnames.extend_dirpath ldir0 id - in - token_list_of_dirpath module_path - | N.MPbound _ -> raise FunctorsXMLExportationNotImplementedYet - in - token_list_of_modpath modpath @ - (if keep_sections then token_list_of_dirpath dirpath else []) @ - [N.string_of_label label ^ "." ^ (ext_of_tag tag)] -;; -*) - let token_list_of_path dir id tag = let module N = Names in let token_list_of_dirpath dirpath = |