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

refactor(kernel): replace_visitor

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-18 23:15:55 -08:00
parent 101888e079
commit 16aa1ebbac
3 changed files with 45 additions and 59 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/CMakeLists.txt
View file

@ -1,12 +1,12 @@
add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp
object.cpp environment.cpp object.cpp environment.cpp replace_visitor.cpp io_state.cpp
# normalizer.cpp # normalizer.cpp
# type_checker.cpp kernel.cpp metavar.cpp # type_checker.cpp kernel.cpp metavar.cpp
# justification.cpp unification_constraint.cpp # justification.cpp unification_constraint.cpp
# type_checker_justification.cpp pos_info_provider.cpp # type_checker_justification.cpp pos_info_provider.cpp
# replace_visitor.cpp update_expr.cpp io_state.cpp # update_expr.cpp
# universe_constraints.cpp # universe_constraints.cpp
) )

84
src/kernel/replace_visitor.cpp
View file

@ -10,65 +10,48 @@ Author: Leonardo de Moura
#include "kernel/replace_visitor.h" #include "kernel/replace_visitor.h"
namespace lean { namespace lean {
expr replace_visitor::visit_type(expr const & e, context const &) { lean_assert(is_type(e)); return e; } expr replace_visitor::visit_sort(expr const & e, context const &) { lean_assert(is_sort(e)); return e; }
expr replace_visitor::visit_value(expr const & e, context const &) { lean_assert(is_value(e)); return e; } expr replace_visitor::visit_macro(expr const & e, context const &) { lean_assert(is_macro(e)); return e; }
expr replace_visitor::visit_var(expr const & e, context const &) { lean_assert(is_var(e)); return e; } expr replace_visitor::visit_var(expr const & e, context const &) { lean_assert(is_var(e)); return e; }
expr replace_visitor::visit_metavar(expr const & e, context const &) { lean_assert(is_metavar(e)); return e; } expr replace_visitor::visit_constant(expr const & e, context const &) { lean_assert(is_constant(e)); return e; }
expr replace_visitor::visit_constant(expr const & e, context const & ctx) { expr replace_visitor::visit_mlocal(expr const & e, context const & ctx) {
lean_assert(is_constant(e)); lean_assert(is_mlocal(e));
return update_const(e, visit(const_type(e), ctx)); return update_mlocal(e, visit(mlocal_type(e), ctx));
} }
expr replace_visitor::visit_meta(expr const & e, context const & ctx) { return visit_mlocal(e, ctx); }
expr replace_visitor::visit_local(expr const & e, context const & ctx) { return visit_mlocal(e, ctx); }
expr replace_visitor::visit_pair(expr const & e, context const & ctx) { expr replace_visitor::visit_pair(expr const & e, context const & ctx) {
lean_assert(is_dep_pair(e)); lean_assert(is_dep_pair(e));
return update_pair(e, [&](expr const & f, expr const & s, expr const & t) { return update_pair(e, visit(pair_first(e), ctx), visit(pair_second(e), ctx), visit(pair_type(e), ctx));
return std::make_tuple(visit(f, ctx), visit(s, ctx), visit(t, ctx));
});
} }
expr replace_visitor::visit_proj(expr const & e, context const & ctx) { expr replace_visitor::visit_proj(expr const & e, context const & ctx) {
lean_assert(is_proj(e));
return update_proj(e, visit(proj_arg(e), ctx)); return update_proj(e, visit(proj_arg(e), ctx));
} }
expr replace_visitor::visit_fst(expr const & e, context const & ctx) { return visit_proj(e, ctx); }
expr replace_visitor::visit_snd(expr const & e, context const & ctx) { return visit_proj(e, ctx); }
expr replace_visitor::visit_app(expr const & e, context const & ctx) { expr replace_visitor::visit_app(expr const & e, context const & ctx) {
lean_assert(is_app(e)); lean_assert(is_app(e));
return update_app(e, [&](expr const & c) { return visit(c, ctx); }); return update_app(e, visit(app_fn(e), ctx), visit(app_arg(e), ctx));
} }
expr replace_visitor::visit_heq(expr const & e, context const & ctx) { expr replace_visitor::visit_binder(expr const & e, context const & ctx) {
lean_assert(is_heq(e)); lean_assert(is_binder(e));
return update_heq(e, visit(heq_lhs(e), ctx), visit(heq_rhs(e), ctx)); expr new_d = visit(binder_domain(e), ctx);
} freset<cache> reset(m_cache);
expr replace_visitor::visit_abst(expr const & e, context const & ctx) { expr new_b = visit(binder_body(e), extend(ctx, binder_name(e), new_d));
lean_assert(is_abstraction(e)); return update_binder(e, new_d, new_b);
return update_abst(e, [&](expr const & t, expr const & b) {
expr new_t = visit(t, ctx);
{
freset<cache> reset(m_cache);
expr new_b = visit(b, extend(ctx, abst_name(e), new_t));
return std::make_pair(new_t, new_b);
}
});
}
expr replace_visitor::visit_lambda(expr const & e, context const & ctx) {
lean_assert(is_lambda(e));
return visit_abst(e, ctx);
}
expr replace_visitor::visit_pi(expr const & e, context const & ctx) {
lean_assert(is_pi(e));
return visit_abst(e, ctx);
}
expr replace_visitor::visit_sigma(expr const & e, context const & ctx) {
lean_assert(is_sigma(e));
return visit_abst(e, ctx);
} }
expr replace_visitor::visit_lambda(expr const & e, context const & ctx) { return visit_binder(e, ctx); }
expr replace_visitor::visit_pi(expr const & e, context const & ctx) { return visit_binder(e, ctx); }
expr replace_visitor::visit_sigma(expr const & e, context const & ctx) { return visit_binder(e, ctx); }
expr replace_visitor::visit_let(expr const & e, context const & ctx) { expr replace_visitor::visit_let(expr const & e, context const & ctx) {
lean_assert(is_let(e)); lean_assert(is_let(e));
return update_let(e, [&](optional<expr> const & t, expr const & v, expr const & b) { optional<expr> new_t = visit(let_type(e), ctx);
optional<expr> new_t = visit(t, ctx); expr new_v = visit(let_value(e), ctx);
expr new_v = visit(v, ctx); freset<cache> reset(m_cache);
{ // TODO(Leo): decide what we should do with let-exprs
freset<cache> reset(m_cache); expr new_b; // = visit(let_body(e), extend(ctx, let_name(e), new_t, new_v));
expr new_b = visit(b, extend(ctx, let_name(e), new_t, new_v)); return update_let(e, new_t, new_v, new_b);
return std::make_tuple(new_t, new_v, new_b);
}
});
} }
expr replace_visitor::save_result(expr const & e, expr && r, bool shared) { expr replace_visitor::save_result(expr const & e, expr && r, bool shared) {
if (shared) if (shared)
@ -86,14 +69,15 @@ expr replace_visitor::visit(expr const & e, context const & ctx) {
} }
switch (e.kind()) { switch (e.kind()) {
case expr_kind::Type: return save_result(e, visit_type(e, ctx), shared); case expr_kind::Sort: return save_result(e, visit_sort(e, ctx), shared);
case expr_kind::Value: return save_result(e, visit_value(e, ctx), shared); case expr_kind::Macro: return save_result(e, visit_macro(e, ctx), shared);
case expr_kind::Constant: return save_result(e, visit_constant(e, ctx), shared); case expr_kind::Constant: return save_result(e, visit_constant(e, ctx), shared);
case expr_kind::Var: return save_result(e, visit_var(e, ctx), shared); case expr_kind::Var: return save_result(e, visit_var(e, ctx), shared);
case expr_kind::MetaVar: return save_result(e, visit_metavar(e, ctx), shared); case expr_kind::Meta: return save_result(e, visit_meta(e, ctx), shared);
case expr_kind::HEq: return save_result(e, visit_heq(e, ctx), shared); case expr_kind::Local: return save_result(e, visit_local(e, ctx), shared);
case expr_kind::Pair: return save_result(e, visit_pair(e, ctx), shared); case expr_kind::Pair: return save_result(e, visit_pair(e, ctx), shared);
case expr_kind::Proj: return save_result(e, visit_proj(e, ctx), shared); case expr_kind::Fst: return save_result(e, visit_fst(e, ctx), shared);
case expr_kind::Snd: return save_result(e, visit_snd(e, ctx), shared);
case expr_kind::App: return save_result(e, visit_app(e, ctx), shared); case expr_kind::App: return save_result(e, visit_app(e, ctx), shared);
case expr_kind::Lambda: return save_result(e, visit_lambda(e, ctx), shared); case expr_kind::Lambda: return save_result(e, visit_lambda(e, ctx), shared);
case expr_kind::Pi: return save_result(e, visit_pi(e, ctx), shared); case expr_kind::Pi: return save_result(e, visit_pi(e, ctx), shared);

16
src/kernel/replace_visitor.h
View file

@ -6,13 +6,12 @@ Author: Leonardo de Moura
*/ */
#pragma once #pragma once
#include "kernel/expr_maps.h" #include "kernel/expr_maps.h"
#include "kernel/replace_fn.h"
#include "kernel/context.h" #include "kernel/context.h"
namespace lean { namespace lean {
/** /**
\brief Base class for implementing operations that apply modifications \brief Base class for implementing operations that apply modifications
an expressions. on expressions.
The default behavior is a NOOP, users must create subclasses and The default behavior is a NOOP, users must create subclasses and
redefine the visit_* methods. redefine the visit_* methods.
@ -25,16 +24,19 @@ protected:
cache m_cache; cache m_cache;
context m_ctx; context m_ctx;
expr save_result(expr const & e, expr && r, bool shared); expr save_result(expr const & e, expr && r, bool shared);
virtual expr visit_type(expr const &, context const &); virtual expr visit_sort(expr const &, context const &);
virtual expr visit_value(expr const &, context const &); virtual expr visit_macro(expr const &, context const &);
virtual expr visit_constant(expr const &, context const &); virtual expr visit_constant(expr const &, context const &);
virtual expr visit_var(expr const &, context const &); virtual expr visit_var(expr const &, context const &);
virtual expr visit_metavar(expr const &, context const &); virtual expr visit_mlocal(expr const &, context const &);
virtual expr visit_heq(expr const &, context const &); virtual expr visit_meta(expr const &, context const &);
virtual expr visit_local(expr const &, context const &);
virtual expr visit_pair(expr const &, context const &); virtual expr visit_pair(expr const &, context const &);
virtual expr visit_proj(expr const &, context const &); virtual expr visit_proj(expr const &, context const &);
virtual expr visit_fst(expr const &, context const &);
virtual expr visit_snd(expr const &, context const &);
virtual expr visit_app(expr const &, context const &); virtual expr visit_app(expr const &, context const &);
virtual expr visit_abst(expr const &, context const &); virtual expr visit_binder(expr const &, context const &);
virtual expr visit_lambda(expr const &, context const &); virtual expr visit_lambda(expr const &, context const &);
virtual expr visit_pi(expr const &, context const &); virtual expr visit_pi(expr const &, context const &);
virtual expr visit_sigma(expr const &, context const &); virtual expr visit_sigma(expr const &, context const &);