Module `Lib`Source

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

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).

Sourcetype is_type = bool

Sourcetype export_flag =

| Export
| Import

Sourcetype export = (export_flag * Libobject.open_filter) option

Sourceval make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name

Sourceval make_foname : Names.Id.t -> Libobject.object_name

Sourceval oname_prefix : Libobject.object_name -> Nametab.object_prefix

Sourcetype 'summary node =

| CompilingLibrary of Nametab.object_prefix
| OpenedModule of is_type * export * Nametab.object_prefix * 'summary
| OpenedSection of Nametab.object_prefix * 'summary

Sourceval node_prefix : 'summary node -> Nametab.object_prefix

Extract the object_prefix component. Note that it is the prefix of the objects *inside* this node, eg in Module M. we have OpenedModule with prefix containing M.

Sourcetype 'summary library_segment = ('summary node * Libobject.t list) list

...

Adding operations (which call the cache method, and getting the current list of operations (most recent ones coming first).

Sourceval add_leaf : Libobject.obj -> unit

...

The function contents gives access to the current entire segment

Sourceval contents : unit -> Summary.Interp.frozen library_segment

Functions relative to current path

Sourceval prefix : unit -> Nametab.object_prefix

User-side names

cwd() is (prefix()).obj_dir current_mp() is (prefix()).obj_mp

Inside a library A.B module M section S, we have

library_dp = A.B
cwd = A.B.M.S
cwd_except_section = A.B.M
current_dirpath true = M.S
current_dirpath false = S
current_mp = MPdot(MPfile A.B, M)

make_path (resp make_path_except_section) uses cwd (resp cwd_except_section) make_kn uses current_mp

Sourceval cwd : unit -> Names.DirPath.t

Sourceval cwd_except_section : unit -> Names.DirPath.t

Sourceval current_dirpath : bool -> Names.DirPath.t

Sourceval make_path : Names.Id.t -> Libnames.full_path

Sourceval make_path_except_section : Names.Id.t -> Libnames.full_path

Sourceval current_mp : unit -> Names.ModPath.t

Kernel-side names

Sourceval make_kn : Names.Id.t -> Names.KerName.t

Sourceval sections_are_opened : unit -> bool

Are we inside an opened section

Sourceval sections_depth : unit -> int

Sourceval is_module_or_modtype : unit -> bool

Are we inside an opened module type

Sourceval is_modtype : unit -> bool

Sourceval is_modtype_strict : unit -> bool

Sourceval is_module : unit -> bool

Sourcemodule type StagedLibS = sig ... end

The StagedLibS abstraction describes operations and traversal for Lib at a given stage.

We provide two instances of StagedLibS, corresponding to the Synterp and Interp stages.

Sourcemodule Synterp : StagedLibS with type summary = Summary.Synterp.frozen

Sourcemodule Interp : StagedLibS with type summary = Summary.Interp.frozen

Compilation units

Sourceval start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit

Source

val end_compilation : 
  Names.DirPath.t ->
  Nametab.object_prefix
  * Library_info.t list
  * Interp.classified_objects
  * Synterp.classified_objects

Finalize the compilation of a library and return respectively the library prefix, the regular objects, and the syntax-related objects.

Sourceval library_dp : unit -> Names.DirPath.t

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

Sourceval split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list

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

Sourceval library_part : Names.GlobRef.t -> Names.DirPath.t

Sourceval section_segment_of_constant : Names.Constant.t -> Cooking.cooking_info

Section management for discharge

Sourceval section_segment_of_inductive : Names.MutInd.t -> Cooking.cooking_info

Sourceval section_segment_of_reference : Names.GlobRef.t -> Cooking.cooking_info

Sourceval section_instance : Names.GlobRef.t -> Constr.t array

Sourceval is_in_section : Names.GlobRef.t -> bool

Discharge: decrease the section level if in the current section

Sourceval discharge_proj_repr : Names.Projection.Repr.t -> Names.Projection.Repr.t

Compatibility layer

Sourceval init : unit -> unit

Sourceval open_section : Names.Id.t -> unit

Sourceval close_section : unit -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Lib/index.html

Module `Lib`Source

...

...

Functions relative to current path

Compilation units

Discharge: decrease the section level if in the current section

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Lib/index.html

Module LibSource

...

...

Functions relative to current path

Compilation units

Discharge: decrease the section level if in the current section

Module `Lib`Source