feat(kernel/default_converter): cache failures for (f t =?= f s) heuristic

See item 4 at
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/oJXwW5wT2Ds/d1Dgr8B-pE0J

See also
https://github.com/leanprover/lean/pull/659

src/kernel/default_converter.cpp

@@ -432,6 +432,25 @@ bool default_converter::is_def_eq_proof_irrel(expr const & t, expr const & s, co
     return false;
 }
 
+bool default_converter::failed_before(expr const & t, expr const & s) const {
+    if (t.hash() < s.hash()) {
+        return m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end();
+    } else if (t.hash() > s.hash()) {
+        return m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
+    } else {
+        return
+            m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end() ||
+            m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
+    }
+}
+
+void default_converter::cache_failure(expr const & t, expr const & s) {
+    if (t.hash() <= s.hash())
+        m_failure_cache.insert(mk_pair(t, s));
+    else
+        m_failure_cache.insert(mk_pair(s, t));
+}
+
 pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, expr const & s) {
     check_system("is_definitionally_equal");
     constraint_seq cs;
@@ -480,11 +499,14 @@ pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, exp
                         // skip the delta-reduction step.
                         // If the flag use_conv_opt() is not true, then we skip this optimization
                         constraint_seq tmp_cs;
-                        if (!is_opaque(*d_t) && d_t->use_conv_opt() &&
-                            is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n)), tmp_cs) &&
-                            is_def_eq_args(t_n, s_n, tmp_cs)) {
-                            cs += tmp_cs;
-                            return to_bcs(true, cs);
+                        if (!is_opaque(*d_t) && d_t->use_conv_opt() && !failed_before(t_n, s_n)) {
+                            if (is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n)), tmp_cs) &&
+                                is_def_eq_args(t_n, s_n, tmp_cs)) {
+                                cs += tmp_cs;
+                                return to_bcs(true, cs);
+                            } else {
+                                cache_failure(t_n, s_n);
+                            }
                         }
                     }
                 }

src/kernel/default_converter.h

@@ -5,22 +5,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <unordered_set>
 #include "util/lbool.h"
 #include "kernel/justification.h"
 #include "kernel/environment.h"
 #include "kernel/converter.h"
 #include "kernel/expr_maps.h"
 #include "kernel/equiv_manager.h"
+#include "kernel/expr_pair.h"
 
 namespace lean {
 /** \breif Converter used in the kernel */
 class default_converter : public converter {
 protected:
+    typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> expr_pair_set;
     environment                                 m_env;
     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;
+    expr_pair_set                               m_failure_cache;
 
     // 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.
@@ -66,6 +70,9 @@ protected:
     bool is_def_eq_app(expr const & t, expr const & s, constraint_seq & cs);
     bool is_def_eq_proof_irrel(expr const & t, expr const & s, constraint_seq & cs);
 
+    bool failed_before(expr const & t, expr const & s) const;
+    void cache_failure(expr const & t, expr const & s);
+
     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);

src/kernel/expr_pair.h

@@ -0,0 +1,27 @@
+/*
+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 "kernel/expr.h"
+namespace lean {
+typedef pair<expr, expr> expr_pair;
+/** \brief Functional object for hashing expression pairs. */
+struct expr_pair_hash {
+    unsigned operator()(expr_pair const & p) const { return hash(p.first.hash(), p.second.hash()); }
+};
+/** \brief Functional object for hashing expression pairs (based on their allocation time). */
+struct expr_pair_hash_alloc {
+    unsigned operator()(expr_pair const & p) const { return hash(p.first.hash_alloc(), p.second.hash_alloc()); }
+};
+/** \brief Functional object for comparing expression pairs. */
+struct expr_pair_eq {
+    bool operator()(expr_pair const & p1, expr_pair const & p2) const { return p1.first == p2.first && p1.second == p2.second; }
+};
+/** \brief Functional object for comparing expression pairs using pointer equality. */
+struct expr_pair_eqp {
+    bool operator()(expr_pair const & p1, expr_pair const & p2) const { return is_eqp(p1.first, p2.first) && is_eqp(p1.second, p2.second); }
+};
+}

src/library/expr_pair.h

@@ -7,27 +7,10 @@ Author: Leonardo de Moura
 #pragma once
 #include <utility>
 #include "util/hash.h"
-#include "kernel/expr.h"
+#include "kernel/expr_pair.h"
 #include "library/expr_lt.h"
 
 namespace lean {
-typedef pair<expr, expr> expr_pair;
-/** \brief Functional object for hashing expression pairs. */
-struct expr_pair_hash {
-    unsigned operator()(expr_pair const & p) const { return hash(p.first.hash(), p.second.hash()); }
-};
-/** \brief Functional object for hashing expression pairs (based on their allocation time). */
-struct expr_pair_hash_alloc {
-    unsigned operator()(expr_pair const & p) const { return hash(p.first.hash_alloc(), p.second.hash_alloc()); }
-};
-/** \brief Functional object for comparing expression pairs. */
-struct expr_pair_eq {
-    bool operator()(expr_pair const & p1, expr_pair const & p2) const { return p1.first == p2.first && p1.second == p2.second; }
-};
-/** \brief Functional object for comparing expression pairs using pointer equality. */
-struct expr_pair_eqp {
-    bool operator()(expr_pair const & p1, expr_pair const & p2) const { return is_eqp(p1.first, p2.first) && is_eqp(p1.second, p2.second); }
-};
 inline bool is_lt(expr_pair const & p1, expr_pair const & p2, bool use_hash) {
     return is_lt(p1.first, p2.first, use_hash) || (p1.first == p2.first && is_lt(p1.second, p2.second, use_hash));
 }

src/shell/CMakeLists.txt

@@ -49,6 +49,9 @@ add_test(NAME "issue_597"
 add_test(NAME "issue_616"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./issue_616.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+add_test(NAME "normalizer_perf"
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
+         COMMAND bash "./timeout.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "1" "slow1.lean")
 
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")

tests/lean/extra/slow1.lean

@@ -0,0 +1,11 @@
+open nat
+
+definition f (a : nat) : nat := a
+definition g (a : nat) : nat := zero
+
+example (a b : nat) :
+@eq nat
+(g (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f a))))))))))))))))))))))
+(g (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f b))))))))))))))))))))))
+:=
+@eq.refl nat (g (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f a))))))))))))))))))))))

tests/lean/extra/timeout.sh

@@ -0,0 +1,16 @@
+#!/bin/sh
+# Execute lean with timeout
+set -e
+if [ $# -ne 3 ]; then
+    echo "Usage: timeout.sh [lean-executable-path] [timeout] [benchmark]"
+    exit 1
+fi
+LEAN=$1
+TIMEOUT=$2
+BENCH=$3
+export LEAN_PATH=../../../library:.
+ulimit -t $2
+if ! $LEAN $BENCH; then
+    echo "Failed to execute $BENCH in $TIMEOUT second(s)"
+    exit 1
+fi