Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130(************************************************************************)(* * 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 Mod_substopen Declarations
type 'a generic_module_bodytype module_body = mod_body generic_module_body
(** For a module, there are five possible situations: - [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T] - [Module M := E] then [mod_expr = Algebraic E; mod_type_alg = None] - [Module M : T := E] then [mod_expr = Algebraic E; mod_type_alg = Some T] - [Module M. ... End M] then [mod_expr = FullStruct; mod_type_alg = None] - [Module M : T. ... End M] then [mod_expr = Struct; mod_type_alg = Some T] And of course, all these situations may be functors or not. *)
type module_type_body = mod_type generic_module_body
(** A [module_type_body] is just a [module_body] with no implementation. Its [mod_type_alg] contains the algebraic definition of this module type, or [None] if it has been built interactively. *)
type structure_field_body = (module_body, module_type_body) Declarations.structure_field_body
type structure_body = (module_body, module_type_body) Declarations.structure_body
(** A module signature is a structure, with possibly functors on top of it *)
type module_signature = (module_type_body,structure_body) functorize
type module_implementation = | Abstract (** no accessible implementation *) | Algebraic of module_expression (** non-interactive algebraic expression *) | Struct of mod_body delta_resolver * structure_body (** interactive body living in the parameter context of [mod_type] *) | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
(** Extra invariants :
- No [MEwith] inside a [mod_expr] implementation : the 'with' syntax is only supported for module types
- A module application is atomic, for instance ((M N) P) : * the head of [MEapply] can only be another [MEapply] or a [MEident] * the argument of [MEapply] is now directly forced to be a [ModPath.t].*)
(** {6 Accessors} *)
val mod_expr : module_body -> module_implementationval mod_type : 'a generic_module_body -> module_signatureval mod_type_alg : 'a generic_module_body -> module_expression optionval mod_delta : 'a generic_module_body -> 'a delta_resolver
val mod_global_delta : 'a generic_module_body -> 'a delta_resolver option(** [None] if the argument is a functor, [mod_delta] otherwise *)
(** {6 Builders} *)
val make_module_body : module_signature -> Mod_subst.mod_body Mod_subst.delta_resolver -> module_bodyval make_module_type : module_signature -> Mod_subst.mod_type Mod_subst.delta_resolver -> module_type_body
val strengthen_module_body : src:ModPath.t -> module_signature -> mod_body delta_resolver -> module_body -> module_body
val strengthen_module_type : structure_body -> mod_type delta_resolver -> module_type_body -> module_type_body
val replace_module_body : structure_body -> mod_body delta_resolver -> module_body -> module_body
val module_type_of_module : module_body -> module_type_bodyval module_body_of_type : module_type_body -> module_body
val functorize_module : (Names.MBId.t * module_type_body) list -> module_body -> module_body
(** {6 Setters} *)
(* This is internal code used by the kernel, you should not mess with this. *)
val set_implementation : module_implementation -> module_body -> module_bodyval set_algebraic_type : module_type_body -> module_expression -> module_type_body
val set_signature : module_signature -> 'a generic_module_body -> 'a generic_module_body(** Replace the expanded type, keeping the implementation and the algebraic type. *)
(** {6 Substitution} *)
type subst_kindval subst_codom : subst_kindval subst_dom_codom : subst_kind
val subst_signature : subst_kind -> substitution -> ModPath.t -> module_signature -> module_signature
val subst_structure : subst_kind -> substitution -> ModPath.t -> structure_body -> structure_body
val subst_module : subst_kind -> substitution -> ModPath.t -> module_body -> module_body
val subst_modtype : subst_kind -> substitution -> ModPath.t -> module_type_body -> module_type_body
(** {6 Hashconsing} *)
val hcons_generic_module_body : 'a generic_module_body -> 'a generic_module_bodyval hcons_module_body : module_body -> module_bodyval hcons_module_type : module_type_body -> module_type_body
(** {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_structure : Names.MBId.Set.t -> structure_body -> structure_body