From 6902d8cb056a4f7271beed8f78b10ccadb5f8134 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 May 2014 20:26:06 -0700 Subject: [PATCH] feat(library): add simple placeholder module Signed-off-by: Leonardo de Moura --- src/library/CMakeLists.txt | 4 +- src/library/placeholder.cpp | 91 ++++++++++++++++------------------- src/library/placeholder.h | 35 +++++--------- src/library/register_module.h | 5 +- tests/lua/place1.lua | 14 ++++++ 5 files changed, 73 insertions(+), 76 deletions(-) create mode 100644 tests/lua/place1.lua diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 9b945be30..f048504da 100644 --- a/src/library/CMakeLists.txt +++ b/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}) diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index dbdfe0cba..35cbc82f9 100644 --- a/src/library/placeholder.cpp +++ b/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 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 * 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 * new2old): - m_menv(menv), - m_new2old(new2old) { - } -}; - -expr replace_placeholders_with_metavars(expr const & e, metavar_env const & menv, expr_map * 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"); } } diff --git a/src/library/placeholder.h b/src/library/placeholder.h index ca458ff79..c4c59ba13 100644 --- a/src/library/placeholder.h +++ b/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 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 (*new2old)[t] = s. -*/ -expr replace_placeholders_with_metavars(expr const & e, metavar_env const & menv, expr_map * new2old = nullptr); - void open_placeholder(lua_State * L); } diff --git a/src/library/register_module.h b/src/library/register_module.h index b2001b866..02b5ad228 100644 --- a/src/library/register_module.h +++ b/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() { diff --git a/tests/lua/place1.lua b/tests/lua/place1.lua new file mode 100644 index 000000000..5d03726f4 --- /dev/null +++ b/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()))))