feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers

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

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();

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})

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);

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) {

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) {

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) {

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);
+    }
 }
 }

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 <unordered_map>
+#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<name, bool, name_hash, name_eq> hidden_defs;
+    hidden_defs m_hidden_defs;
+
+    hidden_defs_extension const * get_parent() const {
+        return environment::extension::get_parent<hidden_defs_extension>();
+    }
+
+    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<environment::extension>(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<hidden_defs_extension>(g_hidden_defs_extension_initializer.m_extid);
+}
+
+static hidden_defs_extension & to_ext(environment & env) {
+    return env.get_extension<hidden_defs_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");
+}
+}

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);
+}

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);
 }
 }

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)

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);
+}
+}

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))