package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

type is_type = bool
type export_flag =
  1. | Export
  2. | Import
type export = (export_flag * Libobject.open_filter) option
val make_foname : Names.Id.t -> Libobject.object_name
type 'summary node =
  1. | CompilingLibrary of Nametab.object_prefix
  2. | OpenedModule of is_type * export * Nametab.object_prefix * 'summary
  3. | OpenedSection of Nametab.object_prefix * 'summary
val 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.

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

val add_leaf : Libobject.obj -> unit
...

The function contents gives access to the current entire segment

val contents : unit -> Summary.Interp.frozen library_segment
Functions relative to current path
val 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

val cwd : unit -> Names.DirPath.t
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
module 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
val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit

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

val library_dp : unit -> Names.DirPath.t

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

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

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

val library_part : Names.GlobRef.t -> Names.DirPath.t
val section_segment_of_constant : Names.Constant.t -> Cooking.cooking_info

Section management for discharge

val section_segment_of_inductive : Names.MutInd.t -> Cooking.cooking_info
val section_segment_of_reference : Names.GlobRef.t -> Cooking.cooking_info
val section_instance : Names.GlobRef.t -> Constr.t array
val is_in_section : Names.GlobRef.t -> bool
Discharge: decrease the section level if in the current section

Compatibility layer

val init : unit -> unit
val open_section : Names.Id.t -> unit
val close_section : unit -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct