From b55b1deaf500e9bcbe4a2b96d97d89f69fcd8ec3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Nov 2018 16:53:44 -0800 Subject: [PATCH] chore(library/compiler): remove `ir.cpp` There is only one missing transformation: insert explicit reference counting instructions. We will implement this transformation at `llnf.cpp`. After that, we are ready to emit C++ code. --- src/library/compiler/CMakeLists.txt | 2 +- src/library/compiler/init_module.cpp | 3 - src/library/compiler/ir.cpp | 353 --------------------------- src/library/compiler/ir.h | 14 -- 4 files changed, 1 insertion(+), 371 deletions(-) delete mode 100644 src/library/compiler/ir.cpp delete mode 100644 src/library/compiler/ir.h diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt index 2e3ee6c585..e4aa12aae6 100644 --- a/src/library/compiler/CMakeLists.txt +++ b/src/library/compiler/CMakeLists.txt @@ -4,4 +4,4 @@ add_library(compiler OBJECT util.cpp lcnf.cpp csimp.cpp elim_dead_let.cpp cse.cpp erase_irrelevant.cpp specialize.cpp compiler.cpp lambda_lifting.cpp extract_closed.cpp simp_app_args.cpp llnf.cpp ll_infer_type.cpp reduce_arity.cpp - closed_term_cache.cpp builtin.cpp ir.cpp) + closed_term_cache.cpp builtin.cpp) diff --git a/src/library/compiler/init_module.cpp b/src/library/compiler/init_module.cpp index 3619e36405..9e9b5f8070 100644 --- a/src/library/compiler/init_module.cpp +++ b/src/library/compiler/init_module.cpp @@ -11,7 +11,6 @@ Author: Leonardo de Moura #include "library/compiler/specialize.h" #include "library/compiler/llnf.h" #include "library/compiler/closed_term_cache.h" -#include "library/compiler/ir.h" #include "library/compiler/compiler.h" #include "library/compiler/builtin.h" @@ -24,7 +23,6 @@ void initialize_compiler_module() { initialize_specialize(); initialize_closed_term_cache(); initialize_llnf(); - initialize_ir(); initialize_compiler(); initialize_builtin(); } @@ -32,7 +30,6 @@ void initialize_compiler_module() { void finalize_compiler_module() { finalize_builtin(); finalize_compiler(); - finalize_ir(); finalize_llnf(); finalize_closed_term_cache(); finalize_specialize(); diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp deleted file mode 100644 index 9e2518f5a4..0000000000 --- a/src/library/compiler/ir.cpp +++ /dev/null @@ -1,353 +0,0 @@ -/* -Copyright (c) 2018 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "kernel/environment.h" -#include "kernel/instantiate.h" -#include "kernel/abstract.h" -#include "kernel/for_each_fn.h" -#include "library/module.h" -#include "library/compiler/util.h" - -namespace lean { -/* Extension used to store data needed when translating LLNF into IR. - TODO(Leo): use the to be implemented new module system. */ -struct ir_ext : public environment_extension { - typedef name_map boxed_map; - boxed_map m_boxed_map; -}; - -struct ir_ext_reg { - unsigned m_ext_id; - ir_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } -}; - -static ir_ext_reg * g_ext = nullptr; -static ir_ext const & get_extension(environment const & env) { - return static_cast(env.get_extension(g_ext->m_ext_id)); -} -static environment update(environment const & env, ir_ext const & ext) { - return env.update(g_ext->m_ext_id, std::make_shared(ext)); -} - -static name * g_inc_instr = nullptr; -static expr * g_dec_instr = nullptr; -static expr * g_apply_instr = nullptr; -static name * g_mk_closure_instr = nullptr; - -expr mk_inc_instr_expr(unsigned n) { - return mk_constant(name(*g_inc_instr, n)); -} - -expr mk_dec_instr_expr() { - return *g_dec_instr; -} - -expr mk_apply_instr_expr() { - return *g_apply_instr; -} - -expr mk_mk_closure_instr_expr(unsigned arity) { - return mk_constant(name(*g_mk_closure_instr, arity)); -} - -class to_ir_fn { - enum var_kind { BObject, Object, Scalar }; - typedef std::unordered_map var_kinds; - environment m_env; - ir_ext m_ext; - name_generator m_ngen; - local_ctx m_lctx; - buffer m_fvars; - buffer m_new_decls; - name m_base_name; - name m_x; - name m_j; - unsigned m_next_idx{1}; - unsigned m_next_jp_idx{1}; - expr_map m_live_obj_vars; - var_kinds m_var_kinds; - - - environment const & env() const { return m_env; } - - name_generator & ngen() { return m_ngen; } - - name next_name() { - name r = m_x.append_after(m_next_idx); - m_next_idx++; - return r; - } - - name next_jp_name() { - name r = m_j.append_after(m_next_jp_idx); - m_next_jp_idx++; - return mk_join_point_name(r); - } - - expr mk_void_type() { - /* TODO(Leo): add void type? */ - return mk_enf_neutral(); - } - - expr mk_dec(expr const & fvar) { - return mk_app(mk_dec_instr_expr(), fvar); - } - - unsigned get_arity(name const & n) const { - /* First, try to infer arity from `_cstage2` auxiliary definition. */ - name c = mk_cstage2_name(n); - optional info = env().find(c); - if (info && info->is_definition()) { - unsigned arity = 0; - expr v = info->get_value(); - while (is_lambda(v)) { - v = binding_body(v); - arity++; - } - return arity; - } - - /* If `_cstage2` declaration is not available, then use the type. - - Remark: we will probably have to add support for some builtin primitives in - the future. */ - unsigned arity = 0; - expr t = env().get(n).get_type(); - while (is_pi(t)) { - t = binding_body(t); - arity++; - } - return arity; - } - - void register_var_kind(expr const & fvar) { - lean_assert(is_fvar(fvar)); - local_decl d = m_lctx.get_local_decl(fvar); - if (is_join_point_name(d.get_user_name())) return; - if (d.get_type() == mk_enf_object_type()) { - /* TODO(Leo): add support for borrowed variables */ - m_var_kinds.insert(mk_pair(fvar_name(fvar), Object)); - } else { - m_var_kinds.insert(mk_pair(fvar_name(fvar), Scalar)); - } - } - - void collect_live_obj_vars(expr const & e, name_set & S) { - name_set visited_jps; - if (!has_fvar(e)) return; - for_each(e, [&](expr const & x, unsigned) { - if (!has_fvar(x)) return false; - if (is_fvar(x)) { - local_decl d = m_lctx.get_local_decl(x); - if (is_join_point_name(d.get_user_name())) { - if (visited_jps.contains(fvar_name(x))) return false; - visited_jps.insert(fvar_name(x)); - name_set jp_vars = get_live_obj_vars(*d.get_value()); - S.merge(jp_vars); - } else { - S.insert(fvar_name(x)); - } - } - return true; - }); - } - - name_set get_live_obj_vars(expr const & e) { - auto it = m_live_obj_vars.find(e); - if (it != m_live_obj_vars.end()) - return it->second; - name_set S; - collect_live_obj_vars(e, S); - m_live_obj_vars.insert(mk_pair(e, S)); - return S; - } - - bool is_dead_obj_var(expr const & e, name_set & live_obj_vars) { - if (!is_fvar(e)) return false; - if (live_obj_vars.contains(fvar_name(e))) return false; - auto it = m_var_kinds.find(fvar_name(e)); - return it != m_var_kinds.end() && it->second == Object; - } - - void insert_live_obj_var(expr const & e, name_set & live_obj_vars) { - if (is_fvar(e)) { - auto it = m_var_kinds.find(fvar_name(e)); - if (it != m_var_kinds.end() && it->second != Scalar) - live_obj_vars.insert(fvar_name(e)); - } - } - - expr process_cases(expr const & e, name_set & live_obj_vars) { - buffer args; - expr const & fn = get_app_args(e, args); - lean_assert(is_constant(fn)); - lean_assert(args.size() >= 3); - insert_live_obj_var(args[0], live_obj_vars); - // TODO(Leo): - return mk_app(fn, args); - } - - expr process(expr const & e, name_set & live_obj_vars) { - if (is_cases_on_app(env(), e)) { - return process_cases(e, live_obj_vars); - } - // TODO(Leo) - return e; - } - - expr mk_let(buffer const & input_vars, unsigned saved_fvars_size, expr r) { - name_set live_obj_vars; - r = process(r, live_obj_vars); - /* `entries` contains pairs (let-decl fvar, new value) for building the resultant let-declaration. - We simplify the value of some let-declarations in this method, but we don't want to create - a new temporary declaration just for this. */ - buffer entries; - while (m_fvars.size() > saved_fvars_size) { - expr x = m_fvars.back(); - m_fvars.pop_back(); - local_decl x_decl = m_lctx.get_local_decl(x); - expr val = *x_decl.get_value(); - if (!is_join_point_name(x_decl.get_user_name())) { - /* If `x` is a dead object variable, we don't even process it */ - if (!is_dead_obj_var(x, live_obj_vars)) { - val = process(val, live_obj_vars); - live_obj_vars.erase(fvar_name(x)); - entries.emplace_back(x, val); - } - } else { - entries.emplace_back(x, val); - } - } - /* We need to add a `dec` instruction for each input variable that is dead at the beginning - of the let-block, and has kind `Object`. */ - for (expr const & input_var : input_vars) { - if (is_dead_obj_var(input_var, live_obj_vars)) { - expr val = mk_dec(input_var); - expr aux_fvar = m_lctx.mk_local_decl(ngen(), next_name(), mk_void_type(), val); - entries.emplace_back(aux_fvar, val); - } - } - buffer user_names; - buffer fvars; - buffer vals; - buffer types; - unsigned i = entries.size(); - while (i > 0) { - --i; - expr const & fvar = entries[i].first; - fvars.push_back(fvar); - vals.push_back(entries[i].second); - local_decl fvar_decl = m_lctx.get_local_decl(fvar); - user_names.push_back(fvar_decl.get_user_name()); - types.push_back(fvar_decl.get_type()); - } - r = abstract(r, fvars.size(), fvars.data()); - i = fvars.size(); - while (i > 0) { - --i; - expr new_value = abstract(vals[i], i, fvars.data()); - expr new_type = types[i]; - r = ::lean::mk_let(user_names[i], new_type, new_value, r); - } - return r; - } - - expr visit_lambda(expr e) { - buffer binding_fvars; - while (is_lambda(e)) { - lean_assert(!has_loose_bvars(binding_domain(e))); - expr new_fvar = m_lctx.mk_local_decl(ngen(), binding_name(e), binding_domain(e), binding_info(e)); - register_var_kind(new_fvar); - binding_fvars.push_back(new_fvar); - e = binding_body(e); - } - e = instantiate_rev(e, binding_fvars.size(), binding_fvars.data()); - unsigned saved_fvars_size = m_fvars.size(); - e = visit(e); - e = mk_let(binding_fvars, saved_fvars_size, e); - e = m_lctx.mk_lambda(binding_fvars, e); - return e; - } - - expr visit_let(expr e) { - buffer fvars; - while (is_let(e)) { - lean_assert(!has_loose_bvars(let_type(e))); - expr val = instantiate_rev(let_value(e), fvars.size(), fvars.data()); - name n = let_name(e); - if (is_internal_name(n)) { - if (is_join_point_name(n)) - n = next_jp_name(); - else - n = next_name(); - } - if (is_join_point_name(n)) { - val = visit(val); - } - expr new_fvar = m_lctx.mk_local_decl(ngen(), n, let_type(e), val); - register_var_kind(new_fvar); - fvars.push_back(new_fvar); - m_fvars.push_back(new_fvar); - e = let_body(e); - } - return visit(instantiate_rev(e, fvars.size(), fvars.data())); - } - - expr visit(expr const & e) { - switch (e.kind()) { - case expr_kind::Lambda: return visit_lambda(e); - case expr_kind::Let: return visit_let(e); - default: return e; - } - } - -public: - to_ir_fn(environment const & env): - m_env(env), m_ext(get_extension(env)), m_x("_x"), m_j("_j") { - } - - pair operator()(comp_decl const & d) { - expr v = d.snd(); - m_base_name = d.fst(); - expr new_v = visit(v); - buffer input; - new_v = mk_let(input, 0, new_v); - comp_decl new_d(d.fst(), new_v); - environment new_env = update(env(), m_ext); - return mk_pair(new_env, comp_decls(new_d, comp_decls(m_new_decls))); - } -}; - -static pair to_ir_core(environment const & env, comp_decl const & d) { - return to_ir_fn(env)(d); -} - -pair to_ir(environment env, comp_decls const & ds) { - comp_decls r; - for (comp_decl const & d : ds) { - comp_decls new_ds; - std::tie(env, new_ds) = to_ir_core(env, d); - r = append(r, new_ds); - } - return mk_pair(env, r); -} - -void initialize_ir() { - g_ext = new ir_ext_reg(); - g_inc_instr = new name("_inc"); - g_dec_instr = new expr(mk_constant("_dec")); - g_apply_instr = new expr(mk_constant("_apply")); - g_mk_closure_instr = new name("_mk_closure"); -} - -void finalize_ir() { - delete g_ext; - delete g_inc_instr; - delete g_dec_instr; - delete g_apply_instr; - delete g_mk_closure_instr; -} -} diff --git a/src/library/compiler/ir.h b/src/library/compiler/ir.h deleted file mode 100644 index 175a997a7b..0000000000 --- a/src/library/compiler/ir.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2018 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/util.h" - -namespace lean { -pair to_ir(environment env, comp_decls const & ds); -void initialize_ir(); -void finalize_ir(); -}