(************************************************************************)
(*         *      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 Declarations
open Mod_declarations
open Environ
open Entries
open Mod_subst
open Names

(** Main functions for translating module entries *)

type 'a vm_handler = { vm_handler : env -> universes -> Constr.t -> 'a -> 'a * Vmlibrary.indirect_code }
type 'a vm_state = 'a * 'a vm_handler

(** [translate_module] produces a [module_body] out of a [module_entry].
    In the output fields:
    - [mod_expr] is [Abstract] for a [MType] entry, or [Algebraic] for [MExpr].
    - [mod_type_alg] is [None] only for a [MExpr] without explicit signature.

    The second component is the resolver an enclosing module type inherits
    from this declaration, or [None] if the module is a functor. It is the
    resolver of the module's type rather than of its body. *)

val translate_module :
  ('a, Conversion.graph_inconsistency) Conversion.universe_state ->
  'b vm_state ->
  env -> ModPath.t -> inline -> module_entry ->
  (module_body * mod_type delta_resolver option) * 'a * 'b

(** [translate_modtype] produces a [module_type_body] whose [mod_type_alg]
    cannot be [None] (and of course [mod_expr] is [Abstract]). *)

val translate_modtype :
  ('a, Conversion.graph_inconsistency) Conversion.universe_state ->
  'b vm_state ->
  env -> ModPath.t -> inline -> module_type_entry -> module_type_body * 'a * 'b

(** From an already-translated (or interactive) implementation and
    an (optional) signature entry, produces a final [module_body] *)

val finalize_module :
  ('a, Conversion.graph_inconsistency) Conversion.universe_state ->
  'b vm_state ->
  env -> ModPath.t -> module_signature * mod_type delta_resolver ->
  (module_type_entry * inline) option ->
  module_body * 'a * 'b

(** [translate_mse_include is_mod state vmstate env mp self inl me] translates
    the mse of a module or module type given to an [Include]. *)

val translate_mse_include :
  bool -> ('a, Conversion.graph_inconsistency) Conversion.universe_state -> 'b vm_state ->
  Environ.env -> ModPath.t -> module_body -> inline ->
  module_struct_entry -> structure_body * mod_type delta_resolver * 'a * 'b