Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263(************************************************************************)(* * 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 Declarationsopen Mod_declarationsopen Environopen Entriesopen Mod_substopen 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