From 9f2172e65efd3fa587e6bd10bb96f8251989a605 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 Jan 2020 13:59:00 -0800
Subject: [PATCH] feat: use new frontend when option `--new-frontend` is
 provided

---
 src/Init/Lean/Elab/Frontend.lean | 12 ++++++++++--
 src/shell/lean.cpp               | 15 ++++++++++-----
 2 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/src/Init/Lean/Elab/Frontend.lean b/src/Init/Lean/Elab/Frontend.lean
index b760921370..a0dc89cccd 100644
--- a/src/Init/Lean/Elab/Frontend.lean
+++ b/src/Init/Lean/Elab/Frontend.lean
@@ -91,8 +91,7 @@ IO.processCommands parserCtx parserStateRef cmdStateRef;
 cmdState ← cmdStateRef.get;
 pure (cmdState.env, cmdState.messages)
 
-def testFrontend (input : String) (opts : Options := {}) (fileName : Option String := none) : IO (Environment × MessageLog) := do
-env ← mkEmptyEnvironment;
+def runFrontend (env : Environment) (input : String) (opts : Options := {}) (fileName : Option String := none) : IO (Environment × MessageLog) := do
 let fileName := fileName.getD "<input>";
 let parserCtx := Parser.mkParserContextCore env input fileName;
 match Parser.parseHeader env parserCtx with
@@ -104,5 +103,14 @@ match Parser.parseHeader env parserCtx with
   cmdState ← cmdStateRef.get;
   pure (cmdState.env, cmdState.messages)
 
+@[export lean_run_frontend]
+def runFrontentExport (env : Environment) (input : String) (fileName : String) (opts : Options) : IO (Option Environment) := do
+(env, messages) ← runFrontend env input opts (some fileName);
+messages.forM $ fun msg => IO.println msg;
+if messages.hasErrors then
+  pure none
+else
+  pure (some env)
+
 end Elab
 end Lean
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 55df07277b..a4110e1683 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -343,21 +343,23 @@ bool test_module_parser(environment const & env, std::string const & input, std:
     return get_io_scalar_result<bool>(lean_test_module_parser(env.to_obj_arg(), mk_string(input), mk_string(filename), false, io_mk_world()));
 }
 
-extern "C" object* lean_init_search_path(object* opt_path, object* w);
+extern "C" object * lean_run_frontend(object * env, object * input, object * filename, object * opts, object * w);
+optional<environment> run_new_frontend(environment const & env, std::string const & input, std::string const & filename, options const & opts) {
+    return get_io_result<option_ref<environment>>(lean_run_frontend(env.to_obj_arg(), mk_string(input), mk_string(filename), opts.to_obj_arg(), io_mk_world())).get();
+}
 
+extern "C" object* lean_init_search_path(object* opt_path, object* w);
 void init_search_path() {
     get_io_scalar_result<unsigned>(lean_init_search_path(mk_option_none(), io_mk_world()));
 }
 
 extern "C" object* lean_module_name_of_file(object* fname, object* w);
-
 optional<name> module_name_of_file(std::string const & fname) {
     return get_io_result<option_ref<name>>(lean_module_name_of_file(mk_string(fname), io_mk_world())).get();
 }
 
 /* def parseImports (input : String) (fileName : Option String := none) : IO (Array Import × Position × MessageLog) */
 extern "C" object* lean_parse_imports(object* input, object* file_name, object* w);
-
 std::tuple<object_ref, position, message_log> parse_imports(std::string const & input, std::string const & fname) {
     auto r = get_io_result<object_ref>(lean_parse_imports(mk_string(input), mk_option_some(mk_string(fname)), io_mk_world()));
     return std::make_tuple(cnstr_get_ref(r, 0), cnstr_get_ref_t<position>(cnstr_get_ref(r, 1), 0),
@@ -365,7 +367,6 @@ std::tuple<object_ref, position, message_log> parse_imports(std::string const &
 }
 
 extern "C" object* lean_print_deps(object* deps, object* w);
-
 void print_deps(object_ref const & deps) {
     consume_io_result(lean_print_deps(deps.to_obj_arg(), io_mk_world()));
 }
@@ -580,7 +581,11 @@ int main(int argc, char ** argv) {
     try {
         bool ok = true;
         if (new_frontend) {
-            ok = lean::test_module_parser(env, contents, mod_fn);
+            optional<environment> new_env = run_new_frontend(env, contents, mod_fn, opts);
+            if (!new_env)
+                ok = false;
+            else
+                env = *new_env;
         } else {
             scope_traces_as_messages scope_trace_msgs(mod_fn, {1, 0});
             simple_pos_info_provider pip(mod_fn.c_str());