diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 127 |
1 files changed, 56 insertions, 71 deletions
diff --git a/library/lib.mli b/library/lib.mli index d546d1ff..9c4d26c5 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -27,7 +27,7 @@ type node = and library_segment = (Libnames.object_name * node) list -type lib_objects = (Names.identifier * Libobject.obj) list +type lib_objects = (Names.Id.t * Libobject.obj) list (** {6 Object iteration functions. } *) @@ -53,36 +53,38 @@ val segment_of_objects : (** 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_leaf : Names.Id.t -> 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] for each of them *) -val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name +val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name val add_frozen_state : unit -> unit (** {6 ... } *) + +(** The function [contents] gives access to the current entire segment *) + +val contents : unit -> library_segment + (** The function [contents_after] returns the current library segment, - starting from a given section path. If not given, the entire segment - is returned. *) + starting from a given section path. *) -val contents_after : Libnames.object_name option -> library_segment +val contents_after : Libnames.object_name -> library_segment (** {6 Functions relative to current path } *) (** 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 *) -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 +val cwd : unit -> Names.DirPath.t +val cwd_except_section : unit -> Names.DirPath.t +val current_dirpath : bool -> Names.DirPath.t (* false = except sections *) +val make_path : Names.Id.t -> Libnames.full_path +val make_path_except_section : Names.Id.t -> Libnames.full_path (** 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 +val current_mp : unit -> Names.module_path +val make_kn : Names.Id.t -> Names.kernel_name (** Are we inside an opened section *) val sections_are_opened : unit -> bool @@ -91,11 +93,14 @@ val sections_depth : unit -> int (** Are we inside an opened module type *) val is_module_or_modtype : unit -> bool val is_modtype : unit -> bool +(* [is_modtype_strict] checks not only if we are in a module type, but + if the latest module started is a module type. *) +val is_modtype_strict : unit -> bool val is_module : unit -> bool val current_mod_id : unit -> Names.module_ident (** Returns the opening node of a given name *) -val find_opening_node : Names.identifier -> node +val find_opening_node : Names.Id.t -> node (** {6 Modules and module types } *) @@ -121,88 +126,68 @@ val end_modtype : (** {6 Compilation units } *) -val start_compilation : Names.dir_path -> Names.module_path -> unit -val end_compilation : Names.dir_path -> Libnames.object_prefix * library_segment +val start_compilation : Names.DirPath.t -> Names.module_path -> unit +val end_compilation_checks : Names.DirPath.t -> Libnames.object_name +val end_compilation : + Libnames.object_name-> Libnames.object_prefix * library_segment -(** The function [library_dp] returns the [dir_path] of the current +(** The function [library_dp] returns the [DirPath.t] of the current compiling library (or [default_library]) *) -val library_dp : unit -> Names.dir_path +val library_dp : unit -> Names.DirPath.t (** 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 +val dp_of_mp : Names.module_path -> Names.DirPath.t +val split_mp : Names.module_path -> Names.DirPath.t * Names.DirPath.t +val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list +val library_part : Globnames.global_reference -> Names.DirPath.t +val remove_section_part : Globnames.global_reference -> Names.DirPath.t (** {6 Sections } *) -val open_section : Names.identifier -> unit +val open_section : Names.Id.t -> unit val close_section : unit -> unit -(** {6 Backtracking } *) - -(** 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] *) - -(** 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 - -(** [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 - (** {6 We can get and set the state of the operations (used in [States]). } *) type frozen -val freeze : unit -> frozen +val freeze : marshallable:Summary.marshallable -> frozen val unfreeze : frozen -> unit val init : unit -> unit -(** 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 - (** {6 Section management for discharge } *) -type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types -type variable_context = variable_info list +type variable_info = Names.Id.t * Decl_kinds.binding_kind * + Term.constr option * Term.types +type variable_context = variable_info list +type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t -val instance_from_variable_context : variable_context -> Names.identifier array -val named_of_variable_context : variable_context -> Sign.named_context +val instance_from_variable_context : variable_context -> Names.Id.t array +val named_of_variable_context : variable_context -> Context.named_context -val section_segment_of_constant : Names.constant -> variable_context -val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context +val section_segment_of_constant : Names.constant -> abstr_info +val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info -val section_instance : Libnames.global_reference -> Names.identifier array -val is_in_section : Libnames.global_reference -> bool +val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array +val is_in_section : Globnames.global_reference -> bool -val add_section_variable : Names.identifier -> binding_kind -> unit +val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit -val add_section_constant : Names.constant -> 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.Mindmap.t) +val add_section_constant : bool (* is_projection *) -> + Names.constant -> Context.named_context -> unit +val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit +val replacement_context : unit -> Opaqueproof.work_list (** {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 -val discharge_global : Libnames.global_reference -> Libnames.global_reference +val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive +(* discharging a constant in one go *) +val full_replacement_context : unit -> Opaqueproof.work_list list +val full_section_segment_of_constant : + Names.constant -> (Context.named_context -> Context.named_context) list + |