From 30cea2dcebb828bbf118007cc201e00eb3738d84 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Jan 2017 18:38:31 -0800 Subject: [PATCH] fix(frontends/lean): auxiliary bind-application in do-notation was not allowing us to obtain type information for the monadic actions. The new test exposes the problem. --- src/frontends/lean/builtin_exprs.cpp | 10 +++++++--- src/frontends/lean/elaborator.cpp | 3 +++ src/frontends/lean/init_module.cpp | 3 +++ src/frontends/lean/util.cpp | 16 ++++++++++++++++ src/frontends/lean/util.h | 6 ++++++ tests/lean/interactive/do_info.lean | 16 ++++++++++++++++ tests/lean/interactive/do_info.lean.expected.out | 7 +++++++ 7 files changed, 58 insertions(+), 3 deletions(-) create mode 100644 tests/lean/interactive/do_info.lean create mode 100644 tests/lean/interactive/do_info.lean.expected.out diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index d701620a1d..cdc731d30a 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -471,6 +471,10 @@ static std::tuple, expr, expr, optional> parse_do_action(pa return std::make_tuple(lhs, type, curr, else_case); } +static expr mk_bind_fn() { + return mk_no_info(mk_constant(get_bind_name())); +} + static expr parse_do(parser & p, unsigned, expr const *, pos_info const &) { parser::local_scope scope(p); buffer es; @@ -524,7 +528,7 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const &) { --i; if (auto lhs = lhss[i]) { if (is_local(*lhs)) { - r = p.rec_save_pos(mk_app(p.save_pos(mk_constant(get_bind_name()), ps[i]), es[i], Fun(*lhs, r, p)), ps[i]); + r = p.rec_save_pos(mk_app(p.save_pos(mk_bind_fn(), ps[i]), es[i], Fun(*lhs, r, p)), ps[i]); } else { // must introduce a "fake" match auto pos = ps[i]; @@ -546,13 +550,13 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const &) { expr eqns = p.save_pos(mk_equations(h, eqs.size(), eqs.data()), pos); expr local = mk_local("p", mk_expr_placeholder()); expr match = p.mk_app(eqns, local, pos); - r = p.rec_save_pos(mk_app(p.save_pos(mk_constant(get_bind_name()), ps[i]), + r = p.rec_save_pos(mk_app(p.save_pos(mk_bind_fn(), ps[i]), es[i], p.save_pos(Fun(local, match, p), pos)), pos); } } else { - r = p.rec_save_pos(mk_app(p.save_pos(mk_constant(get_bind_name()), ps[i]), + r = p.rec_save_pos(mk_app(p.save_pos(mk_bind_fn(), ps[i]), es[i], p.save_pos(mk_lambda("x", mk_expr_placeholder(), r), p.pos_of(r))), ps[i]); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 8166a1554c..f29e202c49 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2380,6 +2380,9 @@ expr elaborator::visit(expr const & e, optional const & expected_type) { return copy_tag(e, visit_have_expr(e, expected_type)); } else if (is_suffices_annotation(e)) { return copy_tag(e, visit_suffices_expr(e, expected_type)); + } else if (is_no_info(e)) { + flet set(m_no_info, true); + return visit(get_annotation_arg(e), expected_type); } else { switch (e.kind()) { case expr_kind::Var: lean_unreachable(); // LCOV_EXCL_LINE diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 2c038d02b2..ac95fba605 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -23,6 +23,7 @@ Author: Leonardo de Moura #include "frontends/lean/notation_cmd.h" #include "frontends/lean/tactic_notation.h" #include "frontends/lean/decl_attributes.h" +#include "frontends/lean/util.h" namespace lean { void initialize_frontend_lean_module() { @@ -45,8 +46,10 @@ void initialize_frontend_lean_module() { initialize_elaborator(); initialize_notation_cmd(); initialize_tactic_notation(); + initialize_frontend_lean_util(); } void finalize_frontend_lean_module() { + finalize_frontend_lean_util(); finalize_tactic_notation(); finalize_notation_cmd(); finalize_elaborator(); diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 60269238dc..79dec9462b 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "kernel/error_msgs.h" #include "kernel/for_each_fn.h" #include "library/scoped_ext.h" +#include "library/annotation.h" #include "library/locals.h" #include "library/explicit.h" #include "library/aliases.h" @@ -348,4 +349,19 @@ expr quote_name(name const & n) { lean_unreachable(); } } + +static name * g_no_info = nullptr; +name const & get_no_info() { return *g_no_info; } + +expr mk_no_info(expr const & e) { return mk_annotation(get_no_info(), e); } +bool is_no_info(expr const & e) { return is_annotation(e, get_no_info()); } + +void initialize_frontend_lean_util() { + g_no_info = new name("no_info"); + register_annotation(*g_no_info); +} + +void finalize_frontend_lean_util() { + delete g_no_info; +} } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index d23d139f8d..a6837e96ce 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -106,4 +106,10 @@ pair parse_option_name(parser & p, char const * error_msg); expr mk_tactic_unit(); expr quote_name(name const & n); + +expr mk_no_info(expr const & e); +bool is_no_info(expr const & e); + +void initialize_frontend_lean_util(); +void finalize_frontend_lean_util(); } diff --git a/tests/lean/interactive/do_info.lean b/tests/lean/interactive/do_info.lean new file mode 100644 index 0000000000..668710cd7a --- /dev/null +++ b/tests/lean/interactive/do_info.lean @@ -0,0 +1,16 @@ +open tactic + +example (a b c : nat) : a = b → c = b → a = c := +by do + h ← intro `h, + --^ "command": "info" + intros, + transitivity, +--^ "command": "info" + trace_state, + assumption, +--^ "command": "info" + symmetry, +--^ "command": "info" + assumption +--^ "command": "info" diff --git a/tests/lean/interactive/do_info.lean.expected.out b/tests/lean/interactive/do_info.lean.expected.out new file mode 100644 index 0000000000..ad221ddfab --- /dev/null +++ b/tests/lean/interactive/do_info.lean.expected.out @@ -0,0 +1,7 @@ +{"msg":{"caption":"trace output","file_name":"f","pos_col":3,"pos_line":4,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"},"response":"additional_message"} +{"message":"file invalidated","response":"ok","seq_num":0} +{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":422},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6} +{"record":{"full-id":"tactic.transitivity","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":30},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":9} +{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":529},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12} +{"record":{"full-id":"tactic.symmetry","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":27},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":14} +{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":529},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16}