aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/entries.mli3
-rw-r--r--kernel/indtypes.ml9
-rw-r--r--library/declare.ml1
-rw-r--r--library/universes.ml11
-rw-r--r--test-suite/bugs/closed/3821.v2
-rw-r--r--toplevel/command.ml5
-rw-r--r--toplevel/discharge.ml17
-rw-r--r--toplevel/record.ml28
-rw-r--r--toplevel/record.mli1
9 files changed, 45 insertions, 32 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli
index f6958849b..baeec31b4 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -37,6 +37,7 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
type one_inductive_entry = {
mind_entry_typename : Id.t;
mind_entry_arity : constr;
+ mind_entry_template : bool; (* Use template polymorphism *)
mind_entry_consnames : Id.t list;
mind_entry_lc : constr list }
@@ -48,7 +49,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_polymorphic : bool;
mind_entry_universes : Univ.universe_context;
mind_entry_private : bool option }
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index afd7cde97..6dd3ab2ba 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -226,7 +226,8 @@ let typecheck_inductive env ctx mie =
List.fold_left
(fun (env_ar,l) ind ->
(* Arities (without params) are typed-checked here *)
- let arity, expltype =
+ let expltype = ind.mind_entry_template in
+ let arity =
if isArity ind.mind_entry_arity then
let (ctx,s) = dest_arity env_params ind.mind_entry_arity in
match s with
@@ -237,12 +238,12 @@ let typecheck_inductive env ctx mie =
let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in
let (cctx, _) = destArity proparity.utj_val in
(* Any universe is well-formed, we don't need to check [s] here *)
- mkArity (cctx, s), not (Sorts.is_small s)
+ mkArity (cctx, s)
| _ ->
let arity = infer_type env_params ind.mind_entry_arity in
- arity.utj_val, not (Sorts.is_small s)
+ arity.utj_val
else let arity = infer_type env_params ind.mind_entry_arity in
- arity.utj_val, false
+ arity.utj_val
in
let (sign, deflev) = dest_arity env_params arity in
let inflev =
diff --git a/library/declare.ml b/library/declare.ml
index fb6e1c9b8..56c789c1e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -353,6 +353,7 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
let dummy_one_inductive_entry mie = {
mind_entry_typename = mie.mind_entry_typename;
mind_entry_arity = mkProp;
+ mind_entry_template = false;
mind_entry_consnames = mie.mind_entry_consnames;
mind_entry_lc = []
}
diff --git a/library/universes.ml b/library/universes.ml
index 438e6cc53..d69386ddf 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -957,10 +957,13 @@ let is_direct_sort_constraint s v = match s with
let solve_constraints_system levels level_bounds level_min =
let open Univ in
let levels =
- Array.map (Option.map
- (fun u -> match Universe.level u with
- | Some u -> u
- | _ -> Errors.anomaly (Pp.str"expects Atom")))
+ Array.mapi (fun i o ->
+ match o with
+ | Some u ->
+ (match Universe.level u with
+ | Some u -> Some u
+ | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
+ | None -> None)
levels in
let v = Array.copy level_bounds in
let nind = Array.length v in
diff --git a/test-suite/bugs/closed/3821.v b/test-suite/bugs/closed/3821.v
new file mode 100644
index 000000000..8da4f7362
--- /dev/null
+++ b/test-suite/bugs/closed/3821.v
@@ -0,0 +1,2 @@
+Inductive quotient {A : Type@{i}} {B : Type@{j}} : Type@{max(i, j)} := .
+
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f8c9f25b8..cd5aa7528 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -529,12 +529,13 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
constructors;
(* Build the inductive entries *)
- let entries = List.map3 (fun ind arity (cnames,ctypes,cimpls) -> {
+ let entries = List.map4 (fun ind arity template (cnames,ctypes,cimpls) -> {
mind_entry_typename = ind.ind_name;
mind_entry_arity = arity;
+ mind_entry_template = template;
mind_entry_consnames = cnames;
mind_entry_lc = ctypes
- }) indl arities constructors in
+ }) indl arities aritypoly constructors in
let impls =
let len = rel_context_nhyps ctx_params in
List.map2 (fun indimpls (_,_,cimpls) ->
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 1823e3a89..7a79b2efb 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -43,26 +43,27 @@ let abstract_inductive hyps nparams inds =
let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
let inds' =
List.map
- (function (tname,arity,cnames,lc) ->
+ (function (tname,arity,template,cnames,lc) ->
let lc' = List.map (substl subs) lc in
let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in
let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in
- (tname,arity',cnames,lc''))
+ (tname,arity',template,cnames,lc''))
inds in
let nparams' = nparams + Array.length args in
(* To be sure to be the same as before, should probably be moved to process_inductive *)
- let params' = let (_,arity,_,_) = List.hd inds' in
+ let params' = let (_,arity,_,_,_) = List.hd inds' in
let (params,_) = decompose_prod_n_assum nparams' arity in
List.map detype_param params
in
let ind'' =
List.map
- (fun (a,arity,c,lc) ->
+ (fun (a,arity,template,c,lc) ->
let _, short_arity = decompose_prod_n_assum nparams' arity in
let shortlc =
List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in
{ mind_entry_typename = a;
mind_entry_arity = short_arity;
+ mind_entry_template = template;
mind_entry_consnames = c;
mind_entry_lc = shortlc })
inds'
@@ -70,10 +71,10 @@ let abstract_inductive hyps nparams inds =
let refresh_polymorphic_type_of_inductive (_,mip) =
match mip.mind_arity with
- | RegularArity s -> s.mind_user_arity
+ | RegularArity s -> s.mind_user_arity, false
| TemplateArity ar ->
let ctx = List.rev mip.mind_arity_ctxt in
- mkArity (List.rev ctx, Type ar.template_level)
+ mkArity (List.rev ctx, Type ar.template_level), true
let process_inductive (sechyps,abs_ctx) modlist mib =
let nparams = mib.mind_nparams in
@@ -87,7 +88,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
let inds =
Array.map_to_list
(fun mip ->
- let ty = refresh_polymorphic_type_of_inductive (mib,mip) in
+ let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
let arity = expmod_constr modlist ty in
let arity = Vars.subst_instance_constr subst arity in
let lc = Array.map
@@ -95,7 +96,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
mip.mind_user_lc
in
(mip.mind_typename,
- arity,
+ arity, template,
Array.to_list mip.mind_consnames,
Array.to_list lc))
mib.mind_packets in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 6d3dcdcb4..4ccf79449 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -105,7 +105,7 @@ let typecheck_params_and_fields def id t ps nots fs =
| LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
in
let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
- let t' = match t with
+ let t', template = match t with
| Some t ->
let env = push_rel_context newps env0 in
let s = interp_type_evars env evars ~impls:empty_internalization_env t in
@@ -113,12 +113,13 @@ let typecheck_params_and_fields def id t ps nots fs =
(match kind_of_term sred with
| Sort s' ->
(match Evd.is_sort_variable !evars s' with
- | Some l -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; sred
- | None -> s)
+ | Some l -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l;
+ sred, true
+ | None -> s, false)
| _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
| None ->
let uvarkind = if (* not def *) true then Evd.univ_flexible_alg else Evd.univ_flexible in
- mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars)
+ mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), false
in
let fullarity = it_mkProd_or_LetIn t' newps in
let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
@@ -144,7 +145,7 @@ let typecheck_params_and_fields def id t ps nots fs =
let ce t = Evarutil.check_evars env0 Evd.empty evars t in
List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps);
List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs);
- Evd.universe_context evars, nf arity, imps, newps, impls, newfs
+ Evd.universe_context evars, nf arity, template, imps, newps, impls, newfs
let degenerate_decl (na,b,t) =
let id = match na with
@@ -339,8 +340,8 @@ let structure_signature ctx =
open Typeclasses
-let declare_structure finite poly ctx id idbuild paramimpls params arity fieldimpls fields
- ?(kind=StructureComponent) ?name is_coe coers sign =
+let declare_structure finite poly ctx id idbuild paramimpls params arity template
+ fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
let nparams = List.length params and nfields = List.length fields in
let args = Termops.extended_rel_list nfields params in
let ind = applist (mkRel (1+nparams+nfields), args) in
@@ -353,6 +354,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity fieldim
let mie_ind =
{ mind_entry_typename = id;
mind_entry_arity = arity;
+ mind_entry_template = not poly && template;
mind_entry_consnames = [idbuild];
mind_entry_lc = [type_constructor] }
in
@@ -382,8 +384,8 @@ let implicits_of_context ctx =
in ExplByPos (i, explname), (true, true, true))
1 (List.rev (Anonymous :: (List.map pi1 ctx)))
-let declare_class finite def poly ctx id idbuild paramimpls params arity fieldimpls fields
- ?(kind=StructureComponent) is_coe coers priorities sign =
+let declare_class finite def poly ctx id idbuild paramimpls params arity
+ template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
let len = List.length params in
@@ -422,7 +424,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
cref, [Name proj_name, sub, Some proj_cst]
| _ ->
let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
- params arity fieldimpls fields
+ params arity template fieldimpls fields
~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
in
let coers = List.map2 (fun coe pri ->
@@ -510,20 +512,20 @@ let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild
if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
error "Priorities only allowed for type class substructures";
(* Now, younger decl in params and fields is on top *)
- let ctx, arity, implpars, params, implfs, fields =
+ let ctx, arity, template, implpars, params, implfs, fields =
States.with_state_protection (fun () ->
typecheck_params_and_fields (kind = Class true) idstruc s ps notations fs) () in
let sign = structure_signature (fields@params) in
match kind with
| Class def ->
let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
- implpars params arity implfs fields is_coe coers priorities sign in
+ implpars params arity template implfs fields is_coe coers priorities sign in
gr
| _ ->
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
- idbuild implpars params arity implfs
+ 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/toplevel/record.mli b/toplevel/record.mli
index 2422b45bd..cead9b6f6 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -29,6 +29,7 @@ val declare_structure : Decl_kinds.recursivity_kind ->
bool (** polymorphic?*) -> Univ.universe_context ->
Id.t -> Id.t ->
manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
+ bool (** template arity ? *) ->
Impargs.manual_explicitation list list -> rel_context -> (** fields *)
?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
bool -> (** coercion? *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 07:01:20 +0000