From af55cb13e79cc148f50ba9b7a8ff319c8db96d3e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 10 Sep 2018 10:25:55 -0700 Subject: [PATCH] fix(library/messages,library/init/lean/message): wrap `message_log` in structure, reverse in the end --- library/init/lean/message.lean | 16 +++++++++---- library/init/lean/parser/basic.lean | 6 ++--- src/frontends/lean/definition_cmds.cpp | 2 +- src/library/messages.cpp | 32 ++++++++++++++++++-------- src/library/messages.h | 14 +++++++---- src/library/module_mgr.cpp | 2 +- src/shell/lean.cpp | 8 +++---- tests/lean/parser1.lean | 18 +++++++-------- tests/lean/parser1.lean.expected.out | 12 +++++----- 9 files changed, 69 insertions(+), 41 deletions(-) diff --git a/library/init/lean/message.lean b/library/init/lean/message.lean index 8fd2733152..c7fbaa5125 100644 --- a/library/init/lean/message.lean +++ b/library/init/lean/message.lean @@ -23,15 +23,23 @@ structure message := (caption : string := "") (text : string) -def message_log := list message +structure message_log := +-- messages are stored in reverse for efficient append +(rev_list : list message) namespace message_log -def add : message → message_log → message_log := -list.cons +def empty : message_log := +⟨[]⟩ + +def add (msg : message) (log : message_log) : message_log := +⟨msg :: log.rev_list⟩ def has_errors (log : message_log) : bool := -log.any $ λ m, match m.severity with +log.rev_list.any $ λ m, match m.severity with | message_severity.error := tt | _ := ff + +def to_list (log : message_log) : list message := +log.rev_list.reverse end message_log end lean diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index 055888ba8b..bdeecf8784 100644 --- a/library/init/lean/parser/basic.lean +++ b/library/init/lean/parser/basic.lean @@ -163,7 +163,7 @@ m (syntax × message_log) := do r ← ((r.run cfg).run st).parse_with_eoi s, pure $ match r with | except.ok (a, st) := (a, st.messages) -| except.error msg := (msg.custom, [message_of_parsec_message cfg msg]) +| except.error msg := (msg.custom, message_log.empty.add (message_of_parsec_message cfg msg)) end open monad_parsec @@ -178,11 +178,11 @@ do cfg ← read, def eoi : syntax_node_kind := ⟨`lean.parser.parser.eoi⟩ protected def parse [monad m] (cfg : parser_config) (s : string) (r : parser_t m syntax) [parser.has_tokens r] : - m (syntax × list message) := + m (syntax × message_log) := -- the only hardcoded tokens, because they are never directly mentioned by a `parser` let builtin_tokens : list token_config := [⟨"/-", 0, none⟩, ⟨"--", 0, none⟩] in let trie := (tokens r ++ builtin_tokens).foldl (λ t cfg, trie.insert t cfg.prefix cfg) trie.mk in -parser.run cfg ⟨trie, [], s.mk_iterator⟩ s $ do +parser.run cfg ⟨trie, message_log.empty, s.mk_iterator⟩ s $ do stx ← catch r $ λ (msg : parsec.message _), do { modify $ λ st, {st with token_start := msg.it}, parser.log_message msg, diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index df7468a268..18ab08da14 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -600,7 +600,7 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta // If we have already logged an error during elaboration, don't // bother showing the less helpful kernel exception - if (!has_errors(*global_message_log())) + if (!global_message_log()->has_errors()) p.mk_message(header_pos, ERROR).set_exception(ex).report(); // As a last resort, try replacing the definition body with `sorry`. // If that doesn't work either, just silently give up since we have diff --git a/src/library/messages.cpp b/src/library/messages.cpp index 675e2a4914..908ece3d3a 100644 --- a/src/library/messages.cpp +++ b/src/library/messages.cpp @@ -33,15 +33,7 @@ std::ostream & operator<<(std::ostream & out, message const & msg) { void report_message(message const & msg0) { lean_assert(global_message_log()); - *global_message_log() = cons(msg0, *global_message_log()); -} - -bool has_errors(message_log const & l) { - for (auto const & m : l) { - if (m.get_severity() == ERROR) - return true; - } - return false; + global_message_log()->add(msg0); } LEAN_THREAD_PTR(message_log, g_message_log); @@ -52,4 +44,26 @@ scope_message_log::scope_message_log(message_log * l) : message_log * global_message_log() { return g_message_log; } + +bool message_log::has_errors() const { + for (auto const & m : m_rev_list) { + if (m.is_error()) { + return true; + } + } + return false; +} + +void message_log::add(message const & m) { + m_rev_list = cons(m, m_rev_list); +} + +buffer message_log::to_buffer() const { + buffer buf; + for (auto const & m : m_rev_list) { + buf.push_back(m); + } + std::reverse(buf.begin(), buf.end()); + return buf; +} } diff --git a/src/library/messages.h b/src/library/messages.h index 3f514fecdc..0c4e48fca5 100644 --- a/src/library/messages.h +++ b/src/library/messages.h @@ -78,11 +78,17 @@ std::ostream & operator<<(std::ostream &, message const &); void report_message(message const &); /* -def message_log := list message +structure message_log := +-- messages are stored in reverse for efficient append +(rev_list : list message) */ -using message_log = list_ref; - -bool has_errors(message_log const &); +class message_log { + list_ref m_rev_list; +public: + bool has_errors() const; + void add(message const &); + buffer to_buffer() const; +}; struct scope_message_log : flet { scope_message_log(message_log *); diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp index fb0d6df95a..bd56cccd2c 100644 --- a/src/library/module_mgr.cpp +++ b/src/library/module_mgr.cpp @@ -83,7 +83,7 @@ static void compile_olean(std::shared_ptr const & mod) { if (dep.m_mod_info) compile_olean(dep.m_mod_info); - if (mod->m_source != module_src::LEAN || has_errors(mod->m_log)) + if (mod->m_source != module_src::LEAN || mod->m_log.has_errors()) return; auto res = mod->m_result; diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index bf3455ef97..87e115724b 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -520,13 +520,13 @@ int main(int argc, char ** argv) { for (auto & mod : mods) { if (test_suite) { std::ofstream out(mod.m_id + ".test_suite.out"); - for (auto const & msg : mod.m_mod_info->m_log) { + for (auto const & msg : mod.m_mod_info->m_log.to_buffer()) { out << msg; } } if (test_suite) { std::ofstream status(mod.m_id + ".status"); - status << (!has_errors(mod.m_mod_info->m_log) ? 0 : 1); + status << (!mod.m_mod_info->m_log.has_errors() ? 0 : 1); } } @@ -535,7 +535,7 @@ int main(int argc, char ** argv) { bool ok = true; if (!test_suite) { for (auto & mod : mods) { - for (auto const & msg : mod.m_mod_info->m_log) { + for (auto const & msg : mod.m_mod_info->m_log.to_buffer()) { if (json_output) { #if defined(LEAN_JSON) print_json(std::cout, msg); @@ -544,7 +544,7 @@ int main(int argc, char ** argv) { std::cout << msg; } } - if (has_errors(mod.m_mod_info->m_log)) + if (mod.m_mod_info->m_log.has_errors()) ok = false; } } diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean index 565ce7184d..504983a328 100644 --- a/tests/lean/parser1.lean +++ b/tests/lean/parser1.lean @@ -3,23 +3,23 @@ open lean open lean.parser open lean.parser.syntax_node_kind.has_view -def show_result (p : syntax × list lean.message) (s : string) : eio unit := -let (stx, errors) := p in +def show_result (p : syntax × message_log) (s : string) : eio unit := +let (stx, msgs) := p in when (stx.reprint ≠ s) ( io.println "reprint fail:" *> io.println stx.reprint ) *> -match errors with +match msgs.to_list with | [] := do io.println "result: ", io.println (to_string stx) -| _ := do - errors.mfor $ λ e, io.println e.text, +| msgs := do + msgs.mfor $ λ e, io.println e.text, io.println "partial syntax tree:", io.println (to_string stx) -def parse_module (s : string) : syntax × list lean.message := -coroutine.finish (λ cmd, ()) (parser.parse ⟨⟩ s module.parser) () +def parse_module (s : string) : syntax × message_log := +coroutine.finish (λ cmd, ()) (parser.parse ⟨""⟩ s module.parser) () def show_parse (s : string) : eio unit := show_result (parse_module s) s @@ -54,7 +54,7 @@ end b" -- expansion example #eval (do { - (stx, []) ← pure $ parse_module "prefix `+`:10 := _", + (stx, ⟨[]⟩) ← pure $ parse_module "prefix `+`:10 := _", some {root := stx, ..} ← pure $ parser.parse.view stx, some {commands := [stx], ..} ← pure $ view module stx, some stx ← pure $ mixfix.expand stx | throw "expand fail", @@ -66,7 +66,7 @@ end b" #eval do s ← io.fs.read_file "../../library/init/core.lean", let s := (s.mk_iterator.nextn 1700).prev_to_string, - let k := parser.parse ⟨⟩ s module.parser, + let k := parser.parse ⟨"foo"⟩ s module.parser, io.prim.iterate_eio k $ λ k, match k.resume () with | coroutine_result_core.done p := show_result p s *> pure (sum.inr ()) | coroutine_result_core.yielded cmd k := do { diff --git a/tests/lean/parser1.lean.expected.out b/tests/lean/parser1.lean.expected.out index 24a0d45b78..18252805c3 100644 --- a/tests/lean/parser1.lean.expected.out +++ b/tests/lean/parser1.lean.expected.out @@ -62,10 +62,10 @@ partial syntax tree: [] [(lean.parser.open "open" [(lean.parser.open_spec me [] [] [] [])])]) (lean.parser.parser.eoi "")] -error at line 1, column 9: -expected identifier error at line 1, column 5: expected identifier +error at line 1, column 9: +expected identifier partial syntax tree: [(lean.parser.module [] @@ -150,12 +150,12 @@ result: ":=" (lean.parser.hole "_")) notation`+`:10 b:10 :=_ -error at line 85, column 0: -expected command -error at line 11, column 26: -expected "_" error at line 10, column 19: expected "_" +error at line 11, column 26: +expected "_" +error at line 85, column 0: +expected command partial syntax tree: [(lean.parser.module [(lean.parser.prelude "prelude")]