diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 47 |
1 files changed, 23 insertions, 24 deletions
diff --git a/library/lib.mli b/library/lib.mli index dacfed59..13c9baf6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli 12187 2009-06-13 19:36:59Z msozeau $ i*) +(*i $Id$ i*) (*s 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 node = +type node = | Leaf of Libobject.obj | CompilingLibrary of Libnames.object_prefix | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen @@ -32,15 +32,15 @@ type lib_objects = (Names.identifier * Libobject.obj) list val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit -val subst_objects : Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects -val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects +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, 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 returned list is the same as in the input list. *) -val classify_segment : +val classify_segment : library_segment -> lib_objects * lib_objects * Libobject.obj list (* [segment_of_objects prefix objs] forms a list of Leafs *) @@ -52,7 +52,6 @@ val segment_of_objects : current list of operations (most recent ones coming first). *) val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name -val add_absolutely_named_leaf : Libnames.object_name -> Libobject.obj -> unit val add_anonymous_leaf : Libobject.obj -> unit (* this operation adds all objects with the same name and calls [load_object] @@ -70,7 +69,7 @@ val current_command_label : unit -> int registered after it. *) val reset_label : int -> unit -(*s The function [contents_after] returns the current library segment, +(*s The function [contents_after] returns the current library segment, starting from a given section path. If not given, the entire segment is returned. *) @@ -80,9 +79,11 @@ val contents_after : Libnames.object_name option -> library_segment (* User-side names *) val cwd : unit -> Names.dir_path -val current_dirpath : bool -> Names.dir_path -val make_path : Names.identifier -> Libnames.section_path -val path_of_include : unit -> Libnames.section_path +val cwd_except_section : unit -> Names.dir_path +val current_dirpath : bool -> Names.dir_path (* false = except sections *) +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 *) val current_prefix : unit -> Names.module_path * Names.dir_path @@ -98,20 +99,19 @@ val is_modtype : unit -> bool val is_module : unit -> bool val current_mod_id : unit -> Names.module_ident -(* Returns the most recent OpenedThing node *) -val what_is_opened : unit -> Libnames.object_name * node - +(* Returns the opening node of a given name *) +val find_opening_node : Names.identifier -> node (*s Modules and module types *) -val start_module : +val start_module : bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix -val end_module : Names.module_ident +val end_module : unit -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment -val start_modtype : +val start_modtype : Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix -val end_modtype : Names.module_ident +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 *) @@ -134,7 +134,7 @@ val remove_section_part : Libnames.global_reference -> Names.dir_path (*s Sections *) val open_section : Names.identifier -> unit -val close_section : Names.identifier -> unit +val close_section : unit -> unit (*s Backtracking (undo). *) @@ -146,7 +146,7 @@ val reset_to_state : Libnames.object_name -> unit val has_top_frozen_state : unit -> Libnames.object_name option -(* [back n] resets to the place corresponding to the $n$-th call of +(* [back n] resets to the place corresponding to the $n$-th call of [mark_end_of_command] (counting backwards) *) val back : int -> unit @@ -182,17 +182,16 @@ val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_cont val section_instance : Libnames.global_reference -> Names.identifier array val is_in_section : Libnames.global_reference -> bool -val add_section_variable : Names.identifier -> binding_kind -> - (Term.types * Names.identifier list) option -> unit +val add_section_variable : Names.identifier -> binding_kind -> unit val add_section_constant : Names.constant -> Sign.named_context -> unit -val add_section_kn : Names.kernel_name -> Sign.named_context -> unit +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.KNmap.t) + (Names.identifier array Names.Cmap.t * Names.identifier array Names.Mindmap.t) (*s Discharge: decrease the section level if in the current section *) -val discharge_kn : Names.kernel_name -> Names.kernel_name +val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant val discharge_global : Libnames.global_reference -> Libnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive |