max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(*): cleanup replace_visitor subclasses, and make sure let-expressions are handled

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-29 16:55:19 -08:00
parent 3c878ecd01
commit 56d7fc4c23
12 changed files with 67 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/compiler/eta_expansion.cpp
View file

@ -32,22 +32,22 @@ class eta_expand_fn : public replace_visitor {
return e;
}
virtual expr visit_var(expr const &) { lean_unreachable(); }
virtual expr visit_var(expr const &) override { lean_unreachable(); }
virtual expr visit_meta(expr const &) { lean_unreachable(); }
virtual expr visit_meta(expr const &) override { lean_unreachable(); }
virtual expr visit_macro(expr const & e) {
virtual expr visit_macro(expr const & e) override {
if (auto r = expand_core(e))
return *r;
else
return replace_visitor::visit_macro(e);
}
virtual expr visit_constant(expr const & e) { return expand(e); }
virtual expr visit_constant(expr const & e) override { return expand(e); }
virtual expr visit_local(expr const & e) { return expand(e); }
virtual expr visit_local(expr const & e) override { return expand(e); }
virtual expr visit_app(expr const & e) {
virtual expr visit_app(expr const & e) override {
if (auto r = expand_core(e)) {
return *r;
} else {
@ -68,13 +68,17 @@ class eta_expand_fn : public replace_visitor {
}
}
virtual expr visit_binding(expr const & b) {
virtual expr visit_binding(expr const & b) override {
expr new_domain = visit(binding_domain(b));
expr l = mk_local(mk_fresh_name(), new_domain);
expr new_body = abstract_local(visit(instantiate(binding_body(b), l)), l);
return update_binding(b, new_domain, new_body);
}
virtual expr visit_let(expr const & e) override {
return visit(instantiate(let_body(e), let_value(e)));
}
public:
eta_expand_fn(environment const & env):m_env(env), m_tc(env) {}
};

9
src/frontends/lean/nested_declaration.cpp
View file

@ -174,7 +174,7 @@ public:
return mk_app(mk_constant(new_real_name, ls), locals.get_collected());
}
expr visit_macro(expr const & e) {
expr visit_macro(expr const & e) override {
if (is_nested_declaration(e)) {
return extract(e);
} else {
@ -182,13 +182,18 @@ public:
}
}
expr visit_binding(expr const & b) {
expr visit_binding(expr const & b) override {
expr new_domain = visit(binding_domain(b));
expr l = mk_local(mk_fresh_name(), new_domain);
expr new_body = abstract(visit(instantiate(binding_body(b), l)), l);
return update_binding(b, new_domain, new_body);
}
expr visit_let(expr const & e) override {
// TODO(Leo): improve
return visit(instantiate(let_body(e), let_value(e)));
}
environment const & get_env() const { return m_env; }
};

8
src/frontends/lean/pp.cpp
View file

@ -1299,10 +1299,10 @@ pretty_fn::pretty_fn(environment const & env, options const & o, abstract_type_c
// Custom beta reduction procedure for the pretty printer.
// We don't want to reduce application in show annotations.
class pp_beta_reduce_fn : public replace_visitor {
virtual expr visit_meta(expr const & e) { return e; }
virtual expr visit_local(expr const & e) { return e; }
virtual expr visit_meta(expr const & e) override { return e; }
virtual expr visit_local(expr const & e) override { return e; }
virtual expr visit_macro(expr const & e) {
virtual expr visit_macro(expr const & e) override {
if (is_show_annotation(e) && is_app(get_annotation_arg(e))) {
expr const & n = get_annotation_arg(e);
expr new_fn = visit(app_fn(n));
@ -1313,7 +1313,7 @@ class pp_beta_reduce_fn : public replace_visitor {
}
}
virtual expr visit_app(expr const & e) {
virtual expr visit_app(expr const & e) override {
expr new_e = replace_visitor::visit_app(e);
if (is_head_beta(new_e))
return visit(head_beta_reduce(new_e));

6
src/frontends/lean/util.cpp
View file

@ -369,11 +369,11 @@ public:
});
}
virtual expr visit_sort(expr const & e) {
virtual expr visit_sort(expr const & e) override {
return update_sort(e, apply(sort_level(e)));
}
virtual expr visit_constant(expr const & e) {
virtual expr visit_constant(expr const & e) override {
levels ls = map(const_levels(e), [&](level const & l) { return apply(l); });
return update_constant(e, ls);
}
@ -458,7 +458,7 @@ expr postprocess(environment const & env, expr const & e) {
// That is, it replaces every (choice a_0 ... a_n), where a_0 is a numeral, with
// a_0.
class elim_choice_num_fn : public replace_visitor {
virtual expr visit_macro(expr const & m) {
virtual expr visit_macro(expr const & m) override {
if (is_choice(m)) {
expr const & e = macro_arg(m, 0);
if (to_num(e)) {

24
src/library/blast/blast.cpp
View file

@ -324,11 +324,11 @@ class blastenv {
lean_unreachable();
}
virtual expr visit_sort(expr const & e) {
virtual expr visit_sort(expr const & e) override {
return mk_sort(to_blast_level(sort_level(e)));
}
virtual expr visit_macro(expr const & e) {
virtual expr visit_macro(expr const & e) override {
buffer<expr> new_args;
for (unsigned i = 0; i < macro_num_args(e); i++) {
new_args.push_back(visit(macro_arg(e, i)));
@ -336,12 +336,12 @@ class blastenv {
return mk_macro(macro_def(e), new_args.size(), new_args.data());
}
virtual expr visit_constant(expr const & e) {
virtual expr visit_constant(expr const & e) override {
levels new_ls = map(const_levels(e), [&](level const & l) { return to_blast_level(l); });
return mk_constant(const_name(e), new_ls);
}
virtual expr visit_var(expr const & e) {
virtual expr visit_var(expr const & e) override {
return mk_var(var_idx(e));
}
@ -419,18 +419,18 @@ class blastenv {
}
}
virtual expr visit_meta(expr const & e) {
virtual expr visit_meta(expr const & e) override {
return visit_meta_app(e);
}
virtual expr visit_local(expr const & e) {
virtual expr visit_local(expr const & e) override {
if (auto r = m_local2href.find(mlocal_name(e)))
return * r;
else
throw blast_exception("blast tactic failed, ill-formed input goal", e);
}
virtual expr visit_app(expr const & e) {
virtual expr visit_app(expr const & e) override {
if (is_meta(e)) {
return visit_meta_app(e);
} else {
@ -439,16 +439,22 @@ class blastenv {
}
}
virtual expr visit_lambda(expr const & e) {
virtual expr visit_lambda(expr const & e) override {
expr d = visit(binding_domain(e));
return mk_lambda(binding_name(e), d, visit(binding_body(e)), binding_info(e));
}
virtual expr visit_pi(expr const & e) {
virtual expr visit_pi(expr const & e) override {
expr d = visit(binding_domain(e));
return mk_pi(binding_name(e), d, visit(binding_body(e)), binding_info(e));
}
virtual expr visit_let(expr const & e) override {
expr t = visit(let_type(e));
expr v = visit(let_value(e));
return mk_let(let_name(e), t, v, visit(let_body(e)));
}
public:
to_blast_expr_fn(environment const & env, state & s,
name_map<level> & uvar2uref, name_map<pair<expr, expr>> & mvar2meta_mref,

2
src/library/blast/proof_expr.cpp
View file

@ -21,7 +21,7 @@ struct unfold_hypotheses_ge_fn : public replace_visitor {
unfold_hypotheses_ge_fn(state const & s, unsigned d):
m_state(s), m_depth(d) {}
virtual expr visit_local(expr const & e) {
virtual expr visit_local(expr const & e) override {
if (is_href(e)) {
hypothesis const & h = m_state.get_hypothesis_decl(e);
if (h.get_proof_depth() >= m_depth && h.get_value()) {

16
src/library/blast/state.cpp
View file

@ -401,15 +401,15 @@ struct instantiate_urefs_mrefs_fn : public replace_visitor {
[](level const & l1, level const & l2) { return is_eqp(l1, l2); });
}
virtual expr visit_sort(expr const & s) {
virtual expr visit_sort(expr const & s) override {
return update_sort(s, visit_level(sort_level(s)));
}
virtual expr visit_constant(expr const & c) {
virtual expr visit_constant(expr const & c) override {
return update_constant(c, visit_levels(const_levels(c)));
}
virtual expr visit_local(expr const & e) {
virtual expr visit_local(expr const & e) override {
if (is_href(e)) {
return e;
} else {
@ -417,7 +417,7 @@ struct instantiate_urefs_mrefs_fn : public replace_visitor {
}
}
virtual expr visit_meta(expr const & m) {
virtual expr visit_meta(expr const & m) override {
lean_assert(is_mref(m));
if (auto v1 = m_state.get_mref_assignment(m)) {
if (!has_mref(*v1)) {
@ -433,7 +433,7 @@ struct instantiate_urefs_mrefs_fn : public replace_visitor {
}
}
virtual expr visit_app(expr const & e) {
virtual expr visit_app(expr const & e) override {
buffer<expr> args;
expr const & f = get_app_rev_args(e, args);
if (is_mref(f)) {
@ -460,7 +460,7 @@ struct instantiate_urefs_mrefs_fn : public replace_visitor {
return mk_rev_app(new_f, new_args, e.get_tag());
}
virtual expr visit_macro(expr const & e) {
virtual expr visit_macro(expr const & e) override {
lean_assert(is_macro(e));
buffer<expr> new_args;
for (unsigned i = 0; i < macro_num_args(e); i++)
@ -468,7 +468,7 @@ struct instantiate_urefs_mrefs_fn : public replace_visitor {
return update_macro(e, new_args.size(), new_args.data());
}
virtual expr visit(expr const & e) {
virtual expr visit(expr const & e) override {
if (!has_mref(e) && !has_univ_metavar(e))
return e;
else
@ -933,7 +933,7 @@ struct expand_hrefs_fn : public replace_visitor {
expand_hrefs_fn(state const & s, list<expr> const & hrefs):
m_state(s), m_hrefs(hrefs) {}
virtual expr visit_local(expr const & e) {
virtual expr visit_local(expr const & e) override {
if (is_href(e) && std::find(m_hrefs.begin(), m_hrefs.end(), e) != m_hrefs.end()) {
hypothesis const & h = m_state.get_hypothesis_decl(e);
if (h.get_value()) {

10
src/library/composition_manager.cpp
View file

@ -42,11 +42,17 @@ struct elim_proj_mk : public replace_visitor {
environment const & m_env;
type_checker_ptr m_tc;
virtual expr visit_binding(expr const & e) {
virtual expr visit_binding(expr const & e) override {
// stop at binders
return e;
}
virtual expr visit_app(expr const & e) {
virtual expr visit_let(expr const & e) override {
// stop at binders
return e;
}
virtual expr visit_app(expr const & e) override {
expr const & fn = get_app_fn(e);
if (is_constant(fn) && is_projection(m_env, const_name(fn))) {
expr new_e = m_tc->whnf(e).first;

1
src/library/fun_info_manager.cpp
View file

@ -10,7 +10,6 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "library/trace.h"
#include "library/replace_visitor.h"
#include "library/fun_info_manager.h"
namespace lean {

4
src/library/normalize.cpp
View file

@ -219,7 +219,7 @@ expr try_eta(expr const & e) {
template<bool Eta, bool Beta>
class eta_beta_reduce_fn : public replace_visitor {
public:
virtual expr visit_app(expr const & e) {
virtual expr visit_app(expr const & e) override {
expr e1 = replace_visitor::visit_app(e);
if (Beta && is_head_beta(e1)) {
return visit(head_beta_reduce(e1));
@ -228,7 +228,7 @@ public:
}
}
virtual expr visit_lambda(expr const & e) {
virtual expr visit_lambda(expr const & e) override {
expr e1 = replace_visitor::visit_lambda(e);
if (Eta) {
while (true) {

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

@ -35,7 +35,7 @@ protected:
return mk_app(fn, args);
}
virtual expr visit_binding(expr const & b) {
virtual expr visit_binding(expr const & b) override {
expr new_domain = visit(binding_domain(b));
expr l = mk_local(mk_fresh_name(), new_domain);
expr new_body = abstract(visit(instantiate(binding_body(b), l)), l);

14
src/library/type_context.cpp
View file

@ -575,19 +575,19 @@ struct instantiate_uvars_mvars_fn : public replace_visitor {
[](level const & l1, level const & l2) { return is_eqp(l1, l2); });
}
virtual expr visit_sort(expr const & s) {
virtual expr visit_sort(expr const & s) override {
return update_sort(s, visit_level(sort_level(s)));
}
virtual expr visit_constant(expr const & c) {
virtual expr visit_constant(expr const & c) override {
return update_constant(c, visit_levels(const_levels(c)));
}
virtual expr visit_local(expr const & e) {
virtual expr visit_local(expr const & e) override {
return update_mlocal(e, visit(mlocal_type(e)));
}
virtual expr visit_meta(expr const & m) {
virtual expr visit_meta(expr const & m) override {
if (m_owner.is_mvar(m)) {
if (auto v1 = m_owner.get_assignment(m)) {
if (!has_expr_metavar(*v1)) {
@ -606,7 +606,7 @@ struct instantiate_uvars_mvars_fn : public replace_visitor {
}
}
virtual expr visit_app(expr const & e) {
virtual expr visit_app(expr const & e) override {
buffer<expr> args;
expr const & f = get_app_rev_args(e, args);
if (m_owner.is_mvar(f)) {
@ -633,7 +633,7 @@ struct instantiate_uvars_mvars_fn : public replace_visitor {
return mk_rev_app(new_f, new_args, e.get_tag());
}
virtual expr visit_macro(expr const & e) {
virtual expr visit_macro(expr const & e) override {
lean_assert(is_macro(e));
buffer<expr> new_args;
for (unsigned i = 0; i < macro_num_args(e); i++)
@ -641,7 +641,7 @@ struct instantiate_uvars_mvars_fn : public replace_visitor {
return update_macro(e, new_args.size(), new_args.data());
}
virtual expr visit(expr const & e) {
virtual expr visit(expr const & e) override {
if (!has_expr_metavar(e) && !has_univ_metavar(e))
return e;
else