feat(kernel): expose imported predicate

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

src/kernel/environment.cpp

@@ -112,7 +112,6 @@ bool is_end_import(object const & obj) {
     return dynamic_cast<end_import_mark const*>(obj.cell());
 }
 
-static name g_builtin_module("builtin_module");
 class extension_factory {
     std::vector<environment_cell::mk_extension> m_makers;
     mutex                                       m_makers_mutex;
@@ -566,12 +565,6 @@ void environment_cell::auxiliary_section(std::function<void()> fn) {
     }
 }
 
-void environment_cell::import_builtin(char const * id, std::function<void()> 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<std::string>());
 }
 
+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;

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<std::string> 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&>(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<void()> 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

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
    <code>Pi (A : Type), Bool -> A -> A -> A</code>
 */
-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<expr> 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");
+}
 }

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

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<environment_tostring>},
@@ -1209,6 +1215,7 @@ static const struct luaL_Reg environment_m[] = {
     {"set_opaque",     safe_function<environment_set_opaque>},
     {"is_opaque",      safe_function<environment_is_opaque>},
     {"import",         safe_function<environment_import>},
+    {"imported",       safe_function<environment_imported>},
     {"load",           safe_function<environment_load>},
     {0, 0}
 };

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

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