diff options
| author | Gaëtan Gilbert | 2018-02-20 00:27:40 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-03-09 16:29:06 +0100 |
| commit | db0918bfa5089f9ab44374504cbd0ddc758ea1e5 (patch) | |
| tree | 5b68a2bd48fc961987a193f4361c46f7b9940b33 /pretyping/evarconv.ml | |
| parent | 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 (diff) | |
Cumulativity: improve treatment of irrelevant universes.
In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 29 |
1 files changed, 4 insertions, 25 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 130aa8cd7e..d37090a653 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -352,34 +352,13 @@ let exact_ise_stack2 env evd f sk1 sk2 = ise_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) -let try_soft evd u u' = - let open Universes in - let make = Univ.Universe.make in - try Evd.add_universe_constraints evd (Constraints.singleton (make u,ULub,make u')) - with UState.UniversesDiffer | Univ.UniverseInconsistency _ -> evd - (* Add equality constraints for covariant/invariant positions. For irrelevant positions, unify universes when flexible. *) let compare_cumulative_instances evd variances u u' = - let cstrs = Univ.Constraint.empty in - let soft = [] in - let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' -> - let open Univ.Variance in - match v with - | Irrelevant -> cstrs, (u,u')::soft - | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft) - (cstrs,soft) variances (Univ.Instance.to_array u) (Univ.Instance.to_array u') - in - match Evd.add_constraints evd cstrs with - | evd -> - Success (List.fold_left (fun evd (u,u') -> try_soft evd u u') evd soft) - | exception Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) - -(* We should only compare constructors at convertible types, so this - is only an opportunity to unify universes. *) -let compare_constructor_instances evd u u' = - Array.fold_left2 try_soft - evd (Univ.Instance.to_array u) (Univ.Instance.to_array u') + match Evarutil.compare_cumulative_instances CONV variances u u' evd with + | Inl evd -> + Success evd + | Inr p -> UnifFailure (evd, UnifUnivInconsistency p) let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in |