michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/parse_table): start support for multiple "actions" in parsing tables

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-16 13:51:41 -07:00
parent df1a847255
commit 1d6bebf3a3
4 changed files with 51 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/frontends/lean/notation_cmd.cpp
View file

@ -132,14 +132,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
optional<action> 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<parse_table> 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<parse_table> const & pt, name const &
transition in \c pt, then return the successor table */
static optional<parse_table> find_match(optional<parse_table> 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<parse_table>(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<parse_table>(at.second);
}
}
}
return optional<parse_table>();
}
/** \brief Lift parse_table::find method to optional<parse_table> */
static optional<pair<action, parse_table>> find_next(optional<parse_table> const & pt, name const & tk) {
static list<pair<action, parse_table>> find_next(optional<parse_table> const & pt, name const & tk) {
if (pt)
return pt->find(tk);
else
return optional<pair<action, parse_table>>();
return list<pair<action, parse_table>>();
}
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())) {

43
src/frontends/lean/parse_table.cpp
View file

@ -301,9 +301,9 @@ transition replace(transition const & t, std::function<expr(expr const &)> const
}
struct parse_table::cell {
bool m_nud;
list<pair<unsigned, expr>> m_accept;
name_map<pair<action, parse_table>> m_children;
bool m_nud;
list<pair<unsigned, expr>> m_accept;
name_map<list<pair<action, parse_table>>> 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<pair<action, parse_table>> parse_table::find(name const & tk) const {
auto * it = m_ptr->m_children.find(tk);
list<pair<action, parse_table>> parse_table::find(name const & tk) const {
list<pair<action, parse_table>> const * it = m_ptr->m_children.find(tk);
if (it)
return optional<pair<action, parse_table>>(*it);
return *it;
else
return optional<pair<action, parse_table>>();
return list<pair<action, parse_table>>();
}
list<pair<unsigned, expr>> 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<pair<action, parse_table>> 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<transition> & ts,
list<pair<unsigned, expr>> 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<action, parse_table> 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<pair<action, parse_table>> 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<pair<action, parse_table>> 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);

2
src/frontends/lean/parse_table.h
View file

@ -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<pair<action, parse_table>> find(name const & tk) const;
list<pair<action, parse_table>> find(name const & tk) const;
list<pair<unsigned, expr>> const & is_accepting() const;
void for_each(std::function<void(unsigned, transition const *, list<pair<unsigned, expr>> const &)> const & fn) const;

5
src/frontends/lean/parser.cpp
View file

@ -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<pair<unsigned, expr>> const & as = t.is_accepting();
save_overload_notation(as, p);