Restore reasonable performance by not allocating during universe checks,

using a fast_compare_neq.

6 files changed, 98 insertions, 12 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0a89a0bfd..396175c9e 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 5d565b89e..f156e6028 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
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 908e59227..bca599305 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -126,6 +126,10 @@ let nf_evar_map_undefined evm =
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
+let has_flexible_level evd l =
+  let a = Univ.Instance.to_array l in
+    Array.exists (fun l -> Evd.is_flexible_level evd l) a
+    
 let has_undefined_evars or_sorts evd t =
   let rec has_ev t =
     match kind_of_term t with
@@ -138,7 +142,7 @@ let has_undefined_evars or_sorts evd t =
     | Sort (Type _) (*FIXME could be finer, excluding Prop and Set universes *) when or_sorts ->
       raise Not_found
     | Ind (_,l) | Const (_,l) | Construct (_,l) 
-	when l <> Univ.Instance.empty && or_sorts -> raise Not_found
+	when or_sorts && not (Univ.Instance.is_empty l) (* has_flexible_level evd l *) -> raise Not_found
     | _ -> iter_constr has_ev t in
   try let _ = has_ev t in false
   with (Not_found | NotInstantiatedEvar) -> true
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ef93a827a..21a0603c3 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1021,6 +1021,9 @@ let is_sort_variable evd s =
     | None -> None)
   | _ -> None
 
+let is_flexible_level evd l = 
+  let uctx = evd.universes in
+    Univ.LMap.mem l uctx.uctx_univ_variables
 
 let is_eq_sort s1 s2 =
   if Sorts.equal s1 s2 then None
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index e44e8e906..020f0a7b4 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -439,6 +439,9 @@ val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
 val is_sort_variable : evar_map -> sorts -> (Univ.universe_level * bool) option 
 (** [is_sort_variable evm s] returns [Some (u, is_rigid)] or [None] if [s] is 
     not a sort variable declared in [evm] *)
+val is_flexible_level : evar_map -> Univ.Level.t -> bool
+
+
 val whd_sort_variable : evar_map -> constr -> constr
 (* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *)
 val normalize_universe : evar_map -> Univ.universe -> Univ.universe
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index a6bc44682..23e131272 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -594,7 +594,7 @@ Section Z_2nZ.
       0 <= [|r|] < [|b|].
  Proof.
   refine (spec_ww_div21 w_0 w_0W div32 ww_1 compare sub w_digits w_to_Z
-   _ _ _ _ _ _ _);wwauto.
+   _ _ _ _ _ _ _);wwauto. 
  Qed.
 
  Let spec_add2: forall x y,