diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 24 | ||||
| -rw-r--r-- | vernac/comInductive.mli | 24 | ||||
| -rw-r--r-- | vernac/record.ml | 22 |
3 files changed, 52 insertions, 18 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 80fcb7bc45..2aee9bd47f 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -323,7 +323,7 @@ let check_named {CAst.loc;v=na} = match na with let msg = str "Parameters must be named." in user_err ?loc msg -let template_polymorphism_candidate env uctx params concl = +let template_polymorphism_candidate env ~ctor_levels uctx params concl = match uctx with | Entries.Monomorphic_entry uctx -> let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in @@ -331,7 +331,9 @@ let template_polymorphism_candidate env uctx params concl = else let template_check = Environ.check_template env in let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in - let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check uctx params conclu in + let params, conclunivs = + IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu + in not (template_check && Univ.LSet.is_empty conclunivs) | Entries.Polymorphic_entry _ -> false @@ -376,14 +378,24 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa (* Build the inductive entries *) let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) -> let template_candidate () = - templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in + templatearity || + let ctor_levels = + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty ctx_params + in + List.fold_left (fun levels c -> add_levels c levels) + param_levels ctypes + in + template_polymorphism_candidate env0 ~ctor_levels uctx ctx_params concl + in let template = match template with | Some template -> if poly && template then user_err Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); - if template && not (template_candidate ()) then - user_err Pp.(strbrk "Inductive " ++ Id.print indname ++ - str" cannot be made template polymorphic."); template | None -> should_auto_template indname (template_candidate ()) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 45e539b1e4..ef05b213d8 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -77,12 +77,18 @@ val should_auto_template : Id.t -> bool -> bool automatically use template polymorphism. [x] is the name of the inductive under consideration. *) -val template_polymorphism_candidate : - Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool -(** [template_polymorphism_candidate env uctx params conclsort] is - [true] iff an inductive with params [params] and conclusion - [conclsort] would be definable as template polymorphic. It should - have at least one universe in its monomorphic universe context that - can be made parametric in its conclusion sort, if one is given. - If the [Template Check] flag is false we just check that the conclusion sort - is not small. *) +val template_polymorphism_candidate + : Environ.env + -> ctor_levels:Univ.LSet.t + -> Entries.universes_entry + -> Constr.rel_context + -> Sorts.t option + -> bool +(** [template_polymorphism_candidate env ~ctor_levels uctx params + conclsort] is [true] iff an inductive with params [params], + conclusion [conclsort] and universe levels appearing in the + constructor arguments [ctor_levels] would be definable as template + polymorphic. It should have at least one universe in its + monomorphic universe context that can be made parametric in its + conclusion sort, if one is given. If the [Template Check] flag is + false we just check that the conclusion sort is not small. *) diff --git a/vernac/record.ml b/vernac/record.ml index 49a73271f0..d85b71df44 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -429,15 +429,31 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let type_constructor = it_mkProd_or_LetIn ind fields in let template = let template_candidate () = - ComInductive.template_polymorphism_candidate (Global.env ()) univs params + (* we use some dummy values for the arities in the rel_context + as univs_of_constr doesn't care about localassums and + getting the real values is too annoying *) + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty params + in + let ctor_levels = List.fold_left + (fun univs d -> + let univs = + RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs + in + univs) + param_levels fields + in + ComInductive.template_polymorphism_candidate (Global.env ()) ~ctor_levels univs params (Some (Sorts.sort_of_univ min_univ)) in match template with | Some template, _ -> (* templateness explicitly requested *) if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); - if template && not (template_candidate ()) then - user_err Pp.(strbrk "record cannot be made template polymorphic on any universe"); template | None, template -> (* auto detect template *) |