feat(kernel/environment): track which modules were already imported

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

src/bindings/lua/environment.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/formatter.h"
 #include "library/type_inferer.h"
+#include "frontends/lean/frontend.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
 #include "bindings/lua/options.h"
@@ -40,10 +41,15 @@ rw_environment::rw_environment(lua_State * L):
     read_write_environment(get_global_environment(L)) {
 }
 
-static int mk_environment(lua_State * L) {
+static int mk_empty_environment(lua_State * L) {
     return push_environment(L, environment());
 }
 
+static int mk_environment(lua_State * L) {
+    frontend f;
+    return push_environment(L, f.get_environment());
+}
+
 static int environment_has_parent(lua_State * L) {
     ro_environment env(L, 1);
     lua_pushboolean(L, env->has_parent());
@@ -263,9 +269,10 @@ void open_environment(lua_State * L) {
     lua_setfield(L, -2, "__index");
     setfuncs(L, environment_m, 0);
 
-    SET_GLOBAL_FUN(mk_environment,   "environment");
-    SET_GLOBAL_FUN(environment_pred, "is_environment");
-    SET_GLOBAL_FUN(get_environment,  "get_environment");
-    SET_GLOBAL_FUN(get_environment,  "get_env");
+    SET_GLOBAL_FUN(mk_empty_environment,   "empty_environment");
+    SET_GLOBAL_FUN(mk_environment,         "environment");
+    SET_GLOBAL_FUN(environment_pred,       "is_environment");
+    SET_GLOBAL_FUN(get_environment,        "get_environment");
+    SET_GLOBAL_FUN(get_environment,        "get_env");
 }
 }

src/bindings/lua/formatter.cpp

@@ -95,6 +95,10 @@ void set_global_formatter(lua_State * L, formatter const & fmt) {
     }
 }
 
+int get_formatter(lua_State * L) {
+    return push_formatter(L, get_global_formatter(L));
+}
+
 void open_formatter(lua_State * L) {
     luaL_newmetatable(L, formatter_mt);
     lua_pushvalue(L, -1);
@@ -102,5 +106,6 @@ void open_formatter(lua_State * L) {
     setfuncs(L, formatter_m, 0);
 
     SET_GLOBAL_FUN(formatter_pred, "is_formatter");
+    SET_GLOBAL_FUN(get_formatter,  "get_formatter");
 }
 }

src/frontends/lean/frontend.cpp

