diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 123 |
1 files changed, 66 insertions, 57 deletions
diff --git a/library/lib.mli b/library/lib.mli index 7eb8b688..42892bdf 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,25 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) +(** Lib: record of operations, backtrack, low-level sections *) -(*s This module provides a general mechanism to keep a trace of all operations +(** This module provides a general mechanism to keep a trace of all operations and to backtrack (undo) those operations. It provides also the section mechanism (at a low level; discharge is not known at this step). *) +type is_type = bool (* Module Type or just Module *) +type export = bool option (* None for a Module Type *) + type node = | Leaf of Libobject.obj | CompilingLibrary of Libnames.object_prefix - | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen + | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen | ClosedModule of library_segment - | OpenedModtype of Libnames.object_prefix * Summary.frozen - | ClosedModtype of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment | FrozenState of Summary.frozen @@ -28,14 +29,14 @@ and library_segment = (Libnames.object_name * node) list type lib_objects = (Names.identifier * Libobject.obj) list -(*s Object iteratation functions. *) +(** {6 Object iteration functions. } *) val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects (*val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*) -(* [classify_segment seg] verifies that there are no OpenedThings, +(** [classify_segment seg] verifies that there are no OpenedThings, clears ClosedSections and FrozenStates and divides Leafs according to their answers to the [classify_object] function in three groups: [Substitute], [Keep], [Anticipate] respectively. The order of each @@ -43,41 +44,34 @@ val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects val classify_segment : library_segment -> lib_objects * lib_objects * Libobject.obj list -(* [segment_of_objects prefix objs] forms a list of Leafs *) +(** [segment_of_objects prefix objs] forms a list of Leafs *) val segment_of_objects : Libnames.object_prefix -> lib_objects -> library_segment -(*s Adding operations (which call the [cache] method, and getting the +(** {6 ... } *) +(** Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : Libobject.obj -> unit -(* this operation adds all objects with the same name and calls [load_object] +(** this operation adds all objects with the same name and calls [load_object] for each of them *) val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name val add_frozen_state : unit -> unit -(* Adds a "dummy" entry in lib_stk with a unique new label number. *) -val mark_end_of_command : unit -> unit -(* Returns the current label number *) -val current_command_label : unit -> int -(* [reset_label n ] resets [lib_stk] to the label n registered by - [mark_end_of_command()]. That is it forgets the label and anything - registered after it. *) -val reset_label : int -> unit - -(*s The function [contents_after] returns the current library segment, +(** {6 ... } *) +(** The function [contents_after] returns the current library segment, starting from a given section path. If not given, the entire segment is returned. *) val contents_after : Libnames.object_name option -> library_segment -(*s Functions relative to current path *) +(** {6 Functions relative to current path } *) -(* User-side names *) +(** User-side names *) val cwd : unit -> Names.dir_path val cwd_except_section : unit -> Names.dir_path val current_dirpath : bool -> Names.dir_path (* false = except sections *) @@ -85,72 +79,91 @@ val make_path : Names.identifier -> Libnames.full_path val make_path_except_section : Names.identifier -> Libnames.full_path val path_of_include : unit -> Libnames.full_path -(* Kernel-side names *) +(** Kernel-side names *) val current_prefix : unit -> Names.module_path * Names.dir_path val make_kn : Names.identifier -> Names.kernel_name val make_con : Names.identifier -> Names.constant -(* Are we inside an opened section *) +(** Are we inside an opened section *) val sections_are_opened : unit -> bool val sections_depth : unit -> int -(* Are we inside an opened module type *) +(** Are we inside an opened module type *) +val is_module_or_modtype : unit -> bool val is_modtype : unit -> bool val is_module : unit -> bool val current_mod_id : unit -> Names.module_ident -(* Returns the opening node of a given name *) +(** Returns the opening node of a given name *) val find_opening_node : Names.identifier -> node -(*s Modules and module types *) +(** {6 Modules and module types } *) val start_module : - bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix -val end_module : unit - -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment + export -> Names.module_ident -> Names.module_path -> + Summary.frozen -> Libnames.object_prefix val start_modtype : - Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix -val end_modtype : unit - -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment -(* [Lib.add_frozen_state] must be called after each of the above functions *) + Names.module_ident -> Names.module_path -> + Summary.frozen -> Libnames.object_prefix + +val end_module : + unit -> + Libnames.object_name * Libnames.object_prefix * + Summary.frozen * library_segment + +val end_modtype : + unit -> + Libnames.object_name * Libnames.object_prefix * + Summary.frozen * library_segment + +(** [Lib.add_frozen_state] must be called after each of the above functions *) -(*s Compilation units *) +(** {6 Compilation units } *) val start_compilation : Names.dir_path -> Names.module_path -> unit val end_compilation : Names.dir_path -> Libnames.object_prefix * library_segment -(* The function [library_dp] returns the [dir_path] of the current +(** The function [library_dp] returns the [dir_path] of the current compiling library (or [default_library]) *) val library_dp : unit -> Names.dir_path -(* Extract the library part of a name even if in a section *) +(** Extract the library part of a name even if in a section *) val dp_of_mp : Names.module_path -> Names.dir_path val split_mp : Names.module_path -> Names.dir_path * Names.dir_path val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list val library_part : Libnames.global_reference -> Names.dir_path val remove_section_part : Libnames.global_reference -> Names.dir_path -(*s Sections *) +(** {6 Sections } *) val open_section : Names.identifier -> unit val close_section : unit -> unit -(*s Backtracking (undo). *) +(** {6 Backtracking } *) -val reset_to : Libnames.object_name -> unit -val reset_name : Names.identifier Util.located -> unit -val remove_name : Names.identifier Util.located -> unit -val reset_mod : Names.identifier Util.located -> unit -val reset_to_state : Libnames.object_name -> unit +(** NB: The next commands are low-level ones, do not use them directly + otherwise the command history stack in [Backtrack] will be out-of-sync. + Also note that [reset_initial] is now [reset_label first_command_label] *) -val has_top_frozen_state : unit -> Libnames.object_name option +(** Adds a "dummy" entry in lib_stk with a unique new label number. *) +val mark_end_of_command : unit -> unit + +(** Returns the current label number *) +val current_command_label : unit -> int + +(** The first label number *) +val first_command_label : int -(* [back n] resets to the place corresponding to the $n$-th call of - [mark_end_of_command] (counting backwards) *) -val back : int -> unit +(** [reset_label n] resets [lib_stk] to the label n registered by + [mark_end_of_command()]. It forgets anything registered after + this label. The label should be strictly in the past. *) +val reset_label : int -> unit + +(** search the label registered immediately before adding some definition *) +val label_before_name : Names.identifier Util.located -> int -(*s We can get and set the state of the operations (used in [States]). *) +(** {6 We can get and set the state of the operations (used in [States]). } *) type frozen @@ -159,17 +172,13 @@ val unfreeze : frozen -> unit val init : unit -> unit -val declare_initial_state : unit -> unit -val reset_initial : unit -> unit - - -(* XML output hooks *) +(** XML output hooks *) val set_xml_open_section : (Names.identifier -> unit) -> unit val set_xml_close_section : (Names.identifier -> unit) -> unit type binding_kind = Explicit | Implicit -(*s Section management for discharge *) +(** {6 Section management for discharge } *) type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types type variable_context = variable_info list @@ -189,7 +198,7 @@ val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit val replacement_context : unit -> (Names.identifier array Names.Cmap.t * Names.identifier array Names.Mindmap.t) -(*s Discharge: decrease the section level if in the current section *) +(** {6 Discharge: decrease the section level if in the current section } *) val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant |