diff options
| -rw-r--r-- | kernel/constr.ml | 46 | ||||
| -rw-r--r-- | kernel/constr.mli | 8 | ||||
| -rw-r--r-- | kernel/reduction.ml | 8 | ||||
| -rw-r--r-- | kernel/univ.ml | 12 |
4 files changed, 66 insertions, 8 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 diff --git a/kernel/constr.mli b/kernel/constr.mli index 0e7bafdc6..e9f736903 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -210,6 +210,14 @@ val eq_constr_univs : constr Univ.check_function alpha, casts, application grouping and the universe inequalities in [u]. *) val leq_constr_univs : constr Univ.check_function +(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, + application grouping and the universe equalities in [u]. *) +val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained + +(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe inequalities in [u]. *) +val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained + (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe equalities in [c]. *) val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5f0684d37..8773f4f34 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -661,11 +661,11 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 = v2 let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = - let b = - if cv_pb == CUMUL then leq_constr_univs univs t1 t2 - else eq_constr_univs univs t1 t2 + let b, cstrs = + if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 + else Constr.eq_constr_univs_infer univs t1 t2 in - if b then Constraint.empty + if b && Univ.check_constraints cstrs univs then cstrs else let (u, cstrs) = clos_fconv reds cv_pb l2r evars env (univs, Some Constraint.empty) t1 t2 diff --git a/kernel/univ.ml b/kernel/univ.ml index 80abf5421..8a48eb5db 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1227,16 +1227,20 @@ let check_equal g u v = let _, arcv = safe_repr g v in arcu == arcv +let set_arc g = + snd (safe_repr g Level.set) + +let prop_arc g = snd (safe_repr g Level.prop) + let check_smaller g strict u v = let g, arcu = safe_repr g u in let g, arcv = safe_repr g v in if strict then is_lt g arcu arcv else - let proparc = snd (safe_repr g Level.prop) in + let proparc = prop_arc g in arcu == proparc || - (let setarc = snd (safe_repr g Level.set) in - (arcu == setarc && arcv != proparc) || + ((arcv != proparc && arcu == set_arc g) || is_leq g arcu arcv) (** Then, checks on universes *) @@ -1448,7 +1452,7 @@ let enforce_univ_lt u v g = | _ -> anomaly (Pp.str "Univ.fast_compare")) let empty_universes = LMap.empty -let initial_universes = enforce_univ_lt Level.prop Level.set LMap.empty +let initial_universes = enforce_univ_leq Level.prop Level.set LMap.empty let is_initial_universes g = LMap.equal (==) g initial_universes (* Constraints and sets of constraints. *) |