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.kernel/Mod_declarations/index.html

Module Mod_declarationsSource

Sourcetype 'a generic_module_body
Sourcetype module_body = Declarations.mod_body generic_module_body

For a module, there are five possible situations:

  • Declare Module M : T then mod_expr = Abstract; mod_type_alg = Some T
  • Module M := E then mod_expr = Algebraic E; mod_type_alg = None
  • Module M : T := E then mod_expr = Algebraic E; mod_type_alg = Some T
  • Module M. ... End M then mod_expr = FullStruct; mod_type_alg = None
  • Module M : T. ... End M then mod_expr = Struct; mod_type_alg = Some T And of course, all these situations may be functors or not.
Sourcetype module_type_body = Declarations.mod_type generic_module_body

A module_type_body is just a module_body with no implementation and also an empty mod_retroknowledge. Its mod_type_alg contains the algebraic definition of this module type, or None if it has been built interactively.

Sourcetype structure_field_body = (module_body, module_type_body) Declarations.structure_field_body
Sourcetype structure_body = (module_body, module_type_body) Declarations.structure_body

A module signature is a structure, with possibly functors on top of it

Sourcetype module_implementation =
  1. | Abstract
    (*

    no accessible implementation

    *)
  2. | Algebraic of Declarations.module_expression
    (*

    non-interactive algebraic expression

    *)
  3. | Struct of structure_body
    (*

    interactive body living in the parameter context of mod_type

    *)
  4. | FullStruct
    (*

    special case of Struct : the body is exactly mod_type

    *)

Extra invariants :

  • No MEwith inside a mod_expr implementation : the 'with' syntax is only supported for module types
  • A module application is atomic, for instance ((M N) P) : * the head of MEapply can only be another MEapply or a MEident * the argument of MEapply is now directly forced to be a ModPath.t.
Accessors
Sourceval mod_retroknowledge : module_body -> Retroknowledge.action list
Sourceval mod_global_delta : 'a generic_module_body -> Mod_subst.delta_resolver option

None if the argument is a functor, mod_delta otherwise

Builders
Sourceval make_module_body : module_signature -> Mod_subst.delta_resolver -> Retroknowledge.action list -> module_body
Sourceval strengthen_module_body : src:Names.ModPath.t -> module_signature -> Mod_subst.delta_resolver -> module_body -> module_body
Sourceval replace_module_body : structure_body -> Mod_subst.delta_resolver -> module_body -> module_body
Sourceval module_type_of_module : module_body -> module_type_body
Sourceval module_body_of_type : module_type_body -> module_body
Sourceval functorize_module : (Names.MBId.t * module_type_body) list -> module_body -> module_body
Setters
Sourceval set_implementation : module_implementation -> module_body -> module_body
Sourceval set_retroknowledge : module_body -> Retroknowledge.action list -> module_body
Substitution
Sourcetype subst_kind
Sourceval subst_dom : subst_kind
Sourceval subst_codom : subst_kind
Sourceval subst_dom_codom : subst_kind
Sourceval subst_shallow_dom_codom : Mod_subst.substitution -> subst_kind
Hashconsing
Sourceval hcons_generic_module_body : 'a generic_module_body -> 'a generic_module_body
Sourceval hcons_module_body : module_body -> module_body
Sourceval hcons_module_type : module_type_body -> module_type_body
Cleaning a module expression from bounded parts

For instance: functor(X:T)->struct module M:=X end) becomes: functor(X:T)->struct module M:=<content of T> end)