feat(kernel): add equivalence manager for speeding up is_def_eq

src/kernel/CMakeLists.txt

@@ -4,6 +4,6 @@ formatter.cpp declaration.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp
 constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp
 normalizer_extension.cpp init_module.cpp extension_context.cpp expr_cache.cpp
-default_converter.cpp)
+default_converter.cpp equiv_manager.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/default_converter.cpp

@@ -284,9 +284,9 @@ bool default_converter::is_def_eq(levels const & ls1, levels const & ls2, constr
 }
 
 /** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
-lbool default_converter::quick_is_def_eq(expr const & t, expr const & s, constraint_seq & cs) {
-    if (t == s)
-        return l_true; // t and s are structurally equal
+lbool default_converter::quick_is_def_eq(expr const & t, expr const & s, constraint_seq & cs, bool use_hash) {
+    if (m_eqv_manager.is_equiv(t, s, use_hash))
+        return l_true;
     if (is_meta(t) || is_meta(s)) {
         // if t or s is a metavariable (or the application of a metavariable), then add constraint
         cs += constraint_seq(mk_eq_cnstr(t, s, m_jst->get()));
@@ -439,10 +439,11 @@ bool default_converter::is_def_eq_proof_irrel(expr const & t, expr const & s, co
     return false;
 }
 
-pair<bool, constraint_seq> default_converter::is_def_eq(expr const & t, expr const & s) {
+pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, expr const & s) {
     check_system("is_definitionally_equal");
     constraint_seq cs;
-    lbool r = quick_is_def_eq(t, s, cs);
+    bool use_hash = true;
+    lbool r = quick_is_def_eq(t, s, cs, use_hash);
     if (r != l_undef) return to_bcs(r == l_true, cs);
 
     // apply whnf (without using delta-reduction or normalizer extensions)
@@ -546,6 +547,13 @@ pair<bool, constraint_seq> default_converter::is_def_eq(expr const & t, expr con
     return to_bcs(false);
 }
 
+pair<bool, constraint_seq> default_converter::is_def_eq(expr const & t, expr const & s) {
+    auto r = is_def_eq_core(t, s);
+    if (r.first && !r.second)
+        m_eqv_manager.add_equiv(t, s);
+    return r;
+}
+
 /** Return true iff t is definitionally equal to s. */
 pair<bool, constraint_seq> default_converter::is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst) {
     flet<type_checker*>          set_tc(m_tc, &c);

src/kernel/default_converter.h

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/converter.h"
 #include "kernel/expr_maps.h"
+#include "kernel/equiv_manager.h"
 
 namespace lean {
 /** \breif Converter used in the kernel */
@@ -20,6 +21,7 @@ protected:
     bool                                        m_memoize;
     expr_struct_map<expr>                       m_whnf_core_cache;
     expr_struct_map<pair<expr, constraint_seq>> m_whnf_cache;
+    equiv_manager                               m_eqv_manager;
 
     // The two auxiliary fields are set when the public methods whnf and is_def_eq are invoked.
     // The goal is to avoid to keep carrying them around.
@@ -54,7 +56,7 @@ protected:
         return mk_pair(to_lbool(bcs.first), bcs.second);
     }
 
-    lbool quick_is_def_eq(expr const & t, expr const & s, constraint_seq & cs);
+    lbool quick_is_def_eq(expr const & t, expr const & s, constraint_seq & cs, bool use_hash = false);
     bool is_def_eq_args(expr t, expr s, constraint_seq & cs);
     bool is_app_of(expr t, name const & f_name);
     bool try_eta_expansion_core(expr const & t, expr const & s, constraint_seq & cs);
@@ -67,6 +69,7 @@ protected:
 
     pair<bool, constraint_seq> is_prop(expr const & e);
     pair<expr, constraint_seq> whnf(expr const & e_prime);
+    pair<bool, constraint_seq> is_def_eq_core(expr const & t, expr const & s);
     pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s);
 
 public:

src/kernel/equiv_manager.cpp

