feat(library/placeholder): allow types to be attached to placeholders

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

src/library/placeholder.cpp

@@ -19,10 +19,27 @@ 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() { return mk_constant(name(g_placeholder_name, next_placeholder_id())); }
+expr mk_expr_placeholder(optional<expr> const & type) {
+    name n(g_placeholder_name, 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; }
 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)); }
+bool is_placeholder(expr const & e) {
+    return
+        (is_constant(e) && is_placeholder(const_name(e))) ||
+        (is_local(e) && is_placeholder(mlocal_name(e)));
+}
+
+optional<expr> placeholder_type(expr const & e) {
+    if (is_local(e) && is_placeholder(e))
+        return some_expr(mlocal_type(e));
+    else
+        return none_expr();
+}
 
 bool has_placeholder(level const & l) {
     bool r = false;
@@ -48,7 +65,13 @@ bool has_placeholder(expr const & e) {
 }
 
 static int mk_level_placeholder(lua_State * L) { return push_level(L, mk_level_placeholder()); }
-static int mk_expr_placeholder(lua_State * L) { return push_expr(L, mk_expr_placeholder()); }
+static int mk_expr_placeholder(lua_State * L) {
+    int nargs = lua_gettop(L);
+    if (nargs == 0)
+        return push_expr(L, mk_expr_placeholder());
+    else
+        return push_expr(L, mk_expr_placeholder(some_expr(to_expr(L, 1))));
+}
 static int is_placeholder(lua_State * L) {
     if (is_expr(L, 1))
         return push_boolean(L, is_placeholder(to_expr(L, 1)));
@@ -61,11 +84,13 @@ static int has_placeholder(lua_State * L) {
     else
         return push_boolean(L, has_placeholder(to_level(L, 1)));
 }
+static int placeholder_type(lua_State * L) { return push_optional_expr(L, placeholder_type(to_expr(L, 1))); }
 
 void open_placeholder(lua_State * L) {
     SET_GLOBAL_FUN(mk_level_placeholder, "mk_level_placeholder");
     SET_GLOBAL_FUN(mk_expr_placeholder,  "mk_expr_placeholder");
     SET_GLOBAL_FUN(is_placeholder,       "is_placeholder");
+    SET_GLOBAL_FUN(placeholder_type,     "placeholder_type");
     SET_GLOBAL_FUN(has_placeholder,      "has_placeholder");
 }
 }

src/library/placeholder.h

@@ -15,7 +15,7 @@ namespace lean {
 level mk_level_placeholder();
 
 /** \brief Return a new expression placeholder expression. */
-expr mk_expr_placeholder();
+expr mk_expr_placeholder(optional<expr> const & type = none_expr());
 
 /** \brief Return true if the given level is a placeholder. */
 bool is_placeholder(level const & e);
@@ -23,6 +23,9 @@ bool is_placeholder(level const & e);
 /** \brief Return true iff the given expression is a placeholder. */
 bool is_placeholder(expr const & e);
 
+/** \brief Return the type of the placeholder (if available) */
+optional<expr> placeholder_type(expr const & e);
+
 /** \brief Return true iff the given expression contains placeholders. */
 bool has_placeholder(expr const & e);
 

tests/lua/place2.lua

@@ -0,0 +1,4 @@
+print(mk_expr_placeholder())
+assert(not placeholder_type(mk_expr_placeholder()))
+assert(placeholder_type(mk_expr_placeholder(Bool)) == Bool)
+assert(is_placeholder(mk_expr_placeholder(Bool)))