fix(frontends/lean): fixes #1468

@kha I had to add yet another hack to fix this issue.

In notation declarations, names are resolved at notation declaration time.
So, users do not expect them to be resolved again at tactic execution time.

I addressed this problem by wrapping constants occurring in notation
declarations with a "frozen_name" annotation. This transformation is
only performed if m_in_quote is true.
Then resolve_names_fn at elaborator.cpp will not try to resolve the
names again.

This change broke two other modules. `-` notation for inverting
equations at `rw`, and `calc` expressions inside quotes.
The broke for the same reason. They were not expecting the constants
to be wrapped with an annotation.

library/init/meta/interactive.lean

@@ -253,8 +253,12 @@ private meta def is_neg (p : pexpr) : option pexpr :=
 /- Remark: we use the low-level to_raw_expr and of_raw_expr to be able to
    pattern match pre-terms. This is a low-level trick (aka hack). -/
 match pexpr.to_raw_expr p with
-| (app (const c []) arg) := if c = `neg then some (pexpr.of_raw_expr arg) else none
-| _                      := none
+| (app fn arg) :=
+  match fn^.erase_annotations with
+  | (const `neg _) := some (pexpr.of_raw_expr arg)
+  | _              := none
+  end
+| _            := none
 end
 
 private meta def resolve_name' (n : name) : tactic expr :=

src/frontends/lean/calc.cpp

@@ -55,7 +55,7 @@ static calc_pred decode_expr(expr const & e, pos_info const & pos) {
         throw parser_error("invalid 'calc' expression, overloaded expressions are not supported", pos);
     } else {
         buffer<expr> args;
-        expr const & fn = get_app_args(e, args);
+        expr const & fn = get_nested_annotation_arg(get_app_args(e, args));
         unsigned nargs  = args.size();
         if (!is_constant(fn) || nargs < 2) {
             throw parser_error("invalid 'calc' expression, expression must be a function application 'f a_1 ... a_k' "

src/frontends/lean/elaborator.cpp

@@ -2808,6 +2808,8 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
         return mk_sorry(expected_type, e);
     } else if (is_structure_instance(e)) {
         return visit_structure_instance(e, expected_type);
+    } else if (is_frozen_name(e)) {
+        return visit(get_annotation_arg(e), expected_type);
     } else if (is_annotation(e)) {
         expr r = visit(get_annotation_arg(e), expected_type);
         return update_macro(e, 1, &r);
@@ -3706,6 +3708,8 @@ struct resolve_names_fn : public replace_visitor {
             return e;
         } else if (is_choice(e)) {
             return visit_choice(e);
+        } else if (is_frozen_name(e)) {
+            return get_annotation_arg(e);
         } else {
             return replace_visitor::visit(e);
         }

src/frontends/lean/parser.cpp

@@ -1438,7 +1438,10 @@ expr parser::parse_notation(parse_table t, expr * left) {
         }
     }
     for (notation::accepting const & a : as) {
-        expr r = copy_with_new_pos(a.get_expr(), p);
+        expr a_expr = a.get_expr();
+        if (m_in_quote)
+            a_expr = freeze_names(a_expr);
+        expr r = copy_with_new_pos(a_expr, p);
         list<notation::action> const & postponed = a.get_postponed();
         if (postponed) {
             buffer<expr> new_args;

src/frontends/lean/util.cpp

@@ -392,12 +392,34 @@ expr parse_auto_param(parser & p, expr const & type) {
     return mk_auto_param(type, const_name(tac_expr));
 }
 
+static name * g_frozen_name = nullptr;
+
+expr mk_frozen_name_annotation(expr const & e) {
+    return mk_annotation(*g_frozen_name, e);
+}
+
+bool is_frozen_name(expr const & e) {
+    return is_annotation(e, *g_frozen_name);
+}
+
+expr freeze_names(expr const & e) {
+    return replace(e, [&](expr const e, unsigned) {
+            if (is_local(e) || is_constant(e))
+                return some_expr(mk_frozen_name_annotation(e));
+            else
+                return none_expr();
+        });
+}
+
 void initialize_frontend_lean_util() {
     g_no_info = new name("no_info");
     register_annotation(*g_no_info);
+    g_frozen_name = new name("frozen_name");
+    register_annotation(*g_frozen_name);
 }
 
 void finalize_frontend_lean_util() {
     delete g_no_info;
+    delete g_frozen_name;
 }
 }

src/frontends/lean/util.h

@@ -117,6 +117,17 @@ expr mk_opt_param(expr const & t, expr const & val);
 expr mk_auto_param(expr const & t, name const & tac_name);
 expr parse_auto_param(parser & p, expr const & type);
 
+/* Add frozen annotation around constants and local constants occurring in \c e.
+   This annotation is used to prevent lean from resolving the names again
+   at tactic execution time. See resolve_names_fn at elaborator.cpp.
+
+   In notation declarations, names are resolved at notation declaration time.
+   Users do not expect them to be resolved again at tactic execution time.
+   See issue #1468. */
+expr freeze_names(expr const & e);
+/* Return true iff \c e is marked with a frozen_name annotation. */
+bool is_frozen_name(expr const & e);
+
 void initialize_frontend_lean_util();
 void finalize_frontend_lean_util();
 }

tests/lean/run/1468.lean

@@ -0,0 +1,17 @@
+local infix * := _root_.mul
+
+namespace Y
+def mul : bool → bool := λ b, b
+
+example (m n : ℕ) : true :=
+begin
+definev k : ℕ := m * n,
+definev a : bool := mul tt,
+trivial
+end
+end Y
+
+
+meta def is_mul : expr → option (expr × expr)
+| ```(%%a * %%b) := some (a, b)
+| _              := none