diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 464e065ed..ab886b426 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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 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 ctx = p.locals_to_context(); level_param_names new_ls; std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 9920bc0a8..7531ce0d4 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/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 elaborator::mk_mvar_suffix(expr const & b) { - if (!infom()) + if (!infom() && !m_nice_mvar_names) return optional(); else return optional(binding_name(b)); @@ -1270,8 +1271,8 @@ pair elaborator::elaborate_nested(list const & ctx, exp static name * g_tmp_prefix = nullptr; std::tuple elaborate(elaborator_context & env, list const & ctx, expr const & e, - bool relax_main_opaque, bool ensure_type) { - return elaborator(env, name_generator(*g_tmp_prefix))(ctx, e, ensure_type, relax_main_opaque); + bool relax_main_opaque, bool ensure_type, bool nice_mvar_names) { + return elaborator(env, name_generator(*g_tmp_prefix), nice_mvar_names)(ctx, e, ensure_type, relax_main_opaque); } std::tuple elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v, diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 2efd4ce8b..369dbb0e7 100644 --- a/src/frontends/lean/elaborator.h +++ b/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 elaborate_nested(list 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 operator()(list const & ctx, expr const & e, bool _ensure_type, bool relax_main_opaque); std::tuple operator()(expr const & t, expr const & v, name const & n, bool is_opaque); }; std::tuple elaborate(elaborator_context & env, list 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 elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v, bool is_opaque); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index d4d02ed59..72573c181 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -634,9 +634,10 @@ std::tuple 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; } diff --git a/tests/lean/check.lean.expected.out b/tests/lean/check.lean.expected.out index 34ad91a3f..4f4683182 100644 --- a/tests/lean/check.lean.expected.out +++ b/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) diff --git a/tests/lean/check2.lean.expected.out b/tests/lean/check2.lean.expected.out index e04c8a2e7..68a1c254e 100644 --- a/tests/lean/check2.lean.expected.out +++ b/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 diff --git a/tests/lean/pp.lean.expected.out b/tests/lean/pp.lean.expected.out index 2f4a648f8..62e780e88 100644 --- a/tests/lean/pp.lean.expected.out +++ b/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 B : Type} (a : A) (b : B), a : ?M_1 → ?M_2 → ?M_1 +λ {A : Type} (B : Type) (a : A) (b : B), a : Π (B : Type), ?A → B → ?A +λ {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 diff --git a/tests/lean/t6.lean.expected.out b/tests/lean/t6.lean.expected.out index cf7d444a0..5d5be7ef8 100644 --- a/tests/lean/t6.lean.expected.out +++ b/tests/lean/t6.lean.expected.out @@ -1,3 +1,3 @@ -id : ?M_1 → ?M_1 -refl : (?M_1 → ?M_1 → Prop) → Prop -symm : (?M_1 → ?M_1 → Prop) → Prop +id : ?A → ?A +refl : (?A → ?A → Prop) → Prop +symm : (?A → ?A → Prop) → Prop diff --git a/tests/lean/t7.lean.expected.out b/tests/lean/t7.lean.expected.out index 022fc6d0b..0b4e495bc 100644 --- a/tests/lean/t7.lean.expected.out +++ b/tests/lean/t7.lean.expected.out @@ -1,6 +1,6 @@ -id : ?M_1 → ?M_1 -trans : (?M_1 → ?M_1 → Prop) → Prop -symm : (?M_1 → ?M_1 → Prop) → Prop -equivalence : (?M_1 → ?M_1 → Prop) → Prop +id : ?A → ?A +trans : (?A → ?A → Prop) → Prop +symm : (?A → ?A → Prop) → Prop +equivalence : (?A → ?A → Prop) → Prop λ (A : Type) (R : A → A → Prop), and (and (refl R) (symm R)) (trans R)