Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Namesopen Constropen Environopen Declarationsopen Mod_declarationsopen Entriesopen Mod_subst
(** {6 Various operations on modules and module types } *)
(** Functors *)
val is_functor : ('ty,'a) functorize -> bool
val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize
val destr_nofunctor : ModPath.t -> ('ty,'a) functorize -> 'a
val check_modpath_equiv : env -> ModPath.t -> ModPath.t -> unit
val annotate_module_expression : module_expression -> module_signature -> (module_type_body, (constr * UVars.AbstractContext.t option) module_alg_expr) functorize
val annotate_struct_body : structure_body -> module_signature -> module_signature
(** {6 Substitutions } *)
val subst_signature : substitution -> ModPath.t -> module_signature -> module_signatureval subst_structure : substitution -> ModPath.t -> structure_body -> structure_body
(** {6 Adding to an environment } *)
val add_structure : ModPath.t -> structure_body -> 'a delta_resolver -> env -> env
(** adds a module and its components, but not the constraints *)val add_module : ModPath.t -> module_body -> env -> env
(** same as add_module, but for a module whose native code has been linked bythe native compiler. The linking information is updated. *)val add_linked_module : ModPath.t -> module_body -> link_info -> env -> env
(** add an abstract module parameter to the environment *)val add_module_parameter : MBId.t -> module_type_body -> env -> env
(** {6 Recompiling the VM bytecode of a module} *)
(** Recompile the VM bytecode of every constant of a signature from its body, discarding whatever code the declarations carry, threading the environment exactly as [add_structure] does. Used by the checker, which does not trust the VM bytecode serialized in a [.vo] file. *)val compile_signature : env -> Vmlibrary.t -> ModPath.t -> 'a delta_resolver -> module_signature -> Vmlibrary.t * module_signature
(** Same, for a whole module (type) body. *)val compile_module_bytecode : env -> Vmlibrary.t -> ModPath.t -> 'a generic_module_body -> Vmlibrary.t * 'a generic_module_body
val add_retroknowledge : Retroknowledge.action list -> env -> env
(** {6 Strengthening } *)
val strengthen : module_type_body -> ModPath.t -> module_type_body
val strengthen_and_subst_module_body : ModPath.t -> module_body -> ModPath.t -> bool -> module_body
(** [include_applied_structure mp_from struc reso mp] includes into [mp] the result of a functor application elaborated at the functor's path [mp_from]. Nothing is strengthened, there being no module at [mp_from], and no equivalence is recorded for [mp] itself. *)val include_applied_structure : ModPath.t -> structure_body -> mod_body delta_resolver -> ModPath.t -> structure_body * mod_body delta_resolver
val subst_modtype_signature_and_resolver : ModPath.t -> ModPath.t -> module_signature -> 'a delta_resolver -> module_signature * 'a delta_resolver
(** {6 Building map of constants to inline } *)
val inline_delta_resolver : env -> inline -> ModPath.t -> MBId.t -> module_type_body -> 'a delta_resolver -> mod_subst delta_resolver(** Enrich the resolver of the module being passed as a functor argument with the bodies of the fields the parameter type declared [Inline]. The result carries inlined bodies, hence is a substitution resolver. *)
(** {6 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 : module_signature -> module_signature
(** {6 Errors } *)
type signature_mismatch_error = | InductiveFieldExpected of mutual_inductive_body | DefinitionFieldExpected | ModuleFieldExpected | ModuleTypeFieldExpected | NotConvertibleInductiveField of Id.t * (env * types * types) option | NotConvertibleConstructorField of Id.t * (env * types * types) option | NotConvertibleBodyField of (env * constr * constr) option | NotConvertibleTypeField of env * types * types | CumulativeStatusExpected of bool | PolymorphicStatusExpected of bool | TemplateStatusExpected of bool | PrivateStatusExpected of bool option | NotSameConstructorNamesField of Id.t array * Id.t array | NotSameInductiveNameInBlockField of Id.t * Id.t | FiniteInductiveFieldExpected of recursivity_kind | InductiveNumbersFieldExpected of { got : int; expected : int } | InductiveParams of { env : Environ.env; got : rel_context; expected : rel_context } | InductiveUniformParams of { got : int; expected : int } | RecordFieldExpected of bool | RecordProjectionsExpected of { expected : Name.t list; got : Name.t list } | NotEqualInductiveAliases of MutInd.t * MutInd.t | IncompatibleUniverses of { err : UGraph.univ_inconsistency; env : env; t1 : types; t2 : types } | IncompatibleQualities of { err : QGraph.elimination_error; env : env; t1 : types; t2 : types } | IncompatiblePolymorphism of env * types * types | IncompatibleUnivConstraints of { env : env; got : UVars.AbstractContext.t; expect : UVars.AbstractContext.t } | IncompatibleVariance | NoRewriteRulesSubtyping
type with_constraint_error = | WithSignatureMismatch of signature_mismatch_error | WithCannotConstrainPrimitive | WithCannotConstrainSymbol
type subtyping_trace_elt = | Submodule of Id.t | FunctorArgument of int
type module_typing_error = | SignatureMismatch of subtyping_trace_elt list * Id.t * signature_mismatch_error | LabelAlreadyDeclared of Id.t | NotAFunctor | IsAFunctor of ModPath.t | IncompatibleModuleTypes of module_type_body * module_type_body | NotEqualModulePaths of ModPath.t * ModPath.t | NoSuchLabel of Id.t * ModPath.t | NotAModuleLabel of Id.t | NotAConstant of Id.t | IncorrectWithConstraint of Id.t * with_constraint_error | GenerativeModuleExpected of Id.t | LabelMissing of Id.t * string | IncludeRestrictedFunctor of ModPath.t
exception ModuleTypingError of module_typing_error
val error_existing_label : Id.t -> 'a
val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a
val error_signature_mismatch : subtyping_trace_elt list -> Id.t -> signature_mismatch_error -> 'a
val error_no_such_label : Id.t -> ModPath.t -> 'a
val error_not_a_module_label : Id.t -> 'a
val error_not_a_constant : Id.t -> 'a
val error_incorrect_with_constraint : Id.t -> with_constraint_error -> 'a
val error_generative_module_expected : Id.t -> 'a
val error_no_such_label_sub : Id.t -> string -> 'a
val error_include_restricted_functor : ModPath.t -> 'a