refactor(library/messages): make an object_ref

library/init/lean/message.lean

@@ -16,6 +16,7 @@ inductive message_severity
 | information | warning | error
 
 structure message :=
+(filename : string)
 (pos      : position)
 (end_pos  : option position  := none)
 (severity : message_severity := message_severity.error)

library/init/lean/parser/basic.lean

@@ -119,7 +119,8 @@ structure parser_state :=
    * During error recovery, skipped input should be associated to the next token -/
 (token_start : string.iterator)
 
-structure parser_config := mk
+structure parser_config :=
+(filename : string)
 
 @[derive monad alternative monad_reader monad_state monad_parsec monad_except]
 def parser_t (m : Type → Type) [monad m] := reader_t parser_config $ state_t parser_state $ parsec_t syntax m
@@ -151,15 +152,18 @@ class syntax_node_kind.has_view (k : syntax_node_kind) (α : out_param Type) :=
 (view : syntax → option α)
 (review : α → syntax)
 
+def message_of_parsec_message {μ : Type} (cfg : parser_config) (msg : parsec.message μ) : message :=
+-- FIXME: translate position
+{filename := cfg.filename, pos := ⟨0, 0⟩, text := to_string msg}
+
 section
 local attribute [reducible] parser_t
 protected def run {m : Type → Type} [monad m] (cfg : parser_config) (st : parser_state) (s : string) (r : parser_t m syntax) :
-  m (syntax × message_log) :=
+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)
-   -- FIXME: translate position
-   | except.error msg  := (msg.custom, [{pos := ⟨0, 0⟩, text := to_string msg}])
+pure $ match r with
+| except.ok (a, st) := (a, st.messages)
+| except.error msg  := (msg.custom, [message_of_parsec_message cfg msg])
 end
 
 open monad_parsec
@@ -167,9 +171,9 @@ open parser.has_view
 variables {α : Type} {m : Type → Type}
 local notation `parser` := m syntax
 
