Restore reasonable performance by not allocating during universe checks,

using a fast_compare_neq.

2 files changed, 86 insertions, 10 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0a89a0bfdb..396175c9e5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -133,7 +133,7 @@ let beta_appvect c v =
         Lambda(_,_,c), arg::stacktl -> stacklam (arg::env) c stacktl
       | _ -> applist (substl env t, stack) in
   stacklam [] c (Array.to_list v)
-
+    
 let betazeta_appvect n c v =
   let rec stacklam n env t stack =
     if Int.equal n 0 then applist (substl env t, stack) else
@@ -165,7 +165,14 @@ let convert_universes (univs,cstrs as cuniv) u u' =
   else
     (match cstrs with 
     | None -> raise NotConvertible
-    | Some cstrs -> (univs, Some (Univ.enforce_eq_instances u u' cstrs)))
+    | Some cstrs -> 
+      (univs, Some (Univ.enforce_eq_instances u u' cstrs)))
+
+      (* try  *)
+      (* 	let cstr = Univ.enforce_eq_instances u u' Univ.Constraint.empty in *)
+      (* 	let univs' = Univ.enforce_constraint cstr univs in *)
+      (* 	  (univs', Some (Univ.enforce_eq_instances u u' cstrs)) *)
+      (* with UniverseInconsistency _ -> raise NotConvertible) *)
       
 let conv_table_key k1 k2 cuniv =
   match k1, k2 with
@@ -239,12 +246,22 @@ let is_pos = function Pos -> true | Null -> false
 let check_eq (univs, cstrs as cuniv) u u' = 
   match cstrs with
   | None -> if check_eq univs u u' then cuniv else raise NotConvertible
-  | Some cstrs -> univs, Some (Univ.enforce_eq u u' cstrs)
+  | Some cstrs -> 
+    univs, Some (Univ.enforce_eq u u' cstrs)
+    (* let cstr = Univ.enforce_eq u u' Univ.Constraint.empty in *)
+    (* try let univs' = Univ.enforce_constraint cstr univs in *)
+    (* 	  univs', Some (Univ.enforce_eq u u' cstrs) *)
+    (* with UniverseInconsistency _ -> raise NotConvertible *)
 
 let check_leq (univs, cstrs as cuniv) u u' = 
   match cstrs with
   | None -> if check_leq univs u u' then cuniv else raise NotConvertible
-  | Some cstrs -> univs, Some (Univ.enforce_leq u u' cstrs)
+  | Some cstrs -> 
+    univs, Some (Univ.enforce_leq u u' cstrs)
+    (* let cstr = Univ.enforce_leq u u' Univ.Constraint.empty in *)
+    (*   try let univs' = Univ.enforce_constraint cstr univs in *)
+    (* 	    univs', Some (Univ.enforce_leq u u' cstrs) *)
+    (*   with UniverseInconsistency _ -> raise NotConvertible *)
 
 let sort_cmp_universes pb s0 s1 univs =
   let dir = if is_cumul pb then check_leq univs else check_eq univs in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 5d565b89ed..f156e6028e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1011,19 +1011,78 @@ let compare_neq strict g arcu arcv =
   in
   cmp NLE [] [] [] [arcu, Lazy.lazy_from_val []]
 
+type fast_order = FastEQ | FastLT | FastLE | FastNLE
+
+let fast_compare_neq strict g arcu arcv =
+  (* [c] characterizes whether arcv has already been related
+     to arcu among the lt_done,le_done universe *)
+  let rec cmp c lt_done le_done lt_todo le_todo = match lt_todo, le_todo with
+  | [],[] -> c
+  | arc::lt_todo, le_todo ->
+    if List.memq arc lt_done then
+      cmp c lt_done le_done lt_todo le_todo
+    else
+      let rec find lt_todo lt le = match le with
+      | [] ->
+        begin match lt with
+        | [] -> cmp c (arc :: lt_done) le_done lt_todo le_todo
+        | u :: lt ->
+          let arc = repr g u in
+          if arc == arcv then
+            if strict then FastLT else FastLE
+          else find (arc :: lt_todo) lt le
+        end
+      | u :: le ->
+        let arc = repr g u in
+        if arc == arcv then
+          if strict then FastLT else FastLE
+        else find (arc :: lt_todo) lt le
+      in
+      find lt_todo arc.lt arc.le
+  | [], arc::le_todo ->
+    if arc == arcv then
+      (* No need to continue inspecting universes above arc:
+	 if arcv is strictly above arc, then we would have a cycle.
+         But we cannot answer LE yet, a stronger constraint may
+	 come later from [le_todo]. *)
+      if strict then cmp FastLE lt_done le_done [] le_todo else FastLE
+    else
+      if (List.memq arc lt_done) || (List.memq arc le_done) then
+        cmp c lt_done le_done [] le_todo
+      else
+        let rec find lt_todo lt = match lt with
+        | [] ->
+          let fold accu u =
+            let node = repr g u in
+            node :: accu
+          in
+          let le_new = List.fold_left fold le_todo arc.le in
+          cmp c lt_done (arc :: le_done) lt_todo le_new
+        | u :: lt ->
+          let arc = repr g u in
+          if arc == arcv then
+            if strict then FastLT else FastLE
+          else find (arc :: lt_todo) lt
+        in
+        find [] arc.lt
+  in
+  cmp FastNLE [] [] [] [arcu]
+
 let compare g arcu arcv =
   if arcu == arcv then EQ else compare_neq true g arcu arcv
 
 let is_leq g arcu arcv =
   arcu == arcv ||
- (match compare_neq false g arcu arcv with
-     NLE -> false
-   | (EQ|LE _|LT _) -> true)
+ (match fast_compare_neq false g arcu arcv with
+     FastNLE -> false
+   | (FastEQ|FastLE|FastLT) -> true)
 
 let is_lt g arcu arcv =
-  match compare g arcu arcv with
-      LT _ -> true
-    | (EQ|LE _|NLE) -> false
+  if arcu == arcv then false
+  else
+    match fast_compare_neq true g arcu arcv with
+      FastLT -> true
+    | (FastEQ|FastLE|FastNLE) -> false
 
 (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
                 compare(u,v) = LT or LE => compare(v,u) = NLE