Mod_declarations (rocq-runtime.Mod

type 'a generic_module_body

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

type module_type_body = Declarations.mod_type generic_module_body

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

type structure_field_body =
  (module_body, module_type_body) Declarations.structure_field_body

type structure_body =
  (module_body, module_type_body) Declarations.structure_body

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

type module_signature =
  (module_type_body, structure_body) Declarations.functorize

type module_implementation =

| Abstract
(*
no accessible implementation
*)
| Algebraic of Declarations.module_expression
(*
non-interactive algebraic expression
*)
| Struct of Mod_subst.delta_resolver * 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

val mod_expr : module_body -> module_implementation

val mod_type : 'a generic_module_body -> module_signature

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

val mod_delta : 'a generic_module_body -> Mod_subst.delta_resolver

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

None if the argument is a functor, mod_delta otherwise

Builders

val make_module_body : 
  module_signature ->
  Mod_subst.delta_resolver ->
  module_body

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

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

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

val replace_module_body : 
  structure_body ->
  Mod_subst.delta_resolver ->
  module_body ->
  module_body

val module_type_of_module : module_body -> module_type_body

val module_body_of_type : module_type_body -> module_body

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

Setters

val set_implementation : module_implementation -> module_body -> module_body

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

Substitution

type subst_kind

val subst_codom : subst_kind

val subst_dom_codom : subst_kind

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

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

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

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

Hashconsing

val hcons_generic_module_body : 
  'a generic_module_body ->
  'a generic_module_body

val hcons_module_body : module_body -> module_body

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

val clean_structure : Names.MBId.Set.t -> structure_body -> structure_body