From 9d88db3941be3de60ccc668779fc87b404909b84 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 Feb 2016 19:44:16 -0800
Subject: [PATCH] perf(library/type_context): add cache for minimizing the
 access to is_opaque and environment::find

---
 src/library/type_context.cpp | 30 ++++++++++++++++++++++--------
 src/library/type_context.h   |  6 +++++-
 2 files changed, 27 insertions(+), 9 deletions(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 76a09ed02b..0b7ebb16e5 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -171,6 +171,20 @@ bool type_context::is_opaque(declaration const & d) const {
     return is_extra_opaque(n);
 }
 
+optional<declaration> type_context::is_transparent(name const & n) {
+    auto it = m_is_transparent_cache[m_relax_is_opaque].find(n);
+    if (it != m_is_transparent_cache[m_relax_is_opaque].end()) {
+        return it->second;
+    }
+    optional<declaration> r;
+    if (auto d = m_env.find(n)) {
+        if (d->is_definition() && !is_opaque(*d))
+            r = d;
+    }
+    m_is_transparent_cache[m_relax_is_opaque].insert(mk_pair(n, r));
+    return r;
+}
+
 optional<expr> type_context::expand_macro(expr const & m) {
     lean_assert(is_macro(m));
     if (should_unfold_macro(m))
@@ -252,9 +266,8 @@ expr type_context::whnf_core(expr const & e) {
 /** \brief Expand \c e if it is non-opaque constant with height >= h */
 expr type_context::unfold_name_core(expr e, unsigned h) {
     if (is_constant(e)) {
-        if (auto d = m_env.find(const_name(e))) {
-            if (d->is_definition() && !is_opaque(*d) && d->get_height() >= h &&
-                length(const_levels(e)) == d->get_num_univ_params())
+        if (auto d = is_transparent(const_name(e))) {
+            if (d->get_height() >= h && length(const_levels(e)) == d->get_num_univ_params())
                 return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), h);
         }
     }
@@ -282,14 +295,13 @@ expr type_context::unfold_names(expr const & e, unsigned h) {
 
 /** \brief Return some definition \c d iff \c e is a target for delta-reduction,
     and the given definition is the one to be expanded. */
-optional<declaration> type_context::is_delta(expr const & e) const {
+optional<declaration> type_context::is_delta(expr const & e) {
     expr const & f = get_app_fn(e);
     if (is_constant(f)) {
-        if (auto d = m_env.find(const_name(f)))
-            if (d->is_definition() && !is_opaque(*d))
-                return d;
+        return is_transparent(const_name(f));
+    } else {
+        return none_declaration();
     }
-    return none_declaration();
 }
 
 /** \brief Weak head normal form core procedure that performs delta reduction
@@ -1237,6 +1249,8 @@ expr type_context::infer(expr const & e) {
 void type_context::clear_cache() {
     m_ci_cache.clear();
     m_ss_cache.clear();
+    m_is_transparent_cache[0].clear();
+    m_is_transparent_cache[1].clear();
     clear_infer_cache();
 }
 
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 3723daa5e7..421b988657 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -189,13 +189,17 @@ class type_context {
     typedef scoped_map<expr, expr, expr_hash, std::equal_to<expr>> infer_cache;
     infer_cache m_infer_cache;
 
+    typedef std::unordered_map<name, optional<declaration>, name_hash> is_transparent_cache;
+    is_transparent_cache m_is_transparent_cache[2];
+
     bool is_opaque(declaration const & d) const;
+    optional<declaration> is_transparent(name const & n);
     optional<expr> reduce_projection(expr const & e);
     optional<expr> norm_ext(expr const & e);
     expr whnf_core(expr const & e);
     expr unfold_name_core(expr e, unsigned h);
     expr unfold_names(expr const & e, unsigned h);
-    optional<declaration> is_delta(expr const & e) const;
+    optional<declaration> is_delta(expr const & e);
     expr whnf_core(expr e, unsigned h);
 
     lbool quick_is_def_eq(level const & l1, level const & l2);