diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-05-24 15:13:47 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-26 14:16:26 +0200 |
commit | d8176e6baaa33692ed82b9ac3c6e57e85f51dff0 (patch) | |
tree | 220abe1095acdff596bbf89b31decd67df11270b /kernel/constr.ml | |
parent | 13deafee96893a5ec332ad221469e3e5460693f1 (diff) |
Update infer_conv to record trivial Prop <= Type i constraints that are needed during
unification.
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r-- | kernel/constr.ml | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index c6eacc289..fbcdc886b 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -577,6 +577,52 @@ let leq_constr_univs univs m n = and leq_constr' m n = m == n || compare_leq m n in compare_leq m n +let eq_constr_univs_infer univs m n = + if m == n then true, Constraint.empty + else + let cstrs = ref Constraint.empty in + let eq_universes strict = Univ.Instance.check_eq univs in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + (cstrs := Univ.enforce_eq u1 u2 !cstrs; + true) + in + let rec eq_constr' m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in + res, !cstrs + +let leq_constr_univs_infer univs m n = + if m == n then true, Constraint.empty + else + let cstrs = ref Constraint.empty in + let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + (cstrs := Univ.enforce_eq u1 u2 !cstrs; + true) + in + let leq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + (cstrs := Univ.enforce_leq u1 u2 !cstrs; + true) + in + let rec eq_constr' m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let rec compare_leq m n = + compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n + and leq_constr' m n = m == n || compare_leq m n in + let res = compare_leq m n in + res, !cstrs + let eq_constr_universes m n = if m == n then true, UniverseConstraints.empty else |