feat(frontends/lean): add synthesis information only for 'explicit' placeholder

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/builtin_exprs.cpp

@@ -130,7 +130,7 @@ static expr parse_let_expr(parser & p, unsigned, expr const *, pos_info const &
 }
 
 static expr parse_placeholder(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(mk_expr_placeholder(), pos);
+    return p.save_pos(mk_explicit_expr_placeholder(), pos);
 }
 
 static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {

src/frontends/lean/elaborator.cpp

@@ -648,11 +648,17 @@ public:
             return none_expr();
     }
 
+    void save_placeholder_info(expr const & e, expr const & r) {
+        if (is_explicit_placeholder(e)) {
+            save_info_data(e, r);
+            save_synth_data(e, r);
+        }
+    }
+
     expr visit_expecting_type(expr const & e) {
         if (is_placeholder(e) && !placeholder_type(e)) {
             expr r = m_context.mk_type_meta(e.get_tag());
-            save_info_data(e, r);
+            save_placeholder_info(e, r);
-            save_synth_data(e, r);
             return r;
         } else {
             return visit(e);
@@ -662,8 +668,7 @@ public:
     expr visit_expecting_type_of(expr const & e, expr const & t) {
         if (is_placeholder(e) && !placeholder_type(e)) {
             expr r = mk_placeholder_meta(some_expr(t), e.get_tag(), is_strict_placeholder(e));
-            save_info_data(e, r);
+            save_placeholder_info(e, r);
-            save_synth_data(e, r);
             return r;
         } else if (is_choice(e)) {
             return visit_choice(e, some_expr(t));
@@ -865,8 +870,7 @@ public:
 
     expr visit_placeholder(expr const & e) {
         expr r = mk_placeholder_meta(placeholder_type(e), e.get_tag(), is_strict_placeholder(e));
-        save_info_data(e, r);
+        save_placeholder_info(e, r);
-        save_synth_data(e, r);
         return r;
     }
 

src/library/placeholder.cpp

@@ -10,8 +10,10 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 
 namespace lean {
-static name g_placeholder_name        = name(name::mk_internal_unique_name(), "_");
+static name g_implicit_placeholder_name = name(name::mk_internal_unique_name(), "_");
+static name const & g_placeholder_name  = g_implicit_placeholder_name;
 static name g_strict_placeholder_name   = name(name::mk_internal_unique_name(), "_");
+static name g_explicit_placeholder_name = name(name::mk_internal_unique_name(), "_");
 MK_THREAD_LOCAL_GET(unsigned, get_placeholder_id, 0)
 static unsigned next_placeholder_id() {
     unsigned & c = get_placeholder_id();
@@ -20,20 +22,33 @@ static unsigned next_placeholder_id() {
     return r;
 }
 level mk_level_placeholder() { return mk_global_univ(name(g_placeholder_name, next_placeholder_id())); }
-expr mk_expr_placeholder(optional<expr> const & type, bool strict) {
+static name const & to_prefix(expr_placeholder_kind k) {
-    name const & prefix = strict ? g_strict_placeholder_name : g_placeholder_name;
+    switch (k) {
-    name n(prefix, next_placeholder_id());
+    case expr_placeholder_kind::Implicit:       return g_implicit_placeholder_name;
+    case expr_placeholder_kind::StrictImplicit: return g_strict_placeholder_name;
+    case expr_placeholder_kind::Explicit:       return g_explicit_placeholder_name;
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
+}
+expr mk_expr_placeholder(optional<expr> const & type, expr_placeholder_kind k) {
+    name n(to_prefix(k), next_placeholder_id());
     if (type)
         return mk_local(n, *type);
     else
         return mk_constant(n);
 }
 static bool is_placeholder(name const & n) {
-    return !n.is_atomic() && (n.get_prefix() == g_placeholder_name || n.get_prefix() == g_strict_placeholder_name);
+    if (n.is_atomic())
+        return false;
+    name const & p = n.get_prefix();
+    return p == g_implicit_placeholder_name || p == g_strict_placeholder_name || p == g_explicit_placeholder_name;
 }
 static bool is_strict_placeholder(name const & n) {
     return !n.is_atomic() && n.get_prefix() == g_strict_placeholder_name;
 }
+static bool is_explicit_placeholder(name const & n) {
+    return !n.is_atomic() && n.get_prefix() == g_explicit_placeholder_name;
+}
 bool is_placeholder(level const & e) { return is_global(e) && is_placeholder(global_id(e)); }
 bool is_placeholder(expr const & e) {
     return (is_constant(e) && is_placeholder(const_name(e))) || (is_local(e) && is_placeholder(mlocal_name(e)));
@@ -41,7 +56,9 @@ bool is_placeholder(expr const & e) {
 bool is_strict_placeholder(expr const & e) {
     return (is_constant(e) && is_strict_placeholder(const_name(e))) || (is_local(e) && is_strict_placeholder(mlocal_name(e)));
 }
-
+bool is_explicit_placeholder(expr const & e) {
+    return (is_constant(e) && is_explicit_placeholder(const_name(e))) || (is_local(e) && is_explicit_placeholder(mlocal_name(e)));
+}
 optional<expr> placeholder_type(expr const & e) {
     if (is_local(e) && is_placeholder(e))
         return some_expr(mlocal_type(e));

src/library/placeholder.h

@@ -14,19 +14,28 @@ namespace lean {
 /** \brief Return a new universe level placeholder. */
 level mk_level_placeholder();
 
+enum class expr_placeholder_kind { Implicit, StrictImplicit, Explicit };
 /** \brief Return a new expression placeholder expression. */
-expr mk_expr_placeholder(optional<expr> const & type = none_expr(), bool strict = false);
+expr mk_expr_placeholder(optional<expr> const & type = none_expr(), expr_placeholder_kind k = expr_placeholder_kind::Implicit);
-inline expr mk_strict_expr_placeholder(optional<expr> const & type = none_expr()) { return mk_expr_placeholder(type, true); }
+inline expr mk_explicit_expr_placeholder(optional<expr> const & type = none_expr()) {
+    return mk_expr_placeholder(type, expr_placeholder_kind::Explicit);
+}
+inline expr mk_strict_expr_placeholder(optional<expr> const & type = none_expr()) {
+    return mk_expr_placeholder(type, expr_placeholder_kind::StrictImplicit);
+}
 
 /** \brief Return true if the given level is a placeholder. */
 bool is_placeholder(level const & e);
 
-/** \brief Return true iff the given expression is a placeholder (strict or not). */
+/** \brief Return true iff the given expression is a placeholder (strict, explicit or implicit). */
 bool is_placeholder(expr const & e);
 
-/** \brief Return true iff the given expression is a strict placeholder (strict or not). */
+/** \brief Return true iff the given expression is a strict placeholder. */
 bool is_strict_placeholder(expr const & e);
 
+/** \brief Return true iff the given expression is an explicit placeholder. */
+bool is_explicit_placeholder(expr const & e);
+
 /** \brief Return the type of the placeholder (if available) */
 optional<expr> placeholder_type(expr const & e);