Add has_free_vars/closed function

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

src/kernel/CMakeLists.txt

@@ -1,2 +1,2 @@
-add_library(kernel expr.cpp max_sharing)
+add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp)
 target_link_libraries(kernel ${EXTRA_LIBS})

src/kernel/expr.cpp

@@ -22,6 +22,7 @@ unsigned hash_vars(unsigned size, uvar const * vars) {
 expr_cell::expr_cell(expr_kind k, unsigned h):
     m_kind(static_cast<unsigned>(k)),
     m_max_shared(0),
+    m_closed(0),
     m_hash(h),
     m_rc(1) {}
 

src/kernel/expr.h

@@ -46,13 +46,19 @@ class max_sharing_functor;
 class expr_cell {
 protected:
     unsigned m_kind:16;
-    unsigned m_max_shared:1; // flag indicating if the cell has maximally shared subexpressions
+    unsigned m_max_shared:1; // flag (used by max_sharing_functor) indicating if the cell has maximally shared subexpressions
+    unsigned m_closed:1;     // flag (used by has_free_var_functor): 1 means it is definitely close, 0 means don't know
     unsigned m_hash;
     MK_LEAN_RC(); // Declare m_rc counter
     void dealloc();
+
     bool max_shared() const { return m_max_shared == 1; }
-    void set_max_shared() { lean_assert(!max_shared()); m_max_shared = 1; }
+    void set_max_shared() { m_max_shared = 1; }
     friend class max_sharing_functor;
+
+    bool is_closed() const { return m_closed == 1; }
+    void set_closed() { m_closed = 1; }
+    friend class has_free_var_functor;
 public:
     expr_cell(expr_kind k, unsigned h);
     expr_kind kind() const { return static_cast<expr_kind>(m_kind); }

src/kernel/free_vars.cpp

@@ -0,0 +1,64 @@
+/*
+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 <algorithm>
+#include "free_vars.h"
+#include "sets.h"
+
+namespace lean {
+
+class has_free_var_functor {
+    expr_cell_offset_set m_visited;
+public:
+    bool apply(expr const & e, unsigned offset) {
+        // handle easy cases
+        switch (e.kind()) {
+        case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
+            return false;
+        case expr_kind::Var:
+            return get_var_idx(e) >= offset;
+        case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi:
+            break;
+        }
+
+        if (e.raw()->is_closed())
+            return false;
+
+        if (is_shared(e)) {
+            expr_cell_offset p(e.raw(), offset);
+            if (m_visited.find(p) != m_visited.end())
+                return false;
+            m_visited.insert(p);
+        }
+
+        bool result = false;
+
+        switch (e.kind()) {
+        case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Var:
+            // easy cases were already handled
+            lean_unreachable(); return false;
+        case expr_kind::App:
+            result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); });
+            break;
+        case expr_kind::Lambda:
+        case expr_kind::Pi:
+            result = apply(get_abs_type(e), offset) || apply(get_abs_expr(e), offset + 1);
+            break;
+        }
+
+        if (!result)
+            e.raw()->set_closed();
+
+        return result;
+    }
+};
+
+bool has_free_vars(expr const & e) {
+    has_free_var_functor f;
+    return f.apply(e, 0);
+}
+
+}

src/kernel/free_vars.h

@@ -0,0 +1,15 @@
+/*
+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 "expr.h"
+namespace lean {
+/**
+   \brief Return true if the given expression has free variables.
+*/
+bool has_free_vars(expr const & a);
+inline bool closed(expr const & a) { return !has_free_vars(a); }
+}

src/tests/kernel/expr.cpp

@@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <algorithm>
 #include "expr.h"
 #include "sets.h"
 #include "max_sharing.h"
+#include "free_vars.h"
 #include "test.h"
-#include <algorithm>
 using namespace lean;
 
 void tst1() {
@@ -29,9 +30,9 @@ void tst1() {
     lean_assert(app(f, app(a, a)) != app(f, a, a));
 }
 
-expr mk_dag(unsigned depth) {
+expr mk_dag(unsigned depth, bool _closed = false) {
     expr f = constant("f");
-    expr a = var(0);
+    expr a = _closed ? constant("a") : var(0);
     while (depth > 0) {
         depth--;
         a = app(f, a, a);
@@ -110,7 +111,7 @@ void tst2() {
 
 expr mk_big(expr f, unsigned depth, unsigned val) {
     if (depth == 1)
-        return var(val);
+        return constant(name(val));
     else
         return app(f, mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
 }
@@ -197,10 +198,61 @@ void tst7() {
     lean_assert(eqp(get_arg(b, 1), get_arg(b, 2)));
 }
 
+void tst8() {
+    expr f = constant("f");
+    expr x = var(0);
+    expr a = constant("a");
+    expr n = numeral(mpz(10));
+    expr p = prop();
+    expr y = var(1);
+    lean_assert(closed(a));
+    lean_assert(!closed(x));
+    lean_assert(closed(f));
+    lean_assert(!closed(app(f, x)));
+    lean_assert(closed(lambda("x", p, x)));
+    lean_assert(!closed(lambda("x", x, x)));
+    lean_assert(!closed(lambda("x", p, y)));
+    lean_assert(closed(app(f, app(f, app(f, a)))));
+    lean_assert(closed(lambda("x", p, app(f, app(f, app(f, a))))));
+    lean_assert(closed(pi("x", p, x)));
+    lean_assert(!closed(pi("x", x, x)));
+    lean_assert(!closed(pi("x", p, y)));
+    lean_assert(closed(pi("x", p, app(f, app(f, app(f, a))))));
+    lean_assert(closed(lambda("y", p, lambda("x", p, y))));
+    lean_assert(closed(lambda("y", p, app(lambda("x", p, y), var(0)))));
+    expr r = lambda("y", p, app(lambda("x", p, y), var(0)));
+    lean_assert(closed(r));
+    lean_assert(closed(r));
+    r = lambda("y", p, app(lambda("x", p, y), var(1)));
+    lean_assert(!closed(r));
+    r = lambda("y", p, app(lambda("x", p, var(0)), var(1)));
+    lean_assert(!closed(r));
+    lean_assert(closed(lambda("z", p, r)));
+}
+
+void tst9() {
+    expr r = mk_dag(20, true);
+    lean_assert(closed(r));
+    r = mk_dag(20, false);
+    lean_assert(!closed(r));
+}
+
+void tst10() {
+    expr f = constant("f");
+    expr r = mk_big(f, 16, 0);
+    for (unsigned i = 0; i < 1000; i++) {
+        lean_assert(closed(r));
+    }
+}
+
 int main() {
     continue_on_violation(true);
     std::cout << "sizeof(expr):     " << sizeof(expr) << "\n";
     std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n";
+    tst8();
+    tst9();
+    tst10();
+    return 0;
     tst1();
     tst2();
     tst3();