From 83e4c0fcec497af9f4d71cd5b22b839d7b0f4198 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Oct 2014 22:32:52 -0700 Subject: [PATCH] feat(frontends/lean): hide tactic "types" it is not very useful to display the type of tactics (e.g., apply, intros, ...) --- src/frontends/lean/elaborator.cpp | 14 ++++++++++++-- src/library/tactic/expr_to_tactic.cpp | 14 +++++++++----- src/library/tactic/expr_to_tactic.h | 1 + .../lean/interactive/apply_info.input.expected.out | 12 ------------ .../proof_state_info.input.expected.out | 3 --- .../proof_state_info2.input.expected.out | 9 --------- 6 files changed, 22 insertions(+), 31 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index bd98fdf2a..3e898c155 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -123,13 +123,22 @@ optional elaborator::mvar_to_meta(expr const & mvar) { return none_expr(); } +static bool is_tactic_type(expr const & e) { + expr const * it = &e; + while (is_pi(*it)) { + it = &binding_body(*it); + } + return *it == get_tactic_type() || *it == get_tactic_expr_type() || *it == get_tactic_expr_list_type(); +} + /** \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) || is_as_atomic(e) || is_consume_args(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); + if (!is_tactic_type(t)) + m_pre_info_data.add_type_info(p->first, p->second, t); } } } @@ -148,7 +157,8 @@ void elaborator::save_extra_type_data(expr const & e, expr const & r) { if (!m_no_info && infom() && pip()) { if (auto p = pip()->get_pos_info(e)) { expr t = m_tc[m_relax_main_opaque]->infer(r).first; - m_pre_info_data.add_extra_type_info(p->first, p->second, r, t); + if (!is_tactic_type(t)) + m_pre_info_data.add_extra_type_info(p->first, p->second, r, t); } } } diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 517477cd8..700387f8a 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -59,9 +59,11 @@ bool has_tactic_decls(environment const & env) { static expr * g_tactic_expr_type = nullptr; static expr * g_tactic_expr_builtin = nullptr; +static expr * g_tactic_expr_list_type = nullptr; expr const & get_tactic_expr_type() { return *g_tactic_expr_type; } expr const & get_tactic_expr_builtin() { return *g_tactic_expr_builtin; } +expr const & get_tactic_expr_list_type() { return *g_tactic_expr_list_type; } static name * g_tactic_expr_name = nullptr; static std::string * g_tactic_expr_opcode = nullptr; @@ -286,11 +288,12 @@ void initialize_expr_to_tactic() { g_tactic_name = new name("tactic"); - g_tactic_expr_type = new expr(mk_constant(name(*g_tactic_name, "expr"))); - g_tactic_expr_builtin = new expr(mk_constant(name(const_name(*g_tactic_expr_type), "builtin"))); - g_tactic_expr_name = new name("tactic-expr"); - g_tactic_expr_opcode = new std::string("TACE"); - g_tactic_expr_macro = new macro_definition(new tactic_expr_macro_definition_cell()); + g_tactic_expr_type = new expr(mk_constant(name(*g_tactic_name, "expr"))); + g_tactic_expr_builtin = new expr(mk_constant(name(const_name(*g_tactic_expr_type), "builtin"))); + g_tactic_expr_list_type = new expr(mk_constant(name(*g_tactic_name, "expr_list"))); + g_tactic_expr_name = new name("tactic-expr"); + g_tactic_expr_opcode = new std::string("TACE"); + g_tactic_expr_macro = new macro_definition(new tactic_expr_macro_definition_cell()); register_macro_deserializer(*g_tactic_expr_opcode, [](deserializer &, unsigned num, expr const * args) { @@ -362,6 +365,7 @@ void finalize_expr_to_tactic() { delete g_expr_list_nil; delete g_tactic_expr_type; delete g_tactic_expr_builtin; + delete g_tactic_expr_list_type; delete g_tactic_expr_name; delete g_tactic_expr_opcode; delete g_tactic_expr_macro; diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index 672545520..d596ebcf8 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -32,6 +32,7 @@ expr mk_tactic_expr(expr const & e); bool is_tactic_expr(expr const & e); expr const & get_tactic_expr_expr(expr const & e); void check_tactic_expr(expr const & e, char const * msg); +expr const & get_tactic_expr_list_type(); name const & tactic_expr_to_id(expr e, char const * error_msg); void get_tactic_expr_list_elements(expr l, buffer & r, char const * error_msg); diff --git a/tests/lean/interactive/apply_info.input.expected.out b/tests/lean/interactive/apply_info.input.expected.out index 886451aa6..0f0f3a14f 100644 --- a/tests/lean/interactive/apply_info.input.expected.out +++ b/tests/lean/interactive/apply_info.input.expected.out @@ -1,9 +1,6 @@ -- BEGINWAIT -- ENDWAIT -- BEGININFO --- TYPE|7|1 -tactic.expr → tactic --- ACK -- IDENTIFIER|7|1 tactic.apply -- ACK @@ -13,14 +10,8 @@ a -- IDENTIFIER|7|7 Ha -- ACK --- TYPE|7|9 -tactic --- ACK -- ENDINFO -- BEGININFO --- TYPE|16|1 -tactic.expr → tactic --- ACK -- IDENTIFIER|16|1 tactic.apply -- ACK @@ -30,7 +21,4 @@ b -- IDENTIFIER|16|7 Hb -- ACK --- TYPE|16|9 -tactic --- ACK -- ENDINFO diff --git a/tests/lean/interactive/proof_state_info.input.expected.out b/tests/lean/interactive/proof_state_info.input.expected.out index 4f426b6fc..fb871341a 100644 --- a/tests/lean/interactive/proof_state_info.input.expected.out +++ b/tests/lean/interactive/proof_state_info.input.expected.out @@ -1,9 +1,6 @@ -- BEGINWAIT -- ENDWAIT -- BEGININFO --- TYPE|7|2 -tactic --- ACK -- IDENTIFIER|7|2 tactic.info -- ACK diff --git a/tests/lean/interactive/proof_state_info2.input.expected.out b/tests/lean/interactive/proof_state_info2.input.expected.out index d3ef665db..c9865cc11 100644 --- a/tests/lean/interactive/proof_state_info2.input.expected.out +++ b/tests/lean/interactive/proof_state_info2.input.expected.out @@ -1,9 +1,6 @@ -- BEGINWAIT -- ENDWAIT -- BEGININFO --- TYPE|5|17 -tactic --- ACK -- PROOF_STATE|5|17 a : Prop, b : Prop, @@ -14,9 +11,6 @@ Hb : b -- ACK -- ENDINFO -- BEGININFO --- TYPE|6|17 -tactic --- ACK -- PROOF_STATE|6|17 a : Prop, b : Prop, @@ -34,9 +28,6 @@ Hb : b -- ACK -- ENDINFO -- BEGININFO --- TYPE|7|10 -tactic --- ACK -- PROOF_STATE|7|10 a : Prop, b : Prop,