From 146fb70f0729285fb4bb59613c73da0bad92d6c6 Mon Sep 17 00:00:00 2001 From: coq Date: Tue, 24 Sep 2002 15:09:43 +0000 Subject: Un peu (plus) d'ordre dans Nametab... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3031 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/nametab.mli | 88 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 55 insertions(+), 33 deletions(-) (limited to 'library/nametab.mli') diff --git a/library/nametab.mli b/library/nametab.mli index 11b6be271..2790e1536 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -23,7 +23,8 @@ open Libnames \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] (and its suffixes according to [visibility]). + [full_user_name] can either be a [section_path] or a [dir_path]. \item [exists : full_user_name -> bool] @@ -42,23 +43,6 @@ open Libnames *) - -(* 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 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 : Sign.named_context option -> global_reference -> std_ppcmds - -val shortest_qualid_of_module : module_path -> qualid -val shortest_qualid_of_modtype : kernel_name -> qualid - exception GlobalizationError of qualid exception GlobalizationConstantError of qualid @@ -67,12 +51,21 @@ 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 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) *) +(* The visibility can be registered either + \begin{itemize} + + \item for all suffixes not shorter then a given int -- when the + object is loaded inside a module -- or + + \item for a precise suffix, when the module containing (the module + containing ...) the object is opened (imported) + \end{itemize} +*) type visibility = Until of int | Exactly of int @@ -84,6 +77,7 @@ 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] *) @@ -111,7 +105,12 @@ 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 *) +(* A variant looking up a [section_path] *) +val absolute_reference : section_path -> global_reference + + +(*s These function tell if the given absolute name is already taken *) + val exists_cci : section_path -> bool val exists_modtype : section_path -> bool @@ -120,23 +119,46 @@ val exists_dir : dir_path -> bool val exists_section : dir_path -> bool (* deprecated *) val exists_module : dir_path -> bool (* deprecated *) + +(*s These functions turn qualids into full user names: [section_path]s + or [dir_path]s *) + val full_name_modtype : qualid -> section_path +val full_name_cci : qualid -> section_path -(*s Roots of the space of absolute names *) +(* As above but checks that the path found is indeed a module *) +val locate_loaded_library : qualid -> dir_path -(* This turns a "user" absolute name into a global reference; - especially, constructor/inductive names are turned into internal - references inside a block of mutual inductive *) -val absolute_reference : section_path -> global_reference -(* [locate_in_absolute_module dir id] finds [id] in module [dir] or in - one of its section/subsection *) -val locate_in_absolute_module : dir_path -> identifier -> global_reference +(*s Reverse lookup -- finding user names corresponding to the given + internal name *) -val locate_loaded_library : qualid -> dir_path +val sp_of_syntactic_definition : kernel_name -> section_path + +val sp_of_global : + Sign.named_context option -> 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 : Sign.named_context option -> global_reference -> std_ppcmds + + +(* The [shortest_qualid] functions given an object with user_name + 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_modtype : kernel_name -> qualid + + + +(* type frozen val freeze : unit -> frozen val unfreeze : frozen -> unit - +*) -- cgit v1.2.3