feat(frontends/lean): lean --server should display meta-variables using the approach used in check command, closes #280

src/frontends/lean/elaborator.cpp

@@ -217,20 +217,27 @@ void elaborator::copy_info_to_manager(substitution s) {
     m_pre_info_data.clear();
 }
 
+optional<name> elaborator::mk_mvar_suffix(expr const & b) {
+    if (!infom())
+        return optional<name>();
+    else
+        return optional<name>(binding_name(b));
+}
+
 /** \brief Create a metavariable, and attach choice constraint for generating
     solutions using class-instances and tactic-hints.
 */
-expr elaborator::mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict,
+expr elaborator::mk_placeholder_meta(optional<name> const & suffix, optional<expr> const & type,
-                                     bool is_inst_implicit, constraint_seq & cs) {
+                                     tag g, bool is_strict, bool is_inst_implicit, constraint_seq & cs) {
     if (is_inst_implicit) {
         auto ec = mk_placeholder_elaborator(env(), ios(), m_context,
-                                            m_ngen.next(), m_relax_main_opaque, use_local_instances(),
+                                            m_ngen.next(), suffix, m_relax_main_opaque, use_local_instances(),
                                             is_strict, type, g, m_unifier_config);
         register_meta(ec.first);
         cs += ec.second;
         return ec.first;
     } else {
-        expr m = m_context.mk_meta(m_ngen, type, g);
+        expr m = m_context.mk_meta(m_ngen, suffix, type, g);
         register_meta(m);
         return m;
     }
@@ -323,7 +330,8 @@ expr elaborator::add_implict_args(expr e, constraint_seq & cs, bool relax) {
         tag g = e.get_tag();
         bool is_strict = true;
         bool inst_imp  = binding_info(type).is_inst_implicit();
-        expr imp_arg   = mk_placeholder_meta(some_expr(binding_domain(type)), g, is_strict, inst_imp, cs);
+        expr imp_arg   = mk_placeholder_meta(mk_mvar_suffix(type), some_expr(binding_domain(type)),
+                                             g, is_strict, inst_imp, cs);
         e              = mk_app(e, imp_arg, g);
         type           = instantiate(binding_body(type), imp_arg);
         constraint_seq new_cs;
@@ -553,7 +561,8 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
             tag g          = f.get_tag();
             bool is_strict = true;
             bool inst_imp  = binding_info(f_type).is_inst_implicit();
-            expr imp_arg   = mk_placeholder_meta(some_expr(binding_domain(f_type)), g, is_strict, inst_imp, f_cs);
+            expr imp_arg   = mk_placeholder_meta(mk_mvar_suffix(f_type), some_expr(binding_domain(f_type)),
+                                                 g, is_strict, inst_imp, f_cs);
             f              = mk_app(f, imp_arg, g);
             auto f_t       = ensure_fun(f, f_cs);
             f              = f_t.first;
@@ -871,7 +880,8 @@ pair<expr, constraint_seq> elaborator::visit(expr const & e) {
                 }
             }
             bool inst_imp = bi.is_inst_implicit();
-            imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, inst_imp, cs);
+            imp_arg = mk_placeholder_meta(mk_mvar_suffix(r_type), some_expr(binding_domain(r_type)),
+                                          g, is_strict, inst_imp, cs);
             r       = mk_app(r, imp_arg, g);
             r_type  = whnf(instantiate(binding_body(r_type), imp_arg), cs);
         }

src/frontends/lean/elaborator.h

@@ -87,7 +87,13 @@ class elaborator : public coercion_info_manager {
     virtual void save_coercion_info(expr const & e, expr const & c);
     virtual void erase_coercion_info(expr const & e);
     void copy_info_to_manager(substitution s);
-    expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, bool inst_implicit, constraint_seq & cs);
+    /** \brief If info manager is being used, then create a metavariable suffix based on binding_name(b) */
+    optional<name> mk_mvar_suffix(expr const & b);
+    expr mk_placeholder_meta(optional<name> const & suffix, optional<expr> const & type,
+                             tag g, bool is_strict, bool inst_implicit, constraint_seq & cs);
+    expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, bool inst_implicit, constraint_seq & cs) {
+        return mk_placeholder_meta(optional<name>(), type, g, is_strict, inst_implicit, cs);
+    }
 
     expr visit_expecting_type(expr const & e, constraint_seq & cs);
     expr visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs);

src/frontends/lean/local_context.cpp

@@ -81,15 +81,17 @@ expr local_context::mk_type_meta(name_generator & ngen, tag g) {
     return apply_context(mk_type_metavar(ngen, g), g);
 }
 
-expr local_context::mk_metavar(name_generator & ngen, optional<expr> const & type, tag g) {
+expr local_context::mk_metavar(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g) {
     name n      = ngen.next();
+    if (suffix)
+        n = n + *suffix;
     expr r_type = type ? *type : mk_type_meta(ngen, g);
     expr t      = pi_abstract_context(r_type, g);
     return ::lean::mk_metavar(n, t, g);
 }
 
-expr local_context::mk_meta(name_generator & ngen, optional<expr> const & type, tag g) {
+expr local_context::mk_meta(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g) {
-    expr mvar = mk_metavar(ngen, type, g);
+    expr mvar = mk_metavar(ngen, suffix, type, g);
     expr meta = apply_context(mvar, g);
     return meta;
 }

src/frontends/lean/local_context.h

@@ -61,8 +61,10 @@ public:
         where ?m2 is another fresh metavariable with type
            <tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u})</tt>,
         and \c ?u is a fresh universe metavariable.
