diff options
Diffstat (limited to 'kernel/indTyping.ml')
| -rw-r--r-- | kernel/indTyping.ml | 107 |
1 files changed, 37 insertions, 70 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 06d2e1bb21..d9ccf81619 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -61,64 +61,6 @@ let mind_check_names mie = (************************************************************************) -(************************** Cumulativity checking************************) -(************************************************************************) - -(* Check arities and constructors *) -let check_subtyping_arity_constructor env subst arcn numparams is_arity = - let numchecked = ref 0 in - let basic_check ev tp = - if !numchecked < numparams then () else Reduction.conv_leq ev tp (subst tp); - numchecked := !numchecked + 1 - in - let check_typ typ typ_env = - match typ with - | LocalAssum (_, typ') -> - begin - try - basic_check typ_env typ'; Environ.push_rel typ typ_env - with Reduction.NotConvertible -> - CErrors.anomaly ~label:"bad inductive subtyping relation" - Pp.(str "Invalid subtyping relation") - end - | _ -> CErrors.anomaly Pp.(str "") - in - let typs, codom = Reduction.dest_prod env arcn in - let last_env = Context.Rel.fold_outside check_typ typs ~init:env in - if not is_arity then basic_check last_env codom else () - -let check_cumulativity univs variances env_ar params data = - let uctx = match univs with - | Monomorphic_entry _ -> raise (InductiveError BadUnivs) - | Polymorphic_entry (_,uctx) -> uctx - in - let instance = UContext.instance uctx in - if Instance.length instance != Array.length variances then raise (InductiveError BadUnivs); - let numparams = Context.Rel.nhyps params in - let new_levels = Array.init (Instance.length instance) - (fun i -> Level.(make (UGlobal.make DirPath.empty i))) - in - let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) - LMap.empty (Instance.to_array instance) new_levels - in - let dosubst = Vars.subst_univs_level_constr lmap in - let instance_other = Instance.of_array new_levels in - let constraints_other = Univ.subst_univs_level_constraints lmap (UContext.constraints uctx) in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx_other env_ar in - let subtyp_constraints = - Univ.enforce_leq_variance_instances variances - instance instance_other - Constraint.empty - in - let env = Environ.add_constraints subtyp_constraints env in - (* process individual inductive types: *) - List.iter (fun (arity,lc) -> - check_subtyping_arity_constructor env dosubst arity numparams true; - Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc) - data - -(************************************************************************) (************************** Type checking *******************************) (************************************************************************) @@ -253,10 +195,11 @@ 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 uctx paramsctxt concl = +let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl = let check_level l = if Univ.LSet.mem l (Univ.ContextSet.levels uctx) && - unbounded_from_below l (Univ.ContextSet.constraints uctx) then + unbounded_from_below l (Univ.ContextSet.constraints uctx) && + not (Univ.LSet.mem l ctor_levels) then Some l else None in @@ -302,10 +245,31 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp | Polymorphic _ -> CErrors.anomaly ~label:"polymorphic_template_ind" Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in - let param_levels, concl_levels = template_polymorphic_univs ~template_check ctx params min_univ in + 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 params + in + Array.fold_left + (fun levels (d,c) -> + let levels = + List.fold_left (fun levels d -> + Context.Rel.Declaration.fold_constr add_levels d levels) + levels d + in + add_levels c levels) + param_levels + splayed_lc + in + let param_levels, concl_levels = + template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ + in if template_check && List.for_all (fun x -> Option.is_empty x) param_levels && Univ.LSet.is_empty concl_levels then - CErrors.anomaly ~label:"polymorphic_template_ind" + 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} @@ -329,8 +293,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = let env_univs = match mie.mind_entry_universes with | Monomorphic_entry ctx -> - let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in - push_context_set ctx env + if has_template_poly then + (* For that particular case, we typecheck the inductive in an environment + where the universes introduced by the definition are only [>= Prop] *) + let env = set_universes_lbound env Univ.Level.prop in + push_context_set ~strict:false ctx env + else + (* In the regular case, all universes are [> Set] *) + push_context_set ~strict:true ctx env | Polymorphic_entry (_, ctx) -> push_context ctx env in @@ -367,11 +337,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = data, Some None in - let () = match mie.mind_entry_variance with - | None -> () - | Some variances -> - check_cumulativity mie.mind_entry_universes variances env_ar params (List.map pi1 data) - in + (* TODO pass only the needed bits *) + let variance = InferCumulativity.infer_inductive env mie in (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in @@ -386,4 +353,4 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = Environ.push_rel_context ctx env in - env_ar_par, univs, mie.mind_entry_variance, record, params, Array.of_list data + env_ar_par, univs, variance, record, params, Array.of_list data |