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

refactor(kernel/expr): for_each_fn, replace_fn, and find_fn without templates

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-16 11:23:25 -08:00
parent 69b9f2dd37
commit 533f44e224
7 changed files with 280 additions and 269 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/CMakeLists.txt
View file

@ -1,5 +1,5 @@
add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
occurs.cpp
for_each_fn.cpp occurs.cpp replace_fn.cpp
# free_vars.cpp abstract.cpp instantiate.cpp
# normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
# type_checker.cpp kernel.cpp occurs.cpp metavar.cpp

19
src/kernel/find_fn.h
View file

@ -9,16 +9,16 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
namespace lean {
template<typename P>
class find_fn {
template<typename P>
struct pred_fn {
optional<expr> & m_result;
P m_p;
P m_p;
pred_fn(optional<expr> & result, P const & p):m_result(result), m_p(p) {}
bool operator()(expr const & e, unsigned) {
bool operator()(expr const & e, unsigned offset) {
if (m_result) {
return false; // already found result, stop the search
} else if (m_p(e)) {
} else if (m_p(e, offset)) {
m_result = e;
return false; // stop the search
} else {
@ -26,18 +26,17 @@ class find_fn {
}
}
};
optional<expr> m_result;
for_each_fn<pred_fn> m_proc;
optional<expr> m_result;
for_each_fn m_proc;
public:
find_fn(P const & p):m_proc(pred_fn(m_result, p)) {}
template<typename P> find_fn(P const & p):m_proc(pred_fn<P>(m_result, p)) {}
optional<expr> operator()(expr const & e) { m_proc(e); return m_result; }
};
/**
\brief Return a subexpression of \c e that satisfies the predicate \c p.
*/
template<typename P>
optional<expr> find(expr const & e, P p) {
return find_fn<P>(p)(e);
template<typename P> optional<expr> find(expr const & e, P p) {
return find_fn(p)(e);
}
}

75
src/kernel/for_each_fn.cpp Normal file
View file

@ -0,0 +1,75 @@
/*
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 "kernel/for_each_fn.h"
namespace lean {
void for_each_fn::apply(expr const & e, unsigned offset) {
buffer<std::pair<expr const &, unsigned>> todo;
todo.emplace_back(e, offset);
while (true) {
begin_loop:
if (todo.empty())
break;
auto p = todo.back();
todo.pop_back();
expr const & e = p.first;
unsigned offset = p.second;
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Var:
case expr_kind::Sort: case expr_kind::Macro:
m_f(e, offset);
goto begin_loop;
default:
break;
}
if (is_shared(e)) {
expr_cell_offset p(e.raw(), offset);
if (!m_visited)
m_visited.reset(new expr_cell_offset_set());
if (m_visited->find(p) != m_visited->end())
goto begin_loop;
m_visited->insert(p);
}
if (!m_f(e, offset))
goto begin_loop;
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Var:
case expr_kind::Sort: case expr_kind::Macro:
goto begin_loop;
case expr_kind::Meta: case expr_kind::Local:
todo.emplace_back(mlocal_type(e), offset);
goto begin_loop;
case expr_kind::App:
todo.emplace_back(app_arg(e), offset);
todo.emplace_back(app_fn(e), offset);
goto begin_loop;
case expr_kind::Pair:
todo.emplace_back(pair_type(e), offset);
todo.emplace_back(pair_second(e), offset);
todo.emplace_back(pair_first(e), offset);
goto begin_loop;
case expr_kind::Fst: case expr_kind::Snd:
todo.emplace_back(proj_arg(e), offset);
goto begin_loop;
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
todo.emplace_back(binder_body(e), offset + 1);
todo.emplace_back(binder_domain(e), offset);
goto begin_loop;
case expr_kind::Let:
todo.emplace_back(let_body(e), offset + 1);
todo.emplace_back(let_value(e), offset);
if (let_type(e))
todo.emplace_back(*let_type(e), offset);
goto begin_loop;
}
}
}
}

99
src/kernel/for_each_fn.h
View file

@ -7,99 +7,34 @@ Author: Leonardo de Moura
#pragma once
#include <memory>
#include <utility>
#include <functional>
#include "util/buffer.h"
#include "kernel/expr.h"
#include "kernel/expr_sets.h"
namespace lean {
/**
\brief Template for implementing expression visitors.
The argument \c F must be a function object containing the method
<code>
void operator()(expr const & e, unsigned offset)
</code>
The \c offset is the number of binders under which \c e occurs.
\brief Expression visitor.
The argument \c F must be a lambda (function object) containing the method
<code>
void operator()(expr const & e, unsigned offset)
</code>
The \c offset is the number of binders under which \c e occurs.
*/
template<typename F, bool CacheAtomic = false>
class for_each_fn {
std::unique_ptr<expr_cell_offset_set> m_visited;
F m_f;
static_assert(std::is_same<typename std::result_of<F(expr const &, unsigned)>::type, bool>::value,
"for_each_fn: return type of m_f is not bool");
void apply(expr const & e, unsigned offset) {
buffer<std::pair<expr const &, unsigned>> todo;
todo.emplace_back(e, offset);
while (true) {
begin_loop:
if (todo.empty())
break;
auto p = todo.back();
todo.pop_back();
expr const & e = p.first;
unsigned offset = p.second;
if (!CacheAtomic) {
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Var:
case expr_kind::Sort: case expr_kind::Macro:
m_f(e, offset);
goto begin_loop;
default:
break;
}
}
if (is_shared(e)) {
expr_cell_offset p(e.raw(), offset);
if (!m_visited)
m_visited.reset(new expr_cell_offset_set());
if (m_visited->find(p) != m_visited->end())
goto begin_loop;
m_visited->insert(p);
}
if (!m_f(e, offset))
goto begin_loop;
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Var:
case expr_kind::Sort: case expr_kind::Macro:
goto begin_loop;
case expr_kind::Meta: case expr_kind::Local:
todo.emplace_back(mlocal_type(e), offset);
goto begin_loop;
case expr_kind::App:
todo.emplace_back(app_arg(e), offset);
todo.emplace_back(app_fn(e), offset);
goto begin_loop;
case expr_kind::Pair:
todo.emplace_back(pair_type(e), offset);
todo.emplace_back(pair_second(e), offset);
todo.emplace_back(pair_first(e), offset);
goto begin_loop;
case expr_kind::Fst: case expr_kind::Snd:
todo.emplace_back(proj_arg(e), offset);
goto begin_loop;
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
todo.emplace_back(binder_body(e), offset + 1);
todo.emplace_back(binder_domain(e), offset);
goto begin_loop;
case expr_kind::Let:
todo.emplace_back(let_body(e), offset + 1);
todo.emplace_back(let_value(e), offset);
if (let_type(e))
todo.emplace_back(*let_type(e), offset);
goto begin_loop;
}
}
}
std::unique_ptr<expr_cell_offset_set> m_visited;
std::function<bool(expr const &, unsigned)> m_f;
void apply(expr const & e, unsigned offset);
public:
for_each_fn(F const & f):m_f(f) {}
template<typename F> for_each_fn(F && f):m_f(f) {}
template<typename F> for_each_fn(F const & f):m_f(f) {}
void operator()(expr const & e) { apply(e, 0); }
};
template<typename F>
void for_each(expr const & e, F f) {
return for_each_fn<F>(f)(e);
template<typename F> void for_each(expr const & e, F && f) {
return for_each_fn(f)(e);
}
}

4
src/kernel/occurs.cpp
View file

@ -9,10 +9,10 @@ Author: Leonardo de Moura
namespace lean {
bool occurs(expr const & n, expr const & m) {
return static_cast<bool>(find(m, [&](expr const & e) { return n == e; }));
return static_cast<bool>(find(m, [&](expr const & e, unsigned) { return n == e; }));
}
bool occurs(name const & n, expr const & m) {
return static_cast<bool>(find(m, [&](expr const & e) { return is_constant(e) && const_name(e) == n; }));
return static_cast<bool>(find(m, [&](expr const & e, unsigned) { return is_constant(e) && const_name(e) == n; }));
}
}

157
src/kernel/replace_fn.cpp Normal file
View file

@ -0,0 +1,157 @@
/*
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 "kernel/replace_fn.h"
namespace lean {
bool replace_fn::is_atomic(expr const & e) {
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Sort:
case expr_kind::Macro: case expr_kind::Var:
return true;
default:
return false;
}
}
void replace_fn::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 replace_fn::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()) {
m_rs.push_back(it->second);
return true;
}
shared = true;
}
expr r = m_f(e, offset);
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;
}
}
/**
\brief Return true iff <tt>f.m_index == idx</tt>.
When the result is true, <tt>f.m_index</tt> is incremented.
*/
bool replace_fn::check_index(frame & f, unsigned idx) {
if (f.m_index == idx) {
f.m_index++;
return true;
} else {
return false;
}
}
expr const & replace_fn::rs(int i) {
lean_assert(i < 0);
return m_rs[m_rs.size() + i];
}
void replace_fn::pop_rs(unsigned num) {
m_rs.shrink(m_rs.size() - num);
}
expr replace_fn::operator()(expr const & e) {
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::Constant: case expr_kind::Sort:
case expr_kind::Macro: case expr_kind::Var:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Meta: case expr_kind::Local:
if (check_index(f, 0) && !visit(mlocal_type(e), offset))
goto begin_loop;
r = update_mlocal(e, rs(-1));
pop_rs(1);
break;
case expr_kind::Pair:
if (check_index(f, 0) && !visit(pair_first(e), offset))
goto begin_loop;
if (check_index(f, 1) && !visit(pair_second(e), offset))
goto begin_loop;
if (check_index(f, 2) && !visit(pair_type(e), offset))
goto begin_loop;
r = update_pair(e, rs(-3), rs(-2), rs(-1));
pop_rs(3);
break;
case expr_kind::Fst: case expr_kind::Snd:
if (check_index(f, 0) && !visit(proj_arg(e), offset))
goto begin_loop;
r = update_proj(e, rs(-1));
pop_rs(1);
break;
case expr_kind::App:
if (check_index(f, 0) && !visit(app_fn(e), offset))
goto begin_loop;
if (check_index(f, 1) && !visit(app_arg(e), offset))
goto begin_loop;
r = update_app(e, rs(-2), rs(-1));
pop_rs(2);
break;
case expr_kind::Sigma: case expr_kind::Pi: case expr_kind::Lambda:
if (check_index(f, 0) && !visit(binder_domain(e), offset))
goto begin_loop;
if (check_index(f, 1) && !visit(binder_body(e), offset + 1))
goto begin_loop;
r = update_binder(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 replace_fn::clear() {
m_cache.clear();
m_fs.clear();
m_rs.clear();
}
}

193
src/kernel/replace_fn.h
View file

@ -35,15 +35,7 @@ public:
P is a "post-processing" functional object that is applied to each
pair (old, new)
*/
template<typename F, typename P = default_replace_postprocessor>
class replace_fn {
static_assert(std::is_same<typename std::result_of<F(expr const &, unsigned)>::type, expr>::value,
"replace_fn: return type of F is not expr");
// the return type of P()(e1, e2) should be void
static_assert(std::is_same<typename std::result_of<decltype(std::declval<P>())(expr const &, expr const &)>::type,
void>::value,
"The return type of P()(e1, e2) is not void");
struct frame {
expr m_expr;
unsigned m_offset;
@ -54,179 +46,32 @@ class replace_fn {
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;
expr_cell_offset_map<expr> m_cache;
std::function<expr(expr const &, unsigned)> m_f;
std::function<void(expr const &, expr const &)> m_post;
frame_stack m_fs;
result_stack m_rs;
static bool is_atomic(expr const & e) {
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
case expr_kind::Var: case expr_kind::MetaVar:
return true;
default:
return 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()) {
m_rs.push_back(it->second);
return true;
}
shared = true;
}
expr r = m_f(e, offset);
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;
}
}
/**
\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;
}
}
expr const & rs(int i) {
lean_assert(i < 0);
return m_rs[m_rs.size() + i];
}
void pop_rs(unsigned num) {
m_rs.shrink(m_rs.size() - num);
}
static bool is_atomic(expr const & e);
void save_result(expr const & e, expr const & r, unsigned offset, bool shared);
bool visit(expr const & e, unsigned offset);
bool check_index(frame & f, unsigned idx);
expr const & rs(int i);
void pop_rs(unsigned num);
public:
template<typename F, typename P = default_replace_postprocessor>
replace_fn(F const & f, P const & p = P()):
m_f(f),
m_post(p) {
}
expr operator()(expr const & e) {
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::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::HEq:
if (check_index(f, 0) && !visit(heq_lhs(e), offset))
goto begin_loop;
if (check_index(f, 1) && !visit(heq_rhs(e), offset))
goto begin_loop;
r = update_heq(e, rs(-2), rs(-1));
pop_rs(2);
break;
case expr_kind::Pair:
if (check_index(f, 0) && !visit(pair_first(e), offset))
goto begin_loop;
if (check_index(f, 1) && !visit(pair_second(e), offset))
goto begin_loop;
if (check_index(f, 2) && !visit(pair_type(e), offset))
goto begin_loop;
r = update_pair(e, rs(-3), rs(-2), rs(-1));
pop_rs(3);
break;
case expr_kind::Proj:
if (check_index(f, 0) && !visit(proj_arg(e), offset))
goto begin_loop;
r = update_proj(e, 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::Sigma: 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();
}
m_f(f), m_post(p) {}
expr operator()(expr const & e);
void clear();
};
template<typename F>
expr replace(expr const & e, F f) {
return replace_fn<F>(f)(e);
template<typename F> expr replace(expr const & e, F const & f) {
return replace_fn(f)(e);
}
template<typename F, typename P>
expr replace(expr const & e, F f, P p) {
return replace_fn<F, P>(f, p)(e);
template<typename F, typename P> expr replace(expr const & e, F const & f, P const & p) {
return replace_fn(f, p)(e);
}
}