diff options
-rw-r--r-- | API/API.mli | 1 | ||||
-rw-r--r-- | kernel/declarations.ml | 2 | ||||
-rw-r--r-- | kernel/declareops.ml | 1 | ||||
-rw-r--r-- | kernel/entries.mli | 4 | ||||
-rw-r--r-- | kernel/indtypes.ml | 29 | ||||
-rw-r--r-- | library/declare.ml | 2 | ||||
-rw-r--r-- | vernac/command.ml | 2 | ||||
-rw-r--r-- | vernac/discharge.ml | 9 | ||||
-rw-r--r-- | vernac/record.ml | 4 | ||||
-rw-r--r-- | vernac/record.mli | 3 |
10 files changed, 38 insertions, 19 deletions
diff --git a/API/API.mli b/API/API.mli index 69278e7c9..e2c43dab8 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1094,6 +1094,7 @@ sig mind_params_ctxt : Context.Rel.t; mind_polymorphic : bool; mind_universes : Univ.UContext.t; + mind_subtyping : Univ.universe_context; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 71e228b19..9536407d3 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -190,6 +190,8 @@ type mutual_inductive_body = { mind_universes : Univ.universe_context; (** Local universe variables and constraints *) + mind_subtyping : Univ.universe_context; (** Constraints for subtyping *) + mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 0a822d6fa..47a23c855 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -261,6 +261,7 @@ let subst_mind_body sub mib = mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; + mind_subtyping = mib.mind_subtyping; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } diff --git a/kernel/entries.mli b/kernel/entries.mli index 1e07c9690..88584e3b3 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -50,7 +50,9 @@ type mutual_inductive_entry = { mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_polymorphic : bool; - mind_entry_universes : Univ.universe_context; + mind_entry_universes : Univ.universe_context * Univ.universe_context; + (* universe constraints and the constraints for subtyping of + inductive types in the block. *) mind_entry_private : bool option; } diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1e13239bf..5d928facc 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -220,7 +220,7 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let env' = push_context mie.mind_entry_universes env in + let env' = push_context (fst mie.mind_entry_universes) 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 *) @@ -822,17 +822,18 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let hyps = used_section_variables env inds in let nparamargs = Context.Rel.nhyps paramsctxt in let nparamsctxt = Context.Rel.length paramsctxt in - let subst, ctx = Univ.abstract_universes p ctx in - let paramsctxt = Vars.subst_univs_level_context subst paramsctxt in + let substunivs, ctxunivs = Univ.abstract_universes p (fst ctx) in + let substsbt, ctxsbt = Univ.abstract_universes p (snd ctx) in + let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in let env_ar = - let ctx = Environ.rel_context env_ar in - let ctx' = Vars.subst_univs_level_context subst ctx in - Environ.push_rel_context ctx' env + let ctxunivs = Environ.rel_context env_ar in + let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in + Environ.push_rel_context ctxunivs' env in (* Check one inductive *) let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg = (* Type of constructors in normal form *) - let lc = Array.map (Vars.subst_univs_level_constr subst) lc in + let lc = Array.map (Vars.subst_univs_level_constr substunivs) lc in let splayed_lc = Array.map (dest_prod_assum env_ar) lc in let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in let consnrealdecls = @@ -841,6 +842,9 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let consnrealargs = Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs) splayed_lc in + (* Check that the subtyping constraints (inferred outside kernel) + are valid. If so return (), otherwise raise an anomaly! *) + let () = () in (* Elimination sorts *) let arkind,kelim = match ar_kind with @@ -851,8 +855,8 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let s = sort_of_univ defs in let kelim = allowed_sorts info s in let ar = RegularArity - { mind_user_arity = Vars.subst_univs_level_constr subst ar; - mind_sort = sort_of_univ (Univ.subst_univs_level_universe subst defs); } in + { mind_user_arity = Vars.subst_univs_level_constr substunivs ar; + mind_sort = sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in ar, kelim in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in @@ -871,7 +875,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm (* Build the inductive packet *) { mind_typename = id; mind_arity = arkind; - mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign; + mind_arity_ctxt = Vars.subst_univs_level_context substunivs ar_sign; mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs; mind_nrealdecls = Context.Rel.length ar_sign - nparamsctxt; mind_kelim = kelim; @@ -895,7 +899,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm (** The elimination criterion ensures that all projections can be defined. *) let u = if p then - subst_univs_level_instance subst (Univ.UContext.instance ctx) + subst_univs_level_instance substunivs (Univ.UContext.instance ctxunivs) else Univ.Instance.empty in let indsp = ((kn, 0), u) in @@ -920,7 +924,8 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_params_ctxt = paramsctxt; mind_packets = packets; mind_polymorphic = p; - mind_universes = ctx; + mind_universes = ctxunivs; + mind_subtyping = ctxsbt; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } diff --git a/library/declare.ml b/library/declare.ml index 7d0edbc8b..06eeeeab5 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -352,7 +352,7 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; - mind_entry_universes = Univ.UContext.empty; + mind_entry_universes = (Univ.UContext.empty, Univ.UContext.empty); mind_entry_private = None; }) diff --git a/vernac/command.ml b/vernac/command.ml index 998e7803e..5f95a42a3 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -656,7 +656,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; - mind_entry_universes = uctx; + mind_entry_universes = (uctx, Univ.UContext.empty); }, pl, impls diff --git a/vernac/discharge.ml b/vernac/discharge.ml index 65ade7887..9c70eb97e 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -86,6 +86,13 @@ let process_inductive (sechyps,abs_ctx) modlist mib = inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs) else Univ.Instance.empty, mib.mind_universes in + let substsbt, univssbt = + if mib.mind_polymorphic then + let inst = Univ.UContext.instance mib.mind_subtyping in + let cstrs = Univ.UContext.constraints mib.mind_subtyping in + inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs) + else Univ.Instance.empty, Univ.UContext.empty + in let inds = Array.map_to_list (fun mip -> @@ -116,5 +123,5 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_inds = inds'; mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; - mind_entry_universes = univs; + mind_entry_universes = (univs, univssbt); } diff --git a/vernac/record.ml b/vernac/record.ml index 2400fa681..5c76bb4b2 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -466,7 +466,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls + let ind = declare_structure BiFinite poly (ctx, Univ.UContext.empty) (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -571,7 +571,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - let ind = declare_structure finite poly ctx idstruc + let ind = declare_structure finite poly (ctx, Univ.UContext.empty) idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind diff --git a/vernac/record.mli b/vernac/record.mli index 3fd651db9..a380b041a 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -26,7 +26,8 @@ val declare_projections : val declare_structure : Decl_kinds.recursivity_kind -> - bool (** polymorphic?*) -> Univ.universe_context -> + bool (** polymorphic?*) -> + (Univ.universe_context * Univ.universe_context) (** universe and subtyping constraints *) -> Id.t -> Id.t -> manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) bool (** template arity ? *) -> |