feat(frontends/lean): add 'print notation' command

src/frontends/lean/builtin_cmds.cpp

@@ -36,6 +36,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/pp_options.h"
+#include "frontends/lean/parse_table.h"
 
 namespace lean {
 static void print_coercions(parser & p, optional<name> const & C) {
@@ -106,6 +107,53 @@ static void print_fields(parser & p) {
     }
 }
 
+static bool uses_token(unsigned num, notation::transition const * ts, name const & token) {
+    for (unsigned i = 0; i < num; i++) {
+        if (ts[i].get_token() == token)
+            return true;
+    }
+    return false;
+}
+
+static bool uses_some_token(unsigned num, notation::transition const * ts, buffer<name> const & tokens) {
+    return
+        tokens.empty() ||
+        std::any_of(tokens.begin(), tokens.end(), [&](name const & token) { return uses_token(num, ts, token); });
+}
+
+static bool print_parse_table(parser & p, parse_table const & t, bool nud, buffer<name> const & tokens) {
+    bool found = false;
+    io_state ios = p.ios();
+    options os   = ios.get_options();
+    os = os.update(get_pp_full_names_option_name(), true);
+    os = os.update(get_pp_notation_option_name(), false);
+    ios.set_options(os);
+    optional<token_table> tt(get_token_table(p.env()));
+    t.for_each([&](unsigned num, notation::transition const * ts, list<expr> const & overloads) {
+            if (uses_some_token(num, ts, tokens)) {
+                found = true;
+                io_state_stream out = regular(p.env(), ios);
+                notation::display(out, num, ts, overloads, nud, tt);
+            }
+        });
+    return found;
+}
+
+static void print_notation(parser & p) {
+    buffer<name> tokens;
+    while (p.curr_is_keyword()) {
+        tokens.push_back(p.get_token_info().token());
+        p.next();
+    }
+    bool found = false;
+    if (print_parse_table(p, get_nud_table(p.env()), true, tokens))
+        found = true;
+    if (print_parse_table(p, get_led_table(p.env()), false, tokens))
+        found = true;
+    if (!found)
+        p.regular_stream() << "no notation" << endl;
+}
+
 environment print_cmd(parser & p) {
     flycheck_information info(p.regular_stream());
     if (info.enabled()) {
@@ -165,6 +213,9 @@ environment print_cmd(parser & p) {
     } else if (p.curr_is_token_or_id(get_fields_tk())) {
         p.next();
         print_fields(p);
+    } else if (p.curr_is_token_or_id(get_notation_tk())) {
+        p.next();
+        print_notation(p);
     } else {
         throw parser_error("invalid print command", p.pos());
     }

src/frontends/lean/parse_table.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/replace_fn.h"
 #include "library/kernel_bindings.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/parse_table.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/info_annotation.h"
@@ -192,7 +193,7 @@ bool action::is_equal(action const & a) const {
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
-void action::display(std::ostream & out) const {
+void action::display(io_state_stream & out) const {
     switch (kind()) {
     case action_kind::Skip:    out << "skip"; break;
     case action_kind::Binder:
@@ -207,7 +208,7 @@ void action::display(std::ostream & out) const {
         else
             out << "binders";
         break;
-    case action_kind::Ext:     out << "ext"; break;
+    case action_kind::Ext:     out << "builtin"; break;
     case action_kind::LuaExt:  out << "luaext"; break;
     case action_kind::Expr:    out << rbp(); break;
     case action_kind::Exprs:
@@ -479,22 +480,47 @@ parse_table parse_table::merge(parse_table const & s, bool overload) const {
 
 bool parse_table::is_nud() const { return m_ptr->m_nud; }
 
-void parse_table::display(std::ostream & out) const {
+void display(io_state_stream & out, unsigned num, transition const * ts, list<expr> const & es, bool nud,
+             optional<token_table> const & tt) {
+    if (!nud)
+        out << "_ ";
+    for (unsigned i = 0; i < num; i++) {
+        if (i > 0) out << " ";
+        out << "`" << ts[i].get_token() << "`";
+        if (tt) {
+            if (auto prec = get_precedence(*tt, ts[i].get_token().to_string().c_str())) {
+                out << ":" << *prec;
+            }
+        }
+        switch (ts[i].get_action().kind()) {
+        case action_kind::Skip:
+            break;
+        case action_kind::Expr:
+            out << " _:"; ts[i].get_action().display(out);
+            break;
+        default:
+            out << " "; ts[i].get_action().display(out);
+            break;
+        }
+    }
+    out << " :=";
+    if (length(es) == 1) {
+        out << " " << head(es) << "\n";
+    } else {
+        buffer<expr> tmp;
+        to_buffer(es, tmp);
+        out << "\n";
+        unsigned i = tmp.size();
+        while (i > 0) {
+            --i;
+            out << "  | " << tmp[i] << "\n";
+        }
+    }
+}
+
+void parse_table::display(io_state_stream & out, optional<token_table> const & tt) const {
     for_each([&](unsigned num, transition const * ts, list<expr> const & es) {
-            for (unsigned i = 0; i < num; i++) {
-                if (i > 0) out << " ";
-                out << "`" << ts[i].get_token() << "`:";
-                ts[i].get_action().display(out);
-            }
-            out << " :=";
-            if (length(es) == 1) {
-                out << " " << head(es) << "\n";
-            } else {
-                out << "\n";
-                for (auto e : es) {
-                    out << "  | " << e << "\n";
-                }
-            }
+            ::lean::notation::display(out, num, ts, es, is_nud(), tt);
         });
 }
 

src/frontends/lean/parse_table.h

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 class parser;
+class io_state_stream;
 namespace notation {
 typedef std::function<expr(parser &, unsigned, expr const *, pos_info const &)> parse_fn;
 
@@ -81,7 +82,7 @@ public:
     std::string const & get_lua_fn() const;
 
     bool is_equal(action const & a) const;
-    void display(std::ostream & out) const;
+    void display(io_state_stream & out) const;
 
     /** \brief Return true iff the action is not Ext or LuaExt */
     bool is_simple() const;
@@ -124,6 +125,9 @@ inline bool operator!=(transition const & t1, transition const & t2) {
 /** \brief Apply \c f to expressions embedded in the given transition */
 transition replace(transition const & t, std::function<expr(expr const &)> const & f);
 
+void display(io_state_stream & out, unsigned num, transition const * ts, list<expr> const & es, bool nud,
+             optional<token_table> const & tt);
+
 /**
    \brief Parse table "transition rules" for implementing a Pratt's parser.
    The table supports "left factoring" in the methods \c add and \c merge.
@@ -152,7 +156,7 @@ public:
     list<expr> const & is_accepting() const;
     void for_each(std::function<void(unsigned, transition const *, list<expr> const &)> const & fn) const;
 
-    void display(std::ostream & out) const;
+    void display(io_state_stream & out, optional<token_table> const & tk) const;
 };
 
 /** \brief Given a notation definition, return the "head symbol" of