refactor(frontends/lean): expose notation_entry and token_entry structures, and add functions for parsing notation without affecting the environment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/notation_cmd.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <utility>
 #include <limits>
 #include <string>
 #include "kernel/abstract.h"
@@ -21,6 +22,11 @@ static name g_foldr("foldr");
 static name g_foldl("foldl");
 static name g_binder("binder");
 static name g_binders("binders");
+static name g_infix("infix");
+static name g_infixl("infixl");
+static name g_infixr("infixr");
+static name g_postfix("postfix");
+static name g_notation("notation");
 
 static std::string parse_symbol(parser & p, char const * msg) {
     name n;
@@ -71,14 +77,15 @@ using notation::mk_skip_action;
 using notation::transition;
 using notation::action;
 
-static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload) {
+static std::pair<notation_entry, optional<token_entry>> parse_mixfix_notation(parser & p, mixfix_kind k, bool overload) {
     std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
     optional<unsigned> prec = parse_optional_precedence(p);
-    environment env = p.env();
+    environment const & env = p.env();
+    optional<token_entry> new_token;
     if (!prec) {
         prec = get_precedence(get_token_table(env), tk.c_str());
     } else if (prec != get_precedence(get_token_table(env), tk.c_str())) {
-        env = add_token(env, tk.c_str(), *prec);
+        new_token = token_entry(tk.c_str(), *prec);
     }
 
     if (!prec)
@@ -91,21 +98,44 @@ static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload) {
     char const * tks = tk.c_str();
     switch (k) {
     case mixfix_kind::infixl:
-        return add_led_notation(env, {transition(tks, mk_expr_action(*prec))}, mk_app(f, Var(1), Var(0)), overload);
+        return mk_pair(notation_entry(false, list<transition>(transition(tks, mk_expr_action(*prec))),
+                                      mk_app(f, Var(1), Var(0)), overload),
+                       new_token);
     case mixfix_kind::infixr:
-        return add_led_notation(env, {transition(tks, mk_expr_action(*prec-1))}, mk_app(f, Var(1), Var(0)), overload);
+        return mk_pair(notation_entry(false, list<transition>(transition(tks, mk_expr_action(*prec-1))),
+                                      mk_app(f, Var(1), Var(0)), overload),
+                       new_token);
     case mixfix_kind::postfix:
-        return add_led_notation(env, {transition(tks, mk_skip_action())}, mk_app(f, Var(0)), overload);
+        return mk_pair(notation_entry(false, list<transition>(transition(tks, mk_skip_action())),
+                                      mk_app(f, Var(0)), overload),
+                       new_token);
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
+static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, buffer<token_entry> & new_tokens) {
+    auto nt = parse_mixfix_notation(p, k, overload);
+    if (nt.second)
+        new_tokens.push_back(*nt.second);
+    return nt.first;
+}
+
+static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload) {
+    auto nt = parse_mixfix_notation(p, k, overload);
+    environment env = p.env();
+    if (nt.second)
+        env = add_token(env, *nt.second);
+    env = add_notation(env, nt.first);
+    return env;
+}
+
 environment infixl_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::infixl, overload); }
 environment infixr_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::infixr, overload); }
 environment postfix_cmd_core(parser & p, bool overload) { return mixfix_cmd(p, mixfix_kind::postfix, overload); }
 
