diff options
| author | Pierre-Marie Pédrot | 2015-11-19 13:36:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-26 14:56:24 +0100 |
| commit | 103ec7205d9038f1f3821f9287e3bb0907a1e3ec (patch) | |
| tree | e80f338121ea2f84d7978ef45d1adc310f308447 /pretyping | |
| parent | 36c6e9508a42d00686e90441999481354152aaa3 (diff) | |
More efficient implementation of equality-up-to-universes in Universes.
Instead of accumulating constraints which are not present in the original
graph, we parametrize the equality function by a function actually merging
those constraints in the current graph. This prevents doing the work twice.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 13 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 19 |
2 files changed, 18 insertions, 14 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 508b9e8027..3c3afac54e 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -860,13 +860,14 @@ let kind_of_term_upto sigma t = let eq_constr_univs_test sigma1 sigma2 t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in - let b, c = + let fold cstr sigma = + try Some (add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | UniversesDiffer -> None + in + let ans = Universes.eq_constr_univs_infer_with (fun t -> kind_of_term_upto sigma1 t) (fun u -> kind_of_term_upto sigma2 u) - (universes sigma2) t u + (universes sigma2) fold t u sigma2 in - if b then - try let _ = add_universe_constraints sigma2 c in true - with Univ.UniverseInconsistency _ | UniversesDiffer -> false - else false + match ans with None -> false | Some _ -> true diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index bdd9ed81cf..d5a93230f3 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1299,18 +1299,21 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = - try + try + let fold cstr sigma = + try Some (Evd.add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None + in let b, sigma = - let b, cstrs = + let ans = if pb == Reduction.CUMUL then - Universes.leq_constr_univs_infer (Evd.universes sigma) x y + Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y sigma else - Universes.eq_constr_univs_infer (Evd.universes sigma) x y + Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y sigma in - if b then - try true, Evd.add_universe_constraints sigma cstrs - with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> false, sigma - else false, sigma + match ans with + | None -> false, sigma + | Some sigma -> true, sigma in if b then sigma, true else |