Add occurs function

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

src/kernel/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp
   instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp
   type_check.cpp context.cpp builtin.cpp basic_thms.cpp toplevel.cpp
-  object.cpp expr_formatter.cpp expr_locator.cpp pp.cpp)
+  object.cpp expr_formatter.cpp expr_locator.cpp occurs.cpp pp.cpp)
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/occurs.cpp

@@ -0,0 +1,60 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "occurs.h"
+#include "for_each.h"
+
+namespace lean {
+template<typename F>
+void for_each(F & f, context const * c, unsigned sz, expr const * es) {
+    for_each_fn<F> visitor(f);
+    if (c) {
+        for (auto const & e : *c) {
+            visitor(e.get_type());
+            if (e.get_body())
+                visitor(e.get_body());
+        }
+    }
+    for (unsigned i = 0; i < sz; i++)
+        visitor(es[i]);
+}
+
+namespace occurs_ns { struct found {}; }
+bool occurs(name const & n, context const * c, unsigned sz, expr const * es) {
+    auto visitor = [&](expr const & e, unsigned offset) -> void {
+        if (is_constant(e)) {
+            if (const_name(e) == n)
+                throw occurs_ns::found();
+        }
+    };
+    try {
+        for_each(visitor, c, sz, es);
+        return false;
+    } catch (occurs_ns::found) {
+        return true;
+    }
+}
+
+bool occurs(expr const & n, context const * c, unsigned sz, expr const * es) {
+    auto visitor = [&](expr const & e, unsigned offset) -> void {
+        if (e == n)
+            throw occurs_ns::found();
+    };
+    try {
+        for_each(visitor, c, sz, es);
+        return false;
+    } catch (occurs_ns::found) {
+        return true;
+    }
+}
+
+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

@@ -0,0 +1,25 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "context.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 ocurs 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 ocurs 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()); }
+}

src/tests/kernel/CMakeLists.txt

@@ -25,3 +25,6 @@ add_test(arith ${CMAKE_CURRENT_BINARY_DIR}/arith)
 add_executable(environment environment.cpp)
 target_link_libraries(environment ${EXTRA_LIBS})
 add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment)
+add_executable(occurs occurs.cpp)
+target_link_libraries(occurs ${EXTRA_LIBS})
+add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)

src/tests/kernel/occurs.cpp

@@ -0,0 +1,45 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "occurs.h"
+#include "abstract.h"
+using namespace lean;
+
+static void tst1() {
+    expr f = Const("f");
+    expr a = Const("a");
+    expr b = Const("b");
+    expr T = Type();
+    lean_assert(occurs(f, f));
+    lean_assert(!occurs(a, f));
+    lean_assert(occurs(a, f(a)));
+    lean_assert(occurs("a", f(a)));
+    lean_assert(!occurs("b", f));
+    lean_assert(!occurs(a, Fun({a, T}, f(a))));
+    context c;
+    c = extend(c, name("x"), T);
+    lean_assert(!occurs(f, c));
+    lean_assert(occurs(f, c, {a, f(a)}));
+    lean_assert(occurs(f(a), c, {a, f(a)}));
+    lean_assert(!occurs(f(b), c, {a, f(a)}));
+    lean_assert(occurs("f", c, {a, f(a)}));
+    lean_assert(!occurs(b, c, {a, f(a)}));
+    c = extend(c, name("y"), T, f(a));
+    lean_assert(!occurs("x", c));
+    lean_assert(occurs(f, c));
+    lean_assert(occurs("f", c));
+    c = extend(c, name("z"), T, f(Const("x")));
+    lean_assert(occurs("x", c));
+    lean_assert(occurs("a", c));
+    lean_assert(occurs(f(Const("x")), c));
+    lean_assert(!occurs(f(b), c));
+}
+
+int main() {
+    continue_on_violation(true);
+    tst1();
+    return has_violations() ? 1 : 0;
+}