From 57d9d23bd4610a5841d681e8ee9820dd520fd565 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Oct 2013 14:58:02 -0700
Subject: [PATCH] feat(kernel/for_each): allow function F to interrupt for_each
 search

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/pp.cpp  | 1 +
 src/kernel/environment.cpp | 1 +
 src/kernel/for_each.h      | 7 ++++---
 src/kernel/metavar.cpp     | 4 ++++
 src/kernel/occurs.cpp      | 6 ++++--
 5 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 1dbedf9a3..134c56724 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1113,6 +1113,7 @@ class pp_fn {
             } else if (is_let(e)) {
                 if (is_prefix_of(prefix, let_name(e))) throw found_prefix();
             }
+            return true;
         };
         try {
             for_each_fn<decltype(f)> visitor(f);
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 1ac4529d6..9fcbb4ad6 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -44,6 +44,7 @@ struct environment::imp {
                 if (obj)
                     w = std::max(w, obj.get_weight());
             }
+            return true;
         };
         for_each_fn<decltype(proc)> visitor(proc);
         visitor(e);
diff --git a/src/kernel/for_each.h b/src/kernel/for_each.h
index e33f7199b..c3231a4d1 100644
--- a/src/kernel/for_each.h
+++ b/src/kernel/for_each.h
@@ -22,8 +22,8 @@ template<typename F>
 class for_each_fn {
     std::unique_ptr<expr_cell_offset_set> m_visited;
     F                                     m_f;
-    static_assert(std::is_same<typename std::result_of<F(expr const &, unsigned)>::type, void>::value,
-                  "for_each_fn: return type of m_f is not void");
+    static_assert(std::is_same<typename std::result_of<F(expr const &, unsigned)>::type, bool>::value,
+                  "for_each_fn: return type of m_f is not bool");
 
     void apply(expr const & e, unsigned offset) {
         if (is_shared(e)) {
@@ -35,7 +35,8 @@ class for_each_fn {
             m_visited->insert(p);
         }
 
-        m_f(e, offset);
+        if (!m_f(e, offset))
+            return;
 
         switch (e.kind()) {
         case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 4ff96a25e..538342b72 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -262,8 +262,11 @@ bool has_assigned_metavar(expr const & e, substitution const & s) {
         return false;
     } else {
         auto proc = [&](expr const & n, unsigned) {
+            if (!has_metavar(n))
+                return false;
             if (is_metavar(n) && s.is_assigned(n))
                 throw found_assigned();
+            return true;
         };
         for_each_fn<decltype(proc)> visitor(proc);
         try {
@@ -342,6 +345,7 @@ bool has_metavar(expr const & e, expr const & m, substitution const & s) {
                     has_metavar(s.get_subst(m2), m, s))
                     throw found_metavar();
             }
+            return true;
         };
         try {
             for_each_fn<decltype(f)> proc(f);
diff --git a/src/kernel/occurs.cpp b/src/kernel/occurs.cpp
index fd6a2a8cd..44188b964 100644
--- a/src/kernel/occurs.cpp
+++ b/src/kernel/occurs.cpp
@@ -27,11 +27,12 @@ namespace occurs_ns {
 struct found {};
 }
 bool occurs(name const & n, context const * c, unsigned sz, expr const * es) {
-    auto visitor = [&](expr const & e, unsigned) -> void {
+    auto visitor = [&](expr const & e, unsigned) -> bool {
         if (is_constant(e)) {
             if (const_name(e) == n)
                 throw occurs_ns::found();
         }
+        return true;
     };
     try {
         for_each(visitor, c, sz, es);
@@ -42,9 +43,10 @@ bool occurs(name const & n, context const * c, unsigned sz, expr const * es) {
 }
 
 bool occurs(expr const & n, context const * c, unsigned sz, expr const * es) {
-    auto visitor = [&](expr const & e, unsigned) -> void {
+    auto visitor = [&](expr const & e, unsigned) -> bool {
         if (e == n)
             throw occurs_ns::found();
+        return true;
     };
     try {
         for_each(visitor, c, sz, es);