fix(frontends/lean/elaborator): incorrect type information being reports in lean-mode, fixes #241

src/frontends/lean/elaborator.cpp

@@ -121,7 +121,8 @@ optional<expr> elaborator::mvar_to_meta(expr const & mvar) {
 
 /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */
 void elaborator::save_type_data(expr const & e, expr const & r) {
-    if (!m_no_info && infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) {
+    if (!m_no_info && infom() && pip() &&
+        (is_constant(e) || is_local(e) || is_placeholder(e) || is_as_atomic(e))) {
         if (auto p = pip()->get_pos_info(e)) {
             expr t = m_tc[m_relax_main_opaque]->infer(r).first;
             m_pre_info_data.add_type_info(p->first, p->second, t);
@@ -742,9 +743,9 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) {
         return visit(get_annotation_arg(e), cs);
     } else if (is_typed_expr(e)) {
         return visit_typed_expr(e, cs);
-    } else if (is_implicit(e)) {
+    } else if (is_as_atomic(e)) {
         // ignore annotation
-        return visit_core(get_implicit_arg(e), cs);
+        return visit_core(get_as_atomic_arg(e), cs);
     } else if (is_consume_args(e)) {
         // ignore annotation
         return visit_core(get_consume_args_arg(e), cs);
@@ -789,10 +790,10 @@ pair<expr, constraint_seq> elaborator::visit(expr const & e) {
         r    = visit_core(e, cs);
     } else {
         bool consume_args = false;
-        if (is_implicit(e)) {
+        if (is_as_atomic(e)) {
-            r = get_implicit_arg(e);
+            flet<bool> let(m_no_info, true);
+            r = get_as_atomic_arg(e);
             if (is_explicit(r)) r = get_explicit_arg(r);
-            b = r;
             r = visit_core(r, cs);
         } else if (is_consume_args(e)) {
             consume_args = true;

src/frontends/lean/inductive_cmd.cpp

@@ -439,7 +439,7 @@ struct inductive_cmd_fn {
                                  [&](inductive_decl const & d) { return const_name(e) == inductive_decl_name(d); }))
                     return none_expr();
                 // found target
-                expr r = mk_implicit(mk_app(mk_explicit(e), section_params));
+                expr r = mk_as_atomic(mk_app(mk_explicit(e), section_params));
                 return some_expr(r);
             });
     }

src/frontends/lean/notation_cmd.cpp

@@ -56,8 +56,8 @@ environment precedence_cmd(parser & p) {
 
 /** \brief Auxiliary function for #cleanup_section_notation. */
 expr cleanup_section_notation_core(parser & p, expr const & e) {
-    if (is_implicit(e)) {
+    if (is_as_atomic(e)) {
-        return cleanup_section_notation_core(p, get_implicit_arg(e));
+        return cleanup_section_notation_core(p, get_as_atomic_arg(e));
     } else if (is_explicit(e)) {
         return cleanup_section_notation_core(p, get_explicit_arg(e));
     } else if (is_app(e)) {
@@ -96,7 +96,7 @@ expr cleanup_section_notation(parser & p, expr const & e) {
             if (is_local(e))
                 throw parser_error(sstream() << "invalid occurrence of local parameter '" << local_pp_name(e)
                                    << "' in (section) notation", p.pos_of(e));
-            if (is_implicit(e))
+            if (is_as_atomic(e))
                 return some_expr(cleanup_section_notation_core(p, e));
             return none_expr();
         });

src/frontends/lean/parser.cpp

@@ -1066,8 +1066,8 @@ name parser::check_constant_next(char const * msg) {
     name id = check_id_next(msg);
     expr e  = id_to_expr(id, p);
 
-    if (in_section_or_context(m_env) && is_implicit(e)) {
+    if (in_section_or_context(m_env) && is_as_atomic(e)) {
-        e = get_app_fn(get_implicit_arg(e));
+        e = get_app_fn(get_as_atomic_arg(e));
         if (is_explicit(e))
             e = get_explicit_arg(e);
     }
@@ -1423,8 +1423,8 @@ void parser::save_type_info(expr const & e) {
         return;
     if (is_explicit(e)) {
         save_type_info(get_explicit_arg(e));
-    } else if (is_implicit(e)) {
+    } else if (is_as_atomic(e)) {
-        save_type_info(get_implicit_arg(e));
+        save_type_info(get_as_atomic_arg(e));
     } else if (is_choice(e)) {
         for (unsigned i = 0; i < get_num_choices(e); i++)
             save_type_info(get_choice(e, i));

src/frontends/lean/util.cpp

@@ -111,13 +111,13 @@ expr mk_section_local_ref(name const & n, levels const & sec_ls, unsigned num_se
     buffer<expr> params;
     for (unsigned i = 0; i < num_sec_params; i++)
         params.push_back(mk_explicit(sec_params[i]));
-    return mk_implicit(mk_app(mk_explicit(mk_constant(n, sec_ls)), params));
+    return mk_as_atomic(mk_app(mk_explicit(mk_constant(n, sec_ls)), params));
 }
 
 bool is_section_local_ref(expr const & e) {
-    if (!is_implicit(e))
+    if (!is_as_atomic(e))
         return false;
-    expr const & imp_arg = get_implicit_arg(e);
+    expr const & imp_arg = get_as_atomic_arg(e);
     if (!is_app(imp_arg))
         return false;
     buffer<expr> locals;
@@ -136,7 +136,7 @@ expr update_section_local_ref(expr const & e, name_set const & lvls_to_remove, n
     if (locals_to_remove.empty() && lvls_to_remove.empty())
         return e;
     buffer<expr> locals;
-    expr const & f = get_app_args(get_implicit_arg(e), locals);
+    expr const & f = get_app_args(get_as_atomic_arg(e), locals);
     lean_assert(is_explicit(f));
 
     expr new_f;
@@ -165,7 +165,7 @@ expr update_section_local_ref(expr const & e, name_set const & lvls_to_remove, n
     if (locals.empty()) {
         return get_explicit_arg(new_f);
     } else {
-        return mk_implicit(mk_app(new_f, locals));
+        return mk_as_atomic(mk_app(new_f, locals));
     }
 }
 

src/library/annotation.cpp

@@ -62,7 +62,7 @@ expr mk_annotation(name const & kind, expr const & e) {
     annotation_macros & ms = get_annotation_macros();
     auto it = ms.find(kind);
     if (it != ms.end()) {
-        return mk_macro(it->second, 1, &e);
+        return copy_tag(e, mk_macro(it->second, 1, &e));
     } else {
         throw exception(sstream() << "unknown annotation kind '" << kind << "'");
     }

src/library/explicit.cpp

@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name * g_explicit_name = nullptr;
-static name * g_implicit_name = nullptr;
+static name * g_as_atomic_name = nullptr;
 static name * g_as_is_name    = nullptr;
 static name * g_consume_args_name = nullptr;
 
@@ -24,9 +24,9 @@ expr mk_as_is(expr const & e) { return mk_annotation(*g_as_is_name, e); }
 bool is_as_is(expr const & e) { return is_annotation(e, *g_as_is_name); }
 expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return get_annotation_arg(e); }
 
-expr mk_implicit(expr const & e) { return mk_annotation(*g_implicit_name, e); }
+expr mk_as_atomic(expr const & e) { return mk_annotation(*g_as_atomic_name, e); }
-bool is_implicit(expr const & e) { return is_annotation(e, *g_implicit_name); }
+bool is_as_atomic(expr const & e) { return is_annotation(e, *g_as_atomic_name); }
-expr const & get_implicit_arg(expr const & e) { lean_assert(is_implicit(e)); return get_annotation_arg(e); }
+expr const & get_as_atomic_arg(expr const & e) { lean_assert(is_as_atomic(e)); return get_annotation_arg(e); }
 
 expr mk_consume_args(expr const & e) { return mk_annotation(*g_consume_args_name, e); }
 bool is_consume_args(expr const & e) { return is_annotation(e, *g_consume_args_name); }
@@ -34,19 +34,19 @@ expr const & get_consume_args_arg(expr const & e) { lean_assert(is_consume_args(
 
 void initialize_explicit() {
     g_explicit_name     = new name("@");
-    g_implicit_name     = new name("@^-1");
+    g_as_atomic_name    = new name("as_atomic");
     g_as_is_name        = new name("as_is");
     g_consume_args_name = new name("!");
 
     register_annotation(*g_explicit_name);
-    register_annotation(*g_implicit_name);
+    register_annotation(*g_as_atomic_name);
     register_annotation(*g_as_is_name);
     register_annotation(*g_consume_args_name);
 }
 
 void finalize_explicit() {
     delete g_as_is_name;
-    delete g_implicit_name;
+    delete g_as_atomic_name;
     delete g_explicit_name;
     delete g_consume_args_name;
 }

src/library/explicit.h

@@ -33,16 +33,16 @@ bool is_as_is(expr const & e);
 */
 expr const & get_as_is_arg(expr const & e);
 
-/** \brief Create an implicit expression '@^-1 f'.
+/** \brief Create an expression that should be treated as an atom by the elaborator.
-    This only affects the elaborator behavior. This expression "cancels" the effect of '@'
+    This expression also "cancels" the effect of a nested '@'.
 */
-expr mk_implicit(expr const & e);
+expr mk_as_atomic(expr const & e);
-/** \brief Return true iff \c e is an implicit expression. */
+/** \brief Return true iff \c e is an atomic expression. */
-bool is_implicit(expr const & e);
+bool is_as_atomic(expr const & e);
-/** \brief Return the argument of an implicit expression.
+/** \brief Return the argument of an atomic expression.
-    \pre is_implicit(e)
+    \pre is_atomic(e)
 */
-expr const & get_implicit_arg(expr const & e);
+expr const & get_as_atomic_arg(expr const & e);
 
 /** \brief Create the expression '! e'.
     This only affects the elaborator behavior.

tests/lean/interactive/sec_info_bug.input

@@ -0,0 +1,14 @@
+VISIT cat.lean
+SYNC 10
+import logic
+constant category : Type -> Type
+namespace category
+  section
+  parameters {ob : Type} {C : category ob}
+  variables {a b c d : ob}
+  definition hom : ob → ob → Type := let aux := C in sorry
+  definition foo := hom
+  end
+end category
+WAIT
+INFO 8

tests/lean/interactive/sec_info_bug.input.expected.out

@@ -0,0 +1,10 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- TYPE|8|20
+ob → ob → Type
+-- ACK
+-- IDENTIFIER|8|20
+hom
+-- ACK
+-- ENDINFO