michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/replace_fn): non-recursive replace_fn

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-17 16:35:39 -08:00
parent af4a6c9364
commit 10f28c7bec
10 changed files with 148 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/CMakeLists.txt
View file

@ -3,6 +3,6 @@ add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
type_checker.cpp builtin.cpp occurs.cpp metavar.cpp justification.cpp
unification_constraint.cpp printer.cpp formatter.cpp
kernel_exception.cpp type_checker_justification.cpp pos_info_provider.cpp
replace_visitor.cpp)
replace_visitor.cpp update_expr.cpp)
target_link_libraries(kernel ${LEAN_LIBS})

177
src/kernel/replace_fn.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "util/interrupt.h"
#include "kernel/expr.h"
#include "kernel/expr_maps.h"
#include "kernel/update_expr.h"
namespace lean {
/**
@ -43,62 +44,87 @@ class replace_fn {
void>::value,
"The return type of P()(e1, e2) is not void");
struct frame {
expr m_expr;
unsigned m_offset;
bool m_shared;
unsigned m_index;
frame(expr const & e, unsigned o, bool s):m_expr(e), m_offset(o), m_shared(s), m_index(0) {}
};
typedef buffer<frame> frame_stack;
typedef buffer<expr> result_stack;
expr_cell_offset_map<expr> m_cache;
F m_f;
P m_post;
frame_stack m_fs;
result_stack m_rs;
optional<expr> apply(optional<expr> const & e, unsigned offset) {
if (e)
return some_expr(apply(*e, offset));
else
return none_expr();
static bool is_atomic(expr const & e) {
switch (e.kind()) {
case expr_kind::Constant:
return !const_type(e);
case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
return true;
default:
return false;
}
}
expr apply(expr const & e, unsigned offset) {
check_system("expression replacer");
bool sh = false;
void save_result(expr const & e, expr const & r, unsigned offset, bool shared) {
if (shared)
m_cache.insert(std::make_pair(expr_cell_offset(e.raw(), offset), r));
m_post(e, r);
m_rs.push_back(r);
}
/**
\brief Visit \c e at the given offset. Return true iff the result is on the
result stack \c m_rs. Return false iff a new frame was pushed on the stack \c m_fs.
The idea is that after the frame is processed, the result will be on the result stack.
*/
bool visit(expr const & e, unsigned offset) {
bool shared = false;
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;
sh = true;
if (it != m_cache.end()) {
m_rs.push_back(it->second);
return true;
}
shared = true;
}
expr r = m_f(e, offset);
if (is_eqp(e, r)) {
switch (e.kind()) {
case expr_kind::Constant:
if (const_type(e))
r = update_const(e, apply(const_type(e), offset));
break;
case expr_kind::Type: case expr_kind::Value:
case expr_kind::Var: case expr_kind::MetaVar:
break;
case expr_kind::App:
r = update_app(e, [=](expr const & c) { return apply(c, offset); });
break;
case expr_kind::Eq:
r = update_eq(e, [=](expr const & l, expr const & r) { return std::make_pair(apply(l, offset), apply(r, offset)); });
break;
case expr_kind::Lambda:
case expr_kind::Pi:
r = update_abst(e, [=](expr const & t, expr const & b) { return std::make_pair(apply(t, offset), apply(b, offset+1)); });
break;
case expr_kind::Let:
r = update_let(e, [=](optional<expr> const & t, expr const & v, expr const & b) {
return std::make_tuple(apply(t, offset), apply(v, offset), apply(b, offset+1));
});
break;
}
if (is_atomic(r) || !is_eqp(e, r)) {
save_result(e, r, offset, shared);
return true;
} else {
m_fs.emplace_back(e, offset, shared);
return false;
}
}
if (sh)
m_cache.insert(std::make_pair(expr_cell_offset(e.raw(), offset), r));
/**
\brief Return true iff <tt>f.m_index == idx</tt>.
When the result is true, <tt>f.m_index</tt> is incremented.
*/
bool check_index(frame & f, unsigned idx) {
if (f.m_index == idx) {
f.m_index++;
return true;
} else {
return false;
}
}
m_post(e, r);
expr const & rs(int i) {
lean_assert(i < 0);
return m_rs[m_rs.size() + i];
}
return r;
void pop_rs(unsigned num) {
m_rs.shrink(m_rs.size() - num);
}
public:
@ -108,11 +134,80 @@ public:
}
expr operator()(expr const & e) {
return apply(e, 0);
expr r;
visit(e, 0);
while (!m_fs.empty()) {
begin_loop:
check_interrupted();
frame & f = m_fs.back();
expr const & e = f.m_expr;
unsigned offset = f.m_offset;
switch (e.kind()) {
case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Constant:
if (check_index(f, 0) && !visit(*const_type(e), offset))
goto begin_loop;
r = update_const(e, some_expr(rs(-1)));
pop_rs(1);
break;
case expr_kind::App: {
unsigned num = num_args(e);
while (f.m_index < num) {
expr const & c = arg(e, f.m_index);
f.m_index++;
if (!visit(c, offset))
goto begin_loop;
}
r = update_app(e, num, m_rs.end() - num_args(e));
pop_rs(num);
break;
}
case expr_kind::Eq:
if (check_index(f, 0) && !visit(eq_lhs(e), offset))
goto begin_loop;
if (check_index(f, 1) && !visit(eq_rhs(e), offset))
goto begin_loop;
r = update_eq(e, rs(-2), rs(-1));
pop_rs(2);
break;
case expr_kind::Pi: case expr_kind::Lambda:
if (check_index(f, 0) && !visit(abst_domain(e), offset))
goto begin_loop;
if (check_index(f, 1) && !visit(abst_body(e), offset + 1))
goto begin_loop;
r = update_abstraction(e, rs(-2), rs(-1));
pop_rs(2);
break;
case expr_kind::Let:
if (check_index(f, 0) && let_type(e) && !visit(*let_type(e), offset))
goto begin_loop;
if (check_index(f, 1) && !visit(let_value(e), offset))
goto begin_loop;
if (check_index(f, 2) && !visit(let_body(e), offset + 1))
goto begin_loop;
if (let_type(e)) {
r = update_let(e, some_expr(rs(-3)), rs(-2), rs(-1));
pop_rs(3);
} else {
r = update_let(e, none_expr(), rs(-2), rs(-1));
pop_rs(2);
}
break;
}
save_result(e, r, offset, f.m_shared);
m_fs.pop_back();
}
lean_assert(m_rs.size() == 1);
r = m_rs.back();
m_rs.pop_back();
return r;
}
void clear() {
m_cache.clear();
m_fs.clear();
m_rs.clear();
}
};
}

