From dd98c86a79015a7e647dddb165e4348b8b2f8f81 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 1 Aug 2016 23:26:34 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): as_atomic elaboration

---
 src/frontends/lean/elaborator.cpp | 13 +++++++++----
 src/frontends/lean/elaborator.h   |  2 +-
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 7eaa42d368..2d458f0dab 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -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);
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index b203c7e1f6..82a22de913 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -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);