diff options
| -rw-r--r-- | checker/checkInductive.ml | 14 | ||||
| -rw-r--r-- | kernel/entries.ml | 2 | ||||
| -rw-r--r-- | kernel/indTyping.ml | 8 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 20 | ||||
| -rw-r--r-- | vernac/record.ml | 17 |
5 files changed, 36 insertions, 25 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 62e732ce69..b93b03ec16 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -52,20 +52,19 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx) in let mind_entry_inds = Array.map_to_list (fun ind -> - let mind_entry_arity, mind_entry_template = match ind.mind_arity with + let mind_entry_arity = match ind.mind_arity with | RegularArity ar -> let ctx, arity = Term.decompose_prod_n_assum nparams ar.mind_user_arity in ignore ctx; (* we will check that the produced user_arity is equal to the input *) - arity, false + arity | TemplateArity ar -> let ctx = ind.mind_arity_ctxt in let ctx = List.firstn (List.length ctx - nparams) ctx in - Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level), true + Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level) in { mind_entry_typename = ind.mind_typename; mind_entry_arity; - mind_entry_template; mind_entry_consnames = Array.to_list ind.mind_consnames; mind_entry_lc = Array.map_to_list (fun c -> let ctx, c = Term.decompose_prod_n_assum nparams c in @@ -75,12 +74,19 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = }) mb.mind_packets in + let check_template ind = match ind.mind_arity with + | RegularArity _ -> false + | TemplateArity _ -> true + in + let mind_entry_template = Array.exists check_template mb.mind_packets in + let () = if mind_entry_template then assert (Array.for_all check_template mb.mind_packets) in { mind_entry_record; mind_entry_finite = mb.mind_finite; mind_entry_params = mb.mind_params_ctxt; mind_entry_inds; mind_entry_universes; + mind_entry_template; mind_entry_cumulative= Option.has_some mb.mind_variance; mind_entry_private = mb.mind_private; } diff --git a/kernel/entries.ml b/kernel/entries.ml index 8d930b521c..983fa822e9 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -37,7 +37,6 @@ 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 } @@ -50,6 +49,7 @@ type mutual_inductive_entry = { mind_entry_params : Constr.rel_context; mind_entry_inds : one_inductive_entry list; mind_entry_universes : universes_entry; + mind_entry_template : bool; (* Use template polymorphism *) mind_entry_cumulative : bool; (* universe constraints and the constraints for subtyping of inductive types in the block. *) diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index d48422909f..1d72d1bd6e 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -101,10 +101,10 @@ let check_indices_matter env_params info indices = else check_context_univs ~ctor:false env_params info indices (* env_ar contains the inductives before the current ones in the block, and no parameters *) -let check_arity env_params env_ar ind = +let check_arity ~template env_params env_ar ind = let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in let indices, ind_sort = Reduction.dest_arity env_params arity in - let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in + let ind_min_univ = if template then Some Universe.type0m else None in let univ_info = { ind_squashed=false; ind_has_relevant_arg=false; @@ -283,7 +283,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = mind_check_names mie; assert (List.is_empty (Environ.rel_context env)); - let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in + let has_template_poly = mie.mind_entry_template in (* universes *) let env_univs = @@ -304,7 +304,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let env_params, params = Typeops.check_context env_univs mie.mind_entry_params in (* Arities *) - let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in + let env_ar, data = List.fold_left_map (check_arity ~template:has_template_poly env_params) env_univs mie.mind_entry_inds in let env_ar_par = push_rel_context params env_ar in (* Constructors *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 08a8d1b320..718e62b9b7 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -367,6 +367,14 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames (* Build the inductive entries *) let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) -> + { mind_entry_typename = indname; + mind_entry_arity = arity; + mind_entry_consnames = cnames; + mind_entry_lc = ctypes + }) + indnames arities arityconcl constructors + in + let template = List.map4 (fun indname (templatearity, _) concl (_, ctypes) -> let template_candidate () = templatearity || let ctor_levels = @@ -382,22 +390,17 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames in template_polymorphism_candidate ~ctor_levels uctx ctx_params concl in - let template = match template with + match template with | Some template -> if poly && template then user_err Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); template | None -> should_auto_template indname (template_candidate ()) - in - { mind_entry_typename = indname; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = cnames; - mind_entry_lc = ctypes - }) + ) indnames arities arityconcl constructors in + let is_template = List.for_all (fun t -> t) template in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; @@ -406,6 +409,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames mind_entry_inds = entries; mind_entry_private = if private_ind then Some false else None; mind_entry_universes = uctx; + mind_entry_template = is_template; mind_entry_cumulative = poly && cumulative; } in diff --git a/vernac/record.ml b/vernac/record.ml index 3e44cd85cc..065641989d 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -423,7 +423,13 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in - let template = + { mind_entry_typename = id; + mind_entry_arity = arity; + mind_entry_consnames = [idbuild]; + mind_entry_lc = [type_constructor] } + in + let blocks = List.mapi mk_block record_data in + let check_template (id, _, min_univ, _, _, fields, _, _) = let template_candidate () = (* we use some dummy values for the arities in the rel_context as univs_of_constr doesn't care about localassums and @@ -454,14 +460,8 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa | None, template -> (* auto detect template *) ComInductive.should_auto_template id (template && template_candidate ()) - in - { mind_entry_typename = id; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = [idbuild]; - mind_entry_lc = [type_constructor] } in - let blocks = List.mapi mk_block record_data in + let template = List.for_all check_template record_data in let primitive = !primitive_flag && List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data @@ -473,6 +473,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; + mind_entry_template = template; mind_entry_cumulative = poly && cumulative; } in |