Mod_typingMain functions for translating module entries
type 'a vm_handler = {vm_handler : Environ.env -> Declarations.universes -> Constr.t -> 'a -> 'a * Vmlibrary.indirect_code option; |
}type 'a vm_state = 'a * 'a vm_handlertranslate_module produces a module_body out of a module_entry. In the output fields:
mod_expr is Abstract for a MType entry, or Algebraic for MExpr.mod_type_alg is None only for a MExpr without explicit signature.val translate_module : ('a, UGraph.univ_inconsistency) Conversion.universe_state -> 'b vm_state -> Environ.env -> Names.ModPath.t -> Entries.inline -> Entries.module_entry -> Declarations.module_body * 'a * 'btranslate_modtype produces a module_type_body whose mod_type_alg cannot be None (and of course mod_expr is Abstract).
val translate_modtype : ('a, UGraph.univ_inconsistency) Conversion.universe_state -> 'b vm_state -> Environ.env -> Names.ModPath.t -> Entries.inline -> Entries.module_type_entry -> Declarations.module_type_body * 'a * 'bFrom an already-translated (or interactive) implementation and an (optional) signature entry, produces a final module_body
val finalize_module : ('a, UGraph.univ_inconsistency) Conversion.universe_state -> 'b vm_state -> Environ.env -> Names.ModPath.t -> (Declarations.module_signature * Mod_subst.delta_resolver) -> (Entries.module_type_entry * Entries.inline) option -> Declarations.module_body * 'a * 'btranslate_mse_incl translate the mse of a module or module type given to an Include
val translate_mse_include : bool -> ('a, UGraph.univ_inconsistency) Conversion.universe_state -> 'b vm_state -> Environ.env -> Names.ModPath.t -> Entries.inline -> Entries.module_struct_entry -> Declarations.module_signature * unit * Mod_subst.delta_resolver * 'a * 'b