From 7c2a4211a8f4f42ab1149f3802cdfd506836ea3e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Jan 2014 16:41:40 -0800 Subject: [PATCH] feat(kernel): expose imported predicate Signed-off-by: Leonardo de Moura --- src/kernel/environment.cpp | 11 ++++------- src/kernel/environment.h | 16 +++++----------- src/library/ite.cpp | 31 ++++++++++++++++++++----------- src/library/ite.h | 3 ++- src/library/kernel_bindings.cpp | 7 +++++++ src/library/register_module.h | 2 ++ tests/lua/import.lua | 12 ++++++++++++ 7 files changed, 52 insertions(+), 30 deletions(-) create mode 100644 tests/lua/import.lua diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index cbf1a48786..1c48867944 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -112,7 +112,6 @@ bool is_end_import(object const & obj) { return dynamic_cast(obj.cell()); } -static name g_builtin_module("builtin_module"); class extension_factory { std::vector m_makers; mutex m_makers_mutex; @@ -566,12 +565,6 @@ void environment_cell::auxiliary_section(std::function fn) { } } -void environment_cell::import_builtin(char const * id, std::function fn) { - if (mark_imported_core(name(g_builtin_module, id))) { - auxiliary_section(fn); - } -} - void environment_cell::set_trusted_imported(bool flag) { m_trust_imported = flag; } @@ -648,6 +641,10 @@ void environment_cell::load(std::string const & fname, io_state const & ios) { load_core(fname, ios, optional()); } +bool environment_cell::imported(std::string const & n) const { + return already_imported(name(realpath(find_file(n, {".olean"}).c_str()))); +} + environment_cell::environment_cell(): m_num_children(0) { m_trust_imported = false; diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 98a2b7c751..3df18e934f 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -83,9 +83,11 @@ class environment_cell { void check_type(name const & n, expr const & t, expr const & v); void check_new_definition(name const & n, expr const & t, expr const & v); - bool already_imported(name const & n) const; bool mark_imported_core(name n); bool load_core(std::string const & fname, io_state const & ios, optional const & mod_name); + bool already_imported(name const & n) const; + /** \brief Return true iff the given file was not already marked as imported. It will also mark the file as imported. */ + bool mark_imported(char const * fname); public: environment_cell(); @@ -321,19 +323,11 @@ public: return static_cast(ext); } - /** - \brief Return true iff the given file was not already marked as imported. - It will also mark the file as imported. - */ - bool mark_imported(char const * fname); - - void import_builtin(char const * id, std::function fn); - void export_objects(std::string const & fname); - bool import(std::string const & fname, io_state const & ios); - void load(std::string const & fname, io_state const & ios); + /** \brief Return true iff module \c n has already been imported */ + bool imported(std::string const & n) const; /** \brief When trusted_imported flag is true, the environment will diff --git a/src/library/ite.cpp b/src/library/ite.cpp index e171635e8b..18d45d3689 100644 --- a/src/library/ite.cpp +++ b/src/library/ite.cpp @@ -7,19 +7,20 @@ Author: Leonardo de Moura #include "kernel/builtin.h" #include "kernel/abstract.h" #include "kernel/decl_macros.h" -#include "library/if_then_else_decls.h" +#include "library/ite.h" #include "library/if_then_else_decls.cpp" +#include "library/kernel_bindings.h" namespace lean { // ======================================= // If-then-else builtin operator -static name g_if_name("ite"); -static format g_if_fmt(g_if_name); +static name g_ite_name("ite"); +static format g_ite_fmt(g_ite_name); /** \brief Semantic attachment for if-then-else operator with type Pi (A : Type), Bool -> A -> A -> A */ -class if_fn_value : public value { +class ite_fn_value : public value { expr m_type; static expr mk_type() { expr A = Const("A"); @@ -27,10 +28,10 @@ class if_fn_value : public value { return Pi({A, TypeU}, Bool >> (A >> (A >> A))); } public: - if_fn_value():m_type(mk_type()) {} - virtual ~if_fn_value() {} + ite_fn_value():m_type(mk_type()) {} + virtual ~ite_fn_value() {} virtual expr get_type() const { return m_type; } - virtual name get_name() const { return g_if_name; } + virtual name get_name() const { return g_ite_name; } virtual optional normalize(unsigned num_args, expr const * args) const { if (num_args == 5 && is_bool_value(args[2]) && is_value(args[3]) && is_value(args[4])) { if (to_bool(args[2])) @@ -43,13 +44,21 @@ public: } virtual void write(serializer & s) const { s << "ite"; } }; -MK_BUILTIN(if_fn, if_fn_value); -MK_IS_BUILTIN(is_if_fn, mk_if_fn()); -static register_builtin_fn if_blt("ite", []() { return mk_if_fn(); }); -static value::register_deserializer_fn if_ds("ite", [](deserializer & ) { return mk_if_fn(); }); +MK_BUILTIN(ite_fn, ite_fn_value); +MK_IS_BUILTIN(is_ite_fn, mk_ite_fn()); +static register_builtin_fn ite_blt("ite", []() { return mk_ite_fn(); }); +static value::register_deserializer_fn ite_ds("ite", [](deserializer & ) { return mk_ite_fn(); }); // ======================================= void import_ite(environment const & env, io_state const & ios) { env->import("if_then_else", ios); } + +static int expr_mk_ite(lua_State * L) { + return push_expr(L, mk_ite(to_expr(L, 1), to_expr(L, 2), to_expr(L, 3), to_expr(L, 4))); +} + +void open_ite(lua_State * L) { + SET_GLOBAL_FUN(expr_mk_ite, "mk_ite"); +} } diff --git a/src/library/ite.h b/src/library/ite.h index 14e47891da..098b2015cf 100644 --- a/src/library/ite.h +++ b/src/library/ite.h @@ -11,6 +11,7 @@ Author: Leonardo de Moura namespace lean { expr mk_ite_fn(); bool is_ite_fn(expr const & e); -inline expr mk_ite(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app(mk_ite_fn, e1, e2, e3, e4); } +inline expr mk_ite(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app(mk_ite_fn(), e1, e2, e3, e4); } void import_ite(environment const & env, io_state const & ios); +void open_ite(lua_State * L); } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 1876186d61..c34aeba564 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1184,6 +1184,12 @@ static int environment_get_universe_distance(lua_State * L) { return 1; } +static int environment_imported(lua_State * L) { + ro_shared_environment env(L, 1); + lua_pushboolean(L, env->imported(std::string(luaL_checkstring(L, 2)))); + return 1; +} + static const struct luaL_Reg environment_m[] = { {"__gc", environment_gc}, // never throws {"__tostring", safe_function}, @@ -1209,6 +1215,7 @@ static const struct luaL_Reg environment_m[] = { {"set_opaque", safe_function}, {"is_opaque", safe_function}, {"import", safe_function}, + {"imported", safe_function}, {"load", safe_function}, {0, 0} }; diff --git a/src/library/register_module.h b/src/library/register_module.h index 65a7cf425d..4377b6a520 100644 --- a/src/library/register_module.h +++ b/src/library/register_module.h @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/fo_unify.h" #include "library/hop_match.h" #include "library/placeholder.h" +#include "library/ite.h" namespace lean { inline void open_core_module(lua_State * L) { @@ -19,6 +20,7 @@ inline void open_core_module(lua_State * L) { open_fo_unify(L); open_placeholder(L); open_hop_match(L); + open_ite(L); } inline void register_core_module() { script_state::register_module(open_core_module); diff --git a/tests/lua/import.lua b/tests/lua/import.lua new file mode 100644 index 0000000000..f945b337b8 --- /dev/null +++ b/tests/lua/import.lua @@ -0,0 +1,12 @@ +local env = get_environment() +assert(env:imported("kernel")) +assert(env:imported("Nat")) +assert(not env:imported("Real")) +print("before import Real") +env:import("Real") +print("after import Real") +assert(env:imported("Real")) +parse_lean_cmds([[ + variables a b c : Real + check a + b + 0 +]])