chore(library/compiler): delete compiler/builtin module

It has been replaced with `compiler/extern_attribute`

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)

src/library/compiler/builtin.cpp

@@ -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 <unordered_map>
-#include <string>
-#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<bool>            m_borrowed_args;
-
-    native_decl() {}
-    native_decl(expr const & ll_type, unsigned arity, std::string cname, bool bres, list<bool> 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> 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<native_decls_ext> decl_reg = std::make_shared<native_decls_ext>();
-        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<native_decls_ext>(ext));
-}
-
-
-void register_builtin(name const & n, expr const & ll_type, unsigned arity, char const * cname,
-                      bool borrowed_res, list<bool> 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<bool> 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<bool> 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<bool> 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<native_decls_ext const & >(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<bool> 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<void(name const & n)> 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<name> get_native_constant_cname(environment const & env, name const & c) {
-    auto d =  get_native_constant_core(env, c);
-    if (d == nullptr)
-        return optional<name>();
-    return optional<name>(d->m_cname);
-}
-
-bool is_native_constant(environment const & env, name const & c) {
-    return get_native_constant_core(env, c) != nullptr;
-}
-
-optional<expr> 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<unsigned> get_native_constant_arity(environment const & env, name const & c) {
-    auto d = get_native_constant_core(env, c);
-    if (d == nullptr)
-        return optional<unsigned>();
-    return optional<unsigned>(d->m_arity);
-}
-
-bool get_native_borrowed_info(environment const & env, name const & c, buffer<bool> &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;
-}
-}

src/library/compiler/builtin.h

@@ -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 <string>
-#include "kernel/expr.h"
-namespace lean {
-bool is_native_constant(environment const & env, name const & c);
-bool is_builtin_constant(name const & c);
-optional<name> get_native_constant_cname(environment const & env, name const & c);
-optional<expr> get_native_constant_ll_type(environment const & env, name const & c);
-optional<unsigned> 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<bool> & 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<bool> const & bargs, list<bool> const & used_args);
-void for_each_native_constant(environment const & env, std::function<void(name const & n)> const & f);
-
-void initialize_builtin();
-void finalize_builtin();
-}

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<unsigned> get_given_arity(environment const & env, name const & c) {
@@ -211,8 +192,7 @@ optional<unsigned> get_extern_constant_arity(environment const & env, name const
         /* Infer arity from type */
         return optional<unsigned>(get_arity(env.get(c).get_type()));
     }
-    // TODO(Leo): replace with return optional<unsigned>
-    return get_native_constant_arity(env, c);
+    return optional<unsigned>();
 }
 
 bool get_extern_borrowed_info(environment const & env, name const & c, buffer<bool> & borrowed_args, bool & borrowed_res) {
@@ -239,8 +219,7 @@ bool get_extern_borrowed_info(environment const & env, name const & c, buffer<bo
         borrowed_res = is_borrowed(type);
         return true;
     }
-    // TODO(Leo): replace with return false
-    return get_native_borrowed_info(env, c, borrowed_args, borrowed_res);
+    return false;
 }
 
 optional<expr> get_extern_constant_ll_type(environment const & env, name const & c) {
@@ -284,8 +263,7 @@ optional<expr> 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() {

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();

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"