Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 86 insertions, 80 deletions

diff --git a/library/nametab.mli b/library/nametab.mli
index 71ea0aa5..b168d59c 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: nametab.mli 10497 2008-02-01 12:18:37Z soubiran $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Util
@@ -16,34 +16,52 @@ open Libnames
 (*i*)
 
 (*s This module contains the tables for globalization, which
-  associates internal object references to qualified names (qualid). *)
+    associates internal object references to qualified names (qualid).
+
+    There are three classes of names:
+
+    1a- internal kernel names: [kernel_name], [constant], [inductive],
+        [module_path], [dir_path]
+
+    1b- other internal names: [global_reference], [syndef_name],
+        [extended_global_reference], [global_dir_reference], ...
+
+    2- full, non ambiguous user names: [full_path]
+
+    3- non necessarily full, possibly ambiguous user names: [reference]
+       and [qualid]
+*)
 
 (* Most functions in this module fall into one of the following categories:
    \begin{itemize}
    \item [push : visibility -> full_user_name -> object_reference -> unit]
-   
+
    Registers the [object_reference] to be referred to by the
    [full_user_name] (and its suffixes according to [visibility]).
-   [full_user_name] can either be a [section_path] or a [dir_path].
+   [full_user_name] can either be a [full_path] or a [dir_path].
+
+   \item [exists : full_user_name -> bool]
 
-   \item [exists : full_user_name -> bool] 
-   
    Is the [full_user_name] already atributed as an absolute user name
-   of some object? 
+   of some object?
 
    \item [locate : qualid -> object_reference]
 
    Finds the object referred to by [qualid] or raises [Not_found]
-   
-   \item [name_of : object_reference -> user_name]
 
-   The [user_name] can be for example the shortest non ambiguous [qualid] or 
-   the [full_user_name] or [identifier]. Such a function can also have a 
-   local context argument. 
+   \item [full_name : qualid -> full_user_name]
+
+   Finds the full user name referred to by [qualid] or raises [Not_found]
+
+   \item [shortest_qualid_of : object_reference -> user_name]
+
+   The [user_name] can be for example the shortest non ambiguous [qualid] or
+   the [full_user_name] or [identifier]. Such a function can also have a
+   local context argument.
    \end{itemize}
 *)
-   
-  
+
+
 exception GlobalizationError of qualid
 exception GlobalizationConstantError of qualid
 
@@ -52,9 +70,6 @@ val error_global_not_found_loc : loc -> qualid -> 'a
 val error_global_not_found     : qualid -> 'a
 val error_global_constant_not_found_loc : loc -> qualid -> 'a
 
-
-
-
 (*s Register visibility of things *)
 
 (* The visibility can be registered either
@@ -64,93 +79,84 @@ val error_global_constant_not_found_loc : loc -> qualid -> 'a
    object is loaded inside a module -- or
 
    \item for a precise suffix, when the module containing (the module
-   containing ...) the object is opened (imported) 
+   containing ...) the object is opened (imported)
    \end{itemize}
 *)
 
 type visibility = Until of int | Exactly of int
 
-val push : visibility -> section_path -> global_reference -> unit
-val push_syntactic_definition : 
-  visibility -> section_path -> kernel_name -> unit
-val push_modtype : visibility -> section_path -> module_path -> unit
+val push : visibility -> full_path -> global_reference -> unit
+val push_modtype : visibility -> full_path -> module_path -> unit
 val push_dir : visibility -> dir_path -> global_dir_reference -> unit
-val push_object : visibility -> section_path -> unit
-val push_tactic : visibility -> section_path -> kernel_name -> unit
-
-
-(*s The following functions perform globalization of qualified names *)
+val push_syndef : visibility -> full_path -> syndef_name -> unit
 
-(* This returns the section path of a constant or fails with [Not_found] *)
-val locate : qualid -> global_reference
-
-(* This function is used to transform a qualified identifier into a
-   global reference, with a nice error message in case of failure *)
-val global : reference -> global_reference
-
-(* The same for inductive types *)
-val inductive_of_reference : reference -> inductive
-
-(* This locates also syntactic definitions; raise [Not_found] if not found *)
-val extended_locate : qualid -> extended_global_reference
+type ltac_constant = kernel_name
+val push_tactic : visibility -> full_path -> ltac_constant -> unit
 
-(* This locates all names with a given suffix, if qualid is valid as
-   such, it comes first in the list *)
-val extended_locate_all : qualid -> extended_global_reference list
 
-(* This locates all global references with a given suffixe *)
-val locate_all : qualid -> global_reference list
+(*s The following functions perform globalization of qualified names *)
 
-val locate_obj : qualid -> section_path
+(* These functions globalize a (partially) qualified name or fail with
+   [Not_found] *)
 
+val locate : qualid -> global_reference
+val locate_extended : qualid -> extended_global_reference
 val locate_constant : qualid -> constant
-val locate_mind : qualid -> mutual_inductive
-val locate_section : qualid -> dir_path
+val locate_syndef : qualid -> syndef_name
 val locate_modtype : qualid -> module_path
-val locate_syntactic_definition : qualid -> kernel_name
-
-type ltac_constant = kernel_name
-val locate_tactic : qualid -> ltac_constant
 val locate_dir : qualid -> global_dir_reference
 val locate_module : qualid -> module_path
+val locate_section : qualid -> dir_path
+val locate_tactic : qualid -> ltac_constant
 
-(* A variant looking up a [section_path] *)
-val absolute_reference : section_path -> global_reference
+(* These functions globalize user-level references into global
+   references, like [locate] and co, but raise a nice error message
+   in case of failure *)
 
+val global : reference -> global_reference
+val global_inductive : reference -> inductive
 
-(*s These function tell if the given absolute name is already taken *)
+(* These functions locate all global references with a given suffix;
+   if [qualid] is valid as such, it comes first in the list *)
 
-val exists_cci : section_path -> bool
-val exists_modtype : section_path -> bool
+val locate_all : qualid -> global_reference list
+val locate_extended_all : qualid -> extended_global_reference list
 
-(* Those three functions are the same *)
-val exists_dir : dir_path -> bool
-val exists_section : dir_path -> bool (* deprecated *)
-val exists_module : dir_path -> bool (* deprecated *)
+(* Mapping a full path to a global reference *)
 
+val global_of_path : full_path -> global_reference
+val extended_global_of_path : full_path -> extended_global_reference
 
-(*s These functions turn qualids into full user names: [section_path]s
-  or [dir_path]s *)
+(*s These functions tell if the given absolute name is already taken *)
 
-val full_name_modtype : qualid -> section_path
-val full_name_cci : qualid -> section_path
+val exists_cci : full_path -> bool
+val exists_modtype : full_path -> bool
+val exists_dir : dir_path -> bool
+val exists_section : dir_path -> bool (* deprecated synonym of [exists_dir] *)
+val exists_module : dir_path -> bool (* deprecated synonym of [exists_dir] *)
 
-(* As above but checks that the path found is indeed a module *)
-val full_name_module : qualid -> dir_path
+(*s These functions locate qualids into full user names *)
 
+val full_name_cci : qualid -> full_path
+val full_name_modtype : qualid -> full_path
+val full_name_module : qualid -> dir_path
 
 (*s Reverse lookup -- finding user names corresponding to the given
   internal name *)
 
-val sp_of_syntactic_definition : kernel_name -> section_path
-val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
-val shortest_qualid_of_syndef : Idset.t -> kernel_name -> qualid
-val shortest_qualid_of_tactic : ltac_constant -> qualid
+(* Returns the full path bound to a global reference or syntactic
+   definition, and the (full) dirpath associated to a module path *)
+
+val path_of_syndef : syndef_name -> full_path
+val path_of_global : global_reference -> full_path
+val dirpath_of_module : module_path -> dir_path
+val path_of_tactic : ltac_constant -> full_path
 
-val dir_of_mp : module_path -> dir_path
+(* Returns in particular the dirpath or the basename of the full path
+   associated to global reference *)
 
-val sp_of_global : global_reference -> section_path
-val id_of_global : global_reference -> identifier
+val dirpath_of_global : global_reference -> dir_path
+val basename_of_global : global_reference -> identifier
 
 (* Printing of global references using names as short as possible *)
 val pr_global_env : Idset.t -> global_reference -> std_ppcmds
@@ -160,13 +166,13 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds
    Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and
    Coq.A.B.x that denotes the same object. *)
 
-val shortest_qualid_of_module : module_path -> qualid
+val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
+val shortest_qualid_of_syndef : Idset.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : module_path -> qualid
+val shortest_qualid_of_module : module_path -> qualid
+val shortest_qualid_of_tactic : ltac_constant -> qualid
 
+(* Deprecated synonyms *)
 
-(*
-type frozen
-
-val freeze : unit -> frozen
-val unfreeze : frozen -> unit
-*)
+val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
+val absolute_reference : full_path -> global_reference (* = global_of_path *)