Make kernel reduction code parametric over the handling of universes,

allowing fast conversion to be used during unification while respecting the
semantics of unification w.r.t universes.
- Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv
is used for module subtyping.
- Outside, infer_conv is wrapped in Reductionops to register the right constraints
in an evarmap.
- In univ, add a flag to universes to cache the fact that they are >= Set, the
most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS).

1 files changed, 15 insertions, 10 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index fbcdc886b..532d44d9e 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -578,16 +578,18 @@ let leq_constr_univs univs m n =
       compare_leq m n
 
 let eq_constr_univs_infer univs m n =
-  if m == n then true, Constraint.empty
+  if m == n then true, UniverseConstraints.empty
   else 
-    let cstrs = ref Constraint.empty in
+    let cstrs = ref UniverseConstraints.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)
+	  if Univ.check_eq univs u1 u2 then true
+	  else
+	    (cstrs := Univ.UniverseConstraints.add (u1, Univ.UEq, u2) !cstrs;
+	     true)
     in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -596,23 +598,26 @@ let eq_constr_univs_infer univs m n =
       res, !cstrs
 
 let leq_constr_univs_infer univs m n =
-  if m == n then true, Constraint.empty
+  if m == n then true, UniverseConstraints.empty
   else 
-    let cstrs = ref Constraint.empty in
+    let cstrs = ref UniverseConstraints.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)
+	  if Univ.check_eq univs u1 u2 then true
+	  else (cstrs := Univ.UniverseConstraints.add (u1, Univ.UEq, 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)
+	  if Univ.check_leq univs u1 u2 then true
+	  else
+	    (cstrs := Univ.UniverseConstraints.add (u1, Univ.ULe, u2) !cstrs; 
+	     true)
     in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n