Speedup free_vars_and_rels_up_alias_expansion (evarconv)

Small cache to avoid checking the same Rel or Var twice.
Consider an unification problem like the following one:

a := huge
b := F1 a + F2 a
c := G1 b + G2 b
===============
 ?i[c,b,a] == ?g[c,c,c]

The old code, as the "not optimal" comment was suggesting,
did process every item in the explicit substitution, even
duplicated ones, unfolding the letins over and over.

This was the cause of the huge slowdown in the definition
of cormen_lup in Ssreflect/theories/matrix.v, that
follows:

Fixpoint cormen_lup {n} :=
  match n return let M := 'M[F]_n.+1 in M -> M * M * M with
  | 0 => fun A => (1, 1, A)
  | _.+1 => fun A =>
    let k := odflt 0 [pick k | A k 0 != 0] in
    let A1 : 'M_(1 + _) := xrow 0 k A in
    let P1 : 'M_(1 + _) := tperm_mx 0 k in
    let Schur := ((A k 0)^-1 *: dlsubmx A1) *m ursubmx A1 in
    let: (P2, L2, U2) := cormen_lup (drsubmx A1 - Schur) in
    let P := block_mx 1 0 0 P2 *m P1 in
    let L := block_mx 1 0 ((A k 0)^-1 *: (P2 *m dlsubmx A1)) L2 in
    let U := block_mx (ulsubmx A1) (ursubmx A1) 0 U2 in
    (P, L, U)
  end.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15116 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 6 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c509fe9dab..13d3ad2f89 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -509,15 +509,25 @@ let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
 
 let free_vars_and_rels_up_alias_expansion aliases c =
   let acc1 = ref Intset.empty and acc2 = ref Idset.empty in
-  let rec frec (aliases,depth) c = match kind_of_term c with
-    | Rel _ | Var _ ->
+  let cache_rel = ref Intset.empty and cache_var = ref Idset.empty in
+  let is_in_cache depth = function
+    | Rel n -> Intset.mem (n-depth) !cache_rel
+    | Var s -> Idset.mem s !cache_var
+    | _ -> false in
+  let put_in_cache depth = function
+    | Rel n -> cache_rel := Intset.add (n-depth) !cache_rel
+    | Var s -> cache_var := Idset.add s !cache_var
+    | _ -> () in
+  let rec frec (aliases,depth) c =
+    match kind_of_term c with
+    | Rel _ | Var _ as ck ->
+      if is_in_cache depth ck then () else begin
+      put_in_cache depth ck;
       let c = expansion_of_var aliases c in
-        (match kind_of_term c with
+        match kind_of_term c with
         | Var id -> acc2 := Idset.add id !acc2
         | Rel n -> if n >= depth+1 then acc1 := Intset.add (n-depth) !acc1
-        | _ -> 
-            (* not optimal: would need sharing if alias occurs more than once *)
-            frec (aliases,depth) c)
+        | _ -> frec (aliases,depth) c end
     | Const _ | Ind _ | Construct _ ->
         acc2 := List.fold_right Idset.add (vars_of_global (Global.env()) c) !acc2
     | _ ->