feat(frontends/lean/builtin_cmds): remove workaround for getting nice metavariable names in the check command

We don't need it anymore after previous commit 2a16050

src/frontends/lean/builtin_cmds.cpp

@@ -205,28 +205,6 @@ environment end_scoped_cmd(parser & p) {
 /** \brief Auxiliary function for check/eval */
 static std::tuple<expr, level_param_names> parse_local_expr(parser & p) {
     expr e   = p.parse_expr();
-    environment const & env = p.env();
-    if (is_constant(e) && !const_levels(e)) {
-        // manually elaborate simple constant using nicer names for meta-variables
-        if (auto decl = env.find(const_name(e))) {
-            levels ls = param_names_to_levels(decl->get_univ_params());
-            e         = mk_constant(const_name(e), ls);
-            expr type = instantiate_type_univ_params(*decl, ls);
-            while (true) {
-                if (!is_pi(type))
-                    break;
-                if (is_explicit(binding_info(type)))
-                    break;
-                std::string q("?");
-                q += binding_name(type).to_string();
-                name n = pick_unused_name(binding_body(type), name(q.c_str()));
-                expr m = mk_local(n, binding_domain(type));
-                type   = instantiate(binding_body(type), m);
-                e      = mk_app(e, m);
-            }
-            return std::make_tuple(e, decl->get_univ_params());
-        }
-    }
     list<expr> ctx = p.locals_to_context();
     level_param_names new_ls;
     std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);

src/frontends/lean/elaborator.cpp

@@ -88,7 +88,7 @@ struct elaborator::choice_expr_elaborator : public choice_iterator {
     }
 };
 
-elaborator::elaborator(elaborator_context & ctx, name_generator const & ngen):
+elaborator::elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names):
     m_ctx(ctx),
     m_ngen(ngen),
     m_context(),
@@ -100,6 +100,7 @@ elaborator::elaborator(elaborator_context & ctx, name_generator const & ngen):
     m_no_info = false;
     m_tc[0]  = mk_type_checker(ctx.m_env, m_ngen.mk_child(), false);
     m_tc[1]  = mk_type_checker(ctx.m_env, m_ngen.mk_child(), true);
+    m_nice_mvar_names = nice_mvar_names;
 }
 
 expr elaborator::mk_local(name const & n, expr const & t, binder_info const & bi) {
@@ -218,7 +219,7 @@ void elaborator::copy_info_to_manager(substitution s) {
 }
 
 optional<name> elaborator::mk_mvar_suffix(expr const & b) {
-    if (!infom())
+    if (!infom() && !m_nice_mvar_names)
         return optional<name>();
     else
         return optional<name>(binding_name(b));
@@ -1270,8 +1271,8 @@ pair<expr, constraints> elaborator::elaborate_nested(list<expr> const & ctx, exp
 static name * g_tmp_prefix = nullptr;
 
 std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
-                                              bool relax_main_opaque, bool ensure_type) {
+                                              bool relax_main_opaque, bool ensure_type, bool nice_mvar_names) {
-    return elaborator(env, name_generator(*g_tmp_prefix))(ctx, e, ensure_type, relax_main_opaque);
+    return elaborator(env, name_generator(*g_tmp_prefix), nice_mvar_names)(ctx, e, ensure_type, relax_main_opaque);
 }
 
 std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,

src/frontends/lean/elaborator.h

@@ -56,6 +56,9 @@ class elaborator : public coercion_info_manager {
     info_manager         m_pre_info_data;
     bool                 m_has_sorry;
     unifier_config       m_unifier_config;
+    // If m_nice_mvar_names is true, we append (when possible) a more informative name for a metavariable.
+    // That is, whenever a metavariables comes from a binding, we add the binding name as a suffix
+    bool                 m_nice_mvar_names;
     struct choice_expr_elaborator;
 
     environment const & env() const { return m_ctx.m_env; }
@@ -147,14 +150,14 @@ class elaborator : public coercion_info_manager {
     pair<expr, constraints> elaborate_nested(list<expr> const & g, expr const & e,
                                              bool relax, bool use_tactic_hints);
 public:
-    elaborator(elaborator_context & ctx, name_generator const & ngen);
+    elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names = false);
     std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type,
                                                    bool relax_main_opaque);
     std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n, bool is_opaque);
 };
 
 std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
