diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 40 |
1 files changed, 24 insertions, 16 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 71e228b19c..e17fb1c38f 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -36,8 +36,6 @@ type ('a, 'b) declaration_arity = | RegularArity of 'a | TemplateArity of 'b -type constant_type = (types, Context.Rel.t * template_arity) declaration_arity - (** Inlining level of parameters at functor applications. None means no inlining *) @@ -64,7 +62,9 @@ type constant_def = | Def of constr Mod_subst.substituted (** or a transparent global definition *) | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) -type constant_universes = Univ.universe_context +type constant_universes = + | Monomorphic_const of Univ.universe_context + | Polymorphic_const of Univ.abstract_universe_context (** The [typing_flags] are instructions to the type-checker which modify its behaviour. The typing flags used in the type-checking @@ -81,9 +81,8 @@ type typing_flags = { type constant_body = { const_hyps : Context.Named.t; (** New: younger hyp at top *) const_body : constant_def; - const_type : constant_type; + const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; - const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; @@ -168,6 +167,11 @@ type one_inductive_body = { mind_reloc_tbl : Cbytecodes.reloc_table; } +type abstract_inductive_universes = + | Monomorphic_ind of Univ.universe_context + | Polymorphic_ind of Univ.abstract_universe_context + | Cumulative_ind of Univ.abstract_cumulativity_info + type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) @@ -186,9 +190,7 @@ type mutual_inductive_body = { mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) - mind_polymorphic : bool; (** Is it polymorphic or not *) - - mind_universes : Univ.universe_context; (** Local universe variables and constraints *) + mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) @@ -248,16 +250,16 @@ and module_implementation = | Struct of module_signature (** interactive body *) | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) -and module_body = +and 'a generic_module_body = { mod_mp : module_path; (** absolute path of the module *) - mod_expr : module_implementation; (** implementation *) + mod_expr : 'a; (** implementation *) mod_type : module_signature; (** expanded type *) mod_type_alg : module_expression option; (** algebraic type *) mod_constraints : Univ.ContextSet.t; (** set of all universes constraints in the module *) mod_delta : Mod_subst.delta_resolver; (** quotiented set of equivalent constants and inductive names *) - mod_retroknowledge : Retroknowledge.action list } + mod_retroknowledge : 'a module_retroknowledge } (** For a module, there are five possible situations: - [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T] @@ -267,13 +269,19 @@ and module_body = - [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. *) -(** A [module_type_body] is just a [module_body] with no - implementation ([mod_expr] always [Abstract]) and also - an empty [mod_retroknowledge]. Its [mod_type_alg] contains +and module_body = module_implementation generic_module_body + +(** A [module_type_body] is just a [module_body] with no implementation and + also an empty [mod_retroknowledge]. Its [mod_type_alg] contains the algebraic definition of this module type, or [None] if it has been built interactively. *) -and module_type_body = module_body +and module_type_body = unit generic_module_body + +and _ module_retroknowledge = +| ModBodyRK : + Retroknowledge.action list -> module_implementation module_retroknowledge +| ModTypeRK : unit module_retroknowledge (** Extra invariants : |