Add has_free_var, lower_free_vars

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

src/kernel/free_vars.cpp

@@ -7,19 +7,26 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include "free_vars.h"
 #include "sets.h"
+#include "replace.h"
 
 namespace lean {
 
-class has_free_var_fn {
+/** \brief Functional object for checking whether a kernel expression has free variables or not. */
+class has_free_vars_fn {
+protected:
     expr_cell_offset_set m_visited;
 
+    virtual bool process_var(expr const & x, unsigned offset) {
+        return var_idx(x) >= offset;
+    }
+
     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 var_idx(e) >= offset;
+            return process_var(e, offset);
         case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi:
             break;
         }
@@ -59,7 +66,43 @@ public:
 };
 
 bool has_free_vars(expr const & e) {
-    return has_free_var_fn()(e);
+    return has_free_vars_fn()(e);
+}
+
+/** \brief Functional object for checking whether a kernel expression has a free variable in the range <tt>[low, high)</tt> or not. */
+class has_free_var_in_range_fn : public has_free_vars_fn {
+    unsigned m_low;
+    unsigned m_high;
+    virtual bool process_var(expr const & x, unsigned offset) {
+        return var_idx(x) >= offset + m_low && var_idx(x) < offset + m_high;
+    }
+public:
+    has_free_var_in_range_fn(unsigned low, unsigned high):m_low(low), m_high(high) {
+        lean_assert(low < high);
+    }
+};
+
+bool has_free_var(expr const & e, unsigned vidx) {
+    return has_free_var_in_range_fn(vidx, vidx+1)(e);
+}
+
+bool has_free_var(expr const & e, unsigned low, unsigned high) {
+    return has_free_var_in_range_fn(low, high)(e);
+}
+
+expr lower_free_vars(expr const & e, unsigned d) {
+    lean_assert(d > 0);
+    lean_assert(!has_free_var(e, 0, d));
+    auto f = [=](expr const & e, unsigned offset) -> expr {
+        if (is_var(e) && var_idx(e) >= offset) {
+            lean_assert(var_idx(e) >= offset + d);
+            return var(var_idx(e) - d);
+        }
+        else {
+            return e;
+        }
+    };
+    return replace_fn<decltype(f)>(f)(e);
 }
 
 }

src/kernel/free_vars.h

@@ -8,11 +8,30 @@ Author: Leonardo de Moura
 #include "expr.h"
 namespace lean {
 /**
-   \brief Return true if the given expression has free variables.
+   \brief Return true iff the given expression has free variables.
 */
 bool has_free_vars(expr const & a);
 /**
-   \brief Return true if the given expression does not have free variables.
+   \brief Return true iff the given expression does not have free variables.
 */
 inline bool closed(expr const & a) { return !has_free_vars(a); }
+
+/**
+    \brief Return true iff \c e contains the free variable <tt>(var i)</tt>.
+*/
+bool has_free_var(expr const & e, unsigned i);
+
+/**
+    \brief Return true iff \c e constains a free variable <tt>(var i)</tt> s.t. \c i in <tt>[low, high)</tt>.
+    \pre low < high
+*/
+bool has_free_var(expr const & e, unsigned low, unsigned high);
+
+/**
+   \brief Lower the free variables in \c e by d. That is, a free variable <tt>(var i)</tt> is mapped into <tt>(var i-d)</tt>.
+
+   \pre d > 0
+   \pre !has_free_var(e, 0, d)
+*/
+expr lower_free_vars(expr const & e, unsigned d);
 }

src/kernel/replace.h

@@ -12,12 +12,12 @@ namespace lean {
 /**
    \brief Functional for applying <tt>F</tt> to the subexpressions of a given expression.
 
-   The signature of \f$F\f$ is
+   The signature of \c F is
    unsigned, expr -> expr
 
-   F is invoked for each subexpression s of the input expression e.
-   In a call F(n, s), n is the scope level, i.e., the number of
-   bindings operators that enclosing s.
+   F is invoked for each subexpression \c s of the input expression e.
+   In a call <tt>F(n, s)</tt>, n is the scope level, i.e., the number of
+   bindings operators that enclosing \c s.
 */
 template<typename F>
 class replace_fn {

src/tests/kernel/CMakeLists.txt

@@ -7,3 +7,6 @@ add_test(normalize ${CMAKE_CURRENT_BINARY_DIR}/normalize)
 add_executable(threads threads.cpp)
 target_link_libraries(threads ${EXTRA_LIBS})
 add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads)
+add_executable(free_vars free_vars.cpp)
+target_link_libraries(free_vars ${EXTRA_LIBS})
+add_test(free_vars ${CMAKE_CURRENT_BINARY_DIR}/free_vars)

src/tests/kernel/free_vars.cpp

@@ -0,0 +1,36 @@
+/*
+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 "free_vars.h"
+#include "test.h"
+using namespace lean;
+
+static void tst1() {
+    expr f = constant("f");
+    expr a = constant("a");
+    expr b = constant("b");
+    expr x = var(0);
+    expr y = var(1);
+    expr t = constant("t");
+    expr F = lambda("_", t, f(x));
+    lean_assert(has_free_var(lambda("_", t, f(var(1))), 0));
+    lean_assert(!has_free_var(lambda("_", t, f(var(0))), 1));
+    lean_assert(!has_free_var(pi("_", t, lambda("_", t, f(var(1)))), 0));
+    lean_assert(has_free_var(f(var(0)), 0));
+    lean_assert(has_free_var(f(var(1)), 1));
+    lean_assert(!has_free_var(f(var(1)), 0));
+    lean_assert(has_free_var(f(var(1)), 0, 2));
+    lean_assert(!has_free_var(f(var(1)), 0, 1));
+    lean_assert(lower_free_vars(f(var(1)), 1) == f(var(0)));
+    lean_assert(lower_free_vars(lambda("_", t, f(var(2))), 1) == lambda("_", t, f(var(1))));
+    lean_assert(lower_free_vars(lambda("_", t, f(var(0))), 1) == lambda("_", t, f(var(0))));
+}
+
+int main() {
+    continue_on_violation(true);
+    tst1();
+    return has_violations() ? 1 : 0;
+}

src/util/debug.h

@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #define lean_verify(COND) (COND)
 #endif
 
+//! Lean namespace
 namespace lean {
 
 void notify_assertion_violation(char const * file_name, int line, char const * condition);