@@ -366,6 +366,8 @@ frontend::frontend() {
     m_state.set_formatter(mk_pp_formatter(*this));
 }
 frontend::frontend(environment const & env, state const & s):m_env(env), m_state(s) {
+    import_all(m_env);
+    init_builtin_notation(*this);
 }
 
 void frontend::add_infix(name const & opn, unsigned p, expr const & d)  {

src/frontends/lean/notation.cpp

@@ -20,6 +20,8 @@ void add_alias(frontend & f, name const & n, name const & m) {
    \brief Initialize builtin notation.
 */
 void init_builtin_notation(frontend & f) {
+    if (!f.get_environment().mark_builtin_imported("lean_notation"))
+        return;
     f.add_infix("=",  50, mk_homo_eq_fn());
     f.mark_implicit_arguments(mk_homo_eq_fn(), {true, false, false});
     f.mark_implicit_arguments(mk_if_fn(), {true, false, false, false});

src/frontends/lean/parser.cpp

@@ -1391,10 +1391,14 @@ class parser::imp {
 
     void parse_import() {
         next();
-        std::string fname = check_string_next("invalid import command, string (i.e., file name) expected");
+        std::string fname  = check_string_next("invalid import command, string (i.e., file name) expected");
         std::ifstream in(fname);
         if (!in.is_open())
             throw parser_error(sstream() << "invalid import command, failed to open file '" << fname << "'", m_last_cmd_pos);
+        if (!m_frontend.get_environment().mark_imported(fname.c_str())) {
+            diagnostic(m_frontend) << "Module '" << fname << "' has already been imported" << endl;
+            return;
+        }
         try {
             if (m_verbose)
                 regular(m_frontend) << "Importing file '" << fname << "'" << endl;

src/kernel/builtin.cpp

@@ -168,6 +168,8 @@ MK_CONSTANT(eta_fn,         name("Eta"));
 MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
 
 void import_basic(environment & env) {
+    if (!env.mark_builtin_imported("basic"))
+        return;
     env.add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
     env.add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
 

src/kernel/environment.cpp

@@ -4,10 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <cstdlib>
 #include <algorithm>
 #include <vector>
 #include <atomic>
 #include <tuple>
+#include <set>
 #include <unordered_map>
 #include <mutex>
 #include "util/safe_arith.h"
@@ -19,7 +21,7 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 
 namespace lean {
-
+static name g_builtin_module("builtin_module");
 class extension_factory {
     std::vector<environment::mk_extension> m_makers;
     std::mutex                             m_makers_mutex;
@@ -67,6 +69,7 @@ struct environment::imp {
     std::vector<object>                  m_objects;
     object_dictionary                    m_object_dictionary;
     std::unique_ptr<type_checker>        m_type_checker;
+    std::set<name>                       m_imported_modules;   // set of imported files and builtin modules
 
     std::vector<std::unique_ptr<extension>> m_extensions;
     friend class extension;
@@ -402,6 +405,34 @@ struct environment::imp {
         }
     }
 
+    bool already_imported(name const & n) const {
+        if (m_imported_modules.find(n) != m_imported_modules.end())
+            return true;
+        else if (has_parent())
+            return m_parent->already_imported(n);
+        else
+            return false;
+    }
+
+    bool mark_imported_core(name n, environment const & env) {
+        if (already_imported(n)) {
+            return false;
+        } else if (has_children()) {
+            throw read_only_environment_exception(env);
+        } else {
+            m_imported_modules.insert(n);
+            return true;
+        }
+    }
+
+    bool mark_imported(char const * fname, environment const & env) {
+        return mark_imported_core(name(realpath(fname, nullptr)), env);
+    }
+
+    bool mark_builtin_imported(char const * id, environment const & env) {
+        return mark_imported_core(name(g_builtin_module, id), env);
+    }
+
     imp():
         m_num_children(0) {
         init_uvars();
@@ -533,6 +564,14 @@ void environment::display(std::ostream & out) const {
     m_ptr->display(out, *this);
 }
 
+bool environment::mark_imported(char const * fname) {
+    return m_ptr->mark_imported(fname, *this);
+}
+
+bool environment::mark_builtin_imported(char const * id) {
+    return m_ptr->mark_builtin_imported(id, *this);
+}
+
 environment::extension const & environment::get_extension_core(unsigned extid) const {
     return m_ptr->get_extension_core(extid);
 }

src/kernel/environment.h

@@ -26,8 +26,13 @@ private:
     friend class read_only_environment;
     friend class read_write_environment;
 public:
+    typedef std::weak_ptr<imp> weak_ref;
+
     environment();
     ~environment();
+    environment(weak_ref const & r);
+
+    weak_ref to_weak_ref() const { return weak_ref(m_ptr); }
 
     friend bool is_eqp(environment const & env1, environment const & env2) { return env1.m_ptr.get() == env2.m_ptr.get(); }
     // =======================================
@@ -281,9 +286,15 @@ public:
         return static_cast<Ext&>(ext);
     }
 
-public:
-    typedef std::weak_ptr<imp> weak_ref;
-    weak_ref to_weak_ref() const { return weak_ref(m_ptr); }
-    environment(weak_ref const & r);
+    /**
+        \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);
+    /**
+        \brief Return true iff the given builtin id was not already marked as imported.
+        It will also mark the id as imported.
+    */
+    bool mark_builtin_imported(char const * id);
 };
 }

src/library/arith/int.cpp

@@ -145,7 +145,7 @@ MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"}));
 MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"}));
 
 void import_int(environment & env) {
-    if (env.find_object(to_value(Int).get_name()))
+    if (!env.mark_builtin_imported("int"))
         return;
     import_nat(env);
     expr i_i  = Int >> Int;

src/library/arith/nat.cpp

@@ -109,7 +109,7 @@ MK_CONSTANT(nat_gt_fn,  name({"Nat", "gt"}));
 MK_CONSTANT(nat_id_fn,  name({"Nat", "id"}));
 
 void import_nat(environment & env) {
-    if (env.find_object(to_value(Nat).get_name()))
+    if (!env.mark_builtin_imported("nat"))
         return;
     expr nn_b = Nat >> (Nat >> Bool);
     expr x    = Const("x");

src/library/arith/real.cpp

@@ -133,7 +133,7 @@ MK_CONSTANT(real_lt_fn, name({"Real", "lt"}));
 MK_CONSTANT(real_gt_fn, name({"Real", "gt"}));
 
 void import_real(environment & env) {
-    if (env.find_object(to_value(Real).get_name()))
+    if (!env.mark_builtin_imported("real"))
         return;
     expr rr_b = Real >> (Real >> Bool);
     expr rr_r = Real >> (Real >> Real);
@@ -172,7 +172,7 @@ MK_BUILTIN(int_to_real_fn,  int_to_real_value);
 MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
 
 void import_int_to_real_coercions(environment & env) {
-    if (env.find_object(to_value(mk_int_to_real_fn()).get_name()))
+    if (!env.mark_builtin_imported("real_coercions"))
         return;
     import_int(env);
     import_real(env);

src/library/arith/special_fn.cpp

@@ -29,7 +29,7 @@ MK_CONSTANT(sech_fn, name("sech"));
 MK_CONSTANT(csch_fn, name("csch"));
 
 void import_special_fn(environment & env) {
-    if (env.find_object(const_name(mk_exp_fn())))
+    if (!env.mark_builtin_imported("special_fn"))
         return;
     import_real(env);
 

src/library/basic_thms.cpp

@@ -47,6 +47,8 @@ MK_CONSTANT(range_inj_fn,      name("range_inj"));
 #endif
 
 void import_basic_thms(environment & env) {
+    if (!env.mark_builtin_imported("basic_thms"))
+        return;
     expr A  = Const("A");
     expr a  = Const("a");
     expr b  = Const("b");

src/library/cast/cast.cpp

@@ -105,7 +105,7 @@ MK_CONSTANT(dom_inj_fn, name("DomInj"));
 MK_CONSTANT(ran_inj_fn, name("RanInj"));
 
 void import_cast(environment & env) {
-    if (env.find_object(to_value(mk_Cast_fn()).get_name()))
+    if (!env.mark_builtin_imported("cast"))
         return;
     expr x         = Const("x");
     expr A         = Const("A");

tests/lean/mod1.lean

@@ -0,0 +1,14 @@
+Import "simple.lean"
+Import "simple.lean"
+(**
+   local env = environment() -- create new environment
+   parse_lean_cmds([[
+      Import "simple.lean"
+      Import "simple.lean"
+      Check x + y
+      Variable z : Int
+      Check z
+   ]], env)
+   -- Remark: z is not defined in the main environment
+**)
+Check z

tests/lean/mod1.lean.expected.out

@@ -0,0 +1,12 @@
+  Set: pp::colors
+  Set: pp::unicode
+Importing file 'simple.lean'
+  Assumed: x
+  Assumed: y
+Importing file 'simple.lean'
+  Assumed: x
+  Assumed: y
+x + y : ℤ
+  Assumed: z
+z : ℤ
+Error (line: 14, pos: 6) unknown identifier 'z'

tests/lean/simple.lean

@@ -0,0 +1,2 @@
+Variable x : Int
+Variable y : Int

tests/lean/simple.lean.expected.out

@@ -0,0 +1,4 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: x
+  Assumed: y

tests/lua/env1.lua

@@ -1,7 +1,7 @@
 e = environment()
 assert(is_environment(e))
-e:add_uvar("M")
-print(e:get_uvar("M"))
+e:add_uvar("M1")
+print(e:get_uvar("M1"))
 e:add_var("N", Type())
 N, M = Consts("N M")
 e:add_var("a", N)

tests/lua/env2.lua

@@ -2,7 +2,9 @@ env = environment()
 env:add_var("N", Type())
 env:add_var("x", Const("N"))
 for v in env:objects() do
-   print(v:get_name())
+   if v:has_name() then
+      print(v:get_name())
+   end
 end
 assert(not env:find_object("N"):is_null())
 assert(env:find_object("Z"):is_null())

tests/lua/fmt1.lua

@@ -0,0 +1,2 @@
+fmt = get_formatter()
+print(fmt(Const("a"), options()))