diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt index 96f0727229..301b232681 100644 --- a/src/library/compiler/CMakeLists.txt +++ b/src/library/compiler/CMakeLists.txt @@ -2,6 +2,6 @@ add_library(compiler OBJECT emit_bytecode.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 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 name_mangling.cpp + reduce_arity.cpp closed_term_cache.cpp name_mangling.cpp emit_cpp.cpp export_attribute.cpp llnf_code.cpp extern_attribute.cpp borrowed_annotation.cpp) diff --git a/src/library/compiler/builtin.cpp b/src/library/compiler/builtin.cpp deleted file mode 100644 index c61af8f24f..0000000000 --- a/src/library/compiler/builtin.cpp +++ /dev/null @@ -1,156 +0,0 @@ -/* -Copyright (c) 2018 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Authors: Leonardo de Moura, Max Wagner - -REMARK: ******* THIS FILE WILL BE DELETED ********* - It is being replaced with extern_attribute.cpp -*/ -#include -#include -#include "util/list.h" -#include "kernel/expr.h" -#include "library/compiler/util.h" - -namespace lean { - -struct native_decl { - expr m_ll_type; - unsigned m_arity; - std::string m_cname; - bool m_borrowed_res; - list m_borrowed_args; - - native_decl() {} - native_decl(expr const & ll_type, unsigned arity, std::string cname, bool bres, list const & bargs): - m_ll_type(ll_type), m_arity(arity), m_cname(cname), m_borrowed_res(bres), m_borrowed_args(bargs) { - } -}; - -typedef name_map native_decl_map; -static native_decl_map * g_initial_native_decls; - -bool is_builtin_constant(name const & c) { - return g_initial_native_decls->contains(c); -} - -struct native_decls_ext : public environment_extension { - native_decl_map m_decls; - - native_decls_ext() { - g_initial_native_decls->for_each([&](name const & n, native_decl const & d) { - m_decls.insert(n, d); - }); - } -}; - -struct native_decls_reg { - unsigned m_ext_id; - native_decls_reg() { - std::shared_ptr decl_reg = std::make_shared(); - m_ext_id = environment::register_extension(decl_reg); - } -}; - -static native_decls_reg * g_ext = nullptr; - -static environment update(environment const & env, native_decls_ext const & ext) { - return env.update(g_ext->m_ext_id, std::make_shared(ext)); -} - - -void register_builtin(name const & n, expr const & ll_type, unsigned arity, char const * cname, - bool borrowed_res, list const & borrowed_arg) { - lean_assert(g_initial_native_decls->find(n) == nullptr); - g_initial_native_decls->insert(n, native_decl(ll_type, arity, cname, borrowed_res, borrowed_arg)); -} - -void register_builtin(name const & n, expr const & ll_type, char const * cname, - bool borrowed_res, list const & borrowed_arg) { - unsigned arity = get_arity(ll_type); - return register_builtin(n, ll_type, arity, cname, borrowed_res, borrowed_arg); -} - -void register_builtin(name const & n, expr const & ll_type, char const * cname, list const & borrowed_arg) { - return register_builtin(n, ll_type, cname, false, borrowed_arg); -} - -void register_builtin(name const & n, expr const & ll_type, unsigned arity, char const * cname) { - buffer borrowed; - borrowed.resize(arity, false); - return register_builtin(n, ll_type, arity, cname, false, to_list(borrowed)); -} - -void register_builtin(name const & n, expr const & ll_type, char const * cname) { - unsigned arity = get_arity(ll_type); - return register_builtin(n, ll_type, arity, cname); -} - -static inline native_decls_ext const & get_ext(environment const & env) { - return static_cast(env.get_extension(g_ext->m_ext_id)); -} - -environment add_native_constant_decl(environment const & env, name const & n, expr const & ll_type, std::string cname, - bool bres, list const & bargs) { - native_decl d(ll_type, get_arity(ll_type), cname, bres, bargs); - native_decls_ext ext = get_ext(env); - ext.m_decls.insert(n, d); - return update(env, ext); -} - -void for_each_native_constant(environment const & env, std::function const & f) { - auto ext = get_ext(env); - ext.m_decls.for_each([&](name const & n, native_decl const &) { f(n); }); -} - -static inline native_decl const * get_native_constant_core(environment const & env, name const & n) { - auto ext = get_ext(env); - return ext.m_decls.find(n); -} - -optional get_native_constant_cname(environment const & env, name const & c) { - auto d = get_native_constant_core(env, c); - if (d == nullptr) - return optional(); - return optional(d->m_cname); -} - -bool is_native_constant(environment const & env, name const & c) { - return get_native_constant_core(env, c) != nullptr; -} - -optional get_native_constant_ll_type(environment const & env, name const & c) { - auto d = get_native_constant_core(env, c); - if (d == nullptr) - return none_expr(); - return some_expr(d->m_ll_type); -} - -optional get_native_constant_arity(environment const & env, name const & c) { - auto d = get_native_constant_core(env, c); - if (d == nullptr) - return optional(); - return optional(d->m_arity); -} - -bool get_native_borrowed_info(environment const & env, name const & c, buffer &borrowed_args, bool &borrowed_res) { - auto d = get_native_constant_core(env, c); - if (d == nullptr) - return false; - - to_buffer(d->m_borrowed_args, borrowed_args); - borrowed_res = d->m_borrowed_res; - return true; -} - -void initialize_builtin() { - g_initial_native_decls = new native_decl_map(); - g_ext = new native_decls_reg(); -} - -void finalize_builtin() { - delete g_ext; - delete g_initial_native_decls; -} -} diff --git a/src/library/compiler/builtin.h b/src/library/compiler/builtin.h deleted file mode 100644 index b77d547721..0000000000 --- a/src/library/compiler/builtin.h +++ /dev/null @@ -1,26 +0,0 @@ -/* -Copyright (c) 2018 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Authors: Leonardo de Moura, Max Wagner -*/ -#pragma once -#include -#include "kernel/expr.h" -namespace lean { -bool is_native_constant(environment const & env, name const & c); -bool is_builtin_constant(name const & c); -optional get_native_constant_cname(environment const & env, name const & c); -optional get_native_constant_ll_type(environment const & env, name const & c); -optional get_native_constant_arity(environment const & env, name const & c); -/* Return true if `c` is a native constant, and store in borrowed_args and - borrowed_res which arguments/results are marked as borrowed. */ -bool get_native_borrowed_info(environment const & env, name const & c, buffer & borrowed_args, bool & borrowed_res); - -environment add_native_constant_decl(environment const & env, name const & n, expr const & ll_type, std::string cname, - bool bres, list const & bargs, list const & used_args); -void for_each_native_constant(environment const & env, std::function const & f); - -void initialize_builtin(); -void finalize_builtin(); -} diff --git a/src/library/compiler/extern_attribute.cpp b/src/library/compiler/extern_attribute.cpp index de12aac558..a17aca9ea6 100644 --- a/src/library/compiler/extern_attribute.cpp +++ b/src/library/compiler/extern_attribute.cpp @@ -13,7 +13,6 @@ Authors: Leonardo de Moura #include "library/compiler/borrowed_annotation.h" #include "library/compiler/util.h" #include "library/compiler/extern_attribute.h" -#include "library/compiler/builtin.h" // TODO(Leo): delete void initialize_init_lean_extern(); @@ -164,20 +163,7 @@ bool emit_extern_call_core(std::ostream & out, environment const & env, name con } void emit_extern_call(std::ostream & out, environment const & env, name const & backend, name const & fn, string_refs const & attrs) { - if (emit_extern_call_core(out, env, backend, fn, attrs)) - return; - { // TODO(Leo): delete this blcok - name _fn = *get_native_constant_cname(env, fn); - out << _fn << "("; - bool first = true; - string_refs it = attrs; - while (!empty(it)) { - if (first) first = false; else out << ", "; - out << string_cstr(head(it).raw()); - it = tail(it); - } - out << ")"; - } + emit_extern_call_core(out, env, backend, fn, attrs); } static inline bool is_extern_constant_core(environment const & env, name const & c) { @@ -185,12 +171,7 @@ static inline bool is_extern_constant_core(environment const & env, name const & } bool is_extern_constant(environment const & env, name const & c) { - if (is_extern_constant_core(env, c)) - return true; - { // TODO(Leo): delete this block - return is_native_constant(env, c); - } - return false; + return is_extern_constant_core(env, c); } static optional get_given_arity(environment const & env, name const & c) { @@ -211,8 +192,7 @@ optional get_extern_constant_arity(environment const & env, name const /* Infer arity from type */ return optional(get_arity(env.get(c).get_type())); } - // TODO(Leo): replace with return optional - return get_native_constant_arity(env, c); + return optional(); } bool get_extern_borrowed_info(environment const & env, name const & c, buffer & borrowed_args, bool & borrowed_res) { @@ -239,8 +219,7 @@ bool get_extern_borrowed_info(environment const & env, name const & c, buffer get_extern_constant_ll_type(environment const & env, name const & c) { @@ -284,8 +263,7 @@ optional get_extern_constant_ll_type(environment const & env, name const & } return some_expr(ll_type); } - // TODO(Leo): replace with return none_expr() - return get_native_constant_ll_type(env, c); + return none_expr(); } void initialize_extern_attribute() { diff --git a/src/library/compiler/init_module.cpp b/src/library/compiler/init_module.cpp index d35fe70f4d..7e0fd7877a 100644 --- a/src/library/compiler/init_module.cpp +++ b/src/library/compiler/init_module.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "library/compiler/llnf.h" #include "library/compiler/closed_term_cache.h" #include "library/compiler/compiler.h" -#include "library/compiler/builtin.h" #include "library/compiler/export_attribute.h" #include "library/compiler/extern_attribute.h" #include "library/compiler/llnf_code.h" @@ -29,7 +28,6 @@ void initialize_compiler_module() { initialize_closed_term_cache(); initialize_llnf(); initialize_compiler(); - initialize_builtin(); initialize_export_attribute(); initialize_extern_attribute(); initialize_llnf_code(); @@ -43,7 +41,6 @@ void finalize_compiler_module() { finalize_llnf_code(); finalize_extern_attribute(); finalize_export_attribute(); - finalize_builtin(); finalize_compiler(); finalize_llnf(); finalize_closed_term_cache(); diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp index 26632879f3..3f0214e2a9 100644 --- a/src/library/compiler/llnf.cpp +++ b/src/library/compiler/llnf.cpp @@ -17,7 +17,6 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" #include "library/util.h" #include "library/trace.h" -#include "library/compiler/builtin.h" #include "library/compiler/util.h" #include "library/compiler/llnf.h" #include "library/compiler/ll_infer_type.h"