@@ -0,0 +1,120 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/interrupt.h"
+#include "util/flet.h"
+#include "kernel/equiv_manager.h"
+
+namespace lean {
+auto equiv_manager::mk_node() -> node_ref {
+    node_ref r = m_nodes.size();
+    node n;
+    n.m_parent = r;
+    n.m_rank   = 0;
+    m_nodes.push_back(n);
+    return r;
+}
+
+auto equiv_manager::find(node_ref n) -> node_ref {
+    while (true) {
+        node_ref p = m_nodes[n].m_parent;
+        if (p == n)
+            return p;
+        n = p;
+    }
+}
+
+void equiv_manager::merge(node_ref n1, node_ref n2) {
+    node_ref r1 = find(n1);
+    node_ref r2 = find(n2);
+    if (r1 != r2) {
+        node & ref1 = m_nodes[r1];
+        node & ref2 = m_nodes[r2];
+        if (ref1.m_rank < ref2.m_rank) {
+            ref1.m_parent = r2;
+        } else if (ref1.m_rank > ref2.m_rank) {
+            ref2.m_parent = r1;
+        } else {
+            ref2.m_parent = r1;
+            ref1.m_rank++;
+        }
+    }
+}
+
+auto equiv_manager::to_node(expr const & e) -> node_ref {
+    auto it = m_to_node.find(e);
+    if (it != m_to_node.end())
+        return it->second;
+    node_ref r = mk_node();
+    m_to_node.insert(mk_pair(e, r));
+    return r;
+}
+
+bool equiv_manager::is_equiv_core(expr const & a, expr const & b) {
+    if (is_eqp(a, b))                       return true;
+    if (m_use_hash && a.hash() != b.hash()) return false;
+    if (is_var(a))                          return var_idx(a) == var_idx(b);
+    node_ref r1 = find(to_node(a));
+    node_ref r2 = find(to_node(b));
+    if (r1 == r2)
+        return true;
+    // fall back to structural equality
+    if (a.kind() != b.kind())
+        return false;
+    check_system("expression equivalence test");
+    bool result = false;
+    switch (a.kind()) {
+    case expr_kind::Var:
+        lean_unreachable(); // LCOV_EXCL_LINE
+    case expr_kind::Constant:
+        result =
+            const_name(a) == const_name(b) &&
+            compare(const_levels(a), const_levels(b), [](level const & l1, level const & l2) { return l1 == l2; });
+        break;
+    case expr_kind::Meta: case expr_kind::Local:
+        result =
+            mlocal_name(a) == mlocal_name(b) &&
+            is_equiv_core(mlocal_type(a), mlocal_type(b));
+        break;
+    case expr_kind::App:
+        result =
+            is_equiv_core(app_fn(a), app_fn(b)) &&
+            is_equiv_core(app_arg(a), app_arg(b));
+        break;
+    case expr_kind::Lambda: case expr_kind::Pi:
+        result =
+            is_equiv_core(binding_domain(a), binding_domain(b)) &&
+            is_equiv_core(binding_body(a), binding_body(b));
+        break;
+    case expr_kind::Sort:
+        result = sort_level(a) == sort_level(b);
+        break;
+    case expr_kind::Macro:
+        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++) {
+            if (!is_equiv_core(macro_arg(a, i), macro_arg(b, i)))
+                return false;
+        }
+        result = true;
+        break;
+    }
+    if (result)
+        merge(r1, r2);
+    return result;
+}
+
+bool equiv_manager::is_equiv(expr const & a, expr const & b, bool use_hash) {
+    flet<bool> set(m_use_hash, use_hash);
+    return is_equiv_core(a, b);
+}
+
+void equiv_manager::add_equiv(expr const & e1, expr const & e2) {
+    node_ref r1 = to_node(e1);
+    node_ref r2 = to_node(e2);
+    merge(r1, r2);
+}
+}

src/kernel/equiv_manager.h

@@ -0,0 +1,34 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <vector>
+#include "kernel/expr_maps.h"
+
+namespace lean {
+class equiv_manager {
+    typedef unsigned node_ref;
+
+    struct node {
+        node_ref m_parent;
+        unsigned m_rank;
+    };
+
+    std::vector<node>  m_nodes;
+    expr_map<node_ref> m_to_node;
+    bool               m_use_hash;
+
+    node_ref mk_node();
+    node_ref find(node_ref n);
+    void merge(node_ref n1, node_ref n2);
+    node_ref to_node(expr const & e);
+    bool is_equiv_core(expr const & e1, expr const & e2);
+public:
+    equiv_manager():m_use_hash(false) {}
+    bool is_equiv(expr const & e1, expr const & e2, bool use_hash = false);
+    void add_equiv(expr const & e1, expr const & e2);
+};
+}