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).

3 files changed, 56 insertions, 27 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 038b91ec61..e125a1c6e5 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -408,11 +408,12 @@ let process_universe_constraints univs vars alg templ cstrs =
 	      | None -> error ("Algebraic universe on the right")
 	      | Some rl ->
 		if Univ.Level.is_small rl then
-		  (if Univ.LSet.for_all (fun l ->
-		    Univ.Level.is_small l || Univ.LMap.mem l !vars)
-		      (Univ.Universe.levels l) then
-		      Univ.enforce_leq l r local
-		   else raise (Univ.UniverseInconsistency (Univ.Le, l, r, [])))
+		  let levels = Univ.Universe.levels l in
+		    Univ.LSet.fold (fun l local ->
+		      if Univ.Level.is_small l || Univ.LMap.mem l !vars then
+			Univ.enforce_eq (Univ.Universe.make l) r local
+		      else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, [])))
+		      levels local
 		else if Univ.LSet.mem rl templ && Univ.Universe.is_level l then
 		  unify_universes fo l Univ.UEq r local
 		else
@@ -446,8 +447,7 @@ let process_universe_constraints univs vars alg templ cstrs =
 	        Univ.enforce_eq_level l' r' local
            | _, _ (* One of the two is algebraic or global *) -> 
 	     if Univ.check_eq univs l r then local
-	     else 
-	       raise UniversesDiffer
+	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, []))
   in
   let local = 
     Univ.UniverseConstraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
@@ -1151,9 +1151,9 @@ let set_eq_level d u1 u2 =
 let set_leq_level d u1 u2 =
   add_constraints d (Univ.enforce_leq_level u1 u2 Univ.Constraint.empty)
 
-let set_eq_instances d u1 u2 =
+let set_eq_instances ?(flex=false) d u1 u2 =
   add_universe_constraints d
-    (Univ.enforce_eq_instances_univs false u1 u2 Univ.UniverseConstraints.empty)
+    (Univ.enforce_eq_instances_univs flex u1 u2 Univ.UniverseConstraints.empty)
 
 let set_leq_sort evd s1 s2 =
   let s1 = normalize_sort evd s1 
@@ -1161,12 +1161,12 @@ let set_leq_sort evd s1 s2 =
   match is_eq_sort s1 s2 with
   | None -> evd
   | Some (u1, u2) ->
-    if Univ.is_type0_univ u2 then
-      if Univ.is_small_univ u1 then evd
-      else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, []))
-    else if Univ.is_type0m_univ u2 then 
-      raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, []))
-    else 
+    (* if Univ.is_type0_univ u2 then *)
+    (*   if Univ.is_small_univ u1 then evd *)
+    (*   else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
+    (* else if Univ.is_type0m_univ u2 then  *)
+    (*   raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
+    (* else  *)
       add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2))
 	    
 let check_eq evd s s' =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 8a9753e5b3..8bdfccb6b1 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -458,7 +458,8 @@ val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
 val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map
 val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
 val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
-val set_eq_instances : evar_map -> Univ.universe_instance -> Univ.universe_instance -> evar_map
+val set_eq_instances : ?flex:bool -> 
+  evar_map -> Univ.universe_instance -> Univ.universe_instance -> evar_map
 
 val check_eq : evar_map -> Univ.universe -> Univ.universe -> bool
 val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2d8e935bb5..f75da1383f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1124,7 +1124,7 @@ let pb_equal = function
   | Reduction.CONV -> Reduction.CONV
 
 let sort_cmp cv_pb s1 s2 u = 
-  ignore(Reduction.sort_cmp_universes cv_pb s1 s2 (u, None))
+  Reduction.check_sort_cmp_universes cv_pb s1 s2 u
 
 let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y =
   try
@@ -1145,22 +1145,50 @@ let is_fconv = function | Reduction.CONV -> is_conv | Reduction.CUMUL -> is_conv
 let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = 
   let f = match pb with
     | Reduction.CONV -> Reduction.trans_conv_universes
-    | Reduction.CUMUL -> Reduction.trans_conv_leq_universes in
+    | Reduction.CUMUL -> Reduction.trans_conv_leq_universes 
+  in
     try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true
     with Reduction.NotConvertible -> false
     | Univ.UniverseInconsistency _ -> false
     | e when is_anomaly e -> error "Conversion test raised an anomaly"
 
+let sigma_compare_sorts pb s0 s1 sigma =
+  match pb with
+  | Reduction.CONV -> Evd.set_eq_sort sigma s0 s1
+  | Reduction.CUMUL -> Evd.set_leq_sort sigma s0 s1
+    
+let sigma_compare_instances flex i0 i1 sigma =
+  try Evd.set_eq_instances ~flex sigma i0 i1
+  with Evd.UniversesDiffer -> raise Reduction.NotConvertible
+
+let sigma_univ_state = 
+  { Reduction.compare = sigma_compare_sorts;
+    Reduction.compare_instances = sigma_compare_instances }
+
 let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = 
-  let f = match pb with
-    | Reduction.CONV -> Reduction.infer_conv
-    | Reduction.CUMUL -> Reduction.infer_conv_leq in
-    try 
-      let cstrs = f ~evars:(safe_evar_value sigma) ~ts env (Evd.universes sigma) x y in
-	Evd.add_constraints sigma cstrs, true
-    with Reduction.NotConvertible -> sigma, false
-    | Univ.UniverseInconsistency _ -> sigma, false
-    | e when is_anomaly e -> error "Conversion test raised an anomaly"
+  try 
+    let b, sigma = 
+      let b, cstrs = 
+	if pb == Reduction.CUMUL then 
+	  Constr.leq_constr_univs_infer (Evd.universes sigma) x y 
+	else
+	  Constr.eq_constr_univs_infer (Evd.universes sigma) x y 
+      in
+	if b then 
+	  try true, Evd.add_universe_constraints sigma cstrs
+	  with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> false, sigma
+	else false, sigma
+    in
+      if b then sigma, true
+      else
+	let sigma' = 
+	  Reduction.generic_conv pb false (safe_evar_value sigma) ts 
+	    env (sigma, sigma_univ_state) x y in
+	  sigma', true
+  with
+  | Reduction.NotConvertible -> sigma, false
+  | Univ.UniverseInconsistency _ -> sigma, false
+  | e when is_anomaly e -> error "Conversion test raised an anomaly"
     
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)