-def log_message {μ : Type} [monad_state parser_state m] (msg : parsec.message μ) : m unit :=
--- FIXME: translate position
-modify (λ st, {st with messages := st.messages.add {pos := ⟨0, 0⟩, text := to_string msg}})
+def log_message {μ : Type} [monad m] [monad_reader parser_config m] [monad_state parser_state m] (msg : parsec.message μ) : m unit :=
+do cfg ← read,
+   modify (λ st, {st with messages := st.messages.add (message_of_parsec_message cfg msg)})
 
 def eoi : syntax_node_kind := ⟨`lean.parser.parser.eoi⟩
 

src/frontends/lean/json.cpp

@@ -28,7 +28,7 @@ json json_of_severity(message_severity sev) {
 
 json json_of_message(message const & msg) {
     json j;
-    j["file_name"] = msg.get_file_name();
+    j["file_name"] = msg.get_filename();
     j["pos_line"]  = msg.get_pos().first;
     j["pos_col"]   = msg.get_pos().second;
     if (auto end_pos = msg.get_end_pos()) {

src/library/messages.cpp

@@ -11,12 +11,11 @@ Author: Gabriel Ebner
 namespace lean {
 
 message::message(parser_exception const & ex) :
-        message(ex.get_file_name(), *ex.get_pos(),
-                ERROR, ex.get_msg()) {}
+        message(ex.get_file_name(), *ex.get_pos(), ERROR, ex.get_msg()) {}
 
 std::ostream & operator<<(std::ostream & out, message const & msg) {
     if (msg.get_severity() != INFORMATION) {
-        out << msg.get_file_name() << ":" << msg.get_pos().first << ":" << msg.get_pos().second << ": ";
+        out << msg.get_filename() << ":" << msg.get_pos().first << ":" << msg.get_pos().second << ": ";
         switch (msg.get_severity()) {
             case INFORMATION: break;
             case WARNING: out << "warning: "; break;
@@ -33,31 +32,24 @@ std::ostream & operator<<(std::ostream & out, message const & msg) {
 }
 
 void report_message(message const & msg0) {
-    auto & l = logtree();
-    auto & loc = logtree().get_location();
-
-    std::shared_ptr<message> msg;
-    if (loc.m_file_name.empty()) {
-        msg = std::make_shared<message>(msg0);
-    } else {
-        auto pos_ok = loc.m_range.m_begin <= msg0.get_pos() && msg0.get_pos() <= loc.m_range.m_end;
-        msg = std::make_shared<message>(loc.m_file_name,
-                                        pos_ok ? msg0.get_pos() : loc.m_range.m_begin,
-                                        pos_ok ? msg0.get_end_pos() : optional<pos_info>(),
-                                        msg0.get_severity(), msg0.get_caption(), msg0.get_text());
-    }
-    l.add(msg);
+    lean_assert(global_message_log());
+    *global_message_log() = cons(msg0, *global_message_log());
 }
 
-task<bool> has_errors(log_tree::node const & n) {
-    return n.has_entry(is_error_message);
-}
-
-bool is_error_message(log_entry const & e) {
-    if (auto msg = dynamic_cast<message const *>(e.get())) {
-        return msg->is_error();
+bool has_errors(message_log const & l) {
+    for (auto const & m : l) {
+        if (m.get_severity() == ERROR)
+            return true;
     }
     return false;
 }
 
+LEAN_THREAD_PTR(message_log, g_message_log);
+
+scope_message_log::scope_message_log(message_log * l) :
+        flet<message_log *>(g_message_log, l) {}
+
+message_log * global_message_log() {
+    return g_message_log;
+}
 }

src/library/messages.h

@@ -6,52 +6,87 @@ Author: Gabriel Ebner
 */
 #pragma once
 #include <string>
-#include "util/log_tree.h"
 #include "util/message_definitions.h"
 #include "util/parser_exception.h"
+#include "util/option_ref.h"
+#include "runtime/flet.h"
 
 namespace lean {
+/*
+structure position :=
+(line column : nat)
+*/
+class position : public object_ref {
+public:
+    position(unsigned line, unsigned column) : object_ref(mk_cnstr(0, nat(line), nat(column))) {}
+    position(pos_info const & pos) : position(pos.first, pos.second) {}
+    unsigned get_line() const { return static_cast<nat const &>(cnstr_get_ref(*this, 0)).get_small_value(); }
+    unsigned get_column() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
+    pos_info to_pos_info() const { return mk_pair(get_line(), get_column()); }
+};
 
+/*
+inductive message_severity
+| information | warning | error
+*/
 enum message_severity { INFORMATION, WARNING, ERROR };
 
-class message : public log_entry_cell {
-    std::string        m_file_name;
-    pos_info           m_pos;
-    optional<pos_info> m_end_pos;
-    message_severity   m_severity;
-    std::string        m_caption, m_text;
+/*
+structure message :=
+(filename : string)
+(pos      : position)
+(end_pos  : option position  := none)
+(severity : message_severity := message_severity.error)
+(caption  : string           := "")
+(text     : string)
+ */
+class message : public object_ref {
 public:
-    message(std::string const & file_name, pos_info const & pos, optional<pos_info> const & end_pos,
+    message(std::string const & filename, pos_info const & pos, optional<pos_info> const & end_pos,
             message_severity severity, std::string const & caption, std::string const & text) :
-        m_file_name(file_name), m_pos(pos), m_end_pos(end_pos),
-        m_severity(severity), m_caption(caption), m_text(text) {}
-    message(std::string const & file_name, pos_info const & pos,
+        object_ref(mk_cnstr(0, string_ref(filename), position(pos),
+                            option_ref<position>(end_pos ? some(position(*end_pos)) : optional<position>()),
+                            nat(static_cast<unsigned>(severity)),
+                            string_ref(caption), string_ref(text))) {}
+    message(std::string const & filename, pos_info const & pos,
             message_severity severity, std::string const & caption, std::string const & text) :
-        m_file_name(file_name), m_pos(pos),
-        m_severity(severity), m_caption(caption), m_text(text) {}
-    message(std::string const & file_name, pos_info const & pos,
+        message(filename, pos, optional<pos_info>(), severity, caption, text) {}
+    message(std::string const & filename, pos_info const & pos,
             message_severity severity, std::string const & text) :
-        message(file_name, pos, severity, std::string(), text) {}
-    message(std::string const & file_name, pos_info const & pos,
+        message(filename, pos, severity, std::string(), text) {}
+    message(std::string const & filename, pos_info const & pos,
             message_severity severity) :
-        message(file_name, pos, severity, std::string()) {}
+        message(filename, pos, severity, std::string()) {}
     message(parser_exception const & ex);
 
-    std::string get_file_name() const { return m_file_name; }
-    pos_info get_pos() const { return m_pos; }
-    optional<pos_info> get_end_pos() const { return m_end_pos; }
-    message_severity get_severity() const { return m_severity; }
-    std::string get_caption() const { return m_caption; }
-    std::string get_text() const { return m_text; }
-    location get_location() const { return {m_file_name, {m_pos, m_pos}}; }
+    std::string get_filename() const { return static_cast<string_ref const &>(cnstr_get_ref(*this, 0)).to_std_string(); }
+    pos_info get_pos() const { return static_cast<position const &>(cnstr_get_ref(*this, 1)).to_pos_info(); }
+    optional<pos_info> get_end_pos() const {
+        auto pos = static_cast<option_ref<position> const &>(cnstr_get_ref(*this, 2)).get();
+        return pos ? some(pos->to_pos_info()) : optional<pos_info>();
+    }
+    message_severity get_severity() const {
+        return static_cast<message_severity>(static_cast<nat const &>(cnstr_get_ref(*this, 3)).get_small_value());
+    }
+    std::string get_caption() const { return static_cast<string_ref const &>(cnstr_get_ref(*this, 4)).to_std_string(); }
+    std::string get_text() const { return static_cast<string_ref const &>(cnstr_get_ref(*this, 5)).to_std_string(); }
 
-    bool is_error() const { return m_severity >= ERROR; }
+    bool is_error() const { return get_severity() >= ERROR; }
 };
 
 std::ostream & operator<<(std::ostream &, message const &);
 void report_message(message const &);
 
-bool is_error_message(log_entry const &);
-task<bool> has_errors(log_tree::node const &);
+/*
+def message_log := list message
+*/
+using message_log = list_ref<message>;
 
+bool has_errors(message_log const &);
+
+struct scope_message_log : flet<message_log *> {
+    scope_message_log(message_log *);
+    scope_message_log(message_log & t) : scope_message_log(&t) {}
+};
+message_log * global_message_log();
 }

src/util/option_ref.h

@@ -0,0 +1,62 @@
+/*
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Sebastian Ullrich
+*/
+#pragma once
+#include "util/object_ref.h"
+
+namespace lean {
+/* Wrapper for manipulating Lean option values in C++ */
+template<typename T>
+class option_ref : public object_ref {
+    explicit option_ref(object * o):object_ref(o) { inc(o); }
+public:
+    option_ref():object_ref(box(0)) {}
+    explicit option_ref(T const & a):object_ref(mk_cnstr(1, a.raw())) { inc(a.raw()); }
+    explicit option_ref(T const * a) { if (a) *this = option_ref(*a); }
+    explicit option_ref(option_ref<T> const * o) { if (o) *this = *o; }
+    explicit option_ref(optional<T> const & o):option_ref(o ? &*o : nullptr) {}
+
+    option_ref & operator=(option_ref const & other) { object_ref::operator=(other); return *this; }
+    option_ref & operator=(option_ref && other) { object_ref::operator=(other); return *this; }
+
+    explicit operator bool() const { return !is_scalar(raw()); }
+    optional<T> get() const { return *this ? some(static_cast<T const &>(cnstr_get_ref(*this, 0))) : optional<T>(); }
+
+    void serialize(serializer & s) const { s.write_object(raw()); }
+    static option_ref deserialize(deserializer & d) { return option_ref(d.read_object()); }
+
+    /** \brief Structural equality. */
+    friend bool operator==(option_ref const & o1, option_ref const & o2) {
+        return o1.get() == o2.get();
+    }
+    friend bool operator!=(option_ref const & o1, option_ref const & o2) { return !(o1 == o2); }
+
+    /*
+    // lexicographical order
+    friend bool operator<(option_ref const & l1, option_ref const & l2) {
+        object * it1 = l1.raw();
+        object * it2 = l2.raw();
+        while (!is_scalar(it1) && !is_scalar(it2)) {
+            if (it1 == it2)
+                return false;
+            T const & h1 = ::lean::head<T>(it1);
+            T const & h2 = ::lean::head<T>(it2);
+            if (h1 < h2)
+                return true;
+            if (h2 < h1)
+                return false;
+            it1 = cnstr_obj(it1, 1);
+            it2 = cnstr_obj(it2, 1);
+        }
+        return is_scalar(it1) && !is_scalar(it2);
+    }
+     */
+};
+
+template<typename T> serializer & operator<<(serializer & s, option_ref<T> const & l) { l.serialize(s); return s; }
+template<typename T> option_ref<T> read_option_ref(deserializer & d) { return option_ref<T>::deserialize(d); }
+
+}