diff options
Diffstat (limited to 'kernel/indTyping.ml')
| -rw-r--r-- | kernel/indTyping.ml | 50 |
1 files changed, 30 insertions, 20 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index b19472dc99..cc15109f06 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -66,7 +66,9 @@ let mind_check_names mie = type univ_info = { ind_squashed : bool; ind_has_relevant_arg : bool; ind_min_univ : Universe.t option; (* Some for template *) - ind_univ : Universe.t } + ind_univ : Universe.t; + missing : Universe.Set.t; (* missing u <= ind_univ constraints *) + } let check_univ_leq ?(is_real_arg=false) env u info = let ind_univ = info.ind_univ in @@ -78,9 +80,8 @@ let check_univ_leq ?(is_real_arg=false) env u info = if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ } else if is_impredicative_univ env ind_univ - then if Option.is_empty info.ind_min_univ then { info with ind_squashed = true } - else raise (InductiveError BadUnivs) - else raise (InductiveError BadUnivs) + && Option.is_empty info.ind_min_univ then { info with ind_squashed = true } + else {info with missing = Universe.Set.add u info.missing} let check_context_univs ~ctor env info ctx = let check_one d (info,env) = @@ -109,6 +110,7 @@ let check_arity env_params env_ar ind = ind_has_relevant_arg=false; ind_min_univ; ind_univ=Sorts.univ_of_sort ind_sort; + missing=Universe.Set.empty; } in let univ_info = check_indices_matter env_params univ_info indices in @@ -174,7 +176,7 @@ let check_record data = (* - all_sorts in case of small, unitary Prop (not smashed) *) (* - logical_sorts in case of large, unitary Prop (smashed) *) -let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} = +let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_;missing=_} = if not ind_squashed then InType else Sorts.family (Sorts.sort_of_univ ind_univ) @@ -195,7 +197,7 @@ let unbounded_from_below u cstrs = (starting from the most recent and ignoring let-definitions) is not contributing to the inductive type's sort or is Some u_k if its level is u_k and is contributing. *) -let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl = +let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl = let check_level l = Univ.LSet.mem l (Univ.ContextSet.levels uctx) && unbounded_from_below l (Univ.ContextSet.constraints uctx) && @@ -203,27 +205,25 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc in let univs = Univ.Universe.levels concl in let univs = - if template_check then - Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs - else univs (* Doesn't check the universes can be generalized *) + Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with | Sort (Type u) -> - if template_check then (match Univ.Universe.level u with | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None | None -> None) - else Univ.Universe.level u | _ -> None) :: acc | LocalDef _ -> acc in let params = List.fold_left fold [] paramsctxt in params, univs -let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = + if not (Universe.Set.is_empty univ_info.missing) + then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ))); let arity = Vars.subst_univs_level_constr usubst arity in let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in let indices = Vars.subst_univs_level_context usubst indices in @@ -263,20 +263,20 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp splayed_lc in let param_levels, concl_levels = - template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ + template_polymorphic_univs ~ctor_levels ctx params min_univ in - if template_check && List.for_all (fun x -> Option.is_empty x) param_levels + if List.for_all (fun x -> Option.is_empty x) param_levels && Univ.LSet.is_empty concl_levels then CErrors.user_err Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") else - TemplateArity {template_param_levels = param_levels; template_level = min_univ} + TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx } in let kelim = allowed_sorts univ_info in (arity,lc), (indices,splayed_lc), kelim -let typecheck_inductive env (mie:mutual_inductive_entry) = +let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let () = match mie.mind_entry_inds with | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.") | _ -> () @@ -335,14 +335,24 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = data, Some None in - (* TODO pass only the needed bits *) - let variance = InferCumulativity.infer_inductive env mie in + let variance = if not mie.mind_entry_cumulative then None + else match mie.mind_entry_universes with + | Monomorphic_entry _ -> + CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.") + | Polymorphic_entry (_,uctx) -> + let univs = Instance.to_array @@ UContext.instance uctx in + let univs = match sec_univs with + | None -> univs + | Some sec_univs -> Array.append sec_univs univs + in + let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in + Some variances + in (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in let params = Vars.subst_univs_level_context usubst params in - let template_check = Environ.check_template env in - let data = List.map (abstract_packets ~template_check univs usubst params) data in + let data = List.map (abstract_packets univs usubst params) data in let env_ar_par = let ctx = Environ.rel_context env_ar_par in |