feat(library): add simple placeholder module

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

src/library/CMakeLists.txt

@@ -2,7 +2,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   kernel_bindings.cpp io_state_stream.cpp bin_app.cpp
   resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp
   normalize.cpp shared_environment.cpp module.cpp coercion.cpp
-  private.cpp)
-# placeholder.cpp fo_unify.cpp hop_match.cpp)
+  private.cpp placeholder.cpp)
+# fo_unify.cpp hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/placeholder.cpp

@@ -1,70 +1,63 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "kernel/occurs.h"
-#include "kernel/metavar.h"
-#include "kernel/expr_maps.h"
-#include "kernel/replace_visitor.h"
-#include "library/expr_pair.h"
+#include "kernel/find_fn.h"
 #include "library/placeholder.h"
 #include "library/kernel_bindings.h"
 
 namespace lean {
-static name g_placeholder_name("_");
-expr mk_placeholder(optional<expr> const & t) {
-    return mk_constant(g_placeholder_name, t);
-}
+static name g_placeholder_name = name(name::mk_internal_unique_name(), "_");
 
-bool is_placeholder(expr const & e) {
-    return is_constant(e) && const_name(e) == g_placeholder_name;
+level mk_level_placeholder() { return mk_global_univ(g_placeholder_name); }
+expr mk_expr_placeholder() { return mk_constant(g_placeholder_name); }
+bool is_placeholder(level const & e) { return is_global(e) && global_id(e) == g_placeholder_name; }
+bool is_placeholder(expr const & e) { return is_constant(e) && const_name(e) == g_placeholder_name; }
+
+bool has_placeholder(level const & l) {
+    bool r = false;
+    for_each(l, [&](level const & e) {
+            if (is_placeholder(e))
+                r = true;
+            return !r;
+        });
+    return r;
 }
 
 bool has_placeholder(expr const & e) {
-    return occurs(mk_placeholder(), e);
+    return (bool) find(e, [](expr const & e, unsigned) { // NOLINT
+            if (is_placeholder(e))
+                return true;
+            else if (is_sort(e))
+                return has_placeholder(sort_level(e));
+            else if (is_constant(e))
+                return std::any_of(const_levels(e).begin(), const_levels(e).end(), [](level const & l) { return has_placeholder(l); });
+            else
+                return false;
+        });
 }
 
-class replace_placeholders_with_metavars_proc : public replace_visitor {
-    metavar_env const & m_menv;
-    expr_map<expr> *    m_new2old;
-protected:
-    expr visit_constant(expr const & e, context const & c) {
-        if (is_placeholder(e)) {
-            return m_menv->mk_metavar(c, const_type(e));
-        } else {
-            return e;
-        }
-    }
-
-    expr visit(expr const & e, context const & c) {
-        expr r = replace_visitor::visit(e, c);
-        if (!is_eqp(r, e) && m_new2old)
-            m_new2old->insert(expr_pair(r, e));
-        return r;
-    }
-public:
-    replace_placeholders_with_metavars_proc(metavar_env const & menv, expr_map<expr> * new2old):
-        m_menv(menv),
-        m_new2old(new2old) {
-    }
-};
-
-expr replace_placeholders_with_metavars(expr const & e, metavar_env const & menv, expr_map<expr> * new2old) {
-    replace_placeholders_with_metavars_proc proc(menv, new2old);
-    return proc(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 is_placeholder(lua_State * L) {
+    if (is_expr(L, 1))
+        return push_boolean(L, is_placeholder(to_expr(L, 1)));
+    else
+        return push_boolean(L, is_placeholder(to_level(L, 1)));
 }
-
-static int mk_placeholder(lua_State * L) {
-    if (lua_gettop(L) == 0) {
-        return push_expr(L, mk_placeholder());
-    } else {
-        return push_expr(L, mk_placeholder(some_expr(to_expr(L, 1))));
-    }
+static int has_placeholder(lua_State * L) {
+    if (is_expr(L, 1))
+        return push_boolean(L, has_placeholder(to_expr(L, 1)));
+    else
+        return push_boolean(L, has_placeholder(to_level(L, 1)));
 }
 
 void open_placeholder(lua_State * L) {
-    SET_GLOBAL_FUN(mk_placeholder, "mk_placeholder");
+    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(has_placeholder,      "has_placeholder");
 }
 }

src/library/placeholder.h

@@ -1,5 +1,5 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
@@ -7,33 +7,24 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/lua.h"
 #include "kernel/expr.h"
-#include "kernel/expr_maps.h"
 
+// Placeholders are used to mark locations where additional
+// metavariables should be inserted.
 namespace lean {
-class metavar_env;
-/**
-    \brief Return a new placeholder expression (with an optional
-    type). To be able to track location, a new constant for each
-    placeholder.
-*/
-expr mk_placeholder(optional<expr> const & t = none_expr());
+/** \brief Return a new universe level placeholder. */
+level mk_level_placeholder();
 
-/**
-    \brief Return true iff the given expression is a placeholder.
-*/
+/** \brief Return a new expression placeholder expression. */
+expr mk_expr_placeholder();
+
+/** \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. */
 bool is_placeholder(expr const & e);
 
-/**
-    \brief Return true iff the given expression contains placeholders.
-*/
+/** \brief Return true iff the given expression contains placeholders. */
 bool has_placeholder(expr const & e);
 
-/**
-   \brief Replace the placeholders in \c e with fresh metavariables from \c menv.
-   if \c new2old is not nullptr, then for each new expression \c t created based on
-   \c s, we store <tt>(*new2old)[t] = s</tt>.
-*/
-expr replace_placeholders_with_metavars(expr const & e, metavar_env const & menv, expr_map<expr> * new2old = nullptr);
-
 void open_placeholder(lua_State * L);
 }

src/library/register_module.h

@@ -10,10 +10,9 @@ Author: Leonardo de Moura
 #include "library/resolve_macro.h"
 #include "library/coercion.h"
 #include "library/private.h"
-
+#include "library/placeholder.h"
 // #include "library/fo_unify.h"
 // #include "library/hop_match.h"
-// #include "library/placeholder.h"
 
 namespace lean {
 inline void open_core_module(lua_State * L) {
@@ -21,8 +20,8 @@ inline void open_core_module(lua_State * L) {
     open_resolve_macro(L);
     open_coercion(L);
     open_private(L);
+    open_placeholder(L);
     // open_fo_unify(L);
-    // open_placeholder(L);
     // open_hop_match(L);
 }
 inline void register_core_module() {

tests/lua/place1.lua

@@ -0,0 +1,14 @@
+print(mk_expr_placeholder())
+print(mk_level_placeholder())
+assert(is_placeholder(mk_expr_placeholder()))
+assert(not is_placeholder(Var(0)))
+assert(not is_placeholder(Const("A")))
+assert(is_placeholder(mk_level_placeholder()))
+assert(not is_placeholder(param_univ("l")))
+local f = Const("f")
+local a = Const("a")
+assert(has_placeholder(f(mk_expr_placeholder())))
+assert(not has_placeholder(f(a)))
+assert(has_placeholder(f(Const("a", { mk_level_placeholder() }))))
+assert(has_placeholder(mk_sort(mk_level_placeholder())))
+assert(has_placeholder(mk_sort(max_univ(1, mk_level_placeholder()))))