diff options
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 82 |
1 files changed, 51 insertions, 31 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 36455875..c4b00d0d 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Type definitions for the Calculus of Inductive Constructions *) @@ -81,7 +83,7 @@ type 'constr pfixpoint = type 'constr pcofixpoint = int * 'constr prec_declaration type 'a puniverses = 'a Univ.puniverses -type pconstant = constant puniverses +type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses @@ -102,7 +104,7 @@ type constr = | Case of case_info * constr * constr * constr array | Fix of constr pfixpoint | CoFix of constr pcofixpoint - | Proj of projection * constr + | Proj of Projection.t * constr type existential = constr pexistential type rec_declaration = constr prec_declaration @@ -127,12 +129,12 @@ type section_context = unit type delta_hint = | Inline of int * constr option - | Equiv of kernel_name + | Equiv of KerName.t -type delta_resolver = module_path MPmap.t * delta_hint KNmap.t +type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t type 'a umap_t = 'a MPmap.t * 'a MBImap.t -type substitution = (module_path * delta_resolver) umap_t +type substitution = (ModPath.t * delta_resolver) umap_t (** {6 Delayed constr} *) @@ -170,6 +172,17 @@ type set_predicativity = ImpredicativeSet | PredicativeSet type engagement = set_predicativity +(** {6 Conversion oracle} *) + +type level = Expand | Level of int | Opaque + +type oracle = { + var_opacity : level Id.Map.t; + cst_opacity : level Cmap.t; + var_trstate : Id.Pred.t; + cst_trstate : Cpred.t; +} + (** {6 Representation of constants (Definition/Axiom) } *) @@ -182,8 +195,6 @@ type ('a, 'b) declaration_arity = | RegularArity of 'a | TemplateArity of 'b -type constant_type = (constr, rel_context * template_arity) declaration_arity - (** Inlining level of parameters at functor applications. This is ignored by the checker. *) @@ -196,7 +207,7 @@ type inline = int option always transparent. *) type projection_body = { - proj_ind : mutual_inductive; + proj_ind : MutInd.t; proj_npars : int; proj_arg : int; proj_type : constr; (* Type under params *) @@ -209,7 +220,9 @@ type constant_def = | Def of constr_substituted | OpaqueDef of lazy_constr -type constant_universes = Univ.universe_context +type constant_universes = + | Monomorphic_const of Univ.ContextSet.t + | 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 @@ -219,14 +232,14 @@ type typing_flags = { check_guarded : bool; (** If [false] then fixed points and co-fixed points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) + conv_oracle : oracle; (** Unfolding strategies for conversion *) } type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; - const_type : constant_type; + const_type : constr; const_body_code : to_patch_substituted; - const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; @@ -242,7 +255,7 @@ type recarg = type wf_paths = recarg Rtree.t -type record_body = (Id.t * constant array * projection_body array) option +type record_body = (Id.t * Constant.t array * projection_body array) option (* The body is empty for non-primitive records, otherwise we get its binder name in projections and list of projections if it is primitive. *) @@ -303,6 +316,11 @@ type one_inductive_body = { mind_reloc_tbl : reloc_table; } +type abstract_inductive_universes = + | Monomorphic_ind of Univ.ContextSet.t + | 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 *) @@ -321,9 +339,7 @@ type mutual_inductive_body = { mind_params_ctxt : rel_context; (** 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; (** Local universe variables and constraints together with subtyping constraints *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) @@ -344,13 +360,11 @@ type ('ty,'a) functorize = and won't play any role into the kernel after that : they are kept only for short module printing and for extraction. *) -type with_declaration = - | WithMod of Id.t list * module_path - | WithDef of Id.t list * (constr * Univ.universe_context) +type with_declaration type module_alg_expr = - | MEident of module_path - | MEapply of module_alg_expr * module_path + | MEident of ModPath.t + | MEapply of module_alg_expr * ModPath.t | MEwith of module_alg_expr * with_declaration (** A component of a module structure *) @@ -383,9 +397,9 @@ and module_implementation = | Struct of module_signature (** interactive body *) | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) -and module_body = - { mod_mp : module_path; (** absolute path of the module *) - mod_expr : module_implementation; (** implementation *) +and 'a generic_module_body = + { mod_mp : ModPath.t; (** absolute path of the module *) + mod_expr : 'a; (** implementation *) mod_type : module_signature; (** expanded type *) (** algebraic type, kept if it's relevant for extraction *) mod_type_alg : module_expression option; @@ -393,13 +407,19 @@ and module_body = mod_constraints : Univ.ContextSet.t; (** quotiented set of equivalent constants and inductive names *) mod_delta : delta_resolver; - mod_retroknowledge : action list } + mod_retroknowledge : 'a module_retroknowledge; } + +and module_body = module_implementation generic_module_body (** A [module_type_body] is just a [module_body] with no - implementation ([mod_expr] always [Abstract]) and also - an empty [mod_retroknowledge] *) + implementation and also an empty [mod_retroknowledge] *) + +and module_type_body = unit generic_module_body -and module_type_body = module_body +and _ module_retroknowledge = +| ModBodyRK : + action list -> module_implementation module_retroknowledge +| ModTypeRK : unit module_retroknowledge (*************************************************************************) (** {4 From safe_typing.ml} *) |