package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.library/Lib/index.html

Module LibSource

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 =
  1. | Export
  2. | Import
Sourcetype export = (export_flag * Libobject.open_filter) option
Sourcetype 'summary node =
  1. | CompilingLibrary of Libobject.object_prefix
  2. | OpenedModule of is_type * export * Libobject.object_prefix * 'summary
  3. | OpenedSection of Libobject.object_prefix * 'summary
Sourceval node_prefix : 'summary node -> Libobject.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
Sourceval add_discharged_leaf : Libobject.discharged_obj -> unit
...

The function contents gives access to the current entire segment

Functions relative to current path
Sourceval prefix : unit -> Libobject.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 = M
  • 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 -> Libnames.full_path
Sourceval cwd_except_section : unit -> Libnames.full_path
Sourceval current_dirpath : bool -> Names.DirPath.t
Sourceval make_path_except_section : Names.Id.t -> Libnames.full_path
Sourceval current_mp : unit -> Names.ModPath.t

Kernel-side names

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
Sourcetype discharged_item =
  1. | DischargedExport of Libobject.ExportObj.t
  2. | DischargedLeaf of Libobject.discharged_obj
Sourcetype classified_objects = {
  1. substobjs : Libobject.t list;
  2. keepobjs : Libobject.keep_objects;
  3. escapeobjs : Libobject.escape_objects;
  4. anticipateobjs : Libobject.t list;
}
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.

Compilation units
Sourceval start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit
Sourcetype compilation_result = {
  1. info : Library_info.t;
  2. synterp_objects : classified_objects;
  3. interp_objects : classified_objects;
}
Sourceval end_compilation : Names.DirPath.t -> compilation_result

Finalize the compilation of a library.

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

Compatibility layer

Sourceval init : unit -> unit

This also does init_summaries