Mod_declarationstype module_body = Declarations.mod_body generic_module_bodyFor a module, there are five possible situations:
Declare Module M : T then mod_expr = Abstract; mod_type_alg = Some TModule M := E then mod_expr = Algebraic E; mod_type_alg = NoneModule M : T := E then mod_expr = Algebraic E; mod_type_alg = Some TModule M. ... End M then mod_expr = FullStruct; mod_type_alg = NoneModule 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_bodyA 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.
type structure_field_body = (module_body, module_type_body) Declarations.structure_field_bodytype structure_body = (module_body, module_type_body) Declarations.structure_bodyA module signature is a structure, with possibly functors on top of it
type module_signature = (module_type_body, structure_body) Declarations.functorizetype 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 |
| FullStruct | (* special case of |
Extra invariants :
MEwith inside a mod_expr implementation : the 'with' syntax is only supported for module typesMEapply can only be another MEapply or a MEident * the argument of MEapply is now directly forced to be a ModPath.t.val mod_expr : module_body -> module_implementationval mod_type : 'a generic_module_body -> module_signatureval mod_type_alg : 'a generic_module_body -> Declarations.module_expression optionval mod_delta : 'a generic_module_body -> Mod_subst.delta_resolverval mod_retroknowledge : module_body -> Retroknowledge.action listval mod_global_delta : 'a generic_module_body -> Mod_subst.delta_resolver optionNone if the argument is a functor, mod_delta otherwise
val make_module_body : module_signature -> Mod_subst.delta_resolver -> Retroknowledge.action list -> module_bodyval make_module_type : module_signature -> Mod_subst.delta_resolver -> module_type_bodyval strengthen_module_body : src:Names.ModPath.t -> module_signature -> Mod_subst.delta_resolver -> module_body -> module_bodyval strengthen_module_type : structure_body -> Mod_subst.delta_resolver -> module_type_body -> module_type_bodyval replace_module_body : structure_body -> Mod_subst.delta_resolver -> module_body -> module_bodyval module_type_of_module : module_body -> module_type_bodyval module_body_of_type : module_type_body -> module_bodyval functorize_module : (Names.MBId.t * module_type_body) list -> module_body -> module_bodyval set_implementation : module_implementation -> module_body -> module_bodyval set_algebraic_type : module_type_body -> Declarations.module_expression -> module_type_bodyval set_retroknowledge : module_body -> Retroknowledge.action list -> module_bodyval subst_dom : subst_kindval subst_codom : subst_kindval subst_dom_codom : subst_kindval subst_shallow_dom_codom : Mod_subst.substitution -> subst_kindval subst_signature : subst_kind -> Mod_subst.substitution -> Names.ModPath.t -> module_signature -> module_signatureval subst_structure : subst_kind -> Mod_subst.substitution -> Names.ModPath.t -> structure_body -> structure_bodyval subst_module : subst_kind -> Mod_subst.substitution -> Names.ModPath.t -> module_body -> module_bodyval subst_modtype : subst_kind -> Mod_subst.substitution -> Names.ModPath.t -> module_type_body -> module_type_bodyval hcons_generic_module_body : 'a generic_module_body -> 'a generic_module_bodyval hcons_module_body : module_body -> module_bodyval hcons_module_type : module_type_body -> module_type_bodyFor instance: functor(X:T)->struct module M:=X end) becomes: functor(X:T)->struct module M:=<content of T> end)
val clean_structure : Names.MBIset.t -> structure_body -> structure_body