From b6afbcb7f51da71a7a6af55fe6f7eff2ff910b73 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Oct 2014 14:15:09 -0700
Subject: [PATCH] perf(kernel/replace_fn): use 'recursive' replace_fn for
 "small" terms

---
 src/kernel/replace_fn.cpp | 60 ++++++++++++++++++++++++++++++++++++++-
 1 file changed, 59 insertions(+), 1 deletion(-)

diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp
index c34984f35..9cd2981a1 100644
--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -197,7 +197,65 @@ public:
     }
 };
 
+class replace_rec_fn {
+    replace_cache_ref                                     m_cache;
+    std::function<optional<expr>(expr const &, unsigned)> m_f;
+
+    expr save_result(expr const & e, unsigned offset, expr const & r, bool shared) {
+        if (shared)
+            m_cache->insert(e, offset, r);
+        return r;
+    }
+
+    expr apply(expr const & e, unsigned offset) {
+        bool shared = false;
+        if (is_shared(e)) {
+            if (auto r = m_cache->find(e, offset))
+                return *r;
+            shared = true;
+        }
+
+        if (optional<expr> r = m_f(e, offset)) {
+            return save_result(e, offset, *r, shared);
+        } else {
+            switch (e.kind()) {
+            case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Var:
+                return save_result(e, offset, e, shared);
+            case expr_kind::Meta:     case expr_kind::Local: {
+                expr new_t = apply(mlocal_type(e), offset);
+                return save_result(e, offset, update_mlocal(e, new_t), shared);
+            }
+            case expr_kind::App: {
+                expr new_f = apply(app_fn(e), offset);
+                expr new_a = apply(app_arg(e), offset);
+                return save_result(e, offset, update_app(e, new_f, new_a), shared);
+            }
+            case expr_kind::Pi: case expr_kind::Lambda: {
+                expr new_d = apply(binding_domain(e), offset);
+                expr new_b = apply(binding_body(e), offset+1);
+                return save_result(e, offset, update_binding(e, new_d, new_b), shared);
+            }
+            case expr_kind::Macro: {
+                buffer<expr> new_args;
+                unsigned nargs = macro_num_args(e);
+                for (unsigned i = 0; i < nargs; i++)
+                    new_args.push_back(apply(macro_arg(e, i), offset));
+                return save_result(e, offset, update_macro(e, new_args.size(), new_args.data()), shared);
+            }}
+            lean_unreachable();
+        }
+    }
+public:
+    template<typename F>
+    replace_rec_fn(F const & f):m_f(f) {}
+
+    expr operator()(expr const & e) { return apply(e, 0); }
+};
+
 expr replace(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f) {
-    return replace_fn(f)(e);
+    if (get_weight(e) < 10000)
+        return replace_rec_fn(f)(e);
+    else
+        return replace_fn(f)(e);
 }
 }