From 56d7fc4c23284f1ff5f2ed4791bd682fcebcaf74 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Feb 2016 16:55:19 -0800 Subject: [PATCH] refactor(*): cleanup replace_visitor subclasses, and make sure let-expressions are handled --- src/compiler/eta_expansion.cpp | 18 ++++++++++------- src/frontends/lean/nested_declaration.cpp | 9 +++++++-- src/frontends/lean/pp.cpp | 8 ++++---- src/frontends/lean/util.cpp | 6 +++--- src/library/blast/blast.cpp | 24 ++++++++++++++--------- src/library/blast/proof_expr.cpp | 2 +- src/library/blast/state.cpp | 16 +++++++-------- src/library/composition_manager.cpp | 10 ++++++++-- src/library/fun_info_manager.cpp | 1 - src/library/normalize.cpp | 4 ++-- src/library/tactic/unfold_rec.cpp | 2 +- src/library/type_context.cpp | 14 ++++++------- 12 files changed, 67 insertions(+), 47 deletions(-) diff --git a/src/compiler/eta_expansion.cpp b/src/compiler/eta_expansion.cpp index 6d2f5caf6c..0f88d8a769 100644 --- a/src/compiler/eta_expansion.cpp +++ b/src/compiler/eta_expansion.cpp @@ -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) {} }; diff --git a/src/frontends/lean/nested_declaration.cpp b/src/frontends/lean/nested_declaration.cpp index cacfa0bf90..baacbcf7fd 100644 --- a/src/frontends/lean/nested_declaration.cpp +++ b/src/frontends/lean/nested_declaration.cpp @@ -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; } }; diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 42b787f10c..d5b1383b53 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -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)); diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index fe1b198bcb..1bb8e86228 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -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)) { diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index d3bf2c0f12..b38a90e07e 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -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 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 & uvar2uref, name_map> & mvar2meta_mref, diff --git a/src/library/blast/proof_expr.cpp b/src/library/blast/proof_expr.cpp index 97c170801a..df72385137 100644 --- a/src/library/blast/proof_expr.cpp +++ b/src/library/blast/proof_expr.cpp @@ -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()) { diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index b0a93cdf41..b1b827e596 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -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 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 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 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()) { diff --git a/src/library/composition_manager.cpp b/src/library/composition_manager.cpp index ab7b59efe8..63d99a87ee 100644 --- a/src/library/composition_manager.cpp +++ b/src/library/composition_manager.cpp @@ -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; diff --git a/src/library/fun_info_manager.cpp b/src/library/fun_info_manager.cpp index 1e99fb265c..2b53bed8b2 100644 --- a/src/library/fun_info_manager.cpp +++ b/src/library/fun_info_manager.cpp @@ -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 { diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 4b9192c66f..0fd21aa0bf 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -219,7 +219,7 @@ expr try_eta(expr const & e) { template 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) { diff --git a/src/library/tactic/unfold_rec.cpp b/src/library/tactic/unfold_rec.cpp index 0c5a4cbb92..bb298175ac 100644 --- a/src/library/tactic/unfold_rec.cpp +++ b/src/library/tactic/unfold_rec.cpp @@ -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); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 1af2496713..58df70df24 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -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 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 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