max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/elaborator): as_atomic elaboration

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-01 23:26:34 -07:00
parent 5ffbc2f94e
commit dd98c86a79
2 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/frontends/lean/elaborator.cpp
View file

@ -587,7 +587,7 @@ expr elaborator::visit_function(expr const & fn, bool has_args, expr const & ref
case expr_kind::App: r = visit(fn, none_expr()); break;
case expr_kind::Local: r = fn; break;
case expr_kind::Constant: r = visit_const_core(fn); break;
case expr_kind::Macro: r = visit_macro(fn, none_expr()); break;
case expr_kind::Macro: r = visit_macro(fn, none_expr(), true); break;
case expr_kind::Lambda: r = visit_lambda(fn, none_expr()); break;
case expr_kind::Let: r = visit_let(fn, none_expr()); break;
}
@ -1032,7 +1032,7 @@ expr elaborator::visit_by(expr const & e, optional<expr> const & expected_type)
return mvar;
}
expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_type) {
expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn) {
if (is_as_is(e)) {
return get_as_is_arg(e);
} else if (is_prenum(e)) {
@ -1048,7 +1048,12 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
lean_unreachable();
} else if (is_as_atomic(e)) {
// ignore annotation
return visit(get_as_atomic_arg(e), expected_type);
expr new_e = visit(get_as_atomic_arg(e), none_expr());
if (is_app_fn)
return new_e;
/* If the as_atomic macro is not the the function in a function application, then we need to consume
implicit arguments. */
return visit_default_app_core(new_e, arg_mask::Default, buffer<expr>(), true, expected_type, e);
} else if (is_annotation(e)) {
expr r = visit(get_annotation_arg(e), expected_type);
return update_macro(e, 1, &r);
@ -1181,7 +1186,7 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
case expr_kind::Sort: return visit_sort(e);
case expr_kind::Local: return visit_local(e, expected_type);
case expr_kind::Constant: return visit_constant(e, expected_type);
case expr_kind::Macro: return visit_macro(e, expected_type);
case expr_kind::Macro: return visit_macro(e, expected_type, false);
case expr_kind::Lambda: return visit_lambda(e, expected_type);
case expr_kind::Pi: return visit_pi(e);
case expr_kind::App: return visit_app(e, expected_type);

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

@ -182,7 +182,7 @@ class elaborator {
expr visit_app_core(expr fn, buffer<expr> const & args, optional<expr> const & expected_type, expr const & ref);
expr visit_local(expr const & e, optional<expr> const & expected_type);
expr visit_constant(expr const & e, optional<expr> const & expected_type);
expr visit_macro(expr const & e, optional<expr> const & expected_type);
expr visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn);
expr visit_lambda(expr const & e, optional<expr> const & expected_type);
expr visit_pi(expr const & e);
expr visit_app(expr const & e, optional<expr> const & expected_type);