From fdadada3a970377a6df8afcd629a6f2eab6e84e8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Mar 2017 13:48:21 -0700 Subject: [PATCH] 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 | 8 ++++++-- src/frontends/lean/calc.cpp | 2 +- src/frontends/lean/elaborator.cpp | 4 ++++ src/frontends/lean/parser.cpp | 5 ++++- src/frontends/lean/util.cpp | 22 ++++++++++++++++++++++ src/frontends/lean/util.h | 11 +++++++++++ tests/lean/run/1468.lean | 17 +++++++++++++++++ 7 files changed, 65 insertions(+), 4 deletions(-) create mode 100644 tests/lean/run/1468.lean diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index a35ef53973..0e8b16880d 100644 --- a/library/init/meta/interactive.lean +++ b/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 := diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp index 90bfbc196f..2a100f1778 100644 --- a/src/frontends/lean/calc.cpp +++ b/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 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' " diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3ac30f44e1..ac2936b644 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2808,6 +2808,8 @@ expr elaborator::visit_macro(expr const & e, optional 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); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 2a222ac00f..adee741849 100644 --- a/src/frontends/lean/parser.cpp +++ b/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 const & postponed = a.get_postponed(); if (postponed) { buffer new_args; diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index d366c51887..d9d7b568ce 100644 --- a/src/frontends/lean/util.cpp +++ b/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; } } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 34131b7bbf..9300d84a5e 100644 --- a/src/frontends/lean/util.h +++ b/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(); } diff --git a/tests/lean/run/1468.lean b/tests/lean/run/1468.lean new file mode 100644 index 0000000000..a824a40cb1 --- /dev/null +++ b/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