From 4be05e1d8c49cb334c7650ebea791c521e5b23ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Jun 2014 10:12:04 -0700 Subject: [PATCH] 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 --- src/frontends/lean/notation_cmd.cpp | 97 ++++++++++++++++++++++------ src/frontends/lean/notation_cmd.h | 7 ++ src/frontends/lean/parser.cpp | 26 ++------ src/frontends/lean/parser_config.cpp | 30 ++++----- src/frontends/lean/parser_config.h | 21 ++++++ 5 files changed, 123 insertions(+), 58 deletions(-) diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index ad50a4b01..6c695225e 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/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 #include #include #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> 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 prec = parse_optional_precedence(p); - environment env = p.env(); + environment const & env = p.env(); + optional 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(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(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(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 & 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 & 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 & locals) { } } -static action parse_action(parser & p, environment & env, buffer & locals) { +static action parse_action(parser & p, buffer & locals, buffer & 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 & 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 & locals) } } -environment notation_cmd_core(parser & p, bool overload) { - environment env = p.env(); +notation_entry parse_notation_core(parser & p, bool overload, buffer & new_tokens) { buffer locals; buffer 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 add_nud_notation(env, ts.size(), ts.data(), n, overload); - else - return add_led_notation(env, ts.size(), ts.data(), n, overload); + return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload); +} + +environment notation_cmd_core(parser & p, bool overload) { + environment env = p.env(); + buffer 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 & 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()); + } } } diff --git a/src/frontends/lean/notation_cmd.h b/src/frontends/lean/notation_cmd.h index 5ce25abdf..7f004107d 100644 --- a/src/frontends/lean/notation_cmd.h +++ b/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 & new_tokens); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 78df97f7d..11be93a85 100644 --- a/src/frontends/lean/parser.cpp +++ b/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 & r) { } bool parser::parse_local_notation_decl() { - if (curr_is_token(g_infix) || curr_is_token(g_infixl)) { - next(); - m_env = infixl_cmd_core(*this, false); - return true; - } else if (curr_is_token(g_infixr)) { - next(); - 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); + if (curr_is_notation_decl(*this)) { + buffer new_tokens; + auto ne = ::lean::parse_notation(*this, false, new_tokens); + for (auto const & te : new_tokens) + m_env = add_token(m_env, te); + m_env = add_notation(m_env, ne); return true; } else { return false; diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 2e06866c7..4ba12986d 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/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; typedef scoped_ext 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 m_transitions; - expr m_expr; - bool m_overload; - notation_entry():m_is_nud(true) {} - notation_entry(bool is_nud, list 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; typedef scoped_ext 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 const & ts, expr const & a, bool overload) { diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h index 672bf143d..ddc75d0d4 100644 --- a/src/frontends/lean/parser_config.h +++ b/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 #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 m_transitions; + expr m_expr; + bool m_overload; + notation_entry():m_is_nud(true) {} + notation_entry(bool is_nud, list 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);