diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.ml | 6 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 12 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 8 | ||||
| -rw-r--r-- | kernel/univ.ml | 3 | ||||
| -rw-r--r-- | kernel/univ.mli | 3 |
6 files changed, 22 insertions, 12 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index c5bcd74072..87fa385a60 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -30,8 +30,8 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; type inductive_universes = | Monomorphic_ind_entry of Univ.ContextSet.t - | Polymorphic_ind_entry of Univ.UContext.t - | Cumulative_ind_entry of Univ.CumulativityInfo.t + | Polymorphic_ind_entry of Name.t list * Univ.UContext.t + | Cumulative_ind_entry of Name.t list * Univ.CumulativityInfo.t type one_inductive_entry = { mind_entry_typename : Id.t; @@ -60,7 +60,7 @@ type 'a const_entry_body = 'a proof_output Future.computation type constant_universes_entry = | Monomorphic_const_entry of Univ.ContextSet.t - | Polymorphic_const_entry of Univ.UContext.t + | Polymorphic_const_entry of Name.t list * Univ.UContext.t type 'a in_constant_universes_entry = 'a * constant_universes_entry diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0346026aa4..2d74f99c15 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -268,8 +268,8 @@ let typecheck_inductive env mie = let env' = match mie.mind_entry_universes with | Monomorphic_ind_entry ctx -> push_context_set ctx env - | Polymorphic_ind_entry ctx -> push_context ctx env - | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env + | Polymorphic_ind_entry (_, ctx) -> push_context ctx env + | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env in let env_params = check_context env' mie.mind_entry_params in let paramsctxt = mie.mind_entry_params in @@ -407,7 +407,7 @@ let typecheck_inductive env mie = match mie.mind_entry_universes with | Monomorphic_ind_entry _ -> () | Polymorphic_ind_entry _ -> () - | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds + | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) @@ -851,12 +851,14 @@ let compute_projections (kn, i as ind) mib = let abstract_inductive_universes iu = match iu with | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) - | Polymorphic_ind_entry ctx -> + | Polymorphic_ind_entry (nas, ctx) -> + let () = assert (Int.equal (List.length nas) (UContext.size ctx)) in let (inst, auctx) = Univ.abstract_universes ctx in let inst = Univ.make_instance_subst inst in (inst, Polymorphic_ind auctx) - | Cumulative_ind_entry cumi -> + | Cumulative_ind_entry (nas, cumi) -> let (inst, acumi) = Univ.abstract_cumulativity_info cumi in + let () = assert (Int.equal (List.length nas) (Instance.length inst)) in let inst = Univ.make_instance_subst inst in (inst, Cumulative_ind acumi) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8b11851bbb..df10398b2f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -682,7 +682,7 @@ let constant_entry_of_side_effect cb u = | Monomorphic_const uctx -> Monomorphic_const_entry uctx | Polymorphic_const auctx -> - Polymorphic_const_entry (Univ.AUContext.repr auctx) + Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) in let pt = match cb.const_body, u with diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index fb1b3e236c..4759625e8a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -68,7 +68,8 @@ let feedback_completion_typecheck = let abstract_constant_universes = function | Monomorphic_const_entry uctx -> Univ.empty_level_subst, Monomorphic_const uctx - | Polymorphic_const_entry uctx -> + | Polymorphic_const_entry (nas, uctx) -> + let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in let sbst, auctx = Univ.abstract_universes uctx in let sbst = Univ.make_instance_subst sbst in sbst, Polymorphic_const auctx @@ -78,7 +79,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env - | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env + | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env in let j = infer env t in let usubst, univs = abstract_constant_universes uctx in @@ -150,7 +151,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let ctx = Univ.ContextSet.union univs ctx in let env = push_context_set ~strict:true ctx env in env, Univ.empty_level_subst, Monomorphic_const ctx - | Polymorphic_const_entry uctx -> + | Polymorphic_const_entry (nas, uctx) -> (** Ensure not to generate internal constraints in polymorphic mode. The only way for this to happen would be that either the body contained deferred universes, or that it contains monomorphic @@ -159,6 +160,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = unconditionally export side-effects from polymorphic definitions, i.e. [trust] is always [Pure]. *) let () = assert (Univ.ContextSet.is_empty ctx) in + let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in let env = push_context ~strict:false uctx env in let sbst, auctx = Univ.abstract_universes uctx in let sbst = Univ.make_instance_subst sbst in diff --git a/kernel/univ.ml b/kernel/univ.ml index d09b54e7ec..35566019a8 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -948,6 +948,9 @@ struct assert (Array.length u = Array.length inst); subst_instance_constraints inst cst + (** FIXME: Actually store this information in the type *) + let names (u, _) = Array.map_to_list (fun _ -> Names.Anonymous) u + end let hcons_abstract_universe_context = AUContext.hcons diff --git a/kernel/univ.mli b/kernel/univ.mli index 7ac8247ca4..bc902d8f4b 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -347,6 +347,9 @@ sig val instantiate : Instance.t -> t -> Constraint.t (** Generate the set of instantiated Constraint.t **) + val names : t -> Names.Name.t list + (** Return the names of the bound universe variables *) + end (** Universe info for cumulative inductive types: A context of |