From dc5dbb3b81f3baefdf30033da521a614caea7fd2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Oct 2018 15:22:49 -0700 Subject: [PATCH] chore(library/compiler): remove dead code --- src/library/compiler/CMakeLists.txt | 2 +- src/library/compiler/elim_unused_lets.cpp | 58 ---- src/library/compiler/elim_unused_lets.h | 11 - src/library/compiler/old_cse.cpp | 307 ---------------------- src/library/compiler/old_cse.h | 14 - src/library/compiler/preprocess.cpp | 22 +- 6 files changed, 10 insertions(+), 404 deletions(-) delete mode 100644 src/library/compiler/elim_unused_lets.cpp delete mode 100644 src/library/compiler/elim_unused_lets.h delete mode 100644 src/library/compiler/old_cse.cpp delete mode 100644 src/library/compiler/old_cse.h diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt index 4201184637..64fee5d4b6 100644 --- a/src/library/compiler/CMakeLists.txt +++ b/src/library/compiler/CMakeLists.txt @@ -1,7 +1,7 @@ add_library(compiler OBJECT old_util.cpp preprocess.cpp compiler_step_visitor.cpp lambda_lifting.cpp simp_inductive.cpp - vm_compiler.cpp old_cse.cpp elim_unused_lets.cpp extract_values.cpp init_module.cpp + vm_compiler.cpp extract_values.cpp init_module.cpp ## New compiler util.cpp lcnf.cpp csimp.cpp elim_dead_let.cpp cse.cpp erase_irrelevant.cpp specialize.cpp compiler.cpp diff --git a/src/library/compiler/elim_unused_lets.cpp b/src/library/compiler/elim_unused_lets.cpp deleted file mode 100644 index da753e008e..0000000000 --- a/src/library/compiler/elim_unused_lets.cpp +++ /dev/null @@ -1,58 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "kernel/instantiate.h" -#include "library/locals.h" -#include "library/compiler/procedure.h" -#include "library/compiler/compiler_step_visitor.h" - -namespace lean { -class elim_unused_lets_fn : public compiler_step_visitor { - virtual expr visit_lambda(expr const & e) override { - type_context_old::tmp_locals locals(m_ctx); - expr t = e; - while (is_lambda(t)) { - expr d = instantiate_rev(binding_domain(t), locals.size(), locals.data()); - locals.push_local(binding_name(t), d, binding_info(t)); - t = binding_body(t); - } - t = instantiate_rev(t, locals.size(), locals.data()); - t = visit(t); - return locals.mk_lambda(t); - } - - virtual expr visit_let(expr const & e) override { - type_context_old::tmp_locals locals(m_ctx); - collected_locals used_locals; - expr t = e; - while (is_let(t)) { - expr d = instantiate_rev(let_type(t), locals.size(), locals.data()); - expr v = visit(instantiate_rev(let_value(t), locals.size(), locals.data())); - collect_locals(d, used_locals); - collect_locals(v, used_locals); - locals.push_let(let_name(t), d, v); - t = let_body(t); - } - t = instantiate_rev(t, locals.size(), locals.data()); - t = visit(t); - collect_locals(t, used_locals); - buffer new_locals; - for (expr const & l : locals.as_buffer()) { - if (used_locals.contains(l)) - new_locals.push_back(l); - } - return m_ctx.mk_lambda(new_locals, t); - } -public: - elim_unused_lets_fn(environment const & env, abstract_context_cache & cache):compiler_step_visitor(env, cache) {} -}; - -void elim_unused_lets(environment const & env, abstract_context_cache & cache, buffer & procs) { - elim_unused_lets_fn fn(env, cache); - for (auto & proc : procs) - proc.m_code = fn(proc.m_code); -} -} diff --git a/src/library/compiler/elim_unused_lets.h b/src/library/compiler/elim_unused_lets.h deleted file mode 100644 index a6d661fc51..0000000000 --- a/src/library/compiler/elim_unused_lets.h +++ /dev/null @@ -1,11 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/compiler/procedure.h" -namespace lean { -void elim_unused_lets(environment const & env, abstract_context_cache & cache, buffer & procs); -} diff --git a/src/library/compiler/old_cse.cpp b/src/library/compiler/old_cse.cpp deleted file mode 100644 index 5af6bd37f4..0000000000 --- a/src/library/compiler/old_cse.cpp +++ /dev/null @@ -1,307 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "kernel/expr_sets.h" -#include "kernel/expr_maps.h" -#include "kernel/instantiate.h" -#include "kernel/replace_fn.h" -#include "library/trace.h" -#include "library/constants.h" -#include "library/locals.h" -#include "library/vm/vm.h" -#include "library/compiler/procedure.h" -#include "library/compiler/util.h" -#include "library/compiler/compiler_step_visitor.h" -#include "library/compiler/simp_inductive.h" - -namespace lean { -class old_cse_fn : public compiler_step_visitor { - unsigned m_counter{1}; - - class visitor_fn { - protected: - expr_set m_visited; /* do we need this? */ - - bool check_visited(expr const & e) { - if (m_visited.find(e) != m_visited.end()) - return true; - m_visited.insert(e); - return false; - } - - virtual void visit_app(expr const & e) = 0; - - void visit_let(expr const & e) { - if (check_visited(e)) return; - visit(let_value(e)); - visit(let_body(e)); - } - - void visit_lambda(expr const & e) { - if (check_visited(e)) return; - visit(binding_body(e)); - } - - void visit(expr const & e) { - switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Sort: - case expr_kind::MVar: case expr_kind::Pi: - case expr_kind::Const: case expr_kind::FVar: - case expr_kind::Lit: - break; - case expr_kind::Lambda: visit_lambda(e); break; - case expr_kind::App: visit_app(e); break; - case expr_kind::Let: visit_let(e); break; - case expr_kind::MData: visit(mdata_expr(e)); break; - case expr_kind::Proj: visit(proj_expr(e)); break; - } - } - public: - void operator()(expr const & e) { return visit(e); } - }; - - class collect_candidates_fn : public visitor_fn { - environment const & m_env; - expr_set m_candidates; - - void add_candidate(expr const & e) { - if (has_loose_bvars(e)) return; - m_candidates.insert(e); - } - - virtual void visit_app(expr const & e) override { - if (check_visited(e)) return; - expr const & fn = get_app_fn(e); - if (is_internal_cnstr(fn)) { - /* Eliminating `_cnstr` applications is problematic because they cannot be curried. - We would have to adjust the replacement logic in `cse_processor::process` to - never replace partial applications of `_cnstr`. Instead, we simply deactivate - CSE for `_cnstr` applications for the time being. (#1968) */ - return; - } - add_candidate(e); - if (is_vm_supported_cases(m_env, fn)) { - /* We do not eliminate a common subexpression if it *only* occurs inside of a cases */ - return; - } - buffer args; - get_app_args(e, args); - for (expr const & arg : args) - visit(arg); - } - public: - collect_candidates_fn(environment const & env):m_env(env) {} - expr_set const & get_candidates() const { return m_candidates; } - }; - - class collect_num_occs_fn : public visitor_fn { - expr_set const & m_candidates; - expr_map m_num_occs; - - void add_occ(expr const & e) { - if (has_loose_bvars(e)) return; - if (m_candidates.find(e) == m_candidates.end()) return; - if (m_num_occs.find(e) == m_num_occs.end()) { - m_num_occs.insert(mk_pair(e, 1)); - } else { - m_num_occs[e]++; - } - } - - virtual void visit_app(expr const & e) override { - add_occ(e); - if (check_visited(e)) return; - buffer args; - get_app_args(e, args); - for (expr const & arg : args) - visit(arg); - } - public: - collect_num_occs_fn(expr_set const & cs):m_candidates(cs) {} - expr_map const & get_num_occs() const { return m_num_occs; } - }; - - void collect_common_subexprs(buffer const & let_values, expr const & body, - expr_set & r) { - /* first pass */ - collect_candidates_fn candidate_collector(m_ctx.env()); - for (expr const & v : let_values) candidate_collector(v); - candidate_collector(body); - - /* second pass */ - collect_num_occs_fn num_occs_collector(candidate_collector.get_candidates()); - for (expr const & v : let_values) num_occs_collector(v); - num_occs_collector(body); - - for (pair const & p : num_occs_collector.get_num_occs()) { - if (p.second > 1) - r.insert(p.first); - } - } - - void collect_common_subexprs(expr const & e, expr_set & r) { - buffer tmp; - collect_common_subexprs(tmp, e, r); - } - - /* Helper functor for converting common subexpressions into fresh let-decls */ - struct cse_processor { - unsigned & m_counter; - expr_set const & m_common_subexprs; - expr_map m_common_subexpr_to_local; - type_context_old::tmp_locals m_all_locals; /* new local declarations, it also include let-decls for common-subexprs */ - local_context const & m_lctx; - - cse_processor(unsigned & counter, type_context_old & ctx, expr_set const & s): - m_counter(counter), - m_common_subexprs(s), - m_all_locals(ctx), - m_lctx(ctx.lctx()) { - } - - virtual expr adjust_locals(expr const & v) { - return v; - } - - expr process(expr const & e, optional const & main = none_expr()) { - expr r = replace(e, [&](expr const & s, unsigned) { - if (main && s == *main) return none_expr(); - if (!is_app(s)) return none_expr(); - if (has_loose_bvars(s)) return none_expr(); - auto it1 = m_common_subexpr_to_local.find(s); - if (it1 != m_common_subexpr_to_local.end()) - return some_expr(it1->second); - if (m_common_subexprs.find(s) == m_common_subexprs.end()) - return none_expr(); - /* Eliminate common subexpressions nested in s */ - expr new_v = process(s, some_expr(s)); - name n = name("_c").append_after(m_counter); - m_counter++; - expr l = m_all_locals.push_let(n, mk_enf_neutral(), new_v); - m_common_subexpr_to_local.insert(mk_pair(s, l)); - return some_expr(l); - }); - return adjust_locals(r); - } - }; - - /* Similar to cse_processor, but has support for binding exprs (lambda and let) */ - struct cse_processor_for_binding : public cse_processor { - type_context_old::tmp_locals const & m_locals; - buffer m_new_locals; - - cse_processor_for_binding(unsigned & counter, type_context_old & ctx, type_context_old::tmp_locals const & locals, expr_set const & s): - cse_processor(counter, ctx, s), - m_locals(locals) { - } - - virtual expr adjust_locals(expr const & v) { - return replace_locals(v, m_new_locals.size(), m_locals.data(), m_new_locals.data()); - } - - void process_locals() { - lean_assert(m_new_locals.empty()); - for (expr const & local : m_locals.as_buffer()) { - local_decl decl = m_lctx.get_local_decl(local); - if (decl.get_value()) { - /* let-entry */ - expr new_v = process(*decl.get_value()); - expr l = m_all_locals.push_let(decl.get_user_name(), adjust_locals(decl.get_type()), new_v); - m_new_locals.push_back(l); - } else { - /* lambda-entry */ - expr l = m_all_locals.push_local(decl.get_user_name(), adjust_locals(decl.get_type()), decl.get_info()); - m_new_locals.push_back(l); - } - } - } - }; - - expr visit_lambda_let(expr const & e) { - type_context_old::tmp_locals locals(m_ctx); - expr t = e; - buffer let_values; - while (true) { - /* Types are ignored in compilation steps. So, we do not invoke visit for d. */ - if (is_lambda(t)) { - expr d = instantiate_rev(binding_domain(t), locals.size(), locals.data()); - locals.push_local(binding_name(t), d, binding_info(t)); - t = binding_body(t); - } else if (is_let(t)) { - expr d = instantiate_rev(let_type(t), locals.size(), locals.data()); - expr v = visit(instantiate_rev(let_value(t), locals.size(), locals.data())); - let_values.push_back(v); - locals.push_let(let_name(t), d, v); - t = let_body(t); - } else { - break; - } - } - t = instantiate_rev(t, locals.size(), locals.data()); - t = visit(t); - - expr_set common_subexprs; - collect_common_subexprs(let_values, t, common_subexprs); - if (common_subexprs.empty()) - return locals.mk_lambda(t); - - cse_processor_for_binding proc(m_counter, m_ctx, locals, common_subexprs); - proc.process_locals(); - expr new_t = proc.process(t); - return proc.m_all_locals.mk_lambda(new_t); - } - - virtual expr visit_lambda(expr const & e) override { - return visit_lambda_let(e); - } - - virtual expr visit_let(expr const & e) override { - return visit_lambda_let(e); - } - - expr visit_cases_on(expr const & e) { - buffer args; - expr const & fn = get_app_args(e, args); - args[0] = visit(args[0]); // major premise - for (unsigned i = 1; i < args.size(); i++) { - expr m = args[i]; - if (is_lambda(m)) { - args[i] = visit(m); - } else { - m = visit(m); - expr_set common_subexprs; - collect_common_subexprs(m, common_subexprs); - if (!common_subexprs.empty()) { - cse_processor proc(m_counter, m_ctx, common_subexprs); - m = proc.process(m); - m = proc.m_all_locals.mk_lambda(m); - } - args[i] = m; - } - } - return mk_app(fn, args); - } - - virtual expr visit_app(expr const & e) override { - expr const & fn = get_app_fn(e); - if (is_vm_supported_cases(m_env, fn)) { - return visit_cases_on(e); - } else { - return compiler_step_visitor::visit_app(e); - } - } - -public: - old_cse_fn(environment const & env, abstract_context_cache & cache): - compiler_step_visitor(env, cache) {} -}; - -void old_cse(environment const & env, abstract_context_cache & cache, buffer & procs) { - old_cse_fn fn(env, cache); - for (auto & proc : procs) - proc.m_code = fn(proc.m_code); -} -} diff --git a/src/library/compiler/old_cse.h b/src/library/compiler/old_cse.h deleted file mode 100644 index 443d9bc4cd..0000000000 --- a/src/library/compiler/old_cse.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/abstract_context_cache.h" -#include "library/compiler/procedure.h" -namespace lean { -/* Common subexpression elimination. - It must be only applied after simp_inductive step. */ -void old_cse(environment const & env, abstract_context_cache & cache, buffer & procs); -} diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index cff8f8d8c7..a047b0636a 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -27,9 +27,7 @@ Author: Leonardo de Moura #include "library/compiler/compiler_step_visitor.h" #include "library/compiler/lambda_lifting.h" #include "library/compiler/simp_inductive.h" -#include "library/compiler/elim_unused_lets.h" #include "library/compiler/extract_values.h" -#include "library/compiler/old_cse.h" #include "library/compiler/util.h" #include "library/compiler/lcnf.h" @@ -144,15 +142,17 @@ public: lambda_lifting(m_env, m_cache, n, procs); lean_trace(name({"compiler", "lambda_lifting"}), tout() << "\n"; display(procs);); - simp_inductive(m_env, m_cache, procs); - lean_trace(name({"compiler", "simplify_inductive"}), tout() << "\n"; display(procs);); - elim_unused_lets(m_env, m_cache, procs); - lean_trace(name({"compiler", "elim_unused_lets"}), tout() << "\n"; display(procs);); + + for (procedure & p : procs) { + p.m_code = elim_dead_let(p.m_code); + p.m_code = cse(m_env, p.m_code); + } + extract_values(m_env, m_cache, n, procs); lean_trace(name({"compiler", "extract_values"}), tout() << "\n"; display(procs);); - old_cse(m_env, m_cache, procs); - lean_trace(name({"compiler", "cse"}), tout() << "\n"; display(procs);); - lean_trace(name({"compiler", "preprocess"}), tout() << "\n"; display(procs);); + + simp_inductive(m_env, m_cache, procs); + lean_trace(name({"compiler", "simplify_inductive"}), tout() << "\n"; display(procs);); return m_env; } }; @@ -181,15 +181,11 @@ void initialize_preprocess() { register_trace_class({"compiler", "simp"}); register_trace_class({"compiler", "stage1"}); register_trace_class({"compiler", "specialize"}); - register_trace_class({"compiler", "expand_aux"}); - register_trace_class({"compiler", "inline"}); register_trace_class({"compiler", "erase_irrelevant"}); register_trace_class({"compiler", "lambda_lifting"}); register_trace_class({"compiler", "simplify_inductive"}); - register_trace_class({"compiler", "elim_unused_lets"}); register_trace_class({"compiler", "extract_values"}); register_trace_class({"compiler", "cse"}); - register_trace_class({"compiler", "preprocess"}); } void finalize_preprocess() {