diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 34 | ||||
| -rw-r--r-- | kernel/univ.ml | 16 | ||||
| -rw-r--r-- | kernel/univ.mli | 7 |
3 files changed, 39 insertions, 18 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 94bf1a770..068332406 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -207,6 +207,24 @@ let param_ccls paramsctxt = in List.fold_left fold [] paramsctxt +(* Check arities and constructors *) +let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) is_arity = + let basic_check ev tp = conv_leq ev tp (subst tp) in + let check_typ typ typ_env = + match typ with + | LocalAssum (_, typ') -> + begin + try + basic_check env typ'; Environ.push_rel typ typ_env + with NotConvertible -> + anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation!") + end + | _ -> anomaly (Pp.str "") + in + let typs, codom = 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 () + (* Type-check an inductive definition. Does not check positivity conditions. *) (* TODO check that we don't overgeneralize construcors/inductive arities with @@ -345,6 +363,22 @@ let typecheck_inductive env mie = in (id,cn,lc,(sign,arity))) inds + in + (* Check that the subtyping information inferred for inductive types in the block is correct. *) + (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) + let () = + let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in + let dosubst = subst_univs_level_constr sbsubst in + let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env_ar_par in + (* process individual inductive types: *) + Array.iter (fun (id,cn,lc,(sign,arity)) -> + match arity with + | RegularArity (_, full_arity, _) -> + check_subtyping_arity_constructor envsb dosubst full_arity true; + Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt true) lc + | TemplateArity _ -> () + (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *) + ) inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) diff --git a/kernel/univ.ml b/kernel/univ.ml index f124bb39e..4a4cf1baa 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1049,7 +1049,7 @@ struct let empty = (UContext.empty, UContext.empty) let is_empty (univcst, subtypcst) = UContext.is_empty univcst && UContext.is_empty subtypcst - let halve_context (ctx : Instance.t) : Instance.t * Instance.t = + let halve_context ctx = let len = Array.length (Instance.to_array ctx) in let halflen = len / 2 in (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen), @@ -1084,17 +1084,9 @@ struct (univcst, UContext.make (Instance.append inst freshunivs, create_trivial_subtyping inst freshunivs)) - (** This function adds universe constraints to the universe - constraints of the given universe_info_ind. However one must be - CAUTIOUS as it resets the subtyping constraints to equality. It - also requires fresh universes for the newly introduced - universes *) - let union (univcst, _) univcst' freshunivs = - assert (Instance.length freshunivs = Instance.length (UContext.instance univcst')); - let (ctx, ctx') = halve_context (UContext.instance univcst) in - let newctx' = Instance.append ctx' freshunivs in - let univcstunion = UContext.union univcst univcst' in - (univcstunion, subtyp_context (from_universe_context univcstunion newctx')) + let subtyping_susbst (univcst, subtypcst) = + let (ctx, ctx') = (halve_context (UContext.instance subtypcst))in + Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx' let dest x = x diff --git a/kernel/univ.mli b/kernel/univ.mli index 630d0d949..f139a8b33 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -345,12 +345,7 @@ sig trivial subtyping relation. *) val from_universe_context : universe_context -> universe_instance -> t - (** This function adds universe constraints to the universe - constraints of the given universe_info_ind. However one must be - CAUTIOUS as it resets the subtyping constraints to equality. It - also requires fresh universes for the newly introduced - universes *) - val union : t -> universe_context -> universe_instance -> t + val subtyping_susbst : t -> universe_level_subst val size : t -> int |