diff options
author | Amin Timany <amintimany@gmail.com> | 2017-06-01 16:18:19 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:19 +0200 |
commit | ff918e4bb0ae23566e038f4b55d84dd2c343f95e (patch) | |
tree | ebab76cc4dedaf307f96088a3756d8292a341433 /kernel | |
parent | 3380f47d2bb38d549fcdac8fb073f9aa1f259a23 (diff) |
Clean up universes of constants and inductives
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/cbytegen.ml | 4 | ||||
-rw-r--r-- | kernel/cbytegen.mli | 2 | ||||
-rw-r--r-- | kernel/cooking.ml | 43 | ||||
-rw-r--r-- | kernel/cooking.mli | 3 | ||||
-rw-r--r-- | kernel/declarations.ml | 16 | ||||
-rw-r--r-- | kernel/declareops.ml | 124 | ||||
-rw-r--r-- | kernel/declareops.mli | 15 | ||||
-rw-r--r-- | kernel/entries.mli | 9 | ||||
-rw-r--r-- | kernel/environ.ml | 46 | ||||
-rw-r--r-- | kernel/environ.mli | 5 | ||||
-rw-r--r-- | kernel/indtypes.ml | 69 | ||||
-rw-r--r-- | kernel/indtypes.mli | 11 | ||||
-rw-r--r-- | kernel/inductive.ml | 10 | ||||
-rw-r--r-- | kernel/mod_typing.ml | 23 | ||||
-rw-r--r-- | kernel/modops.ml | 11 | ||||
-rw-r--r-- | kernel/modops.mli | 1 | ||||
-rw-r--r-- | kernel/nativecode.ml | 7 | ||||
-rw-r--r-- | kernel/opaqueproof.ml | 2 | ||||
-rw-r--r-- | kernel/opaqueproof.mli | 2 | ||||
-rw-r--r-- | kernel/reduction.ml | 67 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 79 | ||||
-rw-r--r-- | kernel/subtyping.ml | 87 | ||||
-rw-r--r-- | kernel/term_typing.ml | 97 | ||||
-rw-r--r-- | kernel/typeops.ml | 2 | ||||
-rw-r--r-- | kernel/univ.ml | 66 | ||||
-rw-r--r-- | kernel/univ.mli | 55 | ||||
-rw-r--r-- | kernel/vconv.ml | 50 |
27 files changed, 568 insertions, 338 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 57b397e6f..02c6a2c71 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -992,8 +992,8 @@ let compile_constant_body fail_on_error env univs = function let body = Mod_subst.force_constr sb in let instance_size = match univs with - | None -> 0 - | Some univ -> Univ.UContext.size univ + | Monomorphic_const _ -> 0 + | Polymorphic_const univ -> Univ.AUContext.size univ in match kind_of_term body with | Const (kn',u) when is_univ_copy instance_size u -> diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index c0f48641c..48c2e4533 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -10,7 +10,7 @@ val compile : bool -> (* Fail on error with a nice user message, otherwise simpl (** init, fun, fv *) val compile_constant_body : bool -> - env -> constant_universes option -> constant_def -> body_code option + env -> constant_universes -> constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 4deadff0a..000865364 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -153,8 +153,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * - bool * constant_universes * inline - * Context.Named.t option + constant_universes * inline * Context.Named.t option let on_body ml hy f = function | Undef _ as x -> x @@ -179,17 +178,21 @@ let cook_constr { Opaqueproof.modlist ; abstract } c = abstract_constant_body (expmod c) hyps let lift_univs cb subst = - if cb.const_polymorphic && not (Univ.LMap.is_empty subst) then - let inst = Univ.UContext.instance cb.const_universes in - let cstrs = Univ.UContext.constraints cb.const_universes in - let len = Univ.LMap.cardinal subst in - let subst = - Array.fold_left_i (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc) - subst (Univ.Instance.to_array inst) - in - let cstrs' = Univ.subst_univs_level_constraints subst cstrs in - subst, Univ.UContext.make (inst,cstrs') - else subst, cb.const_universes + match cb.const_universes with + | Monomorphic_const ctx -> subst, (Monomorphic_const ctx) + | Polymorphic_const auctx -> + if (Univ.LMap.is_empty subst) then + subst, (Polymorphic_const auctx) + else + let inst = Univ.AUContext.instance auctx in + let len = Univ.LMap.cardinal subst in + let subst = + Array.fold_left_i + (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc) + subst (Univ.Instance.to_array inst) + in + let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in + subst, (Polymorphic_const auctx') let cook_constant ~hcons env { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in @@ -243,15 +246,15 @@ let cook_constant ~hcons env { from = cb; info } = proj_eta = etab, etat; proj_type = ty'; proj_body = c' } in - let univs = - let abs' = - if cb.const_polymorphic then abs_ctx - else instantiate_univ_context abs_ctx - in - UContext.union abs' univs + let univs = + match univs with + | Monomorphic_const ctx -> + Monomorphic_const (UContext.union (instantiate_univ_context abs_ctx) ctx) + | Polymorphic_const auctx -> + Polymorphic_const (AUContext.union abs_ctx auctx) in (body, typ, Option.map projection cb.const_proj, - cb.const_polymorphic, univs, cb.const_inline_code, + univs, cb.const_inline_code, Some const_hyps) (* let cook_constant_key = Profile.declare_profile "cook_constant" *) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7d47eba23..9db85a4a1 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -18,8 +18,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * - bool * constant_universes * inline - * Context.Named.t option + constant_universes * inline * Context.Named.t option val cook_constant : hcons:bool -> env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr diff --git a/kernel/declarations.ml b/kernel/declarations.ml index ae4732456..f3b7ae2b2 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -64,7 +64,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 @@ -83,7 +85,6 @@ type constant_body = { const_body : constant_def; const_type : constant_type; 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 +169,11 @@ type one_inductive_body = { mind_reloc_tbl : Cbytecodes.reloc_table; } +type abstrac_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,11 +192,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_cumulative : bool; (** Is it cumulative or not *) - - mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *) + mind_universes : abstrac_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 1d91b2d41..72b490768 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -45,14 +45,15 @@ let hcons_template_arity ar = (** {6 Constants } *) let instantiate cb c = - if cb.const_polymorphic then - Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c - else c + match cb.const_universes with + | Monomorphic_const _ -> c + | Polymorphic_const ctx -> + Vars.subst_instance_constr (Univ.AUContext.instance ctx) c -let instantiate_constraints cb cst = - if cb.const_polymorphic then - Univ.subst_instance_constraints (Univ.UContext.instance cb.const_universes) cst - else cst +let constant_is_polymorphic cb = + match cb.const_universes with + | Monomorphic_const _ -> false + | Polymorphic_const _ -> true let body_of_constant otab cb = match cb.const_body with | Undef _ -> None @@ -67,34 +68,55 @@ let type_of_constant cb = | TemplateArity _ as x -> x let constraints_of_constant otab cb = - let cst = Univ.Constraint.union - (Univ.UContext.constraints cb.const_universes) - (match cb.const_body with - | Undef _ -> Univ.empty_constraint - | Def c -> Univ.empty_constraint - | OpaqueDef o -> - Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) - in instantiate_constraints cb cst + match cb.const_universes with + | Polymorphic_const ctx -> + Univ.UContext.constraints (Univ.instantiate_univ_context ctx) + | Monomorphic_const ctx -> + Univ.Constraint.union + (Univ.UContext.constraints ctx) + (match cb.const_body with + | Undef _ -> Univ.empty_constraint + | Def c -> Univ.empty_constraint + | OpaqueDef o -> + Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) let universes_of_constant otab cb = match cb.const_body with - | Undef _ | Def _ -> cb.const_universes + | Undef _ | Def _ -> + begin + match cb.const_universes with + | Monomorphic_const ctx -> ctx + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + end | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints otab o in - assert(not cb.const_polymorphic || Univ.ContextSet.is_empty body_uctxs); - let uctxs = Univ.ContextSet.of_context cb.const_universes in - Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) + let body_uctxs = Opaqueproof.force_constraints otab o in + match cb.const_universes with + | Monomorphic_const ctx -> + let uctxs = Univ.ContextSet.of_context ctx in + Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) + | Polymorphic_const ctx -> + assert(Univ.ContextSet.is_empty body_uctxs); + Univ.instantiate_univ_context ctx let universes_of_polymorphic_constant otab cb = - if cb.const_polymorphic then - let univs = universes_of_constant otab cb in - Univ.instantiate_univ_context univs - else Univ.UContext.empty + match cb.const_universes with + | Monomorphic_const _ -> Univ.UContext.empty + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx let constant_has_body cb = match cb.const_body with | Undef _ -> false | Def _ | OpaqueDef _ -> true +let constant_polymorphic_instance cb = + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.AUContext.instance ctx + +let constant_polymorphic_context cb = + match cb.const_universes with + | Monomorphic_const _ -> Univ.UContext.empty + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Undef _ | Def _ -> false @@ -142,7 +164,6 @@ let subst_const_body sub cb = const_proj = proj'; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; - const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -173,11 +194,18 @@ let hcons_const_def = function Def (from_val (Term.hcons_constr constr)) | OpaqueDef _ as x -> x (* hashconsed when turned indirect *) +let hcons_const_universes cbu = + match cbu with + | Monomorphic_const ctx -> + Monomorphic_const (Univ.hcons_universe_context ctx) + | Polymorphic_const ctx -> + Polymorphic_const (Univ.hcons_abstract_universe_context ctx) + let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; const_type = hcons_const_type cb.const_type; - const_universes = Univ.hcons_universe_context cb.const_universes } + const_universes = hcons_const_universes cb.const_universes } (** {6 Inductive types } *) @@ -266,22 +294,36 @@ let subst_mind_body sub mib = mind_params_ctxt = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_polymorphic = mib.mind_polymorphic; - mind_cumulative = mib.mind_cumulative; mind_universes = mib.mind_universes; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } -let inductive_instance mib = - if mib.mind_polymorphic then - Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) - else Univ.Instance.empty - -let inductive_context mib = - if mib.mind_polymorphic then - Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) - else Univ.UContext.empty +let inductive_polymorphic_instance mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind ctx -> Univ.AUContext.instance ctx + | Cumulative_ind cumi -> + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + +let inductive_polymorphic_context mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.UContext.empty + | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx + | Cumulative_ind cumi -> + Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) + +let inductive_is_polymorphic mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> true + | Cumulative_ind cumi -> true + +let inductive_is_cumulative mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> false + | Cumulative_ind cumi -> true (** {6 Hash-consing of inductive declarations } *) @@ -309,11 +351,17 @@ let hcons_mind_packet oib = mind_user_lc = user; mind_nf_lc = nf } +let hcons_mind_universes miu = + match miu with + | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx) + | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx) + | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui) + let hcons_mind mib = { mib with mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; - mind_universes = Univ.hcons_universe_info_ind mib.mind_universes } + mind_universes = hcons_mind_universes mib.mind_universes } (** {6 Stm machinery } *) diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 6650b6b7b..811a28aa6 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -27,6 +27,12 @@ val subst_const_body : substitution -> constant_body -> constant_body val constant_has_body : constant_body -> bool +val constant_polymorphic_instance : constant_body -> universe_instance +val constant_polymorphic_context : constant_body -> universe_context + +(** Is the constant polymorphic? *) +val constant_is_polymorphic : constant_body -> bool + (** Accessing const_body, forcing access to opaque proof term if needed. Only use this function if you know what you're doing. *) @@ -66,8 +72,13 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body -val inductive_instance : mutual_inductive_body -> universe_instance -val inductive_context : mutual_inductive_body -> universe_context +val inductive_polymorphic_instance : mutual_inductive_body -> universe_instance +val inductive_polymorphic_context : mutual_inductive_body -> universe_context + +(** Is the inductive polymorphic? *) +val inductive_is_polymorphic : mutual_inductive_body -> bool +(** Is the inductive cumulative? *) +val inductive_is_cumulative : mutual_inductive_body -> bool (** {6 Kernel flags} *) diff --git a/kernel/entries.mli b/kernel/entries.mli index 9c17346f2..f133587c1 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -34,6 +34,11 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; [mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]]. *) +type inductive_universes = + | Monomorphic_ind_entry of Univ.universe_context + | Polymorphic_ind_entry of Univ.universe_context + | Cumulative_ind_entry of Univ.cumulativity_info + type one_inductive_entry = { mind_entry_typename : Id.t; mind_entry_arity : constr; @@ -49,9 +54,7 @@ type mutual_inductive_entry = { mind_entry_finite : Decl_kinds.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; - mind_entry_polymorphic : bool; - mind_entry_cumulative : bool; - mind_entry_universes : Univ.universe_info_ind; + mind_entry_universes : inductive_universes; (* universe constraints and the constraints for subtyping of inductive types in the block. *) mind_entry_private : bool option; diff --git a/kernel/environ.ml b/kernel/environ.ml index 5727bf2ea..1ab5b7a8d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -228,8 +228,10 @@ let add_constant kn cb env = add_constant_key kn cb no_link_info env let constraints_of cb u = - let univs = cb.const_universes in - Univ.subst_instance_constraints u (Univ.UContext.constraints univs) + match cb.const_universes with + | Monomorphic_const _ -> Univ.Constraint.empty + | Polymorphic_const ctx -> + Univ.UContext.constraints (Univ.subst_instance_context u ctx) let map_regular_arity f = function | RegularArity a as ar -> @@ -240,15 +242,23 @@ let map_regular_arity f = function (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then - let csts = constraints_of cb u in - (map_regular_arity (subst_instance_constr u) cb.const_type, csts) - else cb.const_type, Univ.Constraint.empty + match cb.const_universes with + | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty + | Polymorphic_const ctx -> + let csts = constraints_of cb u in + (map_regular_arity (subst_instance_constr u) cb.const_type, csts) + +let constant_instance env kn = + let cb = lookup_constant kn env in + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.AUContext.instance ctx let constant_context env kn = let cb = lookup_constant kn env in - if cb.const_polymorphic then cb.const_universes - else Univ.UContext.empty + match cb.const_universes with + | Monomorphic_const _ -> Univ.UContext.empty + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx type const_evaluation_result = NoBody | Opaque | IsProj @@ -259,10 +269,14 @@ let constant_value env (kn,u) = if cb.const_proj = None then match cb.const_body with | Def l_body -> - if cb.const_polymorphic then - let csts = constraints_of cb u in - (subst_instance_constr u (Mod_subst.force_constr l_body), csts) - else Mod_subst.force_constr l_body, Univ.Constraint.empty + begin + match cb.const_universes with + | Monomorphic_const _ -> + (Mod_subst.force_constr l_body, Univ.Constraint.empty) + | Polymorphic_const _ -> + let csts = constraints_of cb u in + (subst_instance_constr u (Mod_subst.force_constr l_body), csts) + end | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) else raise (NotEvaluableConst IsProj) @@ -273,7 +287,7 @@ let constant_opt_value env cst = let constant_value_and_type env (kn, u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then + if Declareops.constant_is_polymorphic cb then let cst = constraints_of cb u in let b' = match cb.const_body with | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body)) @@ -295,7 +309,7 @@ let constant_value_and_type env (kn, u) = (* constant_type gives the type of a constant *) let constant_type_in env (kn,u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then + if Declareops.constant_is_polymorphic cb then map_regular_arity (subst_instance_constr u) cb.const_type else cb.const_type @@ -321,7 +335,7 @@ let evaluable_constant kn env = | Undef _ -> false let polymorphic_constant cst env = - (lookup_constant cst env).const_polymorphic + Declareops.constant_is_polymorphic (lookup_constant cst env) let polymorphic_pconstant (cst,u) env = if Univ.Instance.is_empty u then false @@ -353,7 +367,7 @@ let is_projection cst env = let lookup_mind = lookup_mind let polymorphic_ind (mind,i) env = - (lookup_mind mind env).mind_polymorphic + Declareops.inductive_is_polymorphic (lookup_mind mind env) let polymorphic_pind (ind,u) env = if Univ.Instance.is_empty u then false diff --git a/kernel/environ.mli b/kernel/environ.mli index b7431dbe5..ae3afcb35 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -161,6 +161,9 @@ val constant_value_and_type : env -> constant puniverses -> (** The universe context associated to the constant, empty if not polymorphic *) val constant_context : env -> constant -> Univ.universe_context +(** The universe isntance associated to the constant, empty if not + polymorphic *) +val constant_instance : env -> constant -> Univ.universe_instance (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant @@ -256,7 +259,7 @@ type unsafe_type_judgment = types punsafe_type_judgment (** {6 Compilation of global declaration } *) -val compile_constant_body : env -> constant_universes option -> constant_def -> Cemitcodes.body_code option +val compile_constant_body : env -> constant_universes -> constant_def -> Cemitcodes.body_code option exception Hyp_not_found diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5cfcbba60..00fbe27a7 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -231,23 +231,23 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter (* Check that the subtyping information inferred for inductive types in the block is correct. *) (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) -let check_subtyping mie paramsctxt env_ar inds = +let check_subtyping cumi paramsctxt env_ar inds = let numparams = Context.Rel.nhyps paramsctxt in - let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in + let sbsubst = CumulativityInfo.subtyping_susbst cumi in let dosubst = subst_univs_level_constr sbsubst in - let uctx = UInfoInd.univ_context mie.mind_entry_universes in + let uctx = CumulativityInfo.univ_context cumi in let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env' = Environ.push_context uctx env_ar in - let env'' = Environ.push_context uctx_other env' in - let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in + let env = Environ.push_context uctx env_ar in + let env = Environ.push_context uctx_other env in + let env = push_context (CumulativityInfo.subtyp_context cumi) env in (* process individual inductive types: *) Array.iter (fun (id,cn,lc,(sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> - check_subtyping_arity_constructor envsb dosubst full_arity numparams true; - Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc + check_subtyping_arity_constructor env dosubst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc | TemplateArity _ -> () ) inds @@ -264,7 +264,13 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let env' = push_context (Univ.UInfoInd.univ_context mie.mind_entry_universes) env in + let univctx = + match mie.mind_entry_universes with + | Monomorphic_ind_entry ctx -> ctx + | Polymorphic_ind_entry ctx -> ctx + | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi + in + let env' = push_context univctx env in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) @@ -383,16 +389,21 @@ let typecheck_inductive env mie = | _ (* Not an explicit occurrence of Type *) -> full_polymorphic () in - let arity = - if mie.mind_entry_polymorphic then full_polymorphic () - else template_polymorphic () + let arity = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ -> template_polymorphic () + | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> full_polymorphic () in (id,cn,lc,(sign,arity))) inds in (* Check that the subtyping information inferred for inductive types in the block is correct. *) (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) - let () = if mie.mind_entry_cumulative then check_subtyping mie paramsctxt env_arities inds + let () = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ -> () + | Polymorphic_ind_entry _ -> () + | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) @@ -864,14 +875,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs = +let abstract_inductive_universes iu = + match iu with + | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) + | Polymorphic_ind_entry ctx -> + let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx) + | Cumulative_ind_entry cumi -> + let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi) + +let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in let nparamargs = Context.Rel.nhyps paramsctxt in let nparamsctxt = Context.Rel.length paramsctxt in - let substunivs, ctxunivs = Univ.abstract_universes p (Univ.UInfoInd.univ_context ctx) in - let substsubtyp, ctxsubtyp = Univ.abstract_universes p (Univ.UInfoInd.subtyp_context ctx) in + let substunivs, aiu = abstract_inductive_universes iu in let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in let env_ar = let ctxunivs = Environ.rel_context env_ar in @@ -942,10 +960,14 @@ let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite ind && Array.length pkt.mind_consnames == 1 && pkt.mind_consnrealargs.(0) > 0 -> (** The elimination criterion ensures that all projections can be defined. *) - let u = - if p then - subst_univs_level_instance substunivs (Univ.UContext.instance ctxunivs) - else Univ.Instance.empty + let u = + let process auctx = + subst_univs_level_instance substunivs (Univ.AUContext.instance auctx) + in + match aiu with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx -> process auctx + | Cumulative_ind acumi -> process (Univ.ACumulativityInfo.univ_context acumi) in let indsp = ((kn, 0), u) in let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in @@ -968,9 +990,7 @@ let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite ind mind_nparams_rec = nmr; mind_params_ctxt = paramsctxt; mind_packets = packets; - mind_polymorphic = p; - mind_cumulative = cum; - mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp); + mind_universes = aiu; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } @@ -985,7 +1005,6 @@ let check_inductive env kn mie = let chkpos = (Environ.typing_flags env).check_guarded in let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in (* Build the inductive packets *) - build_inductive env mie.mind_entry_cumulative mie.mind_entry_polymorphic mie.mind_entry_private - mie.mind_entry_universes + build_inductive env mie.mind_entry_private mie.mind_entry_universes env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 7b0f01794..5b4615399 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -32,17 +32,6 @@ type inductive_error = exception InductiveError of inductive_error -val check_subtyping_arity_constructor : Environ.env -> -(Term.constr -> Term.constr) -> Term.types -> int -> bool -> unit - -(* This needs not be exposed. Exposing for debugging purposes! *) -val check_subtyping : Entries.mutual_inductive_entry -> -Context.Rel.t -> -Environ.env -> -('b * 'c * Term.types array * - ('d * ('e * Term.types * 'f, 'g) Declarations.declaration_arity)) -array -> unit - (** The following function does checks on inductive declarations. *) val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 0f0dc0d60..e81a1cb58 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -54,9 +54,13 @@ let inductive_paramdecls (mib,u) = Vars.subst_instance_context u mib.mind_params_ctxt let instantiate_inductive_constraints mib u = - if mib.mind_polymorphic then - Univ.subst_instance_constraints u (Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes)) - else Univ.Constraint.empty + let process auctx = + Univ.UContext.constraints (Univ.subst_instance_context u auctx) + in + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Constraint.empty + | Polymorphic_ind auctx -> process auctx + | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) (************************************************************************) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index ff44f0f54..79016735b 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -74,12 +74,13 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = as long as they have the right type *) let uctx = Declareops.universes_of_constant (opaque_tables env) cb in let uctx = (* Context of the spec *) - if cb.const_polymorphic then - Univ.instantiate_univ_context uctx - else uctx + match cb.const_universes with + | Monomorphic_const _ -> uctx + | Polymorphic_const auctx -> + Univ.instantiate_univ_context auctx in let c', univs, ctx' = - if not cb.const_polymorphic then + if not (Declareops.constant_is_polymorphic cb) then let env' = Environ.push_context ~strict:true uctx env' in let env' = Environ.push_context ~strict:true ctx env' in let c',cst = match cb.const_body with @@ -92,7 +93,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = | Def cs -> let c' = Mod_subst.force_constr cs in c, Reduction.infer_conv env' (Environ.universes env') c c' - in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) + in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) else let cus, ccst = Univ.UContext.dest uctx in let newus, cst = Univ.UContext.dest ctx in @@ -122,21 +123,17 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = in if not (Univ.Constraint.is_empty cst) then error_incorrect_with_constraint lab; - let subst, ctx = Univ.abstract_universes true ctx in - Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty + let subst, ctx = Univ.abstract_universes ctx in + Vars.subst_univs_level_constr subst c, Polymorphic_const ctx, Univ.ContextSet.empty in let def = Def (Mod_subst.from_val c') in (* let ctx' = Univ.UContext.make (newus, cst) in *) - let univs = - if cb.const_polymorphic then Some cb.const_universes - else None - in let cb' = { cb with const_body = def; - const_universes = ctx ; + const_universes = univs ; const_body_code = Option.map Cemitcodes.from_val - (compile_constant_body env' univs def) } + (compile_constant_body env' cb.const_universes def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else diff --git a/kernel/modops.ml b/kernel/modops.ml index 1f8b97ae6..33d13f1ba 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -35,6 +35,7 @@ type signature_mismatch_error = | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField | NotConvertibleTypeField of env * types * types + | CumulativeStatusExpected of bool | PolymorphicStatusExpected of bool | NotSameConstructorNamesField | NotSameInductiveNameInBlockField @@ -327,12 +328,10 @@ let strengthen_const mp_from l cb resolver = |_ -> let kn = KerName.make2 mp_from l in let con = constant_of_delta_kn resolver kn in - let u = - if cb.const_polymorphic then - let u = Univ.UContext.instance cb.const_universes in - let s = Univ.make_instance_subst u in - Univ.subst_univs_level_instance s u - else Univ.Instance.empty + let u = + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.make_abstract_instance ctx in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); diff --git a/kernel/modops.mli b/kernel/modops.mli index e9f3db6e9..4b533c7ef 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -94,6 +94,7 @@ type signature_mismatch_error = | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField | NotConvertibleTypeField of env * types * types + | CumulativeStatusExpected of bool | PolymorphicStatusExpected of bool | NotSameConstructorNamesField | NotSameInductiveNameInBlockField diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d3cd6b62a..4941d64d8 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1863,8 +1863,9 @@ let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with | None -> let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes - else Univ.Instance.empty + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.AUContext.instance ctx in begin match cb.const_body with | Def t -> @@ -1960,7 +1961,7 @@ let param_name = Name (id_of_string "params") let arg_name = Name (id_of_string "arg") let compile_mind prefix ~interactive mb mind stack = - let u = Declareops.inductive_instance mb in + let u = Declareops.inductive_polymorphic_instance mb in let f i stack ob = let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in let j = push_symbol (SymbInd (mind,i)) in diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 59e90ca2e..3e15ff740 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } + abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } type proofterm = (constr * Univ.universe_context_set) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 3897d5e51..be1f4b13f 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -49,7 +49,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } + abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } (* The type has two caveats: 1) cook_constr is defined after diff --git a/kernel/reduction.ml b/kernel/reduction.ml index ea583fdac..8bf95e5de 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -497,11 +497,12 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if eq_ind ind1 ind2 then let mind = Environ.lookup_mind (fst ind1) env in let cuniv = - if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + convert_instances ~flex:false u1 u2 cuniv + | Declarations.Cumulative_ind cumi -> convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1) u2 (CClosure.stack_args_size v2) cuniv - else - convert_instances ~flex:false u1 u2 cuniv in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible @@ -510,12 +511,13 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if Int.equal j1 j2 && eq_ind ind1 ind2 then let mind = Environ.lookup_mind (fst ind1) env in let cuniv = - if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + convert_instances ~flex:false u1 u2 cuniv + | Declarations.Cumulative_ind _ -> convert_constructors (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1) u2 (CClosure.stack_args_size v2) cuniv - else - convert_instances ~flex:false u1 u2 cuniv in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible @@ -637,22 +639,26 @@ let infer_check_conv_inductives infer_check_convert_instances infer_check_inductive_instances cv_pb (mind, ind) u1 sv1 u2 sv2 univs = - if mind.Declarations.mind_polymorphic then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + infer_check_convert_instances ~flex:false u1 u2 univs + | Declarations.Cumulative_ind cumi -> let num_param_arity = mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs in if not (num_param_arity = sv1 && num_param_arity = sv2) then infer_check_convert_instances ~flex:false u1 u2 univs else - let uinfind = mind.Declarations.mind_universes in - infer_check_inductive_instances cv_pb uinfind u1 u2 univs - else infer_check_convert_instances ~flex:false u1 u2 univs + infer_check_inductive_instances cv_pb cumi u1 u2 univs let infer_check_conv_constructors infer_check_convert_instances infer_check_inductive_instances (mind, ind, cns) u1 sv1 u2 sv2 univs = - if mind.Declarations.mind_polymorphic then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + infer_check_convert_instances ~flex:false u1 u2 univs + | Declarations.Cumulative_ind cumi -> let num_cnstr_args = let nparamsctxt = mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs @@ -662,26 +668,30 @@ let infer_check_conv_constructors if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then infer_check_convert_instances ~flex:false u1 u2 univs else - let uinfind = mind.Declarations.mind_universes in - infer_check_inductive_instances CONV uinfind u1 u2 univs - else infer_check_convert_instances ~flex:false u1 u2 univs + infer_check_inductive_instances CONV cumi u1 u2 univs -let check_inductive_instances cv_pb uinfind u u' univs = - let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in - let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in +let check_inductive_instances cv_pb cumi u u' univs = + let ind_instance = + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + in + let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.subst_instance_constraints comp_subst ind_sbcst + Univ.UContext.constraints + (Univ.subst_instance_context comp_subst ind_subtypctx) in let comp_cst = match cv_pb with CONV -> - let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in + let comp_cst' = + let comp_subst = (Univ.Instance.append u' u) in + Univ.UContext.constraints + (Univ.subst_instance_context comp_subst ind_subtypctx) + in Univ.Constraint.union comp_cst comp_cst' | CUMUL -> comp_cst in @@ -746,22 +756,27 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = else Univ.enforce_eq_instances u u' cstrs in (univs, cstrs') -let infer_inductive_instances cv_pb uinfind u u' (univs, cstrs) = - let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in - let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in +let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) = + let ind_instance = + Univ.AUContext.instance (Univ.ACumulativityInfo.subtyp_context cumi) + in + let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.subst_instance_constraints comp_subst ind_sbcst + Univ.UContext.constraints + (Univ.subst_instance_context comp_subst ind_subtypctx) in let comp_cst = match cv_pb with CONV -> - let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in + let comp_cst' = + let comp_subst = (Univ.Instance.append u' u) in + Univ.UContext.constraints + (Univ.subst_instance_context comp_subst ind_subtypctx) in Univ.Constraint.union comp_cst comp_cst' | CUMUL -> comp_cst in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 1568fe0bf..946222ef2 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -237,20 +237,29 @@ let private_con_of_scheme ~kind env cl = let universes_of_private eff = let open Declarations in - List.fold_left (fun acc { Entries.eff } -> - match eff with - | Entries.SEscheme (l,s) -> - List.fold_left (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (_, ctx) -> ctx :: acc in - if cb.const_polymorphic then acc - else (Univ.ContextSet.of_context cb.const_universes) :: acc) - acc l - | Entries.SEsubproof (c, cb, e) -> - if cb.const_polymorphic then acc - else Univ.ContextSet.of_context cb.const_universes :: acc) - [] (Term_typing.uniq_seff eff) + List.fold_left + (fun acc { Entries.eff } -> + match eff with + | Entries.SEscheme (l,s) -> + List.fold_left + (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (_, ctx) -> ctx :: acc + in + match cb.const_universes with + | Monomorphic_const ctx -> + (Univ.ContextSet.of_context ctx) :: acc + | Polymorphic_const _ -> acc + ) + acc l + | Entries.SEsubproof (c, cb, e) -> + match cb.const_universes with + | Monomorphic_const ctx -> + (Univ.ContextSet.of_context ctx) :: acc + | Polymorphic_const _ -> acc + ) + [] (Term_typing.uniq_seff eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -373,7 +382,11 @@ let safe_push_named d env = let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in + let c,typ,univs = + match Term_typing.translate_local_def senv.revstruct senv.env id de with + | c, typ, Monomorphic_const ctx -> c, typ, ctx + | _, _, Polymorphic_const _ -> assert false + in let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with @@ -410,26 +423,28 @@ let labels_of_mib mib = get () let globalize_constant_universes env cb = - if cb.const_polymorphic then - [Now (true, Univ.ContextSet.empty)] - else - let cstrs = Univ.ContextSet.of_context cb.const_universes in - Now (false, cstrs) :: - (match cb.const_body with - | (Undef _ | Def _) -> [] - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with - | None -> [] - | Some fc -> + match cb.const_universes with + | Monomorphic_const ctx -> + let cstrs = Univ.ContextSet.of_context ctx in + Now (false, cstrs) :: + (match cb.const_body with + | (Undef _ | Def _) -> [] + | OpaqueDef lc -> + match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with + | None -> [] + | Some fc -> match Future.peek_val fc with - | None -> [Later fc] - | Some c -> [Now (false, c)]) + | None -> [Later fc] + | Some c -> [Now (false, c)]) + | Polymorphic_const _ -> + [Now (true, Univ.ContextSet.empty)] let globalize_mind_universes mb = - if mb.mind_polymorphic then - [Now (true, Univ.ContextSet.empty)] - else - [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))] + match mb.mind_universes with + | Monomorphic_ind ctx -> + [Now (false, Univ.ContextSet.of_context ctx)] + | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)] + | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)] let constraints_of_sfb env sfb = match sfb with diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 60e630a6d..1bd9d6e49 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -104,15 +104,21 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 | IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib | _ -> error (InductiveFieldExpected mib2) in - let poly = - if not (mib1.mind_polymorphic == mib2.mind_polymorphic) then - error (PolymorphicStatusExpected mib2.mind_polymorphic) - else mib2.mind_polymorphic - in - let u = - if poly then - CErrors.user_err Pp.(str "Checking of subtyping of polymorphic inductive types not implemented") - else Instance.empty + let u = + let process inst inst' = + if Univ.Instance.equal inst inst' then inst else error IncompatibleInstances + in + match mib1.mind_universes, mib2.mind_universes with + | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx, Polymorphic_ind auctx' -> + process + (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx') + | Cumulative_ind cumi, Cumulative_ind cumi' -> + process + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi')) + | _ -> error + (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2)) in let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name env t1 t2 = @@ -148,7 +154,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 error (NotConvertibleInductiveField name) | _ -> (s1, s2) in check_conv (NotConvertibleInductiveField name) - cst poly u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) + cst (inductive_is_polymorphic mib1) u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) in let check_packet cst p1 p2 = @@ -176,7 +182,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let check_cons_types i cst p1 p2 = Array.fold_left3 (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst - poly u infer_conv env t1 t2) + (inductive_is_polymorphic mib1) u infer_conv env t1 t2) cst p2.mind_consnames (arities_of_specif (mind,u) (mib1,p1)) @@ -293,37 +299,42 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let cb2 = Declareops.subst_const_body subst2 cb2 in (* Start by checking universes *) let poly = - if not (cb1.const_polymorphic == cb2.const_polymorphic) then - error (PolymorphicStatusExpected cb2.const_polymorphic) - else cb2.const_polymorphic + if not (Declareops.constant_is_polymorphic cb1 + == Declareops.constant_is_polymorphic cb2) then + error (PolymorphicStatusExpected (Declareops.constant_is_polymorphic cb2)) + else Declareops.constant_is_polymorphic cb2 in - let cst', env', u = - if poly then - let ctx1 = Univ.instantiate_univ_context cb1.const_universes in - let ctx2 = Univ.instantiate_univ_context cb2.const_universes in - let inst1, ctx1 = Univ.UContext.dest ctx1 in - let inst2, ctx2 = Univ.UContext.dest ctx2 in + let cst', env', u = + match cb1.const_universes, cb2.const_universes with + | Monomorphic_const _, Monomorphic_const _ -> + cst, env, Univ.Instance.empty + | Polymorphic_const auctx1, Polymorphic_const auctx2 -> + begin + let ctx1 = Univ.instantiate_univ_context auctx1 in + let ctx2 = Univ.instantiate_univ_context auctx2 in + let inst1, ctx1 = Univ.UContext.dest ctx1 in + let inst2, ctx2 = Univ.UContext.dest ctx2 in if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then error IncompatibleInstances else let cstrs = Univ.enforce_eq_instances inst1 inst2 cst in let cstrs = Univ.Constraint.union cstrs ctx2 in - try - (* The environment with the expected universes plus equality - of the body instances with the expected instance *) - let ctxi = Univ.Instance.append inst1 inst2 in - let ctx = Univ.UContext.make (ctxi, cstrs) in - let env = Environ.push_context ctx env in - (* Check that the given definition does not add any constraint over - the expected ones, so that it can be used in place of - the original. *) - if UGraph.check_constraints ctx1 (Environ.universes env) then - cstrs, env, inst2 - else error (IncompatibleConstraints ctx1) - with Univ.UniverseInconsistency incon -> - error (IncompatibleUniverses incon) - else - cst, env, Univ.Instance.empty + try + (* The environment with the expected universes plus equality + of the body instances with the expected instance *) + let ctxi = Univ.Instance.append inst1 inst2 in + let ctx = Univ.UContext.make (ctxi, cstrs) in + let env = Environ.push_context ctx env in + (* Check that the given definition does not add any constraint over + the expected ones, so that it can be used in place of + the original. *) + if UGraph.check_constraints ctx1 (Environ.universes env) then + cstrs, env, inst2 + else error (IncompatibleConstraints ctx1) + with Univ.UniverseInconsistency incon -> + error (IncompatibleUniverses incon) + end + | _ -> assert false in (* Now check types *) let typ1 = Typeops.type_of_constant_type env' cb1.const_type in @@ -354,7 +365,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "name.")); let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; - let u1 = inductive_instance mind1 in + let u1 = inductive_polymorphic_instance mind1 in let arity1,cst1 = constrained_type_of_inductive env ((mind1,mind1.mind_packets.(i)),u1) in let cst2 = @@ -371,7 +382,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "name.")); let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; - let u1 = inductive_instance mind1 in + let u1 = inductive_polymorphic_instance mind1 in let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in let cst2 = Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3cf2299d8..5370bcea4 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -121,18 +121,19 @@ let inline_side_effects env body ctx side_eff = | OpaqueDef _, `Opaque (b,_) -> (b, true) | _ -> assert false in - if cb.const_polymorphic then - (** Inline the term to emulate universe polymorphism *) - let data = (Univ.UContext.instance cb.const_universes, b) in - let subst = Cmap_env.add c (Inl data) subst in - (subst, var, ctx, args) - else + match cb.const_universes with + | Monomorphic_const cnstctx -> (** Abstract over the term at the top of the proof *) let ty = Typeops.type_of_constant_type env cb.const_type in let subst = Cmap_env.add c (Inr var) subst in - let univs = Univ.ContextSet.of_context cb.const_universes in + let univs = Univ.ContextSet.of_context cnstctx in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) + | Polymorphic_const auctx -> + (** Inline the term to emulate universe polymorphism *) + let data = (Univ.AUContext.instance auctx, b) in + let subst = Cmap_env.add c (Inl data) subst in + (subst, var, ctx, args) in let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in (** Third step: inline the definitions *) @@ -225,16 +226,25 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> feedback ~id:state_id Feedback.Complete) +let abstract_constant_universes abstract uctx = + if not abstract then + Univ.empty_level_subst, Monomorphic_const uctx + else + let sbst, auctx = Univ.abstract_universes uctx in + sbst, Polymorphic_const auctx + let infer_declaration ~trust env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in let j = infer env t in let abstract = poly && not (Option.is_empty kn) in - let usubst, univs = Univ.abstract_universes abstract uctx in + let usubst, univs = + abstract_constant_universes abstract uctx + in let c = Typeops.assumption_of_judgment env j in let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in - Undef nl, RegularArity t, None, poly, univs, false, ctx + Undef nl, RegularArity t, None, univs, false, ctx (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. @@ -264,9 +274,9 @@ let infer_declaration ~trust env kn dcl = feedback_completion_typecheck feedback_id; c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in - def, RegularArity typ, None, c.const_entry_polymorphic, - c.const_entry_universes, - c.const_entry_inline_code, c.const_entry_secctx + def, RegularArity typ, None, + (Monomorphic_const c.const_entry_universes), + c.const_entry_inline_code, c.const_entry_secctx (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> @@ -279,7 +289,8 @@ let infer_declaration ~trust env kn dcl = let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in let usubst, univs = - Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in + abstract_constant_universes abstract (Univ.ContextSet.to_context ctx) + in let j = infer env body in let typ = match typ with | None -> @@ -298,8 +309,7 @@ let infer_declaration ~trust env kn dcl = else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; - def, typ, None, c.const_entry_polymorphic, - univs, c.const_entry_inline_code, c.const_entry_secctx + def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> let mib, _ = Inductive.lookup_mind_specif env (ind,0) in @@ -311,9 +321,16 @@ let infer_declaration ~trust env kn dcl = else assert false | _ -> assert false in + let univs = + match mib.mind_universes with + | Monomorphic_ind ctx -> Monomorphic_const ctx + | Polymorphic_ind auctx -> Polymorphic_const auctx + | Cumulative_ind acumi -> + Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) + in let term, typ = pb.proj_eta in Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, - mib.mind_polymorphic, Univ.UInfoInd.univ_context mib.mind_universes, false, None + univs, false, None let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t @@ -337,7 +354,7 @@ let record_aux env s_ty s_bo suggested_expr = let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = +let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in @@ -409,9 +426,8 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) check declared inferred) lc) in let tps = let res = - let comp_univs = if poly then Some univs else None in match proj with - | None -> compile_constant_body env comp_univs def + | None -> compile_constant_body env univs def | Some pb -> (* The compilation of primitive projections is a bit tricky, because they refer to themselves (the body of p looks like fun c => @@ -425,14 +441,13 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_type = typ; const_proj = proj; const_body_code = None; - const_polymorphic = poly; const_universes = univs; const_inline_code = inline_code; const_typing_flags = Environ.typing_flags env; } in let env = add_constant kn cb env in - compile_constant_body env comp_univs def + compile_constant_body env univs def in Option.map Cemitcodes.from_val res in { const_hyps = hyps; @@ -440,7 +455,6 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_type = typ; const_proj = proj; const_body_code = tps; - const_polymorphic = poly; const_universes = univs; const_inline_code = inline_code; const_typing_flags = Environ.typing_flags env } @@ -452,6 +466,12 @@ let translate_constant mb env kn ce = (infer_declaration ~trust:mb env (Some kn) ce) let constant_entry_of_side_effect cb u = + let poly, univs = + match cb.const_universes with + | Monomorphic_const ctx -> false, ctx + | Polymorphic_const auctx -> + true, Univ.instantiate_univ_context auctx + in let pt = match cb.const_body, u with | OpaqueDef _, `Opaque (b, c) -> b, c @@ -463,8 +483,8 @@ let constant_entry_of_side_effect cb u = const_entry_feedback = None; const_entry_type = (match cb.const_type with RegularArity t -> Some t | _ -> None); - const_entry_polymorphic = cb.const_polymorphic; - const_entry_universes = cb.const_universes; + const_entry_polymorphic = poly; + const_entry_universes = univs; const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } ;; @@ -508,16 +528,23 @@ let export_side_effects mb env ce = let trusted = check_signatures mb signatures in let push_seff env = function | kn, cb, `Nothing, _ -> - let env = Environ.add_constant kn cb env in - if not cb.const_polymorphic then - Environ.push_context ~strict:true cb.const_universes env - else env - | kn, cb, `Opaque(_, ctx), _ -> - let env = Environ.add_constant kn cb env in - if not cb.const_polymorphic then - let env = Environ.push_context ~strict:true cb.const_universes env in - Environ.push_context_set ~strict:true ctx env - else env in + begin + let env = Environ.add_constant kn cb env in + match cb.const_universes with + | Monomorphic_const ctx -> + Environ.push_context ~strict:true ctx env + | Polymorphic_const _ -> env + end + | kn, cb, `Opaque(_, ctx), _ -> + begin + let env = Environ.add_constant kn cb env in + match cb.const_universes with + | Monomorphic_const cstctx -> + let env = Environ.push_context ~strict:true cstctx env in + Environ.push_context_set ~strict:true ctx env + | Polymorphic_const _ -> env + end + in let rec translate_seff sl seff acc env = match sl, seff with | _, [] -> List.rev acc, ce @@ -553,7 +580,7 @@ let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) let translate_local_def mb env id centry = - let def,typ,proj,poly,univs,inline_code,ctx = + let def,typ,proj,univs,inline_code,ctx = infer_declaration ~trust:mb env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 1a07bb2fc..e08f3362d 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -555,7 +555,7 @@ let type_of_projection_constant env (p,u) = let cb = lookup_constant cst env in match cb.const_proj with | Some pb -> - if cb.const_polymorphic then + if Declareops.constant_is_polymorphic cb then Vars.subst_instance_constr u pb.proj_type else pb.proj_type | None -> raise (Invalid_argument "type_of_projection: not a projection") diff --git a/kernel/univ.ml b/kernel/univ.ml index eb45f022e..8cbb20a05 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1031,7 +1031,13 @@ end type universe_context = UContext.t let hcons_universe_context = UContext.hcons -(** Universe info for inductive types: A context of universe levels +module AUContext = UContext + +type abstract_universe_context = AUContext.t +let hcons_abstract_universe_context = AUContext.hcons + +(** Universe info for cumulative inductive types: + A context of universe levels with universe constraints, representing local universe variables and constraints, together with a context of universe levels with universe constraints, representing conditions for subtyping used @@ -1040,7 +1046,7 @@ let hcons_universe_context = UContext.hcons This data structure maintains the invariant that the context for subtyping constraints is exactly twice as big as the context for universe constraints. *) -module UInfoInd = +module CumulativityInfo = struct type t = universe_context * universe_context @@ -1093,8 +1099,13 @@ struct end -type universe_info_ind = UInfoInd.t -let hcons_universe_info_ind = UInfoInd.hcons +type cumulativity_info = CumulativityInfo.t +let hcons_cumulativity_info = CumulativityInfo.hcons + +module ACumulativityInfo = CumulativityInfo + +type abstract_cumulativity_info = ACumulativityInfo.t +let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons (** A set of universes with universe constraints. We linearize the set to a list after typechecking. @@ -1200,6 +1211,9 @@ let subst_univs_level_constraints subst csts = (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c)) csts Constraint.empty +let subst_univs_level_abstract_universe_context subst (inst, csts) = + inst, subst_univs_level_constraints subst csts + (** With level to universe substitutions. *) type universe_subst_fn = universe_level -> universe @@ -1272,12 +1286,9 @@ let instantiate_univ_context (ctx, csts) = (ctx, subst_instance_constraints ctx csts) (** Substitute instance inst for ctx in universe constraints and subtyping constraints *) -let instantiate_univ_info_ind (univcst, subtpcst) = +let instantiate_cumulativity_info (univcst, subtpcst) = (instantiate_univ_context univcst, instantiate_univ_context subtpcst) -let instantiate_univ_constraints u (_, csts) = - subst_instance_constraints u csts - let make_instance_subst i = let arr = Instance.to_array i in Array.fold_left_i (fun i acc l -> @@ -1290,16 +1301,22 @@ let make_inverse_instance_subst i = LMap.add (Level.var i) l acc) LMap.empty arr -let abstract_universes poly ctx = +let make_abstract_instance (ctx, _) = + Array.mapi (fun i l -> Level.var i) ctx + +let abstract_universes ctx = let instance = UContext.instance ctx in - if poly then - let subst = make_instance_subst instance in - let cstrs = subst_univs_level_constraints subst - (UContext.constraints ctx) - in - let ctx = UContext.make (instance, cstrs) in - subst, ctx - else empty_level_subst, ctx + let subst = make_instance_subst instance in + let cstrs = subst_univs_level_constraints subst + (UContext.constraints ctx) + in + let ctx = UContext.make (instance, cstrs) in + subst, ctx + +let abstract_cumulativity_info (univcst, substcst) = + let instance, univcst = abstract_universes univcst in + let _, substcst = abstract_universes substcst in + (instance, (univcst, substcst)) (** Pretty-printing *) @@ -1307,7 +1324,11 @@ let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.pr -let pr_universe_info_ind = UInfoInd.pr +let pr_cumulativity_info = CumulativityInfo.pr + +let pr_abstract_universe_context = AUContext.pr + +let pr_abstract_cumulativity_info = ACumulativityInfo.pr let pr_universe_context_set = ContextSet.pr @@ -1364,3 +1385,12 @@ let subst_instance_constraints = let key = Profile.declare_profile "subst_instance_constraints" in Profile.profile2 key subst_instance_constraints else subst_instance_constraints + +let subst_instance_context = + let subst_instance_context_body inst (inner_inst, inner_constr) = + (inner_inst, subst_instance_constraints inst inner_constr) + in + if Flags.profile then + let key = Profile.declare_profile "subst_instance_constraints" in + Profile.profile2 key subst_instance_context_body + else subst_instance_context_body diff --git a/kernel/univ.mli b/kernel/univ.mli index 53af80448..ecc72701d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -315,6 +315,23 @@ end type universe_context = UContext.t +module AUContext : +sig + type t + + val empty : t + + val instance : t -> Instance.t + + val size : t -> int + + (** Keeps the order of the instances *) + val union : t -> t -> t + +end + +type abstract_universe_context = AUContext.t + (** Universe info for inductive types: A context of universe levels with universe constraints, representing local universe variables and constraints, together with a context of universe levels with @@ -324,7 +341,7 @@ type universe_context = UContext.t This data structure maintains the invariant that the context for subtyping constraints is exactly twice as big as the context for universe constraints. *) -module UInfoInd : +module CumulativityInfo : sig type t @@ -347,7 +364,17 @@ sig end -type universe_info_ind = UInfoInd.t +type cumulativity_info = CumulativityInfo.t + +module ACumulativityInfo : +sig + type t + + val univ_context : t -> abstract_universe_context + val subtyp_context : t -> abstract_universe_context +end + +type abstract_cumulativity_info = ACumulativityInfo.t (** Universe contexts (as sets) *) @@ -399,6 +426,8 @@ val is_empty_level_subst : universe_level_subst -> bool val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level val subst_univs_level_universe : universe_level_subst -> universe -> universe val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints +val subst_univs_level_abstract_universe_context : + universe_level_subst -> abstract_universe_context -> abstract_universe_context val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance (** Level to universe substitutions. *) @@ -413,27 +442,31 @@ val subst_univs_constraints : universe_subst_fn -> constraints -> constraints (** Substitution of instances *) val subst_instance_instance : universe_instance -> universe_instance -> universe_instance val subst_instance_universe : universe_instance -> universe -> universe -val subst_instance_constraints : universe_instance -> constraints -> constraints +val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context val make_instance_subst : universe_instance -> universe_level_subst val make_inverse_instance_subst : universe_instance -> universe_level_subst -val abstract_universes : bool -> universe_context -> universe_level_subst * universe_context +val abstract_universes : universe_context -> universe_level_subst * abstract_universe_context + +val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abstract_cumulativity_info + +val make_abstract_instance : abstract_universe_context -> universe_instance (** Get the instantiated graph. *) -val instantiate_univ_context : universe_context -> universe_context +val instantiate_univ_context : abstract_universe_context -> universe_context (** Get the instantiated graphs for both universe constraints and subtyping constraints. *) -val instantiate_univ_info_ind : universe_info_ind -> universe_info_ind - -val instantiate_univ_constraints : universe_instance -> universe_context -> constraints +val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info (** {6 Pretty-printing of universes. } *) val pr_constraint_type : constraint_type -> Pp.std_ppcmds val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds -val pr_universe_info_ind : (Level.t -> Pp.std_ppcmds) -> universe_info_ind -> Pp.std_ppcmds +val pr_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> cumulativity_info -> Pp.std_ppcmds +val pr_abstract_universe_context : (Level.t -> Pp.std_ppcmds) -> abstract_universe_context -> Pp.std_ppcmds +val pr_abstract_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> abstract_cumulativity_info -> Pp.std_ppcmds val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> univ_inconsistency -> Pp.std_ppcmds @@ -447,8 +480,10 @@ val hcons_univ : universe -> universe val hcons_constraints : constraints -> constraints val hcons_universe_set : universe_set -> universe_set val hcons_universe_context : universe_context -> universe_context +val hcons_abstract_universe_context : abstract_universe_context -> abstract_universe_context val hcons_universe_context_set : universe_context_set -> universe_context_set -val hcons_universe_info_ind : universe_info_ind -> universe_info_ind +val hcons_cumulativity_info : cumulativity_info -> cumulativity_info +val hcons_abstract_cumulativity_info : abstract_cumulativity_info -> abstract_cumulativity_info (******) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index fa1662270..0e452621c 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -88,30 +88,34 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = (* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *) match a1, a2 with | Aind ((mi,i) as ind1) , Aind ind2 -> - if eq_ind ind1 ind2 && compare_stack stk1 stk2 - then - if Environ.polymorphic_ind ind1 env - then - let mib = Environ.lookup_mind mi env in - let ulen = Univ.UContext.size (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in - match stk1 , stk2 with - | [], [] -> assert (Int.equal ulen 0); cu - | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> - assert (ulen <= nargs args1); - assert (ulen <= nargs args2); - let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in - let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in - let u1 = Univ.Instance.of_array u1 in - let u2 = Univ.Instance.of_array u2 in - let cu = convert_instances ~flex:false u1 u2 cu in - conv_arguments env ~from:ulen k args1 args2 - (conv_stack env k stk1' stk2' cu) - | _, _ -> assert false (* Should not happen if problem is well typed *) - else - conv_stack env k stk1 stk2 cu - else raise NotConvertible + if eq_ind ind1 ind2 && compare_stack stk1 stk2 then + if Environ.polymorphic_ind ind1 env then + let mib = Environ.lookup_mind mi env in + let ulen = + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx + | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx + | Declarations.Cumulative_ind cumi -> + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) + in + match stk1 , stk2 with + | [], [] -> assert (Int.equal ulen 0); cu + | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> + assert (ulen <= nargs args1); + assert (ulen <= nargs args2); + let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in + let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in + let u1 = Univ.Instance.of_array u1 in + let u2 = Univ.Instance.of_array u2 in + let cu = convert_instances ~flex:false u1 u2 cu in + conv_arguments env ~from:ulen k args1 args2 + (conv_stack env k stk1' stk2' cu) + | _, _ -> assert false (* Should not happen if problem is well typed *) + else + conv_stack env k stk1 stk2 cu + else raise NotConvertible | Aid ik1, Aid ik2 -> - if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then + if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible | Atype _ , _ | _, Atype _ -> assert false |