diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-08-10 14:42:22 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-08-10 14:42:22 +0000 |
commit | 8e92ee787e7d1fd48cae1eccf67a9b05e739743e (patch) | |
tree | b33191fbaba0cad4b14a96cf5d7786dd2c07c3d7 /library/nametab.mli | |
parent | c0a3b41ad2f2afba3f060e0d4001bd7aceea0831 (diff) |
Parsing
- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
lieu de string)
Table des noms qualifiés
- Remplacement de la table de visibilité par une table qui ne cache
plus les noms de modules et sections mais seulement les noms des
constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
module A déjà existant : seuls les noms de constructions de l'ancien
A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
constantes définies à l'intérieur de sections et simplification
connexes (suppression de END-SECTION, une seule table de noms qui ne
survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
Require and co, tests de cohérence; pour être cohérent avec la non
survie des tables de noms à la sortie des section, les require à
l'intérieur d'une section eux aussi sont refaits à la fermeture de la
section
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.mli')
-rwxr-xr-x | library/nametab.mli | 52 |
1 files changed, 32 insertions, 20 deletions
diff --git a/library/nametab.mli b/library/nametab.mli index 8506c7a5b..927205dea 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -18,6 +18,10 @@ open Term (*s This module contains the table for globalization, which associates global names (section paths) to qualified names. *) +type extended_global_reference = + | TrueGlobal of global_reference + | SyntacticDef of section_path + (*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 *) @@ -38,19 +42,17 @@ exception GlobalizationError of qualid val error_global_not_found_loc : loc -> qualid -> 'a val error_global_not_found : qualid -> 'a -(*s Names tables *) -type cci_table = global_reference Idmap.t -type obj_table = (section_path * Libobject.obj) Idmap.t -type mod_table = (section_path * module_contents) Stringmap.t -and module_contents = Closed of cci_table * obj_table * mod_table - -(*s Registers absolute paths *) +(*s Register visibility of absolute paths by qualified names *) val push : section_path -> global_reference -> unit -val push_object : section_path -> Libobject.obj -> unit -val push_module : section_path -> module_contents -> unit +val push_syntactic_definition : section_path -> unit + +(*s Register visibility of absolute paths by short names *) +val push_short_name : identifier -> global_reference -> unit +val push_short_name_syntactic_definition : section_path -> unit +val push_short_name_object : section_path -> unit -val push_local : section_path -> global_reference -> unit -val push_local_object : section_path -> Libobject.obj -> unit +(*s Register visibility by all qualifications *) +val push_section : dir_path -> unit (* This should eventually disappear *) val sp_of_id : path_kind -> identifier -> global_reference @@ -61,37 +63,47 @@ val sp_of_id : path_kind -> identifier -> global_reference val constant_sp_of_id : identifier -> section_path val locate : qualid -> global_reference -val locate_obj : qualid -> (section_path * Libobject.obj) + +(* This locates also syntactic definitions *) +val extended_locate : qualid -> extended_global_reference + +val locate_obj : qualid -> section_path + val locate_constant : qualid -> constant_path -val locate_module : qualid -> section_path * module_contents +val locate_section : qualid -> dir_path (* [exists sp] tells if [sp] is already bound to a cci term *) val exists_cci : section_path -> bool -val exists_module : section_path -> bool - +val exists_section : dir_path -> bool +(* val open_module_contents : qualid -> unit val rec_open_module_contents : qualid -> unit (*s Entry points for sections *) val open_section_contents : qualid -> unit val push_section : section_path -> module_contents -> unit - +*) (*s Roots of the space of absolute names *) (* This is the root of the standard library of Coq *) -val coq_root : string +val coq_root : module_ident -(* This is the default root for developments which doesn't mention a root *) -val default_root : string +(* This is the default root prefix for developments which doesn't mention a root *) +val default_root_prefix : dir_path (* This is to declare a new root *) -val push_library_root : string -> unit +val push_library_root : module_ident -> unit (* 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 +val is_absolute_dirpath : dir_path -> bool + (* [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 + +val push_loaded_library : dir_path -> unit +val locate_loaded_library : qualid -> dir_path |