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

fix(frontends/lean/parser): macro precedence

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-26 19:17:43 -08:00
parent 3abfad7a88
commit a9ee92aa3f
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1193,6 +1193,8 @@ class parser::imp {
auto it = m_local_decls.find(id);
if (it != m_local_decls.end()) {
return save(mk_app(left, save(mk_var(m_num_local_decls - it->second - 1), p)), p2);
} else if (m_expr_macros && m_expr_macros->find(id) != m_expr_macros->end()) {
return save(mk_app(left, parse_expr_macro(id, p)), p2);
} else {
operator_info op = find_led(m_env, id);
if (op) {
@ -1644,6 +1646,8 @@ class parser::imp {
auto it = m_local_decls.find(id);
if (it != m_local_decls.end()) {
return g_app_precedence;
} else if (m_expr_macros && m_expr_macros->find(id) != m_expr_macros->end()) {
return m_expr_macros->find(id)->second.m_precedence;
} else {
optional<unsigned> prec = get_lbp(m_env, id);
if (prec)