From adddf06e4460d9f1c3a7b62448dcfd7b9f010c23 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Jul 2014 13:12:29 -0700
Subject: [PATCH] perf(kernel/metavar): avoid destructive update in occurs
 method

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/metavar.cpp | 24 ++++++++++++++++++------
 src/kernel/metavar.h   |  5 +++--
 2 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 231d193c3..58b31a854 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -186,15 +186,20 @@ expr substitution::instantiate_metavars_wo_jst(expr const & e) {
     return instantiate_metavars_fn(*this, false)(e);
 }
 
-bool substitution::occurs_expr(name const & m, expr const & e) {
-    if (!has_expr_metavar(e))
-        return false;
-    expr new_e = instantiate(e);
+
+bool substitution::occurs_expr_core(name const & m, expr const & e, name_set & visited) const {
     bool found = false;
-    for_each(new_e, [&](expr const & e, unsigned) {
+    for_each(e, [&](expr const & e, unsigned) {
             if (found || !has_expr_metavar(e)) return false;
             if (is_metavar(e)) {
-                if (mlocal_name(e) == m)
+                name const & n = mlocal_name(e);
+                if (n == m)
+                    found = true;
+                auto s = get_expr(e);
+                if (!s || visited.contains(n))
+                    return false; // do not visit type
+                visited.insert(n);
+                if (s && occurs_expr_core(m, *s, visited))
                     found = true;
                 return false; // do not visit type
             }
@@ -203,4 +208,11 @@ bool substitution::occurs_expr(name const & m, expr const & e) {
         });
     return found;
 }
+
+bool substitution::occurs_expr(name const & m, expr const & e) const {
+    if (!has_expr_metavar(e))
+        return false;
+    name_set visited;
+    return occurs_expr_core(m, e, visited);
+}
 }
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
index c90466e9e..a6f9179f6 100644
--- a/src/kernel/metavar.h
+++ b/src/kernel/metavar.h
@@ -26,6 +26,7 @@ class substitution {
     friend class instantiate_metavars_fn;
     std::pair<level, justification> instantiate_metavars(level const & l, bool use_jst);
     expr instantiate_metavars_wo_jst(expr const & e);
+    bool occurs_expr_core(name const & m, expr const & e, name_set & visited) const;
 
 public:
     substitution();
@@ -78,7 +79,7 @@ public:
     expr instantiate(expr const & e) { return instantiate_metavars_wo_jst(e); }
 
     /** \brief Return true iff the metavariable \c m occurrs (directly or indirectly) in \c e. */
-    bool occurs_expr(name const & m, expr const & e);
-    bool occurs(expr const & m, expr const & e) { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); }
+    bool occurs_expr(name const & m, expr const & e) const;
+    bool occurs(expr const & m, expr const & e) const { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); }
 };
 }