refactor(library/init/lean): move extern.lean to compiler subdirectory

library/init/lean/compiler/default.lean

@@ -7,4 +7,5 @@ prelude
 import init.lean.compiler.inline
 import init.lean.compiler.constfolding
 import init.lean.compiler.closedtermcache
+import init.lean.compiler.externattr
 import init.lean.compiler.ir

library/init/lean/compiler/ir/basic.lean

@@ -5,8 +5,10 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.data.array
-import init.lean.name init.lean.extern
-import init.lean.kvmap init.lean.format
+import init.lean.name
+import init.lean.kvmap
+import init.lean.format
+import init.lean.compiler.externattr
 /-
 Implements (extended) λPure and λRc proposed in the article
 "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura.

library/init/lean/compiler/ir/boxing.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.control.estate
 import init.control.reader
-import init.lean.extern
+import init.lean.compiler.externattr
 import init.lean.compiler.ir.basic
 import init.lean.compiler.ir.compilerm
 import init.lean.compiler.ir.freevars

library/init/lean/default.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.lean.compiler
-import init.lean.extern
 import init.lean.environment
 import init.lean.modifiers
 import init.lean.runtime

src/shell/lean.cpp

@@ -449,7 +449,8 @@ int main(int argc, char ** argv) {
     scope_trace_env scope_trace(env, opts, trace_ctx);
     name main_module_name;
 
-    std::string mod_fn, contents;
+    std::string mod_fn = "<unknown>";
+    std::string contents;
     if (use_stdin) {
         if (argc - optind != 0) {
             std::cerr << "Expected exactly one of file name or --stdin\n";
@@ -578,7 +579,7 @@ int main(int argc, char ** argv) {
 
         return ok ? 0 : 1;
     } catch (lean::throwable & ex) {
-        std::cerr << lean::message_builder(env, ios, "<unknown>", lean::pos_info(1, 1), lean::ERROR).set_exception(
+        std::cerr << lean::message_builder(env, ios, mod_fn, lean::pos_info(1, 1), lean::ERROR).set_exception(
                 ex).build();
     } catch (std::bad_alloc & ex) {
         std::cerr << "out of memory" << std::endl;

src/stage0/CMakeLists.txt

@@ -1 +1 @@
-add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inline.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/evalconst.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
+add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inline.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/evalconst.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)

src/stage0/init/lean/compiler/default.cpp

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.compiler.default
-// Imports: init.lean.compiler.inline init.lean.compiler.constfolding init.lean.compiler.closedtermcache init.lean.compiler.ir.default
+// Imports: init.lean.compiler.inline init.lean.compiler.constfolding init.lean.compiler.closedtermcache init.lean.compiler.externattr init.lean.compiler.ir.default
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -17,6 +17,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 obj* initialize_init_lean_compiler_inline(obj*);
 obj* initialize_init_lean_compiler_constfolding(obj*);
 obj* initialize_init_lean_compiler_closedtermcache(obj*);
+obj* initialize_init_lean_compiler_externattr(obj*);
 obj* initialize_init_lean_compiler_ir_default(obj*);
 static bool _G_initialized = false;
 obj* initialize_init_lean_compiler_default(obj* w) {
@@ -29,6 +30,8 @@ w = initialize_init_lean_compiler_constfolding(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_closedtermcache(w);
 if (io_result_is_error(w)) return w;
+w = initialize_init_lean_compiler_externattr(w);
+if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_ir_default(w);
 if (io_result_is_error(w)) return w;
 return w;

src/stage0/init/lean/compiler/externattr.cpp

@@ -1,5 +1,5 @@
 // Lean compiler output
-// Module: init.lean.extern
+// Module: init.lean.compiler.externattr
 // Imports: init.lean.expr init.data.option.basic init.lean.environment
 #include "runtime/object.h"
 #include "runtime/apply.h"
@@ -45,6 +45,7 @@ obj* mk_extern_call_core(obj*, obj*, obj*);
 }
 obj* l_String_Iterator_remainingBytes___main(obj*);
 obj* l_Lean_isExtern___boxed(obj*, obj*);
+obj* l___private_init_lean_compiler_externattr_1__parseOptNum(obj*, obj*, obj*);
 obj* l_List_foldl___main___at_Lean_mkSimpleFnCall___spec__1(obj*, obj*);
 namespace lean {
 obj* string_push(obj*, uint32);
@@ -78,11 +79,10 @@ uint8 l_UInt32_decEq(uint32, uint32);
 namespace lean {
 obj* mk_inline_ext_entry_core(obj*, obj*);
 }
-obj* l___private_init_lean_extern_1__parseOptNum(obj*, obj*, obj*);
 obj* l_Lean_getExternAttrData___boxed(obj*, obj*);
 obj* l_Lean_getExternEntryForAux(obj*, obj*);
+obj* l___private_init_lean_compiler_externattr_1__parseOptNum___main(obj*, obj*, obj*);
 obj* l_Lean_getExternEntryForAux___main___boxed(obj*, obj*);
-obj* l___private_init_lean_extern_1__parseOptNum___main(obj*, obj*, obj*);
 uint8 l_String_Iterator_hasNext___main(obj*);
 obj* l_Lean_getExternEntryForAux___main(obj*, obj*);
 namespace lean {
@@ -163,7 +163,7 @@ return x_3;
 }
 }
 }
-obj* l___private_init_lean_extern_1__parseOptNum___main(obj* x_1, obj* x_2, obj* x_3) {
+obj* l___private_init_lean_compiler_externattr_1__parseOptNum___main(obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; uint8 x_5; 
@@ -247,11 +247,11 @@ return x_25;
 }
 }
 }
-obj* l___private_init_lean_extern_1__parseOptNum(obj* x_1, obj* x_2, obj* x_3) {
+obj* l___private_init_lean_compiler_externattr_1__parseOptNum(obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; 
-x_4 = l___private_init_lean_extern_1__parseOptNum___main(x_1, x_2, x_3);
+x_4 = l___private_init_lean_compiler_externattr_1__parseOptNum___main(x_1, x_2, x_3);
 return x_4;
 }
 }
@@ -295,7 +295,7 @@ else
 obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; 
 x_16 = l_String_Iterator_next___main(x_3);
 x_17 = l_String_Iterator_remainingBytes___main(x_16);
-x_18 = l___private_init_lean_extern_1__parseOptNum___main(x_17, x_16, x_5);
+x_18 = l___private_init_lean_compiler_externattr_1__parseOptNum___main(x_17, x_16, x_5);
 x_19 = lean::cnstr_get(x_18, 0);
 lean::inc(x_19);
 x_20 = lean::cnstr_get(x_18, 1);
@@ -874,7 +874,7 @@ obj* initialize_init_lean_expr(obj*);
 obj* initialize_init_data_option_basic(obj*);
 obj* initialize_init_lean_environment(obj*);
 static bool _G_initialized = false;
-obj* initialize_init_lean_extern(obj* w) {
+obj* initialize_init_lean_compiler_externattr(obj* w) {
 if (_G_initialized) return w;
 _G_initialized = true;
 if (io_result_is_error(w)) return w;

src/stage0/init/lean/compiler/ir/basic.cpp

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.compiler.ir.basic
-// Imports: init.data.array.default init.lean.name init.lean.extern init.lean.kvmap init.lean.format
+// Imports: init.data.array.default init.lean.name init.lean.kvmap init.lean.format init.lean.compiler.externattr
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -11061,9 +11061,9 @@ return x_12;
 }
 obj* initialize_init_data_array_default(obj*);
 obj* initialize_init_lean_name(obj*);
-obj* initialize_init_lean_extern(obj*);
 obj* initialize_init_lean_kvmap(obj*);
 obj* initialize_init_lean_format(obj*);
+obj* initialize_init_lean_compiler_externattr(obj*);
 static bool _G_initialized = false;
 obj* initialize_init_lean_compiler_ir_basic(obj* w) {
 if (_G_initialized) return w;
@@ -11073,12 +11073,12 @@ w = initialize_init_data_array_default(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_name(w);
 if (io_result_is_error(w)) return w;
-w = initialize_init_lean_extern(w);
-if (io_result_is_error(w)) return w;
 w = initialize_init_lean_kvmap(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_format(w);
 if (io_result_is_error(w)) return w;
+w = initialize_init_lean_compiler_externattr(w);
+if (io_result_is_error(w)) return w;
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "IR"), "Index"), "lt"), 2, l_Lean_IR_Index_lt___boxed);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "IR"), "VarId"), "HasBeq"), 2, l_Lean_IR_VarId_HasBeq___boxed);
 l_Lean_IR_VarId_HasToString___closed__1 = _init_l_Lean_IR_VarId_HasToString___closed__1();

