Modops (u.4b72d9d53197f808b005effa2cda4f29.coq-core.8.20.1.doc.coq-core.kernel.Modops)

Various operations on modules and module types

Functors

Sourceval is_functor : ('ty, 'a) Declarations.functorize -> bool

val destr_functor : 
  ('ty, 'a) Declarations.functorize ->
  Names.MBId.t * 'ty * ('ty, 'a) Declarations.functorize

Source

val destr_nofunctor : 
  Names.ModPath.t ->
  ('ty, 'a) Declarations.functorize ->
  'a

Conversions between module_body and module_type_body

Source

val module_type_of_module : 
  Declarations.module_body ->
  Declarations.module_type_body

Source

val module_body_of_type : 
  Names.ModPath.t ->
  Declarations.module_type_body ->
  Declarations.module_body

Source

val check_modpath_equiv : 
  Environ.env ->
  Names.ModPath.t ->
  Names.ModPath.t ->
  unit

Source

val implem_smart_map : 
  (Declarations.structure_body -> Declarations.structure_body) ->
  (Declarations.module_expression -> Declarations.module_expression) ->
  Declarations.module_implementation ->
  Declarations.module_implementation

Source

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

Source

val annotate_struct_body : 
  Declarations.structure_body ->
  Declarations.module_signature ->
  Declarations.module_signature

Substitutions

Source

val subst_signature : 
  Mod_subst.substitution ->
  Declarations.module_signature ->
  Declarations.module_signature

Source

val subst_structure : 
  Mod_subst.substitution ->
  Declarations.structure_body ->
  Declarations.structure_body

Adding to an environment

Source

val add_structure : 
  Names.ModPath.t ->
  Declarations.structure_body ->
  Mod_subst.delta_resolver ->
  Environ.env ->
  Environ.env

Sourceval add_module : Declarations.module_body -> Environ.env -> Environ.env

adds a module and its components, but not the constraints

Source

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.

Source

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

same, for a module type

Source

val add_retroknowledge : 
  Declarations.module_implementation Declarations.module_retroknowledge ->
  Environ.env ->
  Environ.env

Strengthening

Source

val strengthen : 
  Declarations.module_type_body ->
  Names.ModPath.t ->
  Declarations.module_type_body

Source

val strengthen_and_subst_module_body : 
  Declarations.module_body ->
  Names.ModPath.t ->
  bool ->
  Declarations.module_body

Source

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

Source

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)

Source

val clean_bounded_mod_expr : 
  Declarations.module_signature ->
  Declarations.module_signature

Errors

Sourcetype 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 {
1. got : UVars.AbstractContext.t;
2. expect : UVars.AbstractContext.t;
}
| IncompatibleVariance
| NoRewriteRulesSubtyping

Sourcetype subtyping_trace_elt =

| Submodule of Names.Label.t
| FunctorArgument of int

Sourcetype 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

Sourceexception ModuleTypingError of module_typing_error

Sourceval error_existing_label : Names.Label.t -> 'a

Source

val error_incompatible_modtypes : 
  Declarations.module_type_body ->
  Declarations.module_type_body ->
  'a

Source

val error_signature_mismatch : 
  subtyping_trace_elt list ->
  Names.Label.t ->
  signature_mismatch_error ->
  'a

Sourceval error_no_such_label : Names.Label.t -> Names.ModPath.t -> 'a

Sourceval error_not_a_module_label : Names.Label.t -> 'a

Sourceval error_not_a_constant : Names.Label.t -> 'a

Sourceval error_incorrect_with_constraint : Names.Label.t -> 'a

Sourceval error_generative_module_expected : Names.Label.t -> 'a

Sourceval error_no_such_label_sub : Names.Label.t -> string -> 'a

Sourceval error_include_restricted_functor : Names.ModPath.t -> 'a