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

0 files changed, 0 insertions, 0 deletions