From 2c4175341cbed153a7f010ea1c86768ffc8570ce Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Jun 2014 14:35:55 -0700
Subject: [PATCH] feat(library/placeholder): allow types to be attached to
 placeholders

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/placeholder.cpp | 31 ++++++++++++++++++++++++++++---
 src/library/placeholder.h   |  5 ++++-
 tests/lua/place2.lua        |  4 ++++
 3 files changed, 36 insertions(+), 4 deletions(-)
 create mode 100644 tests/lua/place2.lua

diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp
index 06e6a385fb..b6c8b5186c 100644
--- a/src/library/placeholder.cpp
+++ b/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");
 }
 }
diff --git a/src/library/placeholder.h b/src/library/placeholder.h
index c4c59ba133..8d55011cd4 100644
--- a/src/library/placeholder.h
+++ b/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);
 
diff --git a/tests/lua/place2.lua b/tests/lua/place2.lua
new file mode 100644
index 0000000000..80146b4d2a
--- /dev/null
+++ b/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)))