From 70e06f8e869c579d9b939d2fc8dcb5174b514a57 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Dec 2013 10:27:27 -0800 Subject: [PATCH] feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers Signed-off-by: Leonardo de Moura --- src/frontends/lua/register_modules.cpp | 4 +- src/library/CMakeLists.txt | 2 +- src/library/all/all.cpp | 2 + src/library/arith/int.cpp | 7 +++ src/library/arith/nat.cpp | 5 ++ src/library/arith/real.cpp | 8 +++ src/library/arith/special_fn.cpp | 6 ++ src/library/hidden_defs.cpp | 87 ++++++++++++++++++++++++++ src/library/hidden_defs.h | 36 +++++++++++ src/library/kernel_bindings.cpp | 8 --- src/library/kernel_bindings.h | 1 - src/library/register_module.h | 24 +++++++ tests/lua/hidden1.lua | 14 +++++ 13 files changed, 192 insertions(+), 12 deletions(-) create mode 100644 src/library/hidden_defs.cpp create mode 100644 src/library/hidden_defs.h create mode 100644 src/library/register_module.h create mode 100644 tests/lua/hidden1.lua diff --git a/src/frontends/lua/register_modules.cpp b/src/frontends/lua/register_modules.cpp index 01facf0c1..4db81a1a0 100644 --- a/src/frontends/lua/register_modules.cpp +++ b/src/frontends/lua/register_modules.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "util/script_state.h" #include "util/numerics/register_module.h" #include "util/sexpr/register_module.h" -#include "library/kernel_bindings.h" +#include "library/register_module.h" #include "library/arith/register_module.h" #include "library/tactic/register_module.h" #include "frontends/lean/register_module.h" @@ -17,7 +17,7 @@ namespace lean { void register_modules() { register_numerics_module(); register_sexpr_module(); - register_kernel_module(); + register_core_module(); register_arith_module(); register_tactic_module(); register_frontend_lean_module(); diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 38c37799e..3b817c947 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(library kernel_bindings.cpp basic_thms.cpp deep_copy.cpp max_sharing.cpp context_to_lambda.cpp io_state.cpp update_expr.cpp - type_inferer.cpp placeholder.cpp expr_lt.cpp) + type_inferer.cpp placeholder.cpp expr_lt.cpp hidden_defs.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/all/all.cpp b/src/library/all/all.cpp index 45b294baa..9a97cedd8 100644 --- a/src/library/all/all.cpp +++ b/src/library/all/all.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/builtin.h" +#include "library/hidden_defs.h" #include "library/basic_thms.h" #include "library/arith/arith.h" #include "library/cast/cast.h" @@ -13,6 +14,7 @@ Author: Leonardo de Moura namespace lean { void import_all(environment & env) { import_basic(env); + hide_builtin(env); import_basic_thms(env); import_cast(env); import_arith(env); diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index f227e02bf..0f070800d 100644 --- a/src/library/arith/int.cpp +++ b/src/library/arith/int.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" +#include "library/hidden_defs.h" #include "library/kernel_bindings.h" #include "library/arith/int.h" #include "library/arith/nat.h" @@ -175,6 +176,12 @@ void import_int(environment & env) { env.add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y)))); env.add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x)))); + + for (auto n : {int_sub_fn_name, int_neg_fn_name, int_mod_fn_name, int_divides_fn_name, + int_ge_fn_name, int_lt_fn_name, int_gt_fn_name, int_abs_fn_name, + nat_sub_fn_name, nat_neg_fn_name}) { + set_hidden_flag(env, n); + } } static int mk_int_value(lua_State * L) { diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp index bdfba2e58..10e2a66e7 100644 --- a/src/library/arith/nat.cpp +++ b/src/library/arith/nat.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" +#include "library/hidden_defs.h" #include "library/kernel_bindings.h" #include "library/arith/nat.h" #include "library/arith/num_type.h" @@ -127,6 +128,10 @@ void import_nat(environment & env) { env.add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x)))); env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y)))); env.add_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x)); + + for (auto n : {nat_ge_fn_name, nat_lt_fn_name, nat_gt_fn_name, nat_id_fn_name}) { + set_hidden_flag(env, n); + } } static int mk_nat_value(lua_State * L) { diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp index 4e21e780f..93c26e03f 100644 --- a/src/library/arith/real.cpp +++ b/src/library/arith/real.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" +#include "library/hidden_defs.h" #include "library/kernel_bindings.h" #include "library/arith/real.h" #include "library/arith/int.h" @@ -156,6 +157,11 @@ void import_real(environment & env) { env.add_definition(real_ge_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, rLe(y, x))); env.add_definition(real_lt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(y, x)))); env.add_definition(real_gt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(x, y)))); + + for (auto n : {real_sub_fn_name, real_neg_fn_name, real_abs_fn_name, real_ge_fn_name, + real_lt_fn_name, real_gt_fn_name}) { + set_hidden_flag(env, n); + } } class int_to_real_value : public const_value { @@ -182,6 +188,8 @@ void import_int_to_real_coercions(environment & env) { env.add_builtin(mk_int_to_real_fn()); expr x = Const("x"); env.add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x)))); + + set_hidden_flag(env, nat_to_real_fn_name); } static int mk_real_value(lua_State * L) { diff --git a/src/library/arith/special_fn.cpp b/src/library/arith/special_fn.cpp index 51f2d4219..2d2baef89 100644 --- a/src/library/arith/special_fn.cpp +++ b/src/library/arith/special_fn.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/environment.h" #include "kernel/abstract.h" +#include "library/hidden_defs.h" #include "library/arith/special_fn.h" #include "library/arith/real.h" @@ -56,5 +57,10 @@ void import_special_fn(environment & env) { env.add_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x)))); env.add_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x)))); env.add_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x)))); + + for (auto n : {cos_fn_name, tan_fn_name, cot_fn_name, sec_fn_name, csc_fn_name, sinh_fn_name, + cosh_fn_name, tanh_fn_name, coth_fn_name, sech_fn_name, csch_fn_name}) { + set_hidden_flag(env, n); + } } } diff --git a/src/library/hidden_defs.cpp b/src/library/hidden_defs.cpp new file mode 100644 index 000000000..127b43193 --- /dev/null +++ b/src/library/hidden_defs.cpp @@ -0,0 +1,87 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/name.h" +#include "util/sstream.h" +#include "kernel/environment.h" +#include "kernel/builtin.h" +#include "library/hidden_defs.h" +#include "library/kernel_bindings.h" + +namespace lean { +struct hidden_defs_extension : public environment::extension { + typedef std::unordered_map hidden_defs; + hidden_defs m_hidden_defs; + + hidden_defs_extension const * get_parent() const { + return environment::extension::get_parent(); + } + + bool is_hidden(name const & n) const { + auto it = m_hidden_defs.find(n); + if (it != m_hidden_defs.end()) + return it->second; + hidden_defs_extension const * parent = get_parent(); + return parent && parent->is_hidden(n); + } + + void set_hidden_flag(name const & d, bool f) { + m_hidden_defs[d] = f; + } +}; + +struct hidden_defs_extension_initializer { + unsigned m_extid; + hidden_defs_extension_initializer() { + m_extid = environment::register_extension([](){ return std::unique_ptr(new hidden_defs_extension()); }); + } +}; + +static hidden_defs_extension_initializer g_hidden_defs_extension_initializer; + +static hidden_defs_extension const & to_ext(environment const & env) { + return env.get_extension(g_hidden_defs_extension_initializer.m_extid); +} + +static hidden_defs_extension & to_ext(environment & env) { + return env.get_extension(g_hidden_defs_extension_initializer.m_extid); +} + +bool is_hidden(environment const & env, name const & d) { + return to_ext(env).is_hidden(d); +} + +void set_hidden_flag(environment & env, name const & d, bool flag) { + if (!env.get_object(d).is_definition()) + throw exception(sstream() << "'" << d << "' is not a definition"); + to_ext(env).set_hidden_flag(d, flag); +} + +void hide_builtin(environment & env) { + for (auto c : { mk_implies_fn(), mk_iff_fn(), mk_not_fn(), mk_or_fn(), mk_and_fn(), + mk_forall_fn(), mk_exists_fn(), mk_homo_eq_fn() }) + set_hidden_flag(env, const_name(c)); +} + +static int is_hidden(lua_State * L) { + ro_environment env(L, 1); + lua_pushboolean(L, is_hidden(env, to_name_ext(L, 2))); + return 1; +} + +static int set_hidden_flag(lua_State * L) { + int nargs = lua_gettop(L); + rw_environment env(L, 1); + set_hidden_flag(env, to_name_ext(L, 2), nargs <= 2 ? true : lua_toboolean(L, 3)); + return 0; +} + +void open_hidden_defs(lua_State * L) { + SET_GLOBAL_FUN(is_hidden, "is_hidden"); + SET_GLOBAL_FUN(set_hidden_flag, "set_hidden_flag"); +} +} diff --git a/src/library/hidden_defs.h b/src/library/hidden_defs.h new file mode 100644 index 000000000..486089f67 --- /dev/null +++ b/src/library/hidden_defs.h @@ -0,0 +1,36 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/lua.h" +namespace lean { +class environment; +class name; +/** + \brief Return true iff the definition named \c d is hidden in + the given environment. + + This information is just a hint used by tactics and solvers. For + example, unfold_tactic uses it to decide whether a definition + should be unfolded or not. +*/ +bool is_hidden(environment const & env, name const & d); +/** + \brief Mark the definition named \c d as hidden in the given environment. + + \see is_hidden + + \remark It throws an exception if \c d is not a definition in \c env. +*/ +void set_hidden_flag(environment & env, name const & d, bool flag = true); +/** + \brief Hide definitions at builtin.cpp. We hide them here because + the hidden_defs module is not part of the kernel. +*/ +void hide_builtin(environment & env); + +void open_hidden_defs(lua_State * L); +} diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index b73c33cb3..2051b3a8e 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1579,8 +1579,6 @@ static void open_metavar_env(lua_State * L) { SET_GLOBAL_FUN(instantiate_metavars, "instantiate_metavars"); } - - void open_kernel_module(lua_State * L) { open_level(L); open_local_context(L); @@ -1591,11 +1589,5 @@ void open_kernel_module(lua_State * L) { open_object(L); open_justification(L); open_metavar_env(L); - open_io_state(L); - open_type_inferer(L); -} - -void register_kernel_module() { - script_state::register_module(open_kernel_module); } } diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h index 6879563f9..e3e018387 100644 --- a/src/library/kernel_bindings.h +++ b/src/library/kernel_bindings.h @@ -10,7 +10,6 @@ Author: Leonardo de Moura namespace lean { void open_kernel_module(lua_State * L); -void register_kernel_module(); UDATA_DEFS(level) UDATA_DEFS(local_entry) UDATA_DEFS_CORE(local_context) diff --git a/src/library/register_module.h b/src/library/register_module.h new file mode 100644 index 000000000..132767c1e --- /dev/null +++ b/src/library/register_module.h @@ -0,0 +1,24 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/script_state.h" +#include "library/kernel_bindings.h" +#include "library/io_state.h" +#include "library/type_inferer.h" +#include "library/hidden_defs.h" + +namespace lean { +inline void open_core_module(lua_State * L) { + open_kernel_module(L); + open_io_state(L); + open_type_inferer(L); + open_hidden_defs(L); +} +inline void register_core_module() { + script_state::register_module(open_core_module); +} +} diff --git a/tests/lua/hidden1.lua b/tests/lua/hidden1.lua new file mode 100644 index 000000000..2927aaa85 --- /dev/null +++ b/tests/lua/hidden1.lua @@ -0,0 +1,14 @@ +local env = environment() +assert(is_hidden(env, "and")) +assert(is_hidden(env, "or")) +assert(is_hidden(env, {"Int", "lt"})) +parse_lean_cmds([[ + Definition a : Bool := true +]], env) +assert(not is_hidden(env, "a")) +set_hidden_flag(env, "a") +assert(is_hidden(env, "a")) +set_hidden_flag(env, "a", false) +assert(not is_hidden(env, "a")) +assert(not is_hidden(env, "b")) +assert(not pcall(function () set_hidden_flag(env, "b") end))