From ab86b9b3999f3860bdb69824f585b9cf461ff295 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Fri, 7 Apr 2017 12:44:12 +0200 Subject: Use inductive subtyping for conv/cumul --- pretyping/reductionops.ml | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'pretyping/reductionops.ml') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c2a648301..971ad78e6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1361,9 +1361,24 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible +let sigma_leq_inductives ~flex uinfind i0 i1 sigma = + let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in + let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + if not ((Univ.Instance.length ind_instance = Univ.Instance.length i0) && + (Univ.Instance.length ind_instance = Univ.Instance.length i1)) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + let comp_subst = (Univ.Instance.append i0 i1) in + let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in + try Evd.add_constraints sigma comp_cst + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible + let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances } + Reduction.compare_instances = sigma_compare_instances; + Reduction.leq_inductives = sigma_leq_inductives } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = -- cgit v1.2.3