-static name parse_quoted_symbol(parser & p, environment & env) {
+static name parse_quoted_symbol(parser & p, buffer<token_entry> & new_tokens) {
     if (p.curr_is_quoted_symbol()) {
+        environment const & env = p.env();
         auto tk   = p.get_name_val();
         auto tks  = tk.to_string();
         auto tkcs = tks.c_str();
@@ -115,9 +145,9 @@ static name parse_quoted_symbol(parser & p, environment & env) {
             unsigned prec = parse_precedence(p, "invalid notation declaration, precedence (small numeral) expected");
             auto old_prec = get_precedence(get_token_table(env), tkcs);
             if (!old_prec || prec != *old_prec)
-                env = add_token(env, tkcs, prec);
+                new_tokens.push_back(token_entry(tkcs, prec));
         } else if (!get_precedence(get_token_table(env), tkcs)) {
-            env = add_token(env, tkcs, 0);
+            new_tokens.push_back(token_entry(tkcs, 0));
         }
         return tk;
     } else {
@@ -144,7 +174,7 @@ static void parse_notation_local(parser & p, buffer<expr> & locals) {
     }
 }
 
-static action parse_action(parser & p, environment & env, buffer<expr> & locals) {
+static action parse_action(parser & p, buffer<expr> & locals, buffer<token_entry> & new_tokens) {
     if (p.curr_is_token(g_colon)) {
         p.next();
         if (p.curr_is_numeral()) {
@@ -159,7 +189,7 @@ static action parse_action(parser & p, environment & env, buffer<expr> & locals)
                 bool is_fold_right = p.curr_is_token_or_id(g_foldr);
                 p.next();
                 auto prec = parse_optional_precedence(p);
-                name sep  = parse_quoted_symbol(p, env);
+                name sep  = parse_quoted_symbol(p, new_tokens);
                 expr rec;
                 {
                     parser::local_scope scope(p);
@@ -197,8 +227,7 @@ static action parse_action(parser & p, environment & env, buffer<expr> & locals)
     }
 }
 
-environment notation_cmd_core(parser & p, bool overload) {
+notation_entry parse_notation_core(parser & p, bool overload, buffer<token_entry> & new_tokens) {
-    environment env = p.env();
     buffer<expr>       locals;
     buffer<transition> ts;
     parser::local_scope scope(p);
@@ -208,7 +237,7 @@ environment notation_cmd_core(parser & p, bool overload) {
         is_nud = false;
     }
     while (!p.curr_is_token(g_assign)) {
-        name tk = parse_quoted_symbol(p, env);
+        name tk = parse_quoted_symbol(p, new_tokens);
         if (p.curr_is_quoted_symbol() || p.curr_is_token(g_assign)) {
             ts.push_back(transition(tk, mk_skip_action()));
         } else if (p.curr_is_token_or_id(g_binder)) {
@@ -220,7 +249,7 @@ environment notation_cmd_core(parser & p, bool overload) {
         } else if (p.curr_is_identifier()) {
             name n   = p.get_name_val();
             p.next();
-            action a = parse_action(p, env, locals);
+            action a = parse_action(p, locals, new_tokens);
             expr l = mk_local(n, g_local_type);
             p.add_local_expr(n, l);
             locals.push_back(l);
@@ -233,9 +262,39 @@ environment notation_cmd_core(parser & p, bool overload) {
     if (ts.empty())
         throw parser_error("invalid notation declaration, empty notation is not allowed", p.pos());
     expr n = parse_notation_expr(p, locals);
-    if (is_nud)
+    return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload);
-        return add_nud_notation(env, ts.size(), ts.data(), n, overload);
+}
-    else
+
-        return add_led_notation(env, ts.size(), ts.data(), n, overload);
+environment notation_cmd_core(parser & p, bool overload) {
+    environment env = p.env();
+    buffer<token_entry> new_tokens;
+    auto ne = parse_notation_core(p, overload, new_tokens);
+    for (auto const & te : new_tokens)
+        env = add_token(env, te);
+    env = add_notation(env, ne);
+    return env;
+}
+
+bool curr_is_notation_decl(parser & p) {
+    return p.curr_is_token(g_infix) || p.curr_is_token(g_infixl) || p.curr_is_token(g_infixr) ||
+        p.curr_is_token(g_postfix) || p.curr_is_token(g_notation);
+}
+
+notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & new_tokens) {
+    if (p.curr_is_token(g_infix) || p.curr_is_token(g_infixl)) {
+        p.next();
+        return parse_mixfix_notation(p, mixfix_kind::infixl, overload, new_tokens);
+    } else if (p.curr_is_token(g_infixr)) {
+        p.next();
+        return parse_mixfix_notation(p, mixfix_kind::infixr, overload, new_tokens);
+    } else if (p.curr_is_token(g_postfix)) {
+        p.next();
+        return parse_mixfix_notation(p, mixfix_kind::postfix, overload, new_tokens);
+    } else if (p.curr_is_token(g_notation)) {
+        p.next();
+        return parse_notation_core(p, overload, new_tokens);
+    } else {
+        throw parser_error("invalid notation, 'infix', 'infixl', 'infixr', 'postfix' or 'notation' expected", p.pos());
+    }
 }
 }

src/frontends/lean/notation_cmd.h

@@ -6,8 +6,10 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/environment.h"
+#include "frontends/lean/parser_config.h"
 namespace lean {
 class parser;
+
 environment precedence_cmd(parser & p);
 environment notation_cmd_core(parser & p, bool overload);
 environment infixl_cmd_core(parser & p, bool overload);
@@ -17,4 +19,9 @@ inline environment notation_cmd(parser & p) { return notation_cmd_core(p, true);
 inline environment infixl_cmd(parser & p) { return infixl_cmd_core(p, true); }
 inline environment infixr_cmd(parser & p) { return infixr_cmd_core(p, true); }
 inline environment postfix_cmd(parser & p) { return postfix_cmd_core(p, true); }
+
+/** \brief Return true iff the current token is a notation declaration */
+bool curr_is_notation_decl(parser & p);
+/** \brief Parse a notation declaration, throws an error if the current token is not a "notation declaration". */
+notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & new_tokens);
 }

src/frontends/lean/parser.cpp

@@ -339,11 +339,6 @@ static name g_add("+");
 static name g_max("max");
 static name g_imax("imax");
 static name g_cup("\u2294");
-static name g_infix("infix");
-static name g_infixl("infixl");
-static name g_infixr("infixr");
-static name g_postfix("postfix");
-static name g_notation("notation");
 static name g_import("import");
 static unsigned g_level_add_prec = 10;
 static unsigned g_level_cup_prec = 5;
@@ -589,21 +584,12 @@ local_environment parser::parse_binders(buffer<parameter> & r) {
 }
 
 bool parser::parse_local_notation_decl() {
-    if (curr_is_token(g_infix) || curr_is_token(g_infixl)) {
+    if (curr_is_notation_decl(*this)) {
-        next();
+        buffer<token_entry> new_tokens;
-        m_env = infixl_cmd_core(*this, false);
+        auto ne = ::lean::parse_notation(*this, false, new_tokens);
-        return true;
+        for (auto const & te : new_tokens)
-    } else if (curr_is_token(g_infixr)) {
+            m_env = add_token(m_env, te);
-        next();
+        m_env = add_notation(m_env, ne);
-        m_env = infixr_cmd_core(*this, false);
-        return true;
-    } else if (curr_is_token(g_postfix)) {
-        next();
-        m_env = postfix_cmd_core(*this, false);
-        return true;
-    } else if (curr_is_token(g_notation)) {
-        next();
-        m_env = notation_cmd_core(*this, false);
         return true;
     } else {
         return false;

src/frontends/lean/parser_config.cpp

@@ -17,12 +17,6 @@ using notation::transition;
 using notation::action;
 using notation::action_kind;
 
-struct token_entry {
-    std::string m_token;
-    unsigned    m_prec;
-    token_entry(std::string const & tk, unsigned prec):m_token(tk), m_prec(prec) {}
-};
-
 struct token_state {
     token_table m_table;
     token_state() { m_table = mk_default_token_table(); }
@@ -55,8 +49,12 @@ struct token_config {
 template class scoped_ext<token_config>;
 typedef scoped_ext<token_config> token_ext;
 
+environment add_token(environment const & env, token_entry const & e) {
+    return token_ext::add_entry(env, get_dummy_ios(), e);
+}
+
 environment add_token(environment const & env, char const * val, unsigned prec) {
-    return token_ext::add_entry(env, get_dummy_ios(), token_entry(val, prec));
+    return add_token(env, token_entry(val, prec));
 }
 
 token_table const & get_token_table(environment const & env) {
@@ -132,16 +130,6 @@ struct notation_state {
     }
 };
 
-struct notation_entry {
-    bool             m_is_nud;
-    list<transition> m_transitions;
-    expr             m_expr;
-    bool             m_overload;
-    notation_entry():m_is_nud(true) {}
-    notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload):
-        m_is_nud(is_nud), m_transitions(ts), m_expr(e), m_overload(overload) {}
-};
-
 struct notation_config {
     typedef notation_state  state;
     typedef notation_entry  entry;
@@ -182,12 +170,16 @@ struct notation_config {
 template class scoped_ext<notation_config>;
 typedef scoped_ext<notation_config> notation_ext;
 
+environment add_notation(environment const & env, notation_entry const & e) {
+    return notation_ext::add_entry(env, get_dummy_ios(), e);
+}
+
 environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, bool overload) {
-    return notation_ext::add_entry(env, get_dummy_ios(), notation_entry(true, to_list(ts, ts+num), a, overload));
+    return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload));
 }
 
 environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, bool overload) {
-    return notation_ext::add_entry(env, get_dummy_ios(), notation_entry(false, to_list(ts, ts+num), a, overload));
+    return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload));
 }
 
 environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a, bool overload) {

src/frontends/lean/parser_config.h

@@ -5,12 +5,33 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <string>
 #include "kernel/environment.h"
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/parse_table.h"
 #include "frontends/lean/cmd_table.h"
 
 namespace lean {
+struct token_entry {
+    std::string m_token;
+    unsigned    m_prec;
+    token_entry(std::string const & tk, unsigned prec):m_token(tk), m_prec(prec) {}
+};
+
+struct notation_entry {
+    typedef notation::transition transition;
+    bool             m_is_nud;
+    list<transition> m_transitions;
+    expr             m_expr;
+    bool             m_overload;
+    notation_entry():m_is_nud(true) {}
+    notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload):
+        m_is_nud(is_nud), m_transitions(ts), m_expr(e), m_overload(overload) {}
+};
+
+environment add_token(environment const & env, token_entry const & e);
+environment add_notation(environment const & env, notation_entry const & e);
+
 environment add_token(environment const & env, char const * val, unsigned prec);
 environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, bool overload = true);
 environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, bool overload = true);