Refactor instantiate/abstract code

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 var_changer.cpp)
+add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp instantiate.cpp)
 target_link_libraries(kernel ${EXTRA_LIBS})

src/kernel/abstract.cpp

@@ -0,0 +1,44 @@
+/*
+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 "replace.h"
+
+namespace lean {
+expr abstract(unsigned n, expr const * s, expr const & e) {
+    lean_assert(std::all_of(s, s+n, closed));
+
+    auto f = [=](expr const & e, unsigned offset) {
+        unsigned i = n;
+        while (i > 0) {
+            --i;
+            if (s[i] == e)
+                return var(offset + n - i - 1);
+        }
+        return e;
+    };
+
+    replace_proc<decltype(f)> proc(f);
+    return proc(e);
+}
+expr abstract_p(unsigned n, expr const * s, expr const & e) {
+    lean_assert(std::all_of(s, s+n, closed));
+
+    auto f = [=](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;
+    };
+
+    replace_proc<decltype(f)> proc(f);
+    return proc(e);
+}
+}

src/kernel/abstract.h

@@ -0,0 +1,30 @@
+/*
+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); }
+}

src/kernel/instantiate.cpp

@@ -0,0 +1,31 @@
+/*
+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 "replace.h"
+
+namespace lean {
+expr instantiate(unsigned n, expr const * s, expr const & e) {
+    lean_assert(std::all_of(s, s+n, closed));
+
+    auto f = [=](expr const & e, unsigned offset) {
+        if (is_var(e)) {
+            unsigned vidx = var_idx(e);
+            if (vidx >= offset) {
+                if (vidx < offset + n)
+                    return s[n - (vidx - offset) - 1];
+                else
+                    return var(vidx - n);
+            }
+        }
+        return e;
+    };
+
+    replace_proc<decltype(f)> proc(f);
+    return proc(e);
+}
+}

src/kernel/instantiate.h

@@ -0,0 +1,18 @@
+/*
+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 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); }
+}

src/kernel/replace.h

@@ -0,0 +1,86 @@
+/*
+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 <vector>
+#include "expr.h"
+#include "maps.h"
+namespace lean {
+/**
+   \brief Functional for applying F to the subexpressions of a given expression.
+
+   The signature of 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.
+*/
+template<typename F>
+class replace_proc {
+    expr_cell_offset_map<expr> m_cache;
+    F                          m_f;
+
+    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_f(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: case expr_kind::Var:
+                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;
+    }
+
+public:
+    replace_proc(F const & f):
+        m_f(f) {
+    }
+
+    expr operator()(expr const & e) {
+        return apply(e, 0);
+    }
+};
+}

src/tests/kernel/expr.cpp

@@ -10,7 +10,8 @@ Author: Leonardo de Moura
 #include "max_sharing.h"
 #include "free_vars.h"
 #include "test.h"
-#include "var_changer.h"
+#include "abstract.h"
+#include "instantiate.h"
 using namespace lean;
 
 void tst1() {
@@ -248,6 +249,15 @@ void tst10() {
     }
 }
 
+/**
+   \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));
+}
+
 void tst11() {
     expr f = constant("f");
     expr a = constant("a");