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

@@ -123,13 +123,22 @@ optional<expr> 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);
         }
     }
 }

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_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_builtin   = new expr(mk_constant(name(const_name(*g_tactic_expr_type), "builtin")));
-    g_tactic_expr_name   = new name("tactic-expr");
+    g_tactic_expr_list_type = new expr(mk_constant(name(*g_tactic_name, "expr_list")));
-    g_tactic_expr_opcode = new std::string("TACE");
+    g_tactic_expr_name      = new name("tactic-expr");
-    g_tactic_expr_macro  = new macro_definition(new tactic_expr_macro_definition_cell());
+    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;

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<expr> & r, char const * error_msg);

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

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

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,