From 12965209478bd99dfbe57f07d5b525e51b903f22 Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 2 Aug 2002 17:17:42 +0000 Subject: Modules dans COQ\!\!\!\! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/nametab.mli | 111 ++++++++++++++++++++++++++++++---------------------- 1 file changed, 64 insertions(+), 47 deletions(-) (limited to 'library/nametab.mli') 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 + -- cgit v1.2.3