From b81d3309b95171cb9d63ccaa129f1d587c2143aa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2014 13:03:25 -0800 Subject: [PATCH] fix(kernel): remove ios hack Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend.cpp | 8 ++++---- src/kernel/builtin.cpp | 3 +-- src/kernel/builtin.h | 4 ++-- src/library/arith/arith.cpp | 8 ++++---- src/library/arith/arith.h | 2 +- src/library/arith/int.cpp | 3 +-- src/library/arith/int.h | 2 +- src/library/arith/nat.cpp | 3 +-- src/library/arith/nat.h | 2 +- src/library/arith/real.cpp | 3 +-- src/library/arith/real.h | 2 +- 11 files changed, 18 insertions(+), 22 deletions(-) diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index 6640fcfaed..e8fb075c8d 100644 --- a/src/frontends/lean/frontend.cpp +++ b/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_nat(env); + import_kernel(env, ios); + 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_real(env); + import_int(env, ios); + import_real(env, ios); } void init_test_frontend(environment const & env) { io_state ios; diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index a0b2d260b3..bee7e12e54 100644 --- a/src/kernel/builtin.cpp +++ b/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) { - io_state ios; +void import_kernel(environment const & env, io_state const & ios) { env->import("kernel", ios); } } diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index bba2b4299a..2a980ecfcc 100644 --- a/src/kernel/builtin.h +++ b/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); } - -void import_kernel(environment const & env); +class io_state; +void import_kernel(environment const & env, io_state const & ios); } diff --git a/src/library/arith/arith.cpp b/src/library/arith/arith.cpp index cb4019f578..25b41289fd 100644 --- a/src/library/arith/arith.cpp +++ b/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) { - import_nat(env); - import_int(env); - import_real(env); +void import_arith(environment const & env, io_state const & ios) { + import_nat(env, ios); + import_int(env, ios); + import_real(env, ios); } } diff --git a/src/library/arith/arith.h b/src/library/arith/arith.h index 819f291268..d214fa75aa 100644 --- a/src/library/arith/arith.h +++ b/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); } diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index 57c4195fb0..2c1a308cb2 100644 --- a/src/library/arith/int.cpp +++ b/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) { - io_state ios; +void import_int(environment const & env, io_state const & ios) { env->import("Int", ios); } diff --git a/src/library/arith/int.h b/src/library/arith/int.h index ddeef15f93..39b8dd971a 100644 --- a/src/library/arith/int.h +++ b/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); } diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp index 6fe36efd5a..52e70aefde 100644 --- a/src/library/arith/nat.cpp +++ b/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) { - io_state ios; +void import_nat(environment const & env, io_state const & ios) { env->import("Nat", ios); } diff --git a/src/library/arith/nat.h b/src/library/arith/nat.h index a9bfbc221a..04db17abe9 100644 --- a/src/library/arith/nat.h +++ b/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); } diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp index 810127ca85..f02d18c5ae 100644 --- a/src/library/arith/real.cpp +++ b/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) { - io_state ios; +void import_real(environment const & env, io_state const & ios) { env->import("Real", ios); } diff --git a/src/library/arith/real.h b/src/library/arith/real.h index b8187096e0..166c8eb0ee 100644 --- a/src/library/arith/real.h +++ b/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();