Add abstract/instantiate for kernel expressions

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

src/kernel/CMakeLists.txt

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

src/kernel/maps.h

@@ -13,7 +13,13 @@ namespace lean {
 template<typename T>
 using expr_map = typename std::unordered_map<expr, T, expr_hash, expr_eqp>;
 
+template<typename T>
+using expr_offset_map = typename std::unordered_map<expr_offset, T, expr_offset_hash, expr_offset_eqp>;
+
 template<typename T>
 using expr_cell_map = typename std::unordered_map<expr_cell *, T, expr_cell_hash, expr_cell_eqp>;
 
+template<typename T>
+using expr_cell_offset_map = typename std::unordered_map<expr_cell_offset, T, expr_cell_offset_hash, expr_cell_offset_eqp>;
+
 };

src/kernel/var_changer.cpp

@@ -0,0 +1,141 @@
+/*
+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 <vector>
+#include <algorithm>
+#include "var_changer.h"
+#include "free_vars.h"
+#include "maps.h"
+
+namespace lean {
+
+template<typename FV, typename FS>
+class var_changer_proc {
+    expr_cell_offset_map<expr> m_cache;
+    FV                         m_fv;
+    FS                         m_fs;
+public:
+    var_changer_proc(FV const & fv, FS const & fs):
+        m_fv(fv),
+        m_fs(fs) {
+    }
+
+    expr apply(expr const & e, unsigned offset) {
+        if (is_shared(e)) {
+            expr_cell_offset p(e.raw(), offset);
+            auto it = m_cache.find(p);
+            if (it != m_cache.end())
+                return it->second;
+        }
+
+        expr r = m_fs(e, offset);
+        if (eqp(e, r)) {
+            switch (e.kind()) {
+            case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Constant:
+                break;
+            case expr_kind::Var:
+                r = m_fv(e, offset);
+                break;
+            case expr_kind::App: {
+                std::vector<expr> new_args;
+                bool modified = false;
+                for (expr const & a : args(e)) {
+                    new_args.push_back(apply(a, offset));
+                    if (!eqp(a, new_args.back()))
+                        modified = true;
+                }
+                if (modified)
+                    r = app(new_args.size(), new_args.data());
+                else
+                    r = e;
+                break;
+            }
+            case expr_kind::Lambda:
+            case expr_kind::Pi: {
+                expr const & old_t = abst_type(e);
+                expr const & old_b = abst_body(e);
+                expr t = apply(old_t, offset);
+                expr b = apply(old_b, offset+1);
+                if (!eqp(t, old_t) || !eqp(b, old_b)) {
+                    name const & n = abst_name(e);
+                    r = is_pi(e) ? pi(n, t, b) : lambda(n, t, b);
+                }
+                else {
+                    r = e;
+                }
+                break;
+            }}
+        }
+
+        if (is_shared(e))
+            m_cache.insert(std::make_pair(expr_cell_offset(e.raw(), offset), r));
+
+        return r;
+    }
+};
+
+expr abstract(unsigned n, expr const * s, expr const & e) {
+    lean_assert(std::all_of(s, s+n, closed));
+
+    auto fv = [](expr const & x, unsigned offset) { return x; };
+
+    auto fs = [=](expr const & e, unsigned offset) {
+        unsigned i = n;
+        while (i > 0) {
+            --i;
+            if (s[i] == e)
+                return var(offset + n - i - 1);
+        }
+        return e;
+    };
+
+    var_changer_proc<decltype(fv), decltype(fs)> proc(fv, fs);
+    return proc.apply(e, 0);
+}
+
+expr abstract_p(unsigned n, expr const * s, expr const & e) {
+    lean_assert(std::all_of(s, s+n, closed));
+
+    auto fv = [](expr const & x, unsigned offset) { return x; };
+
+    auto fs = [=](expr const & e, unsigned offset) {
+        unsigned i = n;
+        while (i > 0) {
+            --i;
+            if (eqp(s[i], e))
+                return var(offset + n - i - 1);
+        }
+        return e;
+    };
+
+    var_changer_proc<decltype(fv), decltype(fs)> proc(fv, fs);
+    return proc.apply(e, 0);
+}
+
+expr instantiate(unsigned n, expr const * s, expr const & e) {
+    lean_assert(std::all_of(s, s+n, closed));
+
+    auto fv = [=](expr const & x, unsigned offset) {
+        lean_assert(is_var(x));
+        unsigned vidx = var_idx(x);
+        if (vidx >= offset) {
+            if (vidx < offset + n)
+                return s[n - (vidx - offset) - 1];
+            else
+                return var(vidx - n);
+        }
+        else {
+            return x;
+        }
+    };
+
+    auto fs = [](expr const & c, unsigned offset) { return c; };
+
+    var_changer_proc<decltype(fv), decltype(fs)> proc(fv, fs);
+    return proc.apply(e, 0);
+}
+
+}

src/kernel/var_changer.h

@@ -0,0 +1,49 @@
+/*
+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 Replace the expressions s[0], ..., s[n-1] in e with var(n-1), ..., var(0).
+
+   Structural equality is used to compare subexpressions of e with the s[i]'s.
+
+   \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables).
+*/
+expr abstract(unsigned n, expr const * s, expr const & e);
+inline expr abstract(expr const & s, expr const & e) { return abstract(1, &s, e); }
+
+/**
+   \brief Replace the expressions s[0], ..., s[n-1] in e with var(n-1), ..., var(0).
+
+   Pointer comparison is used to compare subexpressions of e with the s[i]'s.
+
+   \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables).
+*/
+expr abstract_p(unsigned n, expr const * s, expr const & e);
+inline expr abstract_p(expr const & s, expr const & e) { return abstract_p(1, &s, e); }
+
+/**
+   \brief Replace the free variables with indices 0,...,n-1 with s[n-1],...,s[0] in e.
+
+   \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables).
+*/
+expr instantiate(unsigned n, expr const * s, expr const & e);
+inline expr instantiate(expr const & s, expr const & e) { return instantiate(1, &s, e); }
+
+/**
+   \brief Substitute s with t in e.
+
+   \pre s and t must be closed expressions (i.e., no free variables)
+*/
+inline expr substitute(expr const & s, expr const & t, expr const & e) {
+    return instantiate(t, abstract(s, e));
+}
+
+}