2
src/library/update_expr.cpp → src/kernel/update_expr.cpp
View file

@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/buffer.h"
#include "library/update_expr.h"
#include "kernel/update_expr.h"
namespace lean {
expr update_app(expr const & app, unsigned i, expr const & new_arg) {

0
src/library/update_expr.h → src/kernel/update_expr.h
View file

6
src/library/CMakeLists.txt
View file

@ -1,6 +1,6 @@
add_library(library kernel_bindings.cpp basic_thms.cpp deep_copy.cpp
max_sharing.cpp context_to_lambda.cpp io_state.cpp update_expr.cpp
type_inferer.cpp placeholder.cpp expr_lt.cpp hidden_defs.cpp
substitution.cpp fo_unify.cpp)
max_sharing.cpp context_to_lambda.cpp io_state.cpp type_inferer.cpp
placeholder.cpp expr_lt.cpp hidden_defs.cpp substitution.cpp
fo_unify.cpp)
target_link_libraries(library ${LEAN_LIBS})

2
src/library/elaborator/elaborator.cpp
View file

@ -18,8 +18,8 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/replace_fn.h"
#include "kernel/builtin.h"
#include "kernel/update_expr.h"
#include "library/type_inferer.h"
#include "library/update_expr.h"
#include "library/elaborator/elaborator.h"
#include "library/elaborator/elaborator_justification.h"

2
src/library/tactic/tactic.cpp
View file

@ -14,8 +14,8 @@ Author: Leonardo de Moura
#include "util/lazy_list_fn.h"
#include "kernel/replace_visitor.h"
#include "kernel/instantiate.h"
#include "kernel/update_expr.h"
#include "library/hidden_defs.h"
#include "library/update_expr.h"
#include "library/kernel_bindings.h"
#include "library/tactic/tactic.h"

6
src/tests/kernel/free_vars.cpp
View file

@ -27,9 +27,9 @@ static void tst1() {
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(mk_lambda("_", t, f(Var(2))), 1) == mk_lambda("_", t, f(Var(1))));
lean_assert(lower_free_vars(mk_lambda("_", t, f(Var(0))), 1) == mk_lambda("_", t, f(Var(0))));
lean_assert_eq(lower_free_vars(f(Var(1)), 1), f(Var(0)));
lean_assert_eq(lower_free_vars(mk_lambda("_", t, f(Var(2))), 1), mk_lambda("_", t, f(Var(1))));
lean_assert_eq(lower_free_vars(mk_lambda("_", t, f(Var(0))), 1), mk_lambda("_", t, f(Var(0))));
}
static void tst2() {

2
src/tests/library/update_expr.cpp
View file

@ -6,7 +6,7 @@ Author: Leonardo de Moura
*/
#include "util/test.h"
#include "kernel/abstract.h"
#include "library/update_expr.h"
#include "kernel/update_expr.h"
using namespace lean;
static void tst1() {

2
tests/lean/slow/deep.lean
View file

@ -1,6 +1,6 @@
Definition f1 (f : Int -> Int) (x : Int) : Int := f (f (f (f x)))
Definition f2 (f : Int -> Int) (x : Int) : Int := f1 (f1 (f1 (f1 f))) x
Definition f3 (f : Int -> Int) (x : Int) : Int := (f1 (f1 (f2 f))) x
Definition f3 (f : Int -> Int) (x : Int) : Int := f1 (f2 (f2 f)) x
Variable f : Int -> Int.
Set pp::width 80.
Set lean::pp::max_depth 2000.