From 103ec7205d9038f1f3821f9287e3bb0907a1e3ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 19 Nov 2015 13:36:31 +0100
Subject: 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.
---
 pretyping/evarutil.ml     | 13 +++++++------
 pretyping/reductionops.ml | 19 +++++++++++--------
 2 files changed, 18 insertions(+), 14 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3