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

feat(frontends/lean): save transitions instead of actions in notation::parse_table

Browse source
This commit is contained in:
Sebastian Ullrich 2015-09-28 22:43:04 +02:00 committed by Leonardo de Moura
parent 189a300b11
commit 8f96b725e3
4 changed files with 41 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -136,13 +136,13 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
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;
reserved_action = head(ls).first.get_action();
}
} else {
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;
reserved_action = head(ls).first.get_action();
}
}
}
@ -413,8 +413,8 @@ static unsigned get_default_prec(optional<parse_table> const & pt, name const &
return LEAN_DEFAULT_PRECEDENCE;
if (auto ls = pt->find(tk)) {
for (auto at : ls) {
if (at.first.kind() == notation::action_kind::Expr)
return at.first.rbp();
if (at.first.get_action().kind() == notation::action_kind::Expr)
return at.first.get_action().rbp();
}
}
return LEAN_DEFAULT_PRECEDENCE;
@ -426,7 +426,7 @@ static optional<parse_table> find_match(optional<parse_table> const & pt, transi
if (pt) {
if (auto ls = pt->find(new_trans.get_token())) {
for (auto at : ls) {
if (new_trans.get_action().is_equal(at.first))
if (new_trans.get_action().is_equal(at.first.get_action()))
return optional<parse_table>(at.second);
}
}
@ -435,11 +435,11 @@ static optional<parse_table> find_match(optional<parse_table> const & pt, transi
}
/** \brief Lift parse_table::find method to optional<parse_table> */
static list<pair<action, parse_table>> find_next(optional<parse_table> const & pt, name const & tk) {
static list<pair<transition, parse_table>> find_next(optional<parse_table> const & pt, name const & tk) {
if (pt)
return pt->find(tk);
else
return list<pair<action, parse_table>>();
return list<pair<transition, parse_table>>();
}
static unsigned parse_binders_rbp(parser & p) {
@ -514,7 +514,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
name tk = parse_quoted_symbol_or_token(p, new_tokens, used_default, grp);
if (auto at = find_next(reserved_pt, tk)) {
// Remark: we are ignoring multiple actions in the reserved notation table
action const & a = head(at).first;
action const & a = head(at).first.get_action();
reserved_pt = head(at).second;
switch (a.kind()) {
case notation::action_kind::Skip:

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

@ -333,7 +333,7 @@ transition replace(transition const & t, std::function<expr(expr const &)> const
struct parse_table::cell {
bool m_nud;
list<accepting> m_accept;
name_map<list<pair<action, parse_table>>> m_children;
name_map<list<pair<transition, 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) {}
@ -347,12 +347,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); }
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);
list<pair<transition, parse_table>> parse_table::find(name const & tk) const {
list<pair<transition, parse_table>> const * it = m_ptr->m_children.find(tk);
if (it)
return *it;
else
return list<pair<action, parse_table>>();
return list<pair<transition, parse_table>>();
}
list<accepting> const & parse_table::is_accepting() const {
@ -397,9 +397,9 @@ static list<accepting> insert(list<accepting> const & l, unsigned priority, list
}
}
static bool contains_equivalent_action(list<pair<action, parse_table>> const & l, action const & a) {
static bool contains_equivalent_action(list<pair<transition, parse_table>> const & l, action const & a) {
for (auto const & p : l) {
if (p.first.is_equivalent(a))
if (p.first.get_action().is_equivalent(a))
return true;
}
return false;
@ -419,18 +419,18 @@ parse_table parse_table::add_core(unsigned num, transition const * ts, expr cons
r.m_ptr->m_accept = insert(new_accept, priority, postponed, a);
}
} else {
list<pair<action, parse_table>> const * it = r.m_ptr->m_children.find(ts->get_token());
list<pair<transition, parse_table>> const * it = r.m_ptr->m_children.find(ts->get_token());
action const & ts_act = ts->get_action();
action_kind k = ts_act.kind();
if (k == action_kind::Exprs || k == action_kind::ScopedExpr)
post_buffer.push_back(ts_act);
list<pair<action, parse_table>> new_lst;
list<pair<transition, parse_table>> new_lst;
if (it) {
if (contains_equivalent_action(*it, ts_act)) {
buffer<pair<action, parse_table>> tmp;
buffer<pair<transition, parse_table>> tmp;
to_buffer(*it, tmp);
for (pair<action, parse_table> & p : tmp) {
if (p.first.is_equivalent(ts_act)) {
for (pair<transition, parse_table> & p : tmp) {
if (p.first.get_action().is_equivalent(ts_act)) {
p.second = p.second.add_core(num-1, ts+1, a, priority, overload, post_buffer);
break;
}
@ -438,15 +438,15 @@ parse_table parse_table::add_core(unsigned num, transition const * ts, expr cons
new_lst = to_list(tmp);
} else {
// remove incompatible actions
new_lst = filter(*it, [&](pair<action, parse_table> const & p) {
return p.first.is_compatible(ts_act);
new_lst = filter(*it, [&](pair<transition, parse_table> const & p) {
return p.first.get_action().is_compatible(ts_act);
});
parse_table new_child = parse_table().add_core(num-1, ts+1, a, priority, overload, post_buffer);
new_lst = cons(mk_pair(ts_act, new_child), new_lst);
new_lst = cons(mk_pair(*ts, new_child), new_lst);
}
} else {
parse_table new_child = parse_table().add_core(num-1, ts+1, a, priority, overload, post_buffer);
new_lst = to_list(mk_pair(ts_act, new_child));
new_lst = to_list(mk_pair(*ts, new_child));
}
r.m_ptr->m_children.insert(ts->get_token(), new_lst);
}
@ -527,9 +527,9 @@ void parse_table::for_each(buffer<transition> & ts,
list<accepting> 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, list<pair<action, parse_table>> const & lst) {
m_ptr->m_children.for_each([&](name const & k, list<pair<transition, parse_table>> const & lst) {
for (auto const & p : lst) {
ts.push_back(transition(k, p.first));
ts.push_back(p.first);
p.second.for_each(ts, fn);
ts.pop_back();
}
@ -773,11 +773,11 @@ static int merge(lua_State * L) {
}
static int find(lua_State * L) {
list<pair<action, parse_table>> it = to_parse_table(L, 1).find(to_name_ext(L, 2));
list<pair<transition, 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_notation_action(L, p.first.get_action());
push_parse_table(L, p.second);
return 2;
} else {

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

@ -173,7 +173,7 @@ public:
return add(ts.size(), ts.begin(), a, LEAN_DEFAULT_NOTATION_PRIORITY, true);
}
parse_table merge(parse_table const & s, bool overload) const;\
list<pair<action, parse_table>> find(name const & tk) const;
list<pair<transition, parse_table>> find(name const & tk) const;
list<accepting> const & is_accepting() const;
void for_each(std::function<void(unsigned, transition const *, list<accepting> const &)> const & fn) const;

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

@ -1175,9 +1175,9 @@ void parser::process_postponed(buffer<expr> const & args, bool is_left,
}
// Return true iff the current token is the terminator of some Exprs action, and store the matching pair in r
static bool curr_is_terminator_of_exprs_action(parser const & p, list<pair<notation::action, parse_table>> const & lst, pair<notation::action, parse_table> const * & r) {
static bool curr_is_terminator_of_exprs_action(parser const & p, list<pair<notation::transition, parse_table>> const & lst, pair<notation::transition, parse_table> const * & r) {
for (auto const & pr : lst) {
notation::action const & a = pr.first;
notation::action const & a = pr.first.get_action();
if (a.kind() == notation::action_kind::Exprs &&
a.get_terminator() &&
p.curr_is_token(*a.get_terminator())) {
@ -1189,9 +1189,9 @@ static bool curr_is_terminator_of_exprs_action(parser const & p, list<pair<notat
}
// Return true iff \c lst contains a Skip action, and store the matching pair in r.
static bool has_skip(list<pair<notation::action, parse_table>> const & lst, pair<notation::action, parse_table> const * & r) {
static bool has_skip(list<pair<notation::transition, parse_table>> const & lst, pair<notation::transition, parse_table> const * & r) {
for (auto const & p : lst) {
notation::action const & a = p.first;
notation::action const & a = p.first.get_action();
if (a.kind() == notation::action_kind::Skip) {
r = &p;
return true;
@ -1200,9 +1200,9 @@ static bool has_skip(list<pair<notation::action, parse_table>> const & lst, pair
return false;
}
static pair<notation::action, parse_table> const * get_non_skip(list<pair<notation::action, parse_table>> const & lst) {
static pair<notation::transition, parse_table> const * get_non_skip(list<pair<notation::transition, parse_table>> const & lst) {
for (auto const & p : lst) {
notation::action const & a = p.first;
notation::action const & a = p.first.get_action();
if (a.kind() != notation::action_kind::Skip)
return &p;
}
@ -1234,26 +1234,26 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) {
auto r = t.find(get_token_info().value());
if (!r)
break;
pair<notation::action, parse_table> const * curr_pair = nullptr;
pair<notation::transition, parse_table> const * curr_pair = nullptr;
if (tail(r)) {
// There is more than one possible actions.
// In the current implementation, we support the following possible cases (Skip, Expr), (Skip, Exprs) amd (Skip, ScopedExpr)
next();
if (curr_is_terminator_of_exprs_action(*this, r, curr_pair)) {
lean_assert(curr_pair->first.kind() == notation::action_kind::Exprs);
lean_assert(curr_pair->first.get_action().kind() == notation::action_kind::Exprs);
} else if (has_skip(r, curr_pair) && !curr_starts_expr()) {
lean_assert(curr_pair->first.kind() == notation::action_kind::Skip);
lean_assert(curr_pair->first.get_action().kind() == notation::action_kind::Skip);
} else {
curr_pair = get_non_skip(r);
}
} else {
// there is only one possible action
curr_pair = &head(r);
if (curr_pair->first.kind() != notation::action_kind::Ext)
if (curr_pair->first.get_action().kind() != notation::action_kind::Ext)
next();
}
lean_assert(curr_pair);
notation::action const & a = curr_pair->first;
notation::action const & a = curr_pair->first.get_action();
switch (a.kind()) {
case notation::action_kind::Skip:
break;