Mod_declarations (p.rocq-runtime.9.1.0.doc.rocq-runtime.kernel.Mod

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.

Source

type structure_field_body =
  (module_body, module_type_body) Declarations.structure_field_body

Source

type structure_body =
  (module_body, module_type_body) Declarations.structure_body

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

Source

type module_signature =
  (module_type_body, structure_body) Declarations.functorize

Sourcetype module_implementation =

| Abstract
(*
no accessible implementation
*)
| Algebraic of Declarations.module_expression
(*
non-interactive algebraic expression
*)
| Struct of structure_body
(*
interactive body living in the parameter context of mod_type
*)
| 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_expr : module_body -> module_implementation

Sourceval mod_type : 'a generic_module_body -> module_signature

Source

val mod_type_alg : 
  'a generic_module_body ->
  Declarations.module_expression option

Sourceval mod_delta : 'a generic_module_body -> Mod_subst.delta_resolver

Sourceval mod_retroknowledge : module_body -> Retroknowledge.action list

Source

val mod_global_delta : 
  'a generic_module_body ->
  Mod_subst.delta_resolver option

None if the argument is a functor, mod_delta otherwise

Builders

Source

val make_module_body : 
  module_signature ->
  Mod_subst.delta_resolver ->
  Retroknowledge.action list ->
  module_body

Source

val make_module_type : 
  module_signature ->
  Mod_subst.delta_resolver ->
  module_type_body

Source

val strengthen_module_body : 
  src:Names.ModPath.t ->
  module_signature ->
  Mod_subst.delta_resolver ->
  module_body ->
  module_body

Source

val strengthen_module_type : 
  structure_body ->
  Mod_subst.delta_resolver ->
  module_type_body ->
  module_type_body

Source

val 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

Source

val functorize_module : 
  (Names.MBId.t * module_type_body) list ->
  module_body ->
  module_body

Setters

Sourceval set_implementation : module_implementation -> module_body -> module_body

Source

val set_algebraic_type : 
  module_type_body ->
  Declarations.module_expression ->
  module_type_body

Source

val 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

Source

val subst_signature : 
  subst_kind ->
  Mod_subst.substitution ->
  Names.ModPath.t ->
  module_signature ->
  module_signature

Source

val subst_structure : 
  subst_kind ->
  Mod_subst.substitution ->
  Names.ModPath.t ->
  structure_body ->
  structure_body

Source

val subst_module : 
  subst_kind ->
  Mod_subst.substitution ->
  Names.ModPath.t ->
  module_body ->
  module_body

Source

val subst_modtype : 
  subst_kind ->
  Mod_subst.substitution ->
  Names.ModPath.t ->
  module_type_body ->
  module_type_body

Hashconsing

Source

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

Sourceval clean_structure : Names.MBIset.t -> structure_body -> structure_body