From 1d6bebf3a39328d70fe79fcd354472a6505fe5a2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 16 Aug 2015 13:51:41 -0700 Subject: [PATCH] feat(frontends/lean/parse_table): start support for multiple "actions" in parsing tables --- src/frontends/lean/notation_cmd.cpp | 39 +++++++++++++++----------- src/frontends/lean/parse_table.cpp | 43 ++++++++++++++++------------- src/frontends/lean/parse_table.h | 2 +- src/frontends/lean/parser.cpp | 5 ++-- 4 files changed, 51 insertions(+), 38 deletions(-) diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index a126575e1..cb0c52ecd 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -132,14 +132,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota optional reserved_action; if (grp == notation_entry_group::Main) { if (k == mixfix_kind::prefix) { - if (auto at = get_reserved_nud_table(p.env()).find(tks)) { - reserved_pt = at->second; - reserved_action = at->first; + if (auto ls = get_reserved_nud_table(p.env()).find(tks)) { + // Remark: we are ignoring multiple actions in the reserved notation table + reserved_pt = head(ls).second; + reserved_action = head(ls).first; } } else { - if (auto at = get_reserved_led_table(p.env()).find(tks)) { - reserved_pt = at->second; - reserved_action = at->first; + if (auto ls = get_reserved_led_table(p.env()).find(tks)) { + // Remark: we are ignoring multiple actions in the reserved notation table + reserved_pt = head(ls).second; + reserved_action = head(ls).first; } } } @@ -408,9 +410,11 @@ static action parse_action(parser & p, name const & prev_token, unsigned default static unsigned get_default_prec(optional const & pt, name const & tk) { if (!pt) return LEAN_DEFAULT_PRECEDENCE; - if (auto at = pt->find(tk)) { - if (at->first.kind() == notation::action_kind::Expr) - return at->first.rbp(); + if (auto ls = pt->find(tk)) { + for (auto at : ls) { + if (at.first.kind() == notation::action_kind::Expr) + return at.first.rbp(); + } } return LEAN_DEFAULT_PRECEDENCE; } @@ -419,20 +423,22 @@ static unsigned get_default_prec(optional const & pt, name const & transition in \c pt, then return the successor table */ static optional find_match(optional const & pt, transition const & new_trans) { if (pt) { - if (auto at = pt->find(new_trans.get_token())) { - if (new_trans.get_action().is_equal(at->first)) - return optional(at->second); + if (auto ls = pt->find(new_trans.get_token())) { + for (auto at : ls) { + if (new_trans.get_action().is_equal(at.first)) + return optional(at.second); + } } } return optional(); } /** \brief Lift parse_table::find method to optional */ -static optional> find_next(optional const & pt, name const & tk) { +static list> find_next(optional const & pt, name const & tk) { if (pt) return pt->find(tk); else - return optional>(); + return list>(); } static unsigned parse_binders_rbp(parser & p) { @@ -506,8 +512,9 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en (grp == notation_entry_group::Reserve && !p.curr_is_command() && !p.curr_is_eof())) { name tk = parse_quoted_symbol_or_token(p, new_tokens, used_default, grp); if (auto at = find_next(reserved_pt, tk)) { - action const & a = at->first; - reserved_pt = at->second; + // Remark: we are ignoring multiple actions in the reserved notation table + action const & a = head(at).first; + reserved_pt = head(at).second; switch (a.kind()) { case notation::action_kind::Skip: if (!p.curr_is_quoted_symbol() && !p.curr_is_keyword() && !p.curr_is_token(get_assign_tk())) { diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp index 0a9d972db..4c47e92ee 100644 --- a/src/frontends/lean/parse_table.cpp +++ b/src/frontends/lean/parse_table.cpp @@ -301,9 +301,9 @@ transition replace(transition const & t, std::function const } struct parse_table::cell { - bool m_nud; - list> m_accept; - name_map> m_children; + bool m_nud; + list> m_accept; + name_map>> m_children; MK_LEAN_RC(); // Declare m_rc counter void dealloc() { delete this; } cell(bool nud = true):m_nud(nud), m_rc(1) {} @@ -317,12 +317,12 @@ parse_table::parse_table(parse_table && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } parse_table::~parse_table() { if (m_ptr) m_ptr->dec_ref(); } parse_table & parse_table::operator=(parse_table const & s) { LEAN_COPY_REF(s); } parse_table & parse_table::operator=(parse_table && s) { LEAN_MOVE_REF(s); } -optional> parse_table::find(name const & tk) const { - auto * it = m_ptr->m_children.find(tk); +list> parse_table::find(name const & tk) const { + list> const * it = m_ptr->m_children.find(tk); if (it) - return optional>(*it); + return *it; else - return optional>(); + return list>(); } list> const & parse_table::is_accepting() const { @@ -378,11 +378,12 @@ parse_table parse_table::add_core(unsigned num, transition const * ts, expr cons r.m_ptr->m_accept = insert(new_accept, priority, a); } } else { - auto * it = r.m_ptr->m_children.find(ts->get_token()); + list> const * it = r.m_ptr->m_children.find(ts->get_token()); parse_table new_child; if (it) { - action const & act = it->first; - parse_table const & child = it->second; + // TODO(Leo): support multiple actions + action const & act = head(*it).first; + parse_table const & child = head(*it).second; if (act.is_equal(ts->get_action())) { new_child = child.add_core(num-1, ts+1, a, priority, overload); } else { @@ -391,7 +392,7 @@ parse_table parse_table::add_core(unsigned num, transition const * ts, expr cons } else { new_child = parse_table().add_core(num-1, ts+1, a, priority, overload); } - r.m_ptr->m_children.insert(ts->get_token(), mk_pair(ts->get_action(), new_child)); + r.m_ptr->m_children.insert(ts->get_token(), to_list(mk_pair(ts->get_action(), new_child))); } return r; } @@ -469,10 +470,12 @@ void parse_table::for_each(buffer & ts, list> const &)> const & fn) const { if (!is_nil(m_ptr->m_accept)) fn(ts.size(), ts.data(), m_ptr->m_accept); - m_ptr->m_children.for_each([&](name const & k, pair const & p) { - ts.push_back(transition(k, p.first)); - p.second.for_each(ts, fn); - ts.pop_back(); + m_ptr->m_children.for_each([&](name const & k, list> const & lst) { + for (auto const & p : lst) { + ts.push_back(transition(k, p.first)); + p.second.for_each(ts, fn); + ts.pop_back(); + } }); } @@ -713,10 +716,12 @@ static int merge(lua_State * L) { } static int find(lua_State * L) { - auto p = to_parse_table(L, 1).find(to_name_ext(L, 2)); - if (p) { - push_notation_action(L, p->first); - push_parse_table(L, p->second); + list> it = to_parse_table(L, 1).find(to_name_ext(L, 2)); + if (it) { + // TODO(Leo): support multiple actions + auto p = head(it); + push_notation_action(L, p.first); + push_parse_table(L, p.second); return 2; } else { return push_nil(L); diff --git a/src/frontends/lean/parse_table.h b/src/frontends/lean/parse_table.h index c996bb12d..e14f4718e 100644 --- a/src/frontends/lean/parse_table.h +++ b/src/frontends/lean/parse_table.h @@ -157,7 +157,7 @@ public: return add(ts.size(), ts.begin(), a, LEAN_DEFAULT_NOTATION_PRIORITY, true); } parse_table merge(parse_table const & s, bool overload) const; - optional> find(name const & tk) const; + list> find(name const & tk) const; list> const & is_accepting() const; void for_each(std::function> const &)> const & fn) const; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 58df565cd..a64733075 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1086,7 +1086,8 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) { auto r = t.find(get_token_info().value()); if (!r) break; - notation::action const & a = r->first; + // TODO(Leo): handle multiple actions + notation::action const & a = head(r).first; switch (a.kind()) { case notation::action_kind::Skip: next(); @@ -1214,7 +1215,7 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) { break; } - t = r->second; + t = head(r).second; // TODO(Leo): } list> const & as = t.is_accepting(); save_overload_notation(as, p);