src/tests/kernel/expr.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "max_sharing.h"
 #include "free_vars.h"
 #include "test.h"
+#include "var_changer.h"
 using namespace lean;
 
 void tst1() {
@@ -250,11 +251,24 @@ void tst10() {
 void tst11() {
     expr f = constant("f");
     expr a = constant("a");
-    expr y = var(0);
+    expr b = constant("b");
     expr x = var(0);
-    lean_assert(closed(lambda("bla", prop(), lambda("x", prop(), f(f(a, a, x), y)))));
-}
+    expr y = var(1);
+    std::cout << instantiate(f(a), lambda("x", prop(), f(f(y, b), f(x, y)))) << "\n";
+    lean_assert(instantiate(f(a), lambda("x", prop(), f(f(y, b), f(x, y)))) ==
+                lambda("x", prop(), f(f(f(a), b), f(x, f(a)))));
+    std::cout << abstract(constant("a"), lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) << "\n";
+    lean_assert(abstract(constant("a"), lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) ==
+                lambda("x", prop(), f(var(1), lambda("y", prop(), f(b, var(2))))));
+    std::cout << abstract_p(constant("a"), lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) << "\n";
+    lean_assert(abstract_p(constant("a"), lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) ==
+                lambda("x", prop(), f(a, lambda("y", prop(), f(b, a)))));
+    std::cout << abstract_p(a, lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) << "\n";
+    lean_assert(abstract_p(a, lambda("x", prop(), f(a, lambda("y", prop(), f(b, a))))) ==
+                lambda("x", prop(), f(var(1), lambda("y", prop(), f(b, var(2))))));
 
+    lean_assert(substitute(f(a), b, f(f(f(a)))) == f(f(b)));
+}
 
 int main() {
     continue_on_violation(true);