From 3ffe0e22c8a5448cfc3187e6eb07bfffc7827004 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 May 2019 10:18:31 -0700 Subject: [PATCH] feat(shel/lean): add temporary option for testing new IR compiler code emitter --- library/init/lean/compiler/ir/default.lean | 1 + library/init/lean/compiler/ir/emitcpp.lean | 9 ++-- src/library/compiler/ir.cpp | 18 +++++++ src/library/compiler/ir.h | 1 + src/shell/lean.cpp | 20 ++++++- src/stage0/init/lean/compiler/ir/emitcpp.cpp | 57 ++++++++++---------- 6 files changed, 71 insertions(+), 35 deletions(-) diff --git a/library/init/lean/compiler/ir/default.lean b/library/init/lean/compiler/ir/default.lean index 27366ea756..76b28f58ed 100644 --- a/library/init/lean/compiler/ir/default.lean +++ b/library/init/lean/compiler/ir/default.lean @@ -16,6 +16,7 @@ import init.lean.compiler.ir.checker import init.lean.compiler.ir.borrow import init.lean.compiler.ir.boxing import init.lean.compiler.ir.rc +import init.lean.compiler.ir.emitcpp namespace Lean namespace IR diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean index 43e9847e34..6e155b3d56 100644 --- a/library/init/lean/compiler/ir/emitcpp.lean +++ b/library/init/lean/compiler/ir/emitcpp.lean @@ -19,7 +19,6 @@ structure Context := (env : Environment) (localCtx : LocalContext := {}) (modName : Name) -(modDeps : Array Name) (mainFn : FunId := default _) (mainParams : Array Param := Array.empty) @@ -57,11 +56,11 @@ match d with modName ← getModName, emitLn ("w = initialize_" ++ (modName.mangle "") ++ "(w);"), emitLn "lean::io_mark_end_initialization();", - emitLn "if (io_result_is_ok(w)) {\n", + emitLn "if (io_result_is_ok(w)) {", emitLn "lean::scoped_task_manager tmanager(lean::hardware_concurrency());", if xs.size == 2 then do { emitLn "obj* in = lean::box(0);", - emitLn "int i = argc;\n", + emitLn "int i = argc;", emitLn "while (i > 1) {", emitLn " i--;", emitLn " obj* n = lean::alloc_cnstr(1,2,0); lean::cnstr_set(n, 0, lean::mk_string(argv[i])); lean::cnstr_set(n, 1, in);", @@ -93,8 +92,8 @@ do env ← getEnv, end EmitCpp @[export lean.ir.emit_cpp_core] -def emitCpp (env : Environment) (modName : Name) (modDeps : Array Name) : Except String String := -match (EmitCpp.main { env := env, modName := modName, modDeps := modDeps }).run "" with +def emitCpp (env : Environment) (modName : Name) : Except String String := +match (EmitCpp.main { env := env, modName := modName }).run "" with | EState.Result.ok _ s := Except.ok s | EState.Result.error err _ := Except.error err diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp index 7996c4ae2e..1d680c956b 100644 --- a/src/library/compiler/ir.cpp +++ b/src/library/compiler/ir.cpp @@ -526,5 +526,23 @@ environment compile(environment const & env, options const & opts, comp_decls co environment add_extern(environment const & env, name const & fn) { return ir::add_decl(env, to_ir_fn(env)(fn)); } + +/* +@[export lean.ir.emit_cpp_core] +def emitCpp (env : Environment) (modName : Name) : Except String String : +*/ +object * emit_cpp_core(object * env, object * mod_name); + +string_ref emit_cpp(environment const & env, name const & mod_name) { + object * r = emit_cpp_core(env.to_obj_arg(), mod_name.to_obj_arg()); + string_ref s(cnstr_get(r, 0), true); + if (cnstr_tag(r) == 0) { + dec_ref(r); + throw exception(s.to_std_string()); + } else { + dec_ref(r); + return s; + } +} } } diff --git a/src/library/compiler/ir.h b/src/library/compiler/ir.h index 03efd71f0d..adc5252f53 100644 --- a/src/library/compiler/ir.h +++ b/src/library/compiler/ir.h @@ -15,5 +15,6 @@ std::string decl_to_string(decl const & d); void test(decl const & d); environment compile(environment const & env, options const & opts, comp_decls const & decls); environment add_extern(environment const & env, name const & fn); +string_ref emit_cpp(environment const & env, name const & mod_name); } } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 01312fa34a..15e8becc36 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -35,6 +35,7 @@ Author: Leonardo de Moura #include "library/time_task.h" #include "library/private.h" #include "library/compiler/emit_cpp.h" +#include "library/compiler/ir.h" #include "frontends/lean/parser.h" #include "frontends/lean/pp.h" #include "frontends/lean/json.h" @@ -225,6 +226,7 @@ static struct option g_long_options[] = { {"deps", no_argument, 0, 'd'}, {"timeout", optional_argument, 0, 'T'}, {"cpp", optional_argument, 0, 'c'}, + {"newcpp", optional_argument, 0, 'C'}, // temporary flag for testing new IR #if defined(LEAN_JSON) {"json", no_argument, 0, 'J'}, {"path", no_argument, 0, 'p'}, @@ -241,7 +243,7 @@ static struct option g_long_options[] = { }; static char const * g_opt_str = - "PdD:c:qpgvht:012j:012rM:012T:012a" + "PdD:c:C:qpgvht:012j:012rM:012T:012a" #if defined(LEAN_MULTI_THREAD) "s:012" #endif @@ -333,6 +335,7 @@ int main(int argc, char ** argv) { optional server_in; std::string native_output; optional cpp_output; + optional new_cpp_output; while (true) { int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL); if (c == -1) @@ -353,6 +356,9 @@ int main(int argc, char ** argv) { case 'c': cpp_output = optarg; break; + case 'C': + new_cpp_output = optarg; + break; case 's': lean::lthread::set_thread_stack_size( static_cast((atoi(optarg) / 4) * 4) * static_cast(1024)); @@ -572,6 +578,18 @@ int main(int argc, char ** argv) { auto mod = module_name_of_file(path.get_path(), mod_fn); emit_cpp(out, env, mod, to_list(imports.begin(), imports.end())); } + + if (new_cpp_output && ok) { + std::ofstream out(*new_cpp_output); + if (out.fail()) { + std::cerr << "failed to create '" << *new_cpp_output << "'\n"; + return 1; + } + auto mod = module_name_of_file(path.get_path(), mod_fn); + out << lean::ir::emit_cpp(env, mod).data(); + out.close(); + } + return ok ? 0 : 1; } catch (lean::throwable & ex) { std::cerr << lean::message_builder(env, ios, "", lean::pos_info(1, 1), lean::ERROR).set_exception( diff --git a/src/stage0/init/lean/compiler/ir/emitcpp.cpp b/src/stage0/init/lean/compiler/ir/emitcpp.cpp index 2c438ca6dd..1216b93c6c 100644 --- a/src/stage0/init/lean/compiler/ir/emitcpp.cpp +++ b/src/stage0/init/lean/compiler/ir/emitcpp.cpp @@ -78,7 +78,7 @@ obj* l_Lean_IR_EmitCpp_emitMainFn___closed__25; obj* l_Lean_IR_EmitCpp_emitMainFn___closed__10; namespace lean { namespace ir { -obj* emit_cpp_core(obj*, obj*, obj*); +obj* emit_cpp_core(obj*, obj*); }} obj* l_Lean_IR_EmitCpp_emitMainFn___closed__9; extern obj* l_IO_println___rarg___closed__1; @@ -1215,41 +1215,40 @@ return x_2; } namespace lean { namespace ir { -obj* emit_cpp_core(obj* x_0, obj* x_1, obj* x_2) { +obj* emit_cpp_core(obj* x_0, obj* x_1) { _start: { -obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; +obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; +x_2 = lean::box(0); x_3 = lean::box(0); -x_4 = lean::box(0); -x_5 = l_Array_empty___closed__1; -x_6 = lean::alloc_cnstr(0, 6, 0); -lean::cnstr_set(x_6, 0, x_0); -lean::cnstr_set(x_6, 1, x_3); -lean::cnstr_set(x_6, 2, x_1); -lean::cnstr_set(x_6, 3, x_2); -lean::cnstr_set(x_6, 4, x_4); -lean::cnstr_set(x_6, 5, x_5); -x_7 = l_Lean_IR_emitCpp___closed__1; -x_8 = l_Lean_IR_EmitCpp_main(x_6, x_7); -if (lean::obj_tag(x_8) == 0) +x_4 = l_Array_empty___closed__1; +x_5 = lean::alloc_cnstr(0, 5, 0); +lean::cnstr_set(x_5, 0, x_0); +lean::cnstr_set(x_5, 1, x_2); +lean::cnstr_set(x_5, 2, x_1); +lean::cnstr_set(x_5, 3, x_3); +lean::cnstr_set(x_5, 4, x_4); +x_6 = l_Lean_IR_emitCpp___closed__1; +x_7 = l_Lean_IR_EmitCpp_main(x_5, x_6); +if (lean::obj_tag(x_7) == 0) { -obj* x_9; obj* x_12; -x_9 = lean::cnstr_get(x_8, 1); -lean::inc(x_9); -lean::dec(x_8); -x_12 = lean::alloc_cnstr(1, 1, 0); -lean::cnstr_set(x_12, 0, x_9); -return x_12; +obj* x_8; obj* x_11; +x_8 = lean::cnstr_get(x_7, 1); +lean::inc(x_8); +lean::dec(x_7); +x_11 = lean::alloc_cnstr(1, 1, 0); +lean::cnstr_set(x_11, 0, x_8); +return x_11; } else { -obj* x_13; obj* x_16; -x_13 = lean::cnstr_get(x_8, 0); -lean::inc(x_13); -lean::dec(x_8); -x_16 = lean::alloc_cnstr(0, 1, 0); -lean::cnstr_set(x_16, 0, x_13); -return x_16; +obj* x_12; obj* x_15; +x_12 = lean::cnstr_get(x_7, 0); +lean::inc(x_12); +lean::dec(x_7); +x_15 = lean::alloc_cnstr(0, 1, 0); +lean::cnstr_set(x_15, 0, x_12); +return x_15; } } }