From 9b3c47a521eb732100460fb1e584d92e5b12ceb5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Jul 2013 00:32:01 -0700 Subject: [PATCH] Refactor instantiate/abstract code Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 2 +- src/kernel/abstract.cpp | 44 +++++++++++++++++++ src/kernel/abstract.h | 30 +++++++++++++ src/kernel/instantiate.cpp | 31 ++++++++++++++ src/kernel/instantiate.h | 18 ++++++++ src/kernel/replace.h | 86 ++++++++++++++++++++++++++++++++++++++ src/tests/kernel/expr.cpp | 12 +++++- 7 files changed, 221 insertions(+), 2 deletions(-) create mode 100644 src/kernel/abstract.cpp create mode 100644 src/kernel/abstract.h create mode 100644 src/kernel/instantiate.cpp create mode 100644 src/kernel/instantiate.h create mode 100644 src/kernel/replace.h diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 1291ba00f..8dbf03d14 100644 --- a/src/kernel/CMakeLists.txt +++ b/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}) diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp new file mode 100644 index 000000000..0e05bf7c3 --- /dev/null +++ b/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 +#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 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 proc(f); + return proc(e); +} +} diff --git a/src/kernel/abstract.h b/src/kernel/abstract.h new file mode 100644 index 000000000..036ce91a2 --- /dev/null +++ b/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); } +} diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp new file mode 100644 index 000000000..736b32459 --- /dev/null +++ b/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 +#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 proc(f); + return proc(e); +} +} diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h new file mode 100644 index 000000000..98d606bc4 --- /dev/null +++ b/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); } +} diff --git a/src/kernel/replace.h b/src/kernel/replace.h new file mode 100644 index 000000000..c13d688b9 --- /dev/null +++ b/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 +#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 +class replace_proc { + expr_cell_offset_map 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 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); + } +}; +} diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 9e2509c0f..e17a384e3 100644 --- a/src/tests/kernel/expr.cpp +++ b/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");