Module Modops

Various operations on modules and module types
val is_functor : ('ty, 'a) Declarations.functorize -> bool
val destr_functor : ('ty, 'a) Declarations.functorize -> Names.MBId.t * 'ty * ('ty, 'a) Declarations.functorize
val destr_nofunctor : Names.ModPath.t -> ('ty, 'a) Declarations.functorize -> 'a
val module_type_of_module : Declarations.module_body -> Declarations.module_type_body
val module_body_of_type : Names.ModPath.t -> Declarations.module_type_body -> Declarations.module_body
val check_modpath_equiv : Environ.env -> Names.ModPath.t -> Names.ModPath.t -> unit
val implem_smart_map : (Declarations.structure_body -> Declarations.structure_body) -> (Declarations.module_expression -> Declarations.module_expression) -> Declarations.module_implementation -> Declarations.module_implementation
val annotate_module_expression : Declarations.module_expression -> Declarations.module_signature -> (Declarations.module_type_body, (Constr.constr * UVars.AbstractContext.t option) Declarations.module_alg_expr) Declarations.functorize
val annotate_struct_body : Declarations.structure_body -> Declarations.module_signature -> Declarations.module_signature
Substitutions
val subst_signature : Mod_subst.substitution -> Declarations.module_signature -> Declarations.module_signature
val subst_structure : Mod_subst.substitution -> Declarations.structure_body -> Declarations.structure_body
Adding to an environment
val add_structure : Names.ModPath.t -> Declarations.structure_body -> Mod_subst.delta_resolver -> Environ.env -> Environ.env
val add_module : Declarations.module_body -> Environ.env -> Environ.env

adds a module and its components, but not the constraints

val add_linked_module : Declarations.module_body -> Environ.link_info -> Environ.env -> Environ.env

same as add_module, but for a module whose native code has been linked by the native compiler. The linking information is updated.

val add_module_type : Names.ModPath.t -> Declarations.module_type_body -> Environ.env -> Environ.env

same, for a module type

val add_retroknowledge : Declarations.module_implementation Declarations.module_retroknowledge -> Environ.env -> Environ.env
Strengthening
val strengthen : Declarations.module_type_body -> Names.ModPath.t -> Declarations.module_type_body
val strengthen_and_subst_module_body : Declarations.module_body -> Names.ModPath.t -> bool -> Declarations.module_body
val subst_modtype_signature_and_resolver : Names.ModPath.t -> Names.ModPath.t -> Declarations.module_signature -> Mod_subst.delta_resolver -> Declarations.module_signature * Mod_subst.delta_resolver
Building map of constants to inline
val inline_delta_resolver : Environ.env -> Entries.inline -> Names.ModPath.t -> Names.MBId.t -> Declarations.module_type_body -> Mod_subst.delta_resolver -> Mod_subst.delta_resolver
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_bounded_mod_expr : Declarations.module_signature -> Declarations.module_signature
Errors
type signature_mismatch_error =
| InductiveFieldExpected of Declarations.mutual_inductive_body
| DefinitionFieldExpected
| ModuleFieldExpected
| ModuleTypeFieldExpected
| NotConvertibleInductiveField of Names.Id.t
| NotConvertibleConstructorField of Names.Id.t
| NotConvertibleBodyField
| NotConvertibleTypeField of Environ.env * Constr.types * Constr.types
| CumulativeStatusExpected of bool
| PolymorphicStatusExpected of bool
| NotSameConstructorNamesField
| NotSameInductiveNameInBlockField
| FiniteInductiveFieldExpected of bool
| InductiveNumbersFieldExpected of int
| InductiveParamsNumberField of int
| RecordFieldExpected of bool
| RecordProjectionsExpected of Names.Name.t list
| NotEqualInductiveAliases
| IncompatibleUniverses of UGraph.univ_inconsistency
| IncompatiblePolymorphism of Environ.env * Constr.types * Constr.types
| IncompatibleConstraints of {
got : UVars.AbstractContext.t;
expect : UVars.AbstractContext.t;
}
| IncompatibleVariance
type subtyping_trace_elt =
| Submodule of Names.Label.t
| FunctorArgument of int
type module_typing_error =
| SignatureMismatch of subtyping_trace_elt list * Names.Label.t * signature_mismatch_error
| LabelAlreadyDeclared of Names.Label.t
| NotAFunctor
| IsAFunctor of Names.ModPath.t
| IncompatibleModuleTypes of Declarations.module_type_body * Declarations.module_type_body
| NotEqualModulePaths of Names.ModPath.t * Names.ModPath.t
| NoSuchLabel of Names.Label.t * Names.ModPath.t
| NotAModuleLabel of Names.Label.t
| NotAConstant of Names.Label.t
| IncorrectWithConstraint of Names.Label.t
| GenerativeModuleExpected of Names.Label.t
| LabelMissing of Names.Label.t * string
| IncludeRestrictedFunctor of Names.ModPath.t
exception ModuleTypingError of module_typing_error
val error_existing_label : Names.Label.t -> 'a
val error_incompatible_modtypes : Declarations.module_type_body -> Declarations.module_type_body -> 'a
val error_signature_mismatch : subtyping_trace_elt list -> Names.Label.t -> signature_mismatch_error -> 'a
val error_no_such_label : Names.Label.t -> Names.ModPath.t -> 'a
val error_not_a_module_label : Names.Label.t -> 'a
val error_not_a_constant : Names.Label.t -> 'a
val error_incorrect_with_constraint : Names.Label.t -> 'a
val error_generative_module_expected : Names.Label.t -> 'a
val error_no_such_label_sub : Names.Label.t -> string -> 'a
val error_include_restricted_functor : Names.ModPath.t -> 'a