Stupid but critical unfolding heuristic.

We favour unfolding of variables over constants because it is more frequent
for the former to depend on the latter. This has huge consequences on a few
extremely slow lines in mathcomp, up to dividing by 3 single-line invocations
that were taking about 30s on my laptop before the patch.

2 files changed, 24 insertions, 6 deletions

diff --git a/checker/reduction.ml b/checker/reduction.ml
index d36c0ef2c9..58a3f4e410 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -280,17 +280,26 @@ let get_strategy { var_opacity; cst_opacity } = function
       with Not_found -> default_level)
   | RelKey _ -> Expand
 
+let dep_order l2r k1 k2 = match k1, k2 with
+| RelKey _, RelKey _ -> l2r
+| RelKey _, (VarKey _ | ConstKey _) -> true
+| VarKey _, RelKey _ -> false
+| VarKey _, VarKey _ -> l2r
+| VarKey _, ConstKey _ -> true
+| ConstKey _, (RelKey _ | VarKey _) -> false
+| ConstKey _, ConstKey _ -> l2r
+
 let oracle_order infos l2r k1 k2 =
   let o = Closure.oracle_of_infos infos in
   match get_strategy o k1, get_strategy o k2 with
-  | Expand, Expand -> l2r
+  | Expand, Expand -> dep_order l2r k1 k2
   | Expand, (Opaque | Level _) -> true
   | (Opaque | Level _), Expand -> false
-  | Opaque, Opaque -> l2r
+  | Opaque, Opaque -> dep_order l2r k1 k2
   | Level _, Opaque -> true
   | Opaque, Level _ -> false
   | Level n1, Level n2 ->
-     if Int.equal n1 n2 then l2r
+     if Int.equal n1 n2 then dep_order l2r k1 k2
      else n1 < n2
 
 let eq_table_key univ =
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index c74f2ab318..ac78064235 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -83,18 +83,27 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu =
 
 let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate)
 
+let dep_order l2r k1 k2 = match k1, k2 with
+| RelKey _, RelKey _ -> l2r
+| RelKey _, (VarKey _ | ConstKey _) -> true
+| VarKey _, RelKey _ -> false
+| VarKey _, VarKey _ -> l2r
+| VarKey _, ConstKey _ -> true
+| ConstKey _, (RelKey _ | VarKey _) -> false
+| ConstKey _, ConstKey _ -> l2r
+
 (* Unfold the first constant only if it is "more transparent" than the
    second one. In case of tie, use the recommended default. *)
 let oracle_order f o l2r k1 k2 =
   match get_strategy o f k1, get_strategy o f k2 with
-  | Expand, Expand -> l2r
+  | Expand, Expand -> dep_order l2r k1 k2
   | Expand, (Opaque | Level _) -> true
   | (Opaque | Level _), Expand -> false
-  | Opaque, Opaque -> l2r
+  | Opaque, Opaque -> dep_order l2r k1 k2
   | Level _, Opaque -> true
   | Opaque, Level _ -> false
   | Level n1, Level n2 ->
-     if Int.equal n1 n2 then l2r
+     if Int.equal n1 n2 then dep_order l2r k1 k2
      else n1 < n2
 
 let get_strategy o = get_strategy o (fun x -> x)