diff options
| -rw-r--r-- | kernel/indTyping.ml | 10 | ||||
| -rw-r--r-- | kernel/inferCumulativity.ml | 28 | ||||
| -rw-r--r-- | kernel/inferCumulativity.mli | 13 |
3 files changed, 27 insertions, 24 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index b19472dc99..3f2f9f4fc0 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -335,8 +335,14 @@ 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 + Some (InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds) + in (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 77abe6b410..211c909241 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -188,15 +188,12 @@ let infer_arity_constructor is_arity env variances arcn = open Entries -let infer_inductive_core env params entries uctx = - let uarray = Instance.to_array @@ UContext.instance uctx in - if Array.is_empty uarray then raise TrivialVariance; - let env = Environ.push_context uctx env in +let infer_inductive_core env univs entries = + if Array.is_empty univs then raise TrivialVariance; let variances = Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances) - LMap.empty uarray + LMap.empty univs in - let env, _ = Typeops.check_context env params in let variances = List.fold_left (fun variances entry -> let variances = infer_arity_constructor true env variances entry.mind_entry_arity @@ -210,17 +207,8 @@ let infer_inductive_core env params entries uctx = | exception Not_found -> Invariant | IrrelevantI -> Irrelevant | CovariantI -> Covariant) - uarray - -let infer_inductive env mie = - let open Entries in - let params = mie.mind_entry_params in - let entries = mie.mind_entry_inds in - if not mie.mind_entry_cumulative then None - else - let uctx = match mie.mind_entry_universes with - | Monomorphic_entry _ -> assert false - | Polymorphic_entry (_,uctx) -> uctx - in - try Some (infer_inductive_core env params entries uctx) - with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant) + univs + +let infer_inductive ~env_params univs entries = + try infer_inductive_core env_params univs entries + with TrivialVariance -> Array.make (Array.length univs) Invariant diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli index 2bddfe21e2..a8f593c7f9 100644 --- a/kernel/inferCumulativity.mli +++ b/kernel/inferCumulativity.mli @@ -8,5 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> - Univ.Variance.t array option +val infer_inductive + : env_params:Environ.env + (** Environment containing the polymorphic universes and the + parameters. *) + -> Univ.Level.t array + (** Universes whose cumulativity we want to infer. *) + -> Entries.one_inductive_entry list + (** The inductive block data we want to infer cumulativity for. + NB: we ignore the template bool and the names, only the terms + are used. *) + -> Univ.Variance.t array |