(************************************************************************)
(*         *      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 Names
open Constr
open Environ
open Declarations
open Mod_declarations
open Entries
open 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_signature
val 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 by
the 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