refactor(kernel/expr): for_each and find functional objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/CMakeLists.txt

@@ -1,4 +1,5 @@
 add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
+occurs.cpp
 # free_vars.cpp abstract.cpp instantiate.cpp
 # normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
 # type_checker.cpp kernel.cpp occurs.cpp metavar.cpp

src/kernel/find_fn.h

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/for_each_fn.h"
-#include "kernel/context.h"
+#include "kernel/expr.h"
 
 namespace lean {
 template<typename P>
@@ -40,31 +40,4 @@ template<typename P>
 optional<expr> find(expr const & e, P p) {
     return find_fn<P>(p)(e);
 }
-
-/**
-   \brief Return an expression \c e that satisfies \c p and occurs in \c c or \c es.
-*/
-template<typename P>
-optional<expr> find(context const * c, unsigned sz, expr const * es, P p) {
-    find_fn<P> finder(p);
-    if (c) {
-        for (auto const & e : *c) {
-            auto const & d = e.get_domain();
-            if (d) {
-                if (optional<expr> r = finder(*d))
-                    return r;
-            }
-            auto const & b = e.get_body();
-            if (b) {
-                if (optional<expr> r = finder(*b))
-                    return r;
-            }
-        }
-    }
-    for (unsigned i = 0; i < sz; i++) {
-        if (optional<expr> r = finder(es[i]))
-            return r;
-    }
-    return none_expr();
-}
 }

src/kernel/for_each_fn.h

@@ -40,15 +40,8 @@ class for_each_fn {
             unsigned offset = p.second;
             if (!CacheAtomic) {
                 switch (e.kind()) {
-                case expr_kind::Constant:
+                case expr_kind::Constant: case expr_kind::Var:
-                    if (!const_type(e)) {
+                case expr_kind::Sort:     case expr_kind::Macro:
-                        // only constants without cached types are considered atomic
-                        m_f(e, offset);
-                        goto begin_loop;
-                    }
-                    break;
-                case expr_kind::Type: case expr_kind::Value:
-                case expr_kind::Var: case expr_kind::MetaVar:
                     m_f(e, offset);
                     goto begin_loop;
                 default:
@@ -69,39 +62,27 @@ class for_each_fn {
                 goto begin_loop;
 
             switch (e.kind()) {
-            case expr_kind::Constant:
+            case expr_kind::Constant: case expr_kind::Var:
-                if (const_type(e))
+            case expr_kind::Sort:     case expr_kind::Macro:
-                    todo.emplace_back(*const_type(e), offset);
                 goto begin_loop;
-            case expr_kind::Type: case expr_kind::Value:
+            case expr_kind::Meta: case expr_kind::Local:
-            case expr_kind::Var: case expr_kind::MetaVar:
+                todo.emplace_back(mlocal_type(e), offset);
                 goto begin_loop;
-            case expr_kind::App: {
+            case expr_kind::App:
-                auto it    = end_args(e);
+                todo.emplace_back(app_arg(e), offset);
-                auto begin = begin_args(e);
+                todo.emplace_back(app_fn(e), offset);
-                while (it != begin) {
-                    --it;
-                    todo.emplace_back(*it, offset);
-                }
-                goto begin_loop;
-            }
-            case expr_kind::HEq:
-                todo.emplace_back(heq_lhs(e), offset);
-                todo.emplace_back(heq_rhs(e), offset);
                 goto begin_loop;
             case expr_kind::Pair:
-                todo.emplace_back(pair_first(e), offset);
-                todo.emplace_back(pair_second(e), offset);
                 todo.emplace_back(pair_type(e), offset);
+                todo.emplace_back(pair_second(e), offset);
+                todo.emplace_back(pair_first(e), offset);
                 goto begin_loop;
-            case expr_kind::Proj:
+            case expr_kind::Fst: case expr_kind::Snd:
                 todo.emplace_back(proj_arg(e), offset);
                 goto begin_loop;
-            case expr_kind::Lambda:
+            case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
-            case expr_kind::Pi:
+                todo.emplace_back(binder_body(e), offset + 1);
-            case expr_kind::Sigma:
+                todo.emplace_back(binder_domain(e), offset);
-                todo.emplace_back(abst_body(e), offset + 1);
-                todo.emplace_back(abst_domain(e), offset);
                 goto begin_loop;
             case expr_kind::Let:
                 todo.emplace_back(let_body(e), offset + 1);

src/kernel/occurs.cpp

@@ -8,17 +8,11 @@ Author: Leonardo de Moura
 #include "kernel/find_fn.h"
 
 namespace lean {
-bool occurs(name const & n, context const * c, unsigned sz, expr const * es) {
+bool occurs(expr const & n, expr const & m) {
-    return static_cast<bool>(find(c, sz, es, [&](expr const & e) { return is_constant(e) && const_name(e) == n; }));
+    return static_cast<bool>(find(m, [&](expr const & e) { return n == e; }));
 }
 
-bool occurs(expr const & n, context const * c, unsigned sz, expr const * es) {
+bool occurs(name const & n, expr const & m) {
-    return static_cast<bool>(find(c, sz, es, [&](expr const & e) { return e == n; }));
+    return static_cast<bool>(find(m, [&](expr const & e) { return is_constant(e) && const_name(e) == n; }));
 }
-bool occurs(expr const & n, expr const & m) { return occurs(n, nullptr, 1, &m); }
-bool occurs(name const & n, expr const & m) { return occurs(n, nullptr, 1, &m); }
-bool occurs(expr const & n, context const & c) { return occurs(n, &c, 0, nullptr); }
-bool occurs(name const & n, context const & c) { return occurs(n, &c, 0, nullptr); }
-bool occurs(expr const & n, context const & c, unsigned sz, expr const * es) { return occurs(n, &c, sz, es); }
-bool occurs(name const & n, context const & c, unsigned sz, expr const * es) { return occurs(n, &c, sz, es); }
 }

src/kernel/occurs.h

@@ -5,21 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "kernel/context.h"
+#include "kernel/expr.h"
 
 namespace lean {
 /** \brief Return true iff \c n occurs in \c m */
 bool occurs(expr const & n, expr const & m);
 /** \brief Return true iff there is a constant named \c n in \c m. */
 bool occurs(name const & n, expr const & m);
-/** \brief Return true iff \c n occurs in context \c c. */
-bool occurs(expr const & n, context const & c);
-/** \brief Return true iff there is a constant named \c n in context \c c. */
-bool occurs(name const & n, context const & c);
-/** \brief Return true iff \c n occurs in context \c c or the array of expressions es[sz]. */
-bool occurs(expr const & n, context const & c, unsigned sz, expr const * es);
-inline bool occurs(expr const & n, context const & c, std::initializer_list<expr> const & l) { return occurs(n, c, l.size(), l.begin()); }
-/** \brief Return true iff there is a constant named \c n in context \c c or the array of expressions es[sz]. */
-bool occurs(name const & n, context const & c, unsigned sz, expr const * es);
-inline bool occurs(name const & n, context const & c, std::initializer_list<expr> const & l) { return occurs(n, c, l.size(), l.begin()); }
 }