-                                              bool relax_main_opaque, bool ensure_type = false);
+                                              bool relax_main_opaque, bool ensure_type = false, bool nice_mvar_names = false);
 
 std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,
                                                     bool is_opaque);

src/frontends/lean/parser.cpp

@@ -634,9 +634,10 @@ std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, li
     bool relax            = true;
     bool check_unassigned = false;
     bool ensure_type      = false;
+    bool nice_mvar_names  = true;
     parser_pos_provider pp = get_pos_provider();
     elaborator_context env = mk_elaborator_context(pp, check_unassigned);
-    auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
+    auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type, nice_mvar_names);
     m_pre_info_manager.clear();
     return r;
 }

tests/lean/check.lean.expected.out

@@ -1,4 +1,4 @@
 and.intro : ?a → ?b → ?a ∧ ?b
 or.elim : ?a ∨ ?b → (?a → ?c) → (?b → ?c) → ?c
 eq : ?A → ?A → Prop
-eq.rec : ?C ?a → (Π {a : ?A}, ?a = a → ?C a)
+eq.rec : ?C → (Π {a : ?A}, ?a = a → ?C)

tests/lean/check2.lean.expected.out

@@ -1 +1 @@
-eq.rec_on : ?a = ?a_1 → ?C ?a → ?C ?a_1
+eq.rec_on : ?a = ?a_1 → ?C → ?C

tests/lean/pp.lean.expected.out

@@ -1,7 +1,7 @@
-λ {A : Type} (B : Type) (a : A) (b : B), a : Π (B : Type), ?M_1 → B → ?M_1
+λ {A : Type} (B : Type) (a : A) (b : B), a : Π (B : Type), ?A → B → ?A
-λ {A B : Type} (a : A) (b : B), a : ?M_1 → ?M_2 → ?M_1
+λ {A B : Type} (a : A) (b : B), a : ?A → ?B → ?A
 λ (A : Type) {B : Type} (a : A) (b : B), a : Π (A : Type) {B : Type}, A → B → A
 λ (A B : Type) (a : A) (b : B), a : Π (A B : Type), A → B → A
-λ [A : Type] (B : Type) (a : A) (b : B), a : Π (B : Type), ?M_1 → B → ?M_1
+λ [A : Type] (B : Type) (a : A) (b : B), a : Π (B : Type), ?A → B → ?A
 λ ⦃A : Type⦄ {B : Type} (a : A) (b : B), a : Π ⦃A : Type⦄ {B : Type}, A → B → A
 λ ⦃A B : Type⦄ (a : A) (b : B), a : Π ⦃A B : Type⦄, A → B → A

tests/lean/t6.lean.expected.out

@@ -1,3 +1,3 @@
-id : ?M_1 → ?M_1
+id : ?A → ?A
-refl : (?M_1 → ?M_1 → Prop) → Prop
+refl : (?A → ?A → Prop) → Prop
-symm : (?M_1 → ?M_1 → Prop) → Prop
+symm : (?A → ?A → Prop) → Prop

tests/lean/t7.lean.expected.out

@@ -1,6 +1,6 @@
-id : ?M_1 → ?M_1
+id : ?A → ?A
-trans : (?M_1 → ?M_1 → Prop) → Prop
+trans : (?A → ?A → Prop) → Prop
-symm : (?M_1 → ?M_1 → Prop) → Prop
+symm : (?A → ?A → Prop) → Prop
-equivalence : (?M_1 → ?M_1 → Prop) → Prop
+equivalence : (?A → ?A → Prop) → Prop
 λ (A : Type) (R : A → A → Prop),
   and (and (refl R) (symm R)) (trans R)