perf(kernel/expr_eq_fn): delay cache allocation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/expr_eq_fn.cpp

@@ -6,14 +6,17 @@ Author: Leonardo de Moura
 */
 #include "kernel/expr_eq_fn.h"
 
+#ifndef LEAN_EQ_CACHE_THRESHOLD
+#define LEAN_EQ_CACHE_THRESHOLD 4
+#endif
+
 namespace lean {
 bool expr_eq_fn::apply(expr const & a, expr const & b) {
-    check_system("expression equality test");
     if (is_eqp(a, b))          return true;
     if (a.hash() != b.hash())  return false;
     if (a.kind() != b.kind())  return false;
     if (is_var(a))             return var_idx(a) == var_idx(b);
-    if (is_shared(a) && is_shared(b)) {
+    if (m_counter >= LEAN_EQ_CACHE_THRESHOLD && is_shared(a) && is_shared(b)) {
         auto p = std::make_pair(a.raw(), b.raw());
         if (!m_eq_visited)
             m_eq_visited.reset(new expr_cell_pair_set);
@@ -21,6 +24,7 @@ bool expr_eq_fn::apply(expr const & a, expr const & b) {
             return true;
         m_eq_visited->insert(p);
     }
+    check_system("expression equality test");
     switch (a.kind()) {
     case expr_kind::Var:
         lean_unreachable(); // LCOV_EXCL_LINE
@@ -33,10 +37,12 @@ bool expr_eq_fn::apply(expr const & a, expr const & b) {
             mlocal_name(a) == mlocal_name(b) &&
             apply(mlocal_type(a), mlocal_type(b));
     case expr_kind::App:
+        m_counter++;
         return
             apply(app_fn(a), app_fn(b)) &&
             apply(app_arg(a), app_arg(b));
     case expr_kind::Lambda: case expr_kind::Pi:
+        m_counter++;
         return
             apply(binding_domain(a), binding_domain(b)) &&
             apply(binding_body(a), binding_body(b)) &&
@@ -44,6 +50,7 @@ bool expr_eq_fn::apply(expr const & a, expr const & b) {
     case expr_kind::Sort:
         return sort_level(a) == sort_level(b);
     case expr_kind::Macro:
+        m_counter++;
         if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b))
             return false;
         for (unsigned i = 0; i < macro_num_args(a); i++) {
@@ -52,6 +59,7 @@ bool expr_eq_fn::apply(expr const & a, expr const & b) {
         }
         return true;
     case expr_kind::Let:
+        m_counter++;
         return
             apply(let_type(a), let_type(b)) &&
             apply(let_value(a), let_value(b)) &&

src/kernel/expr_eq_fn.h

@@ -16,12 +16,16 @@ namespace lean {
 */
 class expr_eq_fn {
     bool m_compare_binder_info;
+    // We only use the cache m_eq_visited when m_counter > LEAN_EQ_CACHE_THRESHOLD.
+    // The idea is that most queries fail quickly, and it is a wast of time
+    // to create the cache.
+    unsigned m_counter;
     std::unique_ptr<expr_cell_pair_set> m_eq_visited;
     bool apply(expr const & a, expr const & b);
 public:
     /** \brief If \c is true, then functional object will also compare binder information attached to lambda and Pi expressions */
-    expr_eq_fn(bool c = false):m_compare_binder_info(c) {}
+    expr_eq_fn(bool c = false):m_compare_binder_info(c), m_counter(0) {}
-    bool operator()(expr const & a, expr const & b) { return apply(a, b); }
+    bool operator()(expr const & a, expr const & b) { m_counter = 0; return apply(a, b); }
     void clear() { m_eq_visited.reset(); }
 };
 }