src/stage0/init/lean/compiler/ir/boxing.cpp

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.compiler.ir.boxing
-// Imports: init.control.estate init.control.reader init.lean.extern init.lean.compiler.ir.basic init.lean.compiler.ir.compilerm init.lean.compiler.ir.freevars
+// Imports: init.control.estate init.control.reader init.lean.compiler.externattr init.lean.compiler.ir.basic init.lean.compiler.ir.compilerm init.lean.compiler.ir.freevars
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -6334,7 +6334,7 @@ return x_4;
 }
 obj* initialize_init_control_estate(obj*);
 obj* initialize_init_control_reader(obj*);
-obj* initialize_init_lean_extern(obj*);
+obj* initialize_init_lean_compiler_externattr(obj*);
 obj* initialize_init_lean_compiler_ir_basic(obj*);
 obj* initialize_init_lean_compiler_ir_compilerm(obj*);
 obj* initialize_init_lean_compiler_ir_freevars(obj*);
@@ -6347,7 +6347,7 @@ w = initialize_init_control_estate(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_control_reader(w);
 if (io_result_is_error(w)) return w;
-w = initialize_init_lean_extern(w);
+w = initialize_init_lean_compiler_externattr(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_ir_basic(w);
 if (io_result_is_error(w)) return w;

src/stage0/init/lean/default.cpp

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.default
-// Imports: init.lean.compiler.default init.lean.extern init.lean.environment init.lean.modifiers init.lean.runtime init.lean.attributes init.lean.evalconst init.lean.parser.default init.lean.reducibilityattrs init.lean.elaborator.default
+// Imports: init.lean.compiler.default init.lean.environment init.lean.modifiers init.lean.runtime init.lean.attributes init.lean.evalconst init.lean.parser.default init.lean.reducibilityattrs init.lean.elaborator.default
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -15,7 +15,6 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
 obj* initialize_init_lean_compiler_default(obj*);
-obj* initialize_init_lean_extern(obj*);
 obj* initialize_init_lean_environment(obj*);
 obj* initialize_init_lean_modifiers(obj*);
 obj* initialize_init_lean_runtime(obj*);
@@ -31,8 +30,6 @@ _G_initialized = true;
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_default(w);
 if (io_result_is_error(w)) return w;
-w = initialize_init_lean_extern(w);
-if (io_result_is_error(w)) return w;
 w = initialize_init_lean_environment(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_modifiers(w);