fix(kernel): remove ios hack

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

src/frontends/lean/frontend.cpp

@@ -559,15 +559,15 @@ static lean_extension & to_ext(environment const & env) {
 void init_frontend(environment const & env, io_state & ios, bool no_kernel) {
     ios.set_formatter(mk_pp_formatter(env));
     if (!no_kernel) {
-        import_kernel(env);
+        import_kernel(env, ios);
-        import_nat(env);
+        import_nat(env, ios);
     }
 }
 void init_test_frontend(environment const & env, io_state & ios) {
     env->set_trusted_imported(true);
     init_frontend(env, ios);
-    import_int(env);
+    import_int(env, ios);
-    import_real(env);
+    import_real(env, ios);
 }
 void init_test_frontend(environment const & env) {
     io_state ios;

src/kernel/builtin.cpp

@@ -171,8 +171,7 @@ MK_CONSTANT(forall_intro_fn,    name("ForallIntro"));
 MK_CONSTANT(exists_elim_fn,     name("ExistsElim"));
 MK_CONSTANT(exists_intro_fn,    name("ExistsIntro"));
 
-void import_kernel(environment const & env) {
+void import_kernel(environment const & env, io_state const & ios) {
-    io_state ios;
     env->import("kernel", ios);
 }
 }

src/kernel/builtin.h

@@ -218,6 +218,6 @@ inline expr ExistsElim(expr const & A, expr const & P, expr const & B, expr cons
 
 expr mk_exists_intro_fn();
 inline expr ExistsIntro(expr const & A, expr const & P, expr const & a, expr const & H) { return mk_app(mk_exists_intro_fn(), A, P, a, H); }
-
+class io_state;
-void import_kernel(environment const & env);
+void import_kernel(environment const & env, io_state const & ios);
 }

src/library/arith/arith.cpp

@@ -7,9 +7,9 @@ Author: Leonardo de Moura
 #include "library/arith/arith.h"
 
 namespace lean {
-void import_arith(environment const & env) {
+void import_arith(environment const & env, io_state const & ios) {
-    import_nat(env);
+    import_nat(env, ios);
-    import_int(env);
+    import_int(env, ios);
-    import_real(env);
+    import_real(env, ios);
 }
 }

src/library/arith/arith.h

@@ -14,5 +14,5 @@ class environment;
 /**
    \brief Import all arithmetic related builtin libraries.
 */
-void import_arith(environment const & env);
+void import_arith(environment const & env, io_state const & ios);
 }

src/library/arith/int.cpp

@@ -156,8 +156,7 @@ static register_builtin_fn nat_to_int_blt("nat_to_int", []() { return mk_nat_to_
 MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"}));
 MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"}));
 
-void import_int(environment const & env) {
+void import_int(environment const & env, io_state const & ios) {
-    io_state ios;
     env->import("Int", ios);
 }
 

src/library/arith/int.h

@@ -90,7 +90,7 @@ class environment;
     \brief Import Integer number library in the given environment (if it has not been imported already).
     It will also load the natural number library.
 */
-void import_int(environment const & env);
+void import_int(environment const & env, io_state const & ios);
 
 void open_int(lua_State * L);
 }

src/library/arith/nat.cpp

@@ -115,8 +115,7 @@ MK_CONSTANT(nat_lt_fn,  name({"Nat", "lt"}));
 MK_CONSTANT(nat_gt_fn,  name({"Nat", "gt"}));
 MK_CONSTANT(nat_id_fn,  name({"Nat", "id"}));
 
-void import_nat(environment const & env) {
+void import_nat(environment const & env, io_state const & ios) {
-    io_state ios;
     env->import("Nat", ios);
 }
 

src/library/arith/nat.h

@@ -55,7 +55,7 @@ inline expr nIf(expr const & c, expr const & t, expr const & e) { return mk_if(N
 
 class environment;
 /** \brief Import Natural number library in the given environment (if it has not been imported already). */
-void import_nat(environment const & env);
+void import_nat(environment const & env, io_state const & ios);
 
 void open_nat(lua_State * L);
 }

src/library/arith/real.cpp

@@ -157,8 +157,7 @@ MK_CONSTANT(real_lt_fn, name({"Real", "lt"}));
 MK_CONSTANT(real_gt_fn, name({"Real", "gt"}));
 MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
 
-void import_real(environment const & env) {
+void import_real(environment const & env, io_state const & ios) {
-    io_state ios;
     env->import("Real", ios);
 }
 

src/library/arith/real.h

@@ -67,7 +67,7 @@ inline expr rIf(expr const & c, expr const & t, expr const & e) { return mk_if(R
 
 class environment;
 /** \brief Import (basic) Real number library in the given environment (if it has not been imported already). */
-void import_real(environment const & env);
+void import_real(environment const & env, io_state const & ios);
 
 /** \brief Coercion from int to real */
 expr mk_int_to_real_fn();