Modops (coq-core.Modops)

Various operations on modules and module types

Functors

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

Conversions between module_body and module_type_body

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.module_signature -> Declarations.module_signature) -> (Declarations.module_expression -> Declarations.module_expression) -> Declarations.module_implementation -> Declarations.module_implementation

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 : Univ.AbstractContext.t;

expect : Univ.AbstractContext.t;

}

| IncompatibleVariance

type module_typing_error =

| SignatureMismatch of Names.Label.t * Declarations.structure_field_body * 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 : Names.Label.t -> Declarations.structure_field_body -> 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