diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-04-07 12:44:12 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:15 +0200 |
| commit | ab86b9b3999f3860bdb69824f585b9cf461ff295 (patch) | |
| tree | b48f8201447f59e76abf64a443c353f668dfca61 /pretyping | |
| parent | c07215582ab75faeea864827b153eed80a28527a (diff) | |
Use inductive subtyping for conv/cumul
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 17 |
1 files changed, 16 insertions, 1 deletions
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 = |