perf(library/unification_hint): improve performance

src/library/type_context.cpp

@@ -287,6 +287,7 @@ void type_context::init_core(transparency_mode m) {
         init_local_instances();
         flush_instance_cache();
     }
+    m_uhints = get_unification_hints(env());
     lean_assert(m_cache->m_instance_fingerprint == m_lctx.get_instance_fingerprint());
 }
 
@@ -332,6 +333,7 @@ void type_context::set_env(environment const & env) {
         m_cache->m_local_instances      = m_local_instances;
     }
     lean_assert(m_cache->m_instance_fingerprint == m_lctx.get_instance_fingerprint());
+    m_uhints = get_unification_hints(env);
 }
 
 void type_context::update_local_instances(expr const & new_local, expr const & new_type) {
@@ -3068,7 +3070,7 @@ bool type_context::try_unification_hints(expr const & e1, expr const & e2) {
     expr e2_fn = get_app_fn(e2);
     if (is_constant(e1_fn) && is_constant(e2_fn)) {
         buffer<unification_hint> hints;
-        get_unification_hints(env(), const_name(e1_fn), const_name(e2_fn), hints);
+        get_unification_hints(m_uhints, const_name(e1_fn), const_name(e2_fn), hints);
         for (unification_hint const & hint : hints) {
             lean_trace(name({"type_context", "unification_hint"}),
                        scope_trace_env scope(env(), *this);

src/library/type_context.h

@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "library/metavar_context.h"
 #include "library/expr_pair_maps.h"
 #include "library/exception.h"
+#include "library/unification_hint.h"
 
 namespace lean {
 class class_exception : public generic_exception {
@@ -169,8 +170,6 @@ public:
     void recycle(type_context_cache_ptr const & ptr);
 };
 
-class unification_hint;
-
 class type_context : public abstract_type_context {
     typedef type_context_cache_ptr cache_ptr;
     typedef type_context_cache_manager cache_manager;
@@ -290,6 +289,7 @@ class type_context : public abstract_type_context {
           are no output parameters.
     */
     bool                       m_assign_regular_uvars_in_tmp_mode{false};
+    unification_hints          m_uhints;
 
     std::function<bool(expr const & e)> const * m_unfold_pred; // NOLINT
     std::function<bool(name const & e)> const * m_transparency_pred; // NOLINT

src/library/unification_hint.cpp

@@ -1,7 +1,7 @@
 /*
 Copyright (c) 2015 Daniel Selsam. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Daniel Selsam
+Authors: Daniel Selsam, Leonardo de Moura
 */
 #include <string>
 #include "util/sexpr/format.h"
@@ -81,6 +81,11 @@ struct unification_hint_state {
             throw exception("invalid unification hint, the heads of both sides of pattern must be constants");
         }
 
+        if (quick_cmp(const_name(e_pattern_lhs_fn), const_name(e_pattern_rhs_fn)) > 0) {
+            swap(e_pattern_lhs_fn, e_pattern_rhs_fn);
+            swap(e_pattern_lhs, e_pattern_rhs);
+        }
+
         name_pair key = mk_pair(const_name(e_pattern_lhs_fn), const_name(e_pattern_rhs_fn));
 
         buffer<expr_pair> constraints;
@@ -150,14 +155,19 @@ unification_hints get_unification_hints(environment const & env) {
     return unification_hint_ext::get_state(env).m_hints;
 }
 
+void get_unification_hints(unification_hints const & hints, name const & n1, name const & n2, buffer<unification_hint> & uhints) {
+    if (quick_cmp(n1, n2) > 0) {
+        if (auto const * q_ptr = hints.find(mk_pair(n2, n1)))
+            q_ptr->to_buffer(uhints);
+    } else {
+        if (auto const * q_ptr = hints.find(mk_pair(n1, n2)))
+            q_ptr->to_buffer(uhints);
+    }
+}
+
 void get_unification_hints(environment const & env, name const & n1, name const & n2, buffer<unification_hint> & uhints) {
     unification_hints hints = unification_hint_ext::get_state(env).m_hints;
-    if (auto const & q_ptr = hints.find(mk_pair(n1, n2))) {
-        q_ptr->to_buffer(uhints);
-    }
-    if (auto const & q_ptr = hints.find(mk_pair(n2, n1))) {
-        q_ptr->to_buffer(uhints);
-    }
+    get_unification_hints(hints, n1, n2, uhints);
 }
 
 /* Pretty-printing */

src/library/unification_hint.h

@@ -33,7 +33,6 @@ m_num_vars: #4
 
 Note that once we have an assignment to all variables from matching, we must substitute the assignments in the constraints.
 */
-
 class unification_hint {
     expr m_lhs;
     expr m_rhs;
@@ -59,6 +58,7 @@ typedef priority_queue<unification_hint, unification_hint_cmp> unification_hint_
 typedef rb_map<name_pair, unification_hint_queue, name_pair_quick_cmp> unification_hints;
 
 unification_hints get_unification_hints(environment const & env);
+void get_unification_hints(unification_hints const & hints, name const & n1, name const & n2, buffer<unification_hint> & uhints);
 
 void get_unification_hints(environment const & env, name const & n1, name const & n2, buffer<unification_hint> & hints);