From 139d6c64e684e7f2d9540ae24be8e13d461e3420 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Jan 2020 20:43:36 -0800 Subject: [PATCH] feat: add `new_frontend` command cc @kha --- src/Init/Lean/Elab/Frontend.lean | 5 +++ src/Init/Lean/Parser/Module.lean | 1 + src/Init/Lean/Util/Message.lean | 6 ++++ src/frontends/lean/parser.cpp | 49 +++++++++++++++++++++++++++++- src/frontends/lean/parser.h | 1 + src/frontends/lean/scanner.cpp | 24 ++++++++++++--- src/frontends/lean/scanner.h | 3 +- src/frontends/lean/token_table.cpp | 2 +- 8 files changed, 84 insertions(+), 7 deletions(-) diff --git a/src/Init/Lean/Elab/Frontend.lean b/src/Init/Lean/Elab/Frontend.lean index a0dc89cccd..fdc0fa6d15 100644 --- a/src/Init/Lean/Elab/Frontend.lean +++ b/src/Init/Lean/Elab/Frontend.lean @@ -91,6 +91,11 @@ IO.processCommands parserCtx parserStateRef cmdStateRef; cmdState ← cmdStateRef.get; pure (cmdState.env, cmdState.messages) +@[export lean_process_input] +def processExport (env : Environment) (input : String) (opts : Options) (fileName : String) : IO (Environment × List Message) := do +(env, messages) ← process input env opts fileName; +pure (env, messages.toList) + def runFrontend (env : Environment) (input : String) (opts : Options := {}) (fileName : Option String := none) : IO (Environment × MessageLog) := do let fileName := fileName.getD ""; let parserCtx := Parser.mkParserContextCore env input fileName; diff --git a/src/Init/Lean/Parser/Module.lean b/src/Init/Lean/Parser/Module.lean index 3a6c8d0f92..f9dda147bd 100644 --- a/src/Init/Lean/Parser/Module.lean +++ b/src/Init/Lean/Parser/Module.lean @@ -72,6 +72,7 @@ partial def parseCommand (env : Environment) (c : ParserContextCore) : ModulePar else let c := c.toParserContext env; let s := { ParserState . cache := initCacheForInput c.input, pos := pos }; + let s := whitespace c s; let s := (commandParser : Parser).fn (0:Nat) c s; match s.errorMsg with | none => diff --git a/src/Init/Lean/Util/Message.lean b/src/Init/Lean/Util/Message.lean index 6e7e5b9531..b75975e5b1 100644 --- a/src/Init/Lean/Util/Message.lean +++ b/src/Init/Lean/Util/Message.lean @@ -123,11 +123,17 @@ mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column | MessageSeverity.error => "error: ") ++ (if msg.caption == "" then "" else msg.caption ++ ":\n") ++ toString (fmt msg.data)) + instance : Inhabited Message := ⟨{ fileName := "", pos := ⟨0, 1⟩, data := arbitrary _}⟩ instance : HasToString Message := ⟨Message.toString⟩ + +@[export lean_message_pos] def getPostEx (msg : Message) : Position := msg.pos +@[export lean_message_severity] def getSeverityEx (msg : Message) : MessageSeverity := msg.severity +@[export lean_message_string] def getMessageStringEx (msg : Message) : String := toString (fmt msg.data) + end Message structure MessageLog := diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index bf0690779e..3b1a3e8a31 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "runtime/flet.h" #include "runtime/utf8.h" #include "util/option_declarations.h" +#include "util/io.h" #include "kernel/for_each_fn.h" #include "kernel/replace_fn.h" #include "kernel/find_fn.h" @@ -1959,7 +1960,7 @@ unsigned parser::curr_lbp() const { return get_token_info().expr_precedence(); case token_kind::CommandKeyword: case token_kind::Eof: case token_kind::QuotedSymbol: case token_kind::DocBlock: - case token_kind::ModDocBlock: + case token_kind::ModDocBlock: case token_kind::NewFrontend: return 0; case token_kind::Identifier: case token_kind::Numeral: case token_kind::Decimal: case token_kind::String: @@ -2103,6 +2104,49 @@ void parser::parse_mod_doc_block() { next(); } +extern "C" object * lean_process_input(object * env, object * input, object * opts, object * filename, object * w); + +typedef list_ref messages; + +pair_ref process_input(environment const & env, std::string const & input, options const & opts, std::string const & file_name) { + return get_io_result>(lean_process_input(env.to_obj_arg(), mk_string(input), opts.to_obj_arg(), mk_string(file_name), io_mk_world())); +} + +extern "C" object * lean_message_pos(object * msg); +extern "C" uint8 lean_message_severity(object * msg); +extern "C" object * lean_message_string(object * msg); + +static pos_info get_message_pos(object_ref const & msg) { + auto p = pair_ref(lean_message_pos(msg.to_obj_arg())); + return pos_info(p.fst().get_small_value(), p.snd().get_small_value()); +} + +static message_severity get_message_severity(object_ref const & msg) { + return static_cast(lean_message_severity(msg.to_obj_arg())); +} + +static std::string get_message_string(object_ref const & msg) { + string_ref r(lean_message_string(msg.to_obj_arg())); + return r.to_std_string(); +} + +void parser::parse_new_frontend_cmd() { + auto curr_pos = pos(); + std::string input = m_scanner.get_str_val(); + next(); + pair_ref result = process_input(m_env, input, get_options(), m_file_name); + set_env(result.fst()); + for (auto msg : result.snd()) { + pos_info pos = get_message_pos(msg); + pos.first += curr_pos.first; + message_severity sev = get_message_severity(msg); + std::string str = get_message_string(msg); + auto builder = mk_message(pos, sev); + builder << str; + builder.report(); + } +} + #if defined(__GNUC__) && !defined(__CLANG__) #pragma GCC diagnostic ignored "-Wmaybe-uninitialized" #endif @@ -2146,6 +2190,9 @@ bool parser::parse_command_like() { case token_kind::ModDocBlock: parse_mod_doc_block(); break; + case token_kind::NewFrontend: + parse_new_frontend_cmd(); + break; case token_kind::Eof: if (has_open_scopes(m_env)) { maybe_throw_error({"invalid end of module, expecting 'end'", pos()}); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 5dce5d4214..7975dcf23c 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -92,6 +92,7 @@ struct parser : public abstract_parser { std::string parse_doc_block(); void parse_mod_doc_block(); + void parse_new_frontend_cmd(); void process_imports(); void process_postponed(buffer const & args, bool is_left, buffer const & kinds, diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index 06baaad68c..09ad7c5a9f 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -377,6 +377,17 @@ auto scanner::read_mod_doc_block() -> token_kind { return token_kind::ModDocBlock; } +auto scanner::read_new_frontend() -> token_kind { + m_buffer.clear(); + while (true) { + uchar c = curr(); + if (c == Eof) break; + next(); + m_buffer += c; + } + return token_kind::NewFrontend; +} + void scanner::read_comment_block() { unsigned nesting = 1; while (true) { @@ -620,6 +631,7 @@ static name * g_begin_comment_block_tk = nullptr; static name * g_begin_doc_block_tk = nullptr; static name * g_begin_mod_doc_block_tk = nullptr; static name * g_tick_tk = nullptr; +static name * g_new_frontend_tk = nullptr; void initialize_scanner() { g_begin_comment_tk = new name("--"); @@ -627,6 +639,7 @@ void initialize_scanner() { g_begin_doc_block_tk = new name("/--"); g_begin_mod_doc_block_tk = new name("/-!"); g_tick_tk = new name("'"); + g_new_frontend_tk = new name("new_frontend"); } void finalize_scanner() { @@ -635,6 +648,7 @@ void finalize_scanner() { delete g_begin_doc_block_tk; delete g_begin_mod_doc_block_tk; delete g_tick_tk; + delete g_new_frontend_tk; } auto scanner::scan(environment const & env) -> token_kind { @@ -676,6 +690,8 @@ auto scanner::scan(environment const & env) -> token_kind { return read_mod_doc_block(); else if (n == *g_tick_tk) return read_char(); + else if (n == *g_new_frontend_tk) + return read_new_frontend(); else return k; } else { @@ -756,7 +772,7 @@ void token::dealloc() { case token_kind::Numeral: case token_kind::Decimal: case token_kind::FieldNum: if (m_num_val != nullptr) delete m_num_val; return; - case token_kind::String: case token_kind::Char: + case token_kind::String: case token_kind::Char: case token_kind::NewFrontend: case token_kind::DocBlock: case token_kind::ModDocBlock: if (m_str_val != nullptr) delete m_str_val; return; @@ -778,7 +794,7 @@ void token::copy(token const & tk) { case token_kind::Numeral: case token_kind::Decimal: case token_kind::FieldNum: m_num_val = new mpq(*tk.m_num_val); return; - case token_kind::String: case token_kind::Char: + case token_kind::String: case token_kind::Char: case token_kind::NewFrontend: case token_kind::DocBlock: case token_kind::ModDocBlock: m_str_val = new std::string(*tk.m_str_val); return; @@ -803,7 +819,7 @@ void token::steal(token && tk) { m_num_val = tk.m_num_val; tk.m_num_val = nullptr; return; - case token_kind::String: case token_kind::Char: + case token_kind::String: case token_kind::Char: case token_kind::NewFrontend: case token_kind::DocBlock: case token_kind::ModDocBlock: m_str_val = tk.m_str_val; tk.m_str_val = nullptr; @@ -833,7 +849,7 @@ token read_tokens(environment & env, io_state const & ios, scanner & s, buffer", 0}, {".", 0}, {":", 0}, {"!", 0}, {":=", 0}, {"--", 0}, {"#", g_max_prec}, - {"/-", 0}, {"/--", 0}, {"/-!", 0}, {"begin", g_max_prec}, {"using", 0}, + {"/-", 0}, {"/--", 0}, {"new_frontend", 0}, {"/-!", 0}, {"begin", g_max_prec}, {"using", 0}, {"@@", g_max_prec}, {"@", g_max_prec}, {"@&", g_max_prec}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0}, {"match", 0}, {"nomatch", 0}, {"^.", g_max_prec+1}, {"::", 67},