+
+        \remark If \c suffix is not none, then it is appended to the (fresh) metavariable name.
     */
-    expr mk_metavar(name_generator & ngen, optional<expr> const & type, tag g);
+    expr mk_metavar(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g);
 
     /** \brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
            <tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
@@ -70,8 +72,13 @@ public:
         created using \c mk_metavar.
 
         \see mk_metavar
+
+        \remark If \c suffix is not none, then it is appended to the (fresh) metavariable name.
     */
-    expr mk_meta(name_generator & ngen, optional<expr> const & type, tag g);
+    expr mk_meta(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g);
+    expr mk_meta(name_generator & ngen, optional<expr> const & type, tag g) {
+        return mk_meta(ngen, optional<name>(), type, g);
+    }
 
     /** \brief Return context as a list */
     list<expr> const & get_data() const;

src/frontends/lean/placeholder_elaborator.cpp

@@ -268,10 +268,10 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
 */
 pair<expr, constraint> mk_placeholder_elaborator(
     environment const & env, io_state const & ios, local_context const & ctx,
-    name const & prefix, bool relax, bool use_local_instances,
+    name const & prefix, optional<name> const & suffix, bool relax, bool use_local_instances,
     bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg) {
     auto C       = std::make_shared<placeholder_context>(env, ios, ctx, prefix, relax, use_local_instances);
-    expr m       = C->m_ctx.mk_meta(C->m_ngen, type, g);
+    expr m       = C->m_ctx.mk_meta(C->m_ngen, suffix, type, g);
     constraint c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, delay_factor());
     return mk_pair(m, c);
 }

src/frontends/lean/placeholder_elaborator.h

@@ -15,6 +15,7 @@ namespace lean {
 
     \param ctx Local context where placeholder is located
     \param prefix Prefix for metavariables that will be created by this procedure
+    \param suffix If provided, then it is added to the main metavariable created by this procedure.
     \param relax True if opaque constants in the current module should be treated
                  as transparent
     \param use_local_instances If instances in the local context should be used
@@ -26,6 +27,6 @@ namespace lean {
 */
 pair<expr, constraint> mk_placeholder_elaborator(
     environment const & env, io_state const & ios, local_context const & ctx,
-    name const & prefix, bool relax_opaque, bool use_local_instances,
+    name const & prefix, optional<name> const & suffix, bool relax_opaque, bool use_local_instances,
     bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg);
 }

src/frontends/lean/pp.cpp

@@ -96,14 +96,56 @@ void finalize_pp() {
     delete g_tmp_prefix;
 }
 
+/** \brief We assume a metavariable name has a suggestion embedded in it WHEN its
+    last component is a string. */
+static bool has_embedded_suggestion(name const & m) {
+    return m.is_string();
+}
+
+/** \see extract_suggestion */
+static name extract_suggestion_core(name const & m) {
+    if (m.is_string()) {
+        if (m.is_atomic())
+            return m;
+        else
+            return name(extract_suggestion_core(m.get_prefix()), m.get_string());
+    } else {
+        return name();
+    }
+}
+
+/** \brief Extract "suggested name" embedded in a metavariable name
+
+    \pre has_embedded_suggestion(m)
+*/
+static name extract_suggestion(name const & m) {
+    lean_assert(has_embedded_suggestion(m));
+    name r = extract_suggestion_core(m);
+    lean_assert(!r.is_anonymous());
+    return r;
+}
+
 name pretty_fn::mk_metavar_name(name const & m) {
     if (auto it = m_purify_meta_table.find(m))
         return *it;
+    if (has_embedded_suggestion(m)) {
+        name suggested = extract_suggestion(m);
+        name r         = suggested;
+        unsigned i     = 1;
+        while (m_purify_used_metas.contains(r)) {
+            r = suggested.append_after(i);
+            i++;
+        }
+        m_purify_used_metas.insert(r);
+        m_purify_meta_table.insert(m, r);
+        return r;
+    } else {
         name new_m = m_meta_prefix.append_after(m_next_meta_idx);
         m_next_meta_idx++;
         m_purify_meta_table.insert(m, new_m);
         return new_m;
     }
+}
 
 name pretty_fn::mk_local_name(name const & n, name const & suggested) {
     if (auto it = m_purify_local_table.find(n))

src/frontends/lean/pp.h

@@ -44,6 +44,7 @@ private:
     name                m_meta_prefix;
     unsigned            m_next_meta_idx;
     name_map<name>      m_purify_meta_table;
+    name_set            m_purify_used_metas;
     name_map<name>      m_purify_local_table;
     name_set            m_purify_used_locals;
     // cached configuration

tests/lean/interactive/info.input.expected.out

@@ -2,7 +2,7 @@
 -- ENDWAIT
 -- BEGININFO
 -- TYPE|6|8
-?M_1 → ?M_2 → ?M_1 ∧ ?M_2
+?a → ?b → ?a ∧ ?b
 -- ACK
 -- IDENTIFIER|6|8
 and.intro