diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 118 |
1 files changed, 57 insertions, 61 deletions
diff --git a/library/lib.mli b/library/lib.mli index d35fcc09..23af7c17 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -6,41 +6,34 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: lib.mli 11671 2008-12-12 12:43:03Z herbelin $ i*) -(*i*) -open Util -open Names -open Libnames -open Libobject -open Summary -open Mod_subst -(*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 = - | Leaf of obj - | CompilingLibrary of object_prefix - | OpenedModule of bool option * object_prefix * Summary.frozen + | Leaf of Libobject.obj + | CompilingLibrary of Libnames.object_prefix + | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen | ClosedModule of library_segment - | OpenedModtype of object_prefix * Summary.frozen + | OpenedModtype of Libnames.object_prefix * Summary.frozen | ClosedModtype of library_segment - | OpenedSection of object_prefix * Summary.frozen + | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment | FrozenState of Summary.frozen -and library_segment = (object_name * node) list +and library_segment = (Libnames.object_name * node) list -type lib_objects = (identifier * obj) list +type lib_objects = (Names.identifier * Libobject.obj) list (*s Object iteratation functions. *) -val open_objects : int -> object_prefix -> lib_objects -> unit -val load_objects : int -> object_prefix -> lib_objects -> unit -val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects +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 (* [classify_segment seg] verifies that there are no OpenedThings, clears ClosedSections and FrozenStates and divides Leafs according @@ -48,23 +41,23 @@ val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects [Substitute], [Keep], [Anticipate] respectively. The order of each returned list is the same as in the input list. *) val classify_segment : - library_segment -> lib_objects * lib_objects * obj list + library_segment -> lib_objects * lib_objects * Libobject.obj list (* [segment_of_objects prefix objs] forms a list of Leafs *) val segment_of_objects : - object_prefix -> lib_objects -> library_segment + Libnames.object_prefix -> lib_objects -> library_segment (*s Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) -val add_leaf : identifier -> obj -> object_name -val add_absolutely_named_leaf : object_name -> obj -> unit -val add_anonymous_leaf : obj -> unit +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] for each of them *) -val add_leaves : identifier -> obj list -> object_name +val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name val add_frozen_state : unit -> unit @@ -81,19 +74,20 @@ val reset_label : int -> unit starting from a given section path. If not given, the entire segment is returned. *) -val contents_after : object_name option -> library_segment +val contents_after : Libnames.object_name option -> library_segment (*s Functions relative to current path *) (* User-side names *) -val cwd : unit -> dir_path -val make_path : identifier -> section_path -val path_of_include : unit -> section_path +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 (* Kernel-side names *) -val current_prefix : unit -> module_path * dir_path -val make_kn : identifier -> kernel_name -val make_con : identifier -> constant +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 *) val sections_are_opened : unit -> bool @@ -102,53 +96,55 @@ val sections_depth : unit -> int (* Are we inside an opened module type *) val is_modtype : unit -> bool val is_module : unit -> bool -val current_mod_id : unit -> module_ident +val current_mod_id : unit -> Names.module_ident (* Returns the most recent OpenedThing node *) -val what_is_opened : unit -> object_name * node +val what_is_opened : unit -> Libnames.object_name * node (*s Modules and module types *) val start_module : - bool option -> module_ident -> module_path -> Summary.frozen -> object_prefix -val end_module : module_ident - -> object_name * object_prefix * Summary.frozen * library_segment + bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix +val end_module : Names.module_ident + -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment val start_modtype : - module_ident -> module_path -> Summary.frozen -> object_prefix -val end_modtype : module_ident - -> object_name * object_prefix * Summary.frozen * library_segment + Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix +val end_modtype : Names.module_ident + -> 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 *) -val start_compilation : dir_path -> module_path -> unit -val end_compilation : dir_path -> object_prefix * library_segment +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 compiling library (or [default_library]) *) -val library_dp : unit -> dir_path +val library_dp : unit -> Names.dir_path (* Extract the library part of a name even if in a section *) -val dp_of_mp : module_path -> dir_path -val library_part : global_reference -> dir_path -val remove_section_part : global_reference -> dir_path +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 *) -val open_section : identifier -> unit -val close_section : identifier -> unit +val open_section : Names.identifier -> unit +val close_section : Names.identifier -> unit (*s Backtracking (undo). *) -val reset_to : object_name -> unit -val reset_name : identifier located -> unit -val remove_name : identifier located -> unit -val reset_mod : identifier located -> unit -val reset_to_state : object_name -> unit +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 -val has_top_frozen_state : unit -> object_name option +val has_top_frozen_state : unit -> Libnames.object_name option (* [back n] resets to the place corresponding to the $n$-th call of [mark_end_of_command] (counting backwards) *) @@ -168,8 +164,8 @@ val reset_initial : unit -> unit (* XML output hooks *) -val set_xml_open_section : (identifier -> unit) -> unit -val set_xml_close_section : (identifier -> unit) -> unit +val set_xml_open_section : (Names.identifier -> unit) -> unit +val set_xml_close_section : (Names.identifier -> unit) -> unit type binding_kind = Explicit | Implicit @@ -190,13 +186,13 @@ val add_section_variable : Names.identifier -> binding_kind -> Term.types option val add_section_constant : Names.constant -> Sign.named_context -> unit val add_section_kn : Names.kernel_name -> Sign.named_context -> unit val replacement_context : unit -> - (identifier array Cmap.t * identifier array KNmap.t) + (Names.identifier array Names.Cmap.t * Names.identifier array Names.KNmap.t) (*s Discharge: decrease the section level if in the current section *) -val discharge_kn : kernel_name -> kernel_name -val discharge_con : constant -> constant -val discharge_global : global_reference -> global_reference -val discharge_inductive : inductive -> inductive +val discharge_kn : Names.kernel_name -> Names.kernel_name +val discharge_con : Names.constant -> Names.constant +val discharge_global : Libnames.global_reference -> Libnames.global_reference +val discharge_inductive : Names.inductive -> Names.inductive |