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

@@ -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)

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<pair<environment, comp_decl>> 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() {

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

src/library/compiler/llnf_code.cpp

@@ -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<llnf_code_ext const &>(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;
-}
-}

src/library/compiler/llnf_code.h

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