Modules dans COQ\!\!\!\!

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

1 files changed, 64 insertions, 47 deletions

diff --git a/library/nametab.mli b/library/nametab.mli
index d71e3e379..b64fe0d9d 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -12,44 +12,49 @@
 open Util
 open Pp
 open Names
+open Libnames
 (*i*)
 
-(*s This module contains the table for globalization, which associates global
-   names (section paths) to qualified names. *)
+(*s This module contains the tables for globalization, which
+  associates internal object references to qualified names (qualid). *)
 
-type global_reference =
-  | VarRef of variable
-  | ConstRef of constant
-  | IndRef of inductive
-  | ConstructRef of constructor
+(* 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])
 
-(* Finds the real name of a global (e.g. fetch the constructor names
-   from the inductive name and constructor number) *)
-val sp_of_global : Environ.env -> global_reference -> section_path
-
-type extended_global_reference =
-  | TrueGlobal of global_reference
-  | SyntacticDef of section_path
+   \item [exists : full_user_name -> bool] 
+   
+   Is the [full_user_name] already atributed as an absolute user name
+   of some object? 
 
-(*s A [qualid] is a partially qualified ident; it includes fully
-    qualified names (= absolute names) and all intermediate partial
-    qualifications of absolute names, including single identifiers *)
-type qualid
+   \item [locate : qualid -> object_reference]
 
-val make_qualid : dir_path -> identifier -> qualid
-val repr_qualid : qualid -> dir_path * identifier
-val make_short_qualid : identifier -> qualid
+   Finds the object referred to by [qualid] or raises Not_found 
+   
+   \item [name_of] : object_reference -> user_name
 
-val string_of_qualid : qualid -> string
-val pr_qualid : qualid -> std_ppcmds
+   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. 
+*)
+   
+  
 
-val qualid_of_sp : section_path -> qualid
+(* Finds the real name of a global (e.g. fetch the constructor names
+   from the inductive name and constructor number) *)
+val sp_of_global : Sign.named_context option -> global_reference -> section_path
+val sp_of_syntactic_definition : kernel_name -> section_path
 
 (* Turns an absolute name into a qualified name denoting the same name *)
-val shortest_qualid_of_global : Environ.env -> global_reference -> qualid
+val full_name : global_reference -> section_path
+val shortest_qualid_of_global : Sign.named_context option -> global_reference -> qualid
+val id_of_global : Sign.named_context option -> global_reference -> identifier
 
 (* Printing of global references using names as short as possible *)
-val pr_global_env : Environ.env -> global_reference -> std_ppcmds
+val pr_global_env : Sign.named_context option -> global_reference -> std_ppcmds
 
 exception GlobalizationError of qualid
 exception GlobalizationConstantError of qualid
@@ -59,29 +64,29 @@ 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 absolute paths by qualified names *)
-val push : visibility:int -> section_path -> global_reference -> unit
-val push_syntactic_definition : section_path -> unit
+(*s Register visibility of things *)
 
-(*s Register visibility of absolute paths by short names *)
-val push_short_name_syntactic_definition : section_path -> unit
-val push_short_name_object : section_path -> unit
+(* The visibility can be registered either for all suffixes not
+   shorter then a given int - when the object is loaded inside a module,
+   or for a precise suffix, when the module containing (the module
+   containing ...) the object is open (imported) *)
 
-(*s Register visibility of absolute paths by short names *)
-val push_tactic_path : section_path -> unit
-val locate_tactic : qualid -> section_path
+type visibility = Until of int | Exactly of int
 
-(*s Register visibility by all qualifications *)
-val push_section : dir_path -> unit
+(* is the short name visible? tests for 1 *)
+val is_short_visible : visibility -> section_path -> bool
 
-(* This should eventually disappear *)
-val sp_of_id : identifier -> global_reference
+val push : visibility -> section_path -> global_reference -> unit
+val push_syntactic_definition : 
+  visibility -> section_path -> kernel_name -> unit
+val push_modtype : visibility -> section_path -> kernel_name -> unit
+val push_dir : visibility -> dir_path -> global_dir_reference -> unit
+val push_object : visibility -> section_path -> unit
+val push_tactic : visibility -> section_path -> unit
 
 (*s The following functions perform globalization of qualified names *)
 
 (* This returns the section path of a constant or fails with [Not_found] *)
-val constant_sp_of_id : identifier -> section_path
-
 val locate : qualid -> global_reference
 
 (* This function is used to transform a qualified identifier into a
@@ -97,11 +102,23 @@ val extended_locate : qualid -> extended_global_reference
 val locate_obj : qualid -> section_path
 
 val locate_constant : qualid -> constant
+val locate_mind : qualid -> mutual_inductive
 val locate_section : qualid -> dir_path
+val locate_modtype : qualid -> kernel_name
+val locate_syntactic_definition : qualid -> kernel_name
+
+val locate_tactic : qualid -> section_path
+val locate_dir : qualid -> global_dir_reference
+val locate_module : qualid -> module_path
 
 (* [exists sp] tells if [sp] is already bound to a cci term *)
 val exists_cci : section_path -> bool
-val exists_section : dir_path -> bool
+val exists_modtype : section_path -> bool
+
+(* 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 *)
 
 (*s Roots of the space of absolute names *)
 
@@ -114,10 +131,10 @@ val absolute_reference : section_path -> global_reference
    one of its section/subsection *)
 val locate_in_absolute_module : dir_path -> identifier -> global_reference
 
-val push_loaded_library : dir_path -> unit
 val locate_loaded_library : qualid -> dir_path
 
-type strength = 
-  | NotDeclare
-  | DischargeAt of dir_path * int
-  | NeverDischarge
+type frozen
+
+val freeze : unit -> frozen
+val unfreeze : frozen -> unit
+