From 51a9208ea917ca2d59bfa8f0ec2e1ed7dd50ab9c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 May 2019 21:12:39 -0700 Subject: [PATCH] chore(library/compiler): remove environment extension: llnf_code We don't need it anymore. It was used by the old IR compiler --- src/library/compiler/CMakeLists.txt | 2 +- src/library/compiler/compiler.cpp | 18 ++-------- src/library/compiler/init_module.cpp | 3 -- src/library/compiler/llnf_code.cpp | 54 ---------------------------- src/library/compiler/llnf_code.h | 17 --------- 5 files changed, 3 insertions(+), 91 deletions(-) delete mode 100644 src/library/compiler/llnf_code.cpp delete mode 100644 src/library/compiler/llnf_code.h diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt index b8df5df2a8..0d2519f276 100644 --- a/src/library/compiler/CMakeLists.txt +++ b/src/library/compiler/CMakeLists.txt @@ -3,6 +3,6 @@ add_library(compiler OBJECT init_module.cpp ## New 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 name_mangling.cpp - export_attribute.cpp llnf_code.cpp extern_attribute.cpp + export_attribute.cpp extern_attribute.cpp borrowed_annotation.cpp init_attribute.cpp eager_lambda_lifting.cpp struct_cases_on.cpp find_jp.cpp ir.cpp implemented_by_attribute.cpp) diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index 0cf6070227..77ffac68d0 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -24,7 +24,6 @@ Author: Leonardo de Moura #include "library/compiler/ll_infer_type.h" #include "library/compiler/simp_app_args.h" #include "library/compiler/llnf.h" -#include "library/compiler/llnf_code.h" #include "library/compiler/export_attribute.h" #include "library/compiler/extern_attribute.h" #include "library/compiler/struct_cases_on.h" @@ -174,15 +173,7 @@ environment compile(environment const & env, options const & opts, names cs) { if (length(cs) == 1 && is_extern_constant(env, head(cs))) { /* Generate boxed version for extern/native constant if needed. */ - environment new_env = ir::add_extern(env, head(cs)); - unsigned arity = *get_extern_constant_arity(env, head(cs)); - if (optional> p = mk_boxed_version(new_env, head(cs), arity)) { - /* Remark: we don't need boxed version for the bytecode. */ - return save_llnf_code(p->first, comp_decls(p->second)); - } else { - /* We always generate boxed versions for extern. */ - lean_unreachable(); - } + return ir::add_extern(env, head(cs)); } for (name const & c : cs) { @@ -243,12 +234,7 @@ environment compile(environment const & env, options const & opts, names cs) { ds = apply(elim_dead_let, ds); trace_compiler(name({"compiler", "simp_app_args"}), ds); /* compile IR. */ - new_env = compile_ir(new_env, opts, ds); - // TODO(Leo): remove rest of the code - std::tie(new_env, ds) = to_llnf(new_env, ds); - new_env = save_llnf_code(new_env, ds); - trace_compiler(name({"compiler", "result"}), ds); - return new_env; + return compile_ir(new_env, opts, ds); } void initialize_compiler() { diff --git a/src/library/compiler/init_module.cpp b/src/library/compiler/init_module.cpp index 2f43610920..f22316fa9a 100644 --- a/src/library/compiler/init_module.cpp +++ b/src/library/compiler/init_module.cpp @@ -14,7 +14,6 @@ Author: Leonardo de Moura #include "library/compiler/export_attribute.h" #include "library/compiler/extern_attribute.h" #include "library/compiler/implemented_by_attribute.h" -#include "library/compiler/llnf_code.h" #include "library/compiler/borrowed_annotation.h" #include "library/compiler/ll_infer_type.h" #include "library/compiler/init_attribute.h" @@ -32,7 +31,6 @@ void initialize_compiler_module() { initialize_compiler(); initialize_export_attribute(); initialize_extern_attribute(); - initialize_llnf_code(); initialize_borrowed_annotation(); initialize_ll_infer_type(); } @@ -40,7 +38,6 @@ void initialize_compiler_module() { void finalize_compiler_module() { finalize_ll_infer_type(); finalize_borrowed_annotation(); - finalize_llnf_code(); finalize_extern_attribute(); finalize_export_attribute(); finalize_compiler(); diff --git a/src/library/compiler/llnf_code.cpp b/src/library/compiler/llnf_code.cpp deleted file mode 100644 index cfd0d51827..0000000000 --- a/src/library/compiler/llnf_code.cpp +++ /dev/null @@ -1,54 +0,0 @@ -/* -Copyright (c) 2019 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "runtime/sstream.h" -#include "library/compiler/util.h" -#include "library/compiler/init_attribute.h" - -namespace lean { -struct llnf_code_ext : public environment_extension { - comp_decls m_code; -}; - -struct llnf_code_ext_reg { - unsigned m_ext_id; - llnf_code_ext_reg() { m_ext_id = environment::register_extension(new llnf_code_ext()); } -}; - -static llnf_code_ext_reg * g_ext = nullptr; -static llnf_code_ext const & get_extension(environment const & env) { - return static_cast(env.get_extension(g_ext->m_ext_id)); -} -static environment update(environment const & env, llnf_code_ext const & ext) { - return env.update(g_ext->m_ext_id, new llnf_code_ext(ext)); -} - -environment save_llnf_code(environment const & env, comp_decls const & ds) { - llnf_code_ext ext = get_extension(env); - /* Check whether constants with `[init]` attribute have arity 0. - We cannot perform this check at registration time because attributes are set before - code generation. */ - for (comp_decl const & d : ds) { - if (has_init_attribute(env, d.fst()) && get_num_nested_lambdas(d.snd()) != 0) { - throw exception(sstream() << "invalid [init] attribute, '" << d.fst() << "' must not be a function"); - } - } - ext.m_code = append(ext.m_code, ds); - return update(env, ext); -} - -comp_decls get_llnf_code(environment const & env) { - return get_extension(env).m_code; -} - -void initialize_llnf_code() { - g_ext = new llnf_code_ext_reg(); -} - -void finalize_llnf_code() { - delete g_ext; -} -} diff --git a/src/library/compiler/llnf_code.h b/src/library/compiler/llnf_code.h deleted file mode 100644 index 6e7de321b1..0000000000 --- a/src/library/compiler/llnf_code.h +++ /dev/null @@ -1,17 +0,0 @@ -/* -Copyright (c) 2019 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 { -/* Store `ds` in the current module LLNF code sequence. */ -environment save_llnf_code(environment const & env, comp_decls const & ds); -/* Return the LLNF code for the current module. */ -comp_decls get_llnf_code(environment const & env); -void initialize_llnf_code(); -void finalize_llnf_code(); -}