From c01d225f9e112bb08f9df26f70805bde0c0d127a Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 24 May 2017 13:45:08 +0200 Subject: Enable the checking of ind subtyping in checker --- checker/indtypes.ml | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) (limited to 'checker/indtypes.ml') diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 69dd6f57a..cac7e6313 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -549,25 +549,24 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con (* 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 check_subtyping mib paramsctxt env_ar inds = - let numparams = rel_context_nhyps paramsctxt in - let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in - let dosubst = subst_instance_constr sbsubst in - let uctx = Univ.UInfoInd.univ_context mib.mind_universes in - let instance_other = Univ.subst_instance_instance sbsubst (Univ.UContext.instance uctx) in - let constraints_other = Univ.subst_instance_constraints sbsubst (Univ.UContext.constraints uctx) in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env' = Environ.push_context uctx env_ar in - let env'' = Environ.push_context uctx_other env' in - let envsb = push_context (Univ.UInfoInd.subtyp_context mib.mind_universes) env'' in - (* process individual inductive types: *) - Array.iter (fun { mind_user_lc = lc; mind_arity = arity } -> + let numparams = rel_context_nhyps paramsctxt in + let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in + let other_instnace = Univ.UInfoInd.subtyping_other_instance mib.mind_universes in + let dosubst = subst_univs_level_constr sbsubst in + let uctx = Univ.UInfoInd.univ_context mib.mind_universes in + let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) in + let env = Environ.push_context uctx env_ar in + let env = Environ.push_context uctx_other env in + let env = Environ.push_context (Univ.instantiate_univ_context (Univ.UInfoInd.subtyp_context mib.mind_universes)) env in + (* process individual inductive types: *) + Array.iter (fun { mind_user_lc = lc; mind_arity = arity } -> match arity with - | RegularArity { mind_user_arity = full_arity} -> - check_subtyping_arity_constructor envsb dosubst full_arity numparams true; - Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc - | TemplateArity _ -> () + | RegularArity { mind_user_arity = full_arity} -> + check_subtyping_arity_constructor env dosubst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc + | TemplateArity _ -> () ) inds - + (************************************************************************) (************************************************************************) @@ -592,7 +591,8 @@ let check_inductive env kn mib = (* - check constructor types *) Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; (* check the inferred subtyping relation *) - (* check_subtyping mib params env_ar mib.mind_packets; *) + if mib.mind_cumulative then + check_subtyping mib params env_ar mib.mind_packets; (* check mind_nparams_rec: positivity condition *) check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets; (* check mind_equiv... *) -- cgit v1.2.3