Module Lib

Lib: record of operations, backtrack, low-level sections

type is_type = bool
type export = bool option
val make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name
type node =
| Leaf of Libobject.obj
| CompilingLibrary of Nametab.object_prefix
| OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen
| OpenedSection of Nametab.object_prefix * Summary.frozen
type library_segment = (Libobject.object_name * node) list
type lib_objects = (Names.Id.t * Libobject.obj) list
Object iteration functions.
val open_objects : int -> Nametab.object_prefix -> lib_objects -> unit
val load_objects : int -> Nametab.object_prefix -> lib_objects -> unit
val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects
val classify_segment : library_segment -> lib_objects * lib_objects * Libobject.obj list

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 segment_of_objects : Nametab.object_prefix -> lib_objects -> library_segment

segment_of_objects prefix objs forms a list of Leafs

...
val add_leaf : Names.Id.t -> Libobject.obj -> Libobject.object_name
val add_anonymous_leaf : ?⁠cache_first:bool -> Libobject.obj -> unit
val pull_to_head : Libobject.object_name -> unit
val add_leaves : Names.Id.t -> Libobject.obj list -> Libobject.object_name

this operation adds all objects with the same name and calls load_object for each of them

...
val contents : unit -> library_segment
val contents_after : Libobject.object_name -> library_segment
Functions relative to current path
val cwd : unit -> Names.DirPath.t

User-side names

val cwd_except_section : unit -> Names.DirPath.t
val current_dirpath : bool -> Names.DirPath.t
val make_path : Names.Id.t -> Libnames.full_path
val make_path_except_section : Names.Id.t -> Libnames.full_path
val current_mp : unit -> Names.ModPath.t

Kernel-side names

val make_kn : Names.Id.t -> Names.KerName.t
val sections_are_opened : unit -> bool

Are we inside an opened section

val sections_depth : unit -> int
val is_module_or_modtype : unit -> bool

Are we inside an opened module type

val is_modtype : unit -> bool
val is_modtype_strict : unit -> bool
val is_module : unit -> bool
val current_mod_id : unit -> Names.module_ident
val find_opening_node : Names.Id.t -> node

Returns the opening node of a given name

Modules and module types
val start_module : export -> Names.module_ident -> Names.ModPath.t -> Summary.frozen -> Nametab.object_prefix
val start_modtype : Names.module_ident -> Names.ModPath.t -> Summary.frozen -> Nametab.object_prefix
val end_module : unit -> Libobject.object_name * Nametab.object_prefix * Summary.frozen * library_segment
val end_modtype : unit -> Libobject.object_name * Nametab.object_prefix * Summary.frozen * library_segment
Compilation units
val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit
val end_compilation_checks : Names.DirPath.t -> Libobject.object_name
val end_compilation : Libobject.object_name -> Nametab.object_prefix * library_segment
val library_dp : unit -> Names.DirPath.t

The function library_dp returns the DirPath.t of the current compiling library (or default_library)

val dp_of_mp : Names.ModPath.t -> Names.DirPath.t

Extract the library part of a name even if in a section

val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list
val library_part : Names.GlobRef.t -> Names.DirPath.t
Sections
val open_section : Names.Id.t -> unit
val close_section : unit -> unit
We can get and set the state of the operations (used in States).
type frozen
val freeze : marshallable:bool -> frozen
val unfreeze : frozen -> unit
val drop_objects : frozen -> frozen

Keep only the libobject structure, not the objects themselves

val init : unit -> unit
type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
Section management for discharge
type variable_context = variable_info list
type abstr_info = private {
abstr_ctx : variable_context;

Section variables of this prefix

abstr_subst : Univ.Instance.t;

Actual names of the abstracted variables

abstr_uctx : Univ.AUContext.t;

Universe quantification, same length as the substitution

}
val instance_from_variable_context : variable_context -> Names.Id.t array
val named_of_variable_context : variable_context -> Constr.named_context
val section_segment_of_constant : Names.Constant.t -> abstr_info
val section_segment_of_mutual_inductive : Names.MutInd.t -> abstr_info
val section_segment_of_reference : Names.GlobRef.t -> abstr_info
val variable_section_segment_of_reference : Names.GlobRef.t -> variable_context
val section_instance : Names.GlobRef.t -> Univ.Instance.t * Names.Id.t array
val is_in_section : Names.GlobRef.t -> bool
val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
val add_section_context : Univ.ContextSet.t -> unit
val add_section_constant : Decl_kinds.polymorphic -> Names.Constant.t -> Constr.named_context -> unit
val add_section_kn : Decl_kinds.polymorphic -> Names.MutInd.t -> Constr.named_context -> unit
val replacement_context : unit -> Opaqueproof.work_list
val is_polymorphic_univ : Univ.Level.t -> bool
Discharge: decrease the section level if in the current section
val discharge_proj_repr : Names.Projection.Repr.t -> Names.Projection.Repr.t
val discharge_abstract_universe_context : abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t