From 08718e33dc0de70befa3637d6ec974cb0fb73433 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2013 13:35:37 -0800 Subject: [PATCH] refactor(builtin): only load the kernel and natural numbers by default Signed-off-by: Leonardo de Moura --- examples/lean/ex4.lean | 1 + src/builtin/CMakeLists.txt | 4 +- src/builtin/cast.olean | Bin 925 -> 902 bytes src/builtin/int.olean | Bin 1738 -> 1752 bytes src/builtin/real.olean | Bin 1195 -> 1220 bytes src/builtin/specialfn.olean | Bin 1122 -> 1111 bytes src/frontends/lean/frontend.cpp | 22 ++- src/frontends/lean/frontend.h | 10 +- src/library/kernel_bindings.cpp | 19 +++ src/tests/frontends/lean/parser.cpp | 6 +- src/tests/kernel/environment.cpp | 12 +- src/tests/kernel/metavar.cpp | 4 +- src/tests/kernel/normalizer.cpp | 10 +- src/tests/kernel/threads.cpp | 2 +- src/tests/kernel/type_checker.cpp | 36 ++--- src/tests/library/arith.cpp | 12 +- src/tests/library/elaborator/elaborator.cpp | 56 +++---- src/tests/library/rewriter/rewriter.cpp | 28 ++-- src/tests/library/tactic/tactic.cpp | 4 +- tests/lean/abst.lean | 1 + tests/lean/abst.lean.expected.out | 1 + tests/lean/apply_tac1.lean | 3 +- tests/lean/apply_tac1.lean.expected.out | 2 + tests/lean/arith1.lean | 1 + tests/lean/arith1.lean.expected.out | 1 + tests/lean/arith2.lean | 2 + tests/lean/arith2.lean.expected.out | 2 + tests/lean/arith3.lean | 1 + tests/lean/arith3.lean.expected.out | 1 + tests/lean/arith6.lean | 1 + tests/lean/arith6.lean.expected.out | 1 + tests/lean/arith7.lean | 1 + tests/lean/arith7.lean.expected.out | 1 + tests/lean/arith8.lean | 1 + tests/lean/arith8.lean.expected.out | 1 + tests/lean/arrow.lean | 1 + tests/lean/arrow.lean.expected.out | 1 + tests/lean/bad1.lean | 1 + tests/lean/bad1.lean.expected.out | 1 + tests/lean/bad2.lean | 1 + tests/lean/bad2.lean.expected.out | 1 + tests/lean/bad3.lean | 1 + tests/lean/bad3.lean.expected.out | 1 + tests/lean/bad4.lean | 1 + tests/lean/bad4.lean.expected.out | 1 + tests/lean/bad5.lean | 1 + tests/lean/bad5.lean.expected.out | 1 + tests/lean/bad6.lean | 2 + tests/lean/bad6.lean.expected.out | 2 + tests/lean/bad7.lean | 1 + tests/lean/bad7.lean.expected.out | 1 + tests/lean/bad8.lean | 1 + tests/lean/bad8.lean.expected.out | 1 + tests/lean/cast1.lean | 3 +- tests/lean/cast1.lean.expected.out | 3 +- tests/lean/conv.lean | 1 + tests/lean/conv.lean.expected.out | 1 + tests/lean/elab1.lean.expected.out | 114 ++------------ tests/lean/elab4.lean.expected.out | 2 - tests/lean/elab5.lean.expected.out | 2 - tests/lean/eq1.lean | 2 +- tests/lean/eq1.lean.expected.out | 1 + tests/lean/eq2.lean | 1 + tests/lean/eq2.lean.expected.out | 1 + tests/lean/exists1.lean | 1 + tests/lean/exists1.lean.expected.out | 1 + tests/lean/exists2.lean | 1 + tests/lean/exists2.lean.expected.out | 1 + tests/lean/exists3.lean | 1 + tests/lean/exists3.lean.expected.out | 1 + tests/lean/exists6.lean | 1 + tests/lean/exists6.lean.expected.out | 1 + tests/lean/explicit.lean | 1 + tests/lean/explicit.lean.expected.out | 3 +- tests/lean/forall1.lean | 1 + tests/lean/forall1.lean.expected.out | 1 + tests/lean/ho.lean | 1 + tests/lean/ho.lean.expected.out | 1 + tests/lean/implicit1.lean | 2 + tests/lean/implicit1.lean.expected.out | 2 + tests/lean/implicit2.lean | 1 + tests/lean/implicit2.lean.expected.out | 3 +- tests/lean/implicit3.lean | 2 + tests/lean/implicit3.lean.expected.out | 1 + tests/lean/implicit4.lean | 1 + tests/lean/implicit4.lean.expected.out | 1 + tests/lean/implicit5.lean | 2 + tests/lean/implicit5.lean.expected.out | 2 + tests/lean/implicit6.lean | 1 + tests/lean/implicit6.lean.expected.out | 1 + tests/lean/interactive/t7.lean | 1 + tests/lean/interactive/t7.lean.expected.out | 3 +- tests/lean/let1.lean | 1 + tests/lean/let1.lean.expected.out | 1 + tests/lean/let3.lean | 1 + tests/lean/let3.lean.expected.out | 1 + tests/lean/let4.lean | 1 + tests/lean/let4.lean.expected.out | 7 +- tests/lean/loop2.lean | 2 + tests/lean/loop2.lean.expected.out | 1 + tests/lean/lua1.lean | 1 + tests/lean/lua1.lean.expected.out | 1 + tests/lean/lua11.lean | 1 + tests/lean/lua11.lean.expected.out | 1 + tests/lean/lua12.lean | 1 + tests/lean/lua12.lean.expected.out | 1 + tests/lean/lua13.lean | 1 + tests/lean/lua13.lean.expected.out | 1 + tests/lean/lua14.lean | 1 + tests/lean/lua14.lean.expected.out | 1 + tests/lean/lua15.lean | 1 + tests/lean/lua15.lean.expected.out | 163 +++++--------------- tests/lean/lua16.lean | 2 +- tests/lean/lua16.lean.expected.out | 1 + tests/lean/lua17.lean | 2 +- tests/lean/lua17.lean.expected.out | 1 + tests/lean/lua18.lean | 1 + tests/lean/lua18.lean.expected.out | 1 + tests/lean/lua3.lean | 2 +- tests/lean/lua3.lean.expected.out | 1 + tests/lean/lua4.lean | 1 + tests/lean/lua4.lean.expected.out | 1 + tests/lean/lua5.lean | 1 + tests/lean/lua5.lean.expected.out | 1 + tests/lean/lua6.lean | 1 + tests/lean/lua6.lean.expected.out | 1 + tests/lean/lua8.lean | 1 + tests/lean/lua8.lean.expected.out | 1 + tests/lean/lua9.lean | 1 + tests/lean/lua9.lean.expected.out | 1 + tests/lean/norm_tac.lean | 1 + tests/lean/norm_tac.lean.expected.out | 1 + tests/lean/overload2.lean | 2 + tests/lean/overload2.lean.expected.out | 22 +-- tests/lean/push.lean | 1 + tests/lean/push.lean.expected.out | 7 +- tests/lean/revapp.lean | 1 + tests/lean/revapp.lean.expected.out | 1 + tests/lean/scope.lean | 1 + tests/lean/scope.lean.expected.out | 1 + tests/lean/simple.lean | 1 + tests/lean/simple.lean.expected.out | 1 + tests/lean/single.lean | 1 + tests/lean/single.lean.expected.out | 1 + tests/lean/slow/deep.lean | 1 + tests/lean/slow/deep.lean.expected.out | 1 + tests/lean/slow/tactic1.lean | 1 + tests/lean/slow/tactic1.lean.expected.out | 1 + tests/lean/subst.lean | 1 + tests/lean/subst.lean.expected.out | 1 + tests/lean/tactic13.lean | 1 + tests/lean/tactic13.lean.expected.out | 1 + tests/lean/tactic14.lean | 1 + tests/lean/tactic14.lean.expected.out | 1 + tests/lean/tst14.lean | 1 + tests/lean/tst14.lean.expected.out | 1 + tests/lean/tst8.lean | 1 + tests/lean/tst8.lean.expected.out | 1 + tests/lean/ty1.lean | 1 + tests/lean/ty1.lean.expected.out | 3 +- tests/lean/vars1.lean | 1 + tests/lean/vars1.lean.expected.out | 3 +- tests/lua/coercion_bug1.lua | 2 +- tests/lua/env4.lua | 1 + tests/lua/front.lua | 2 + tests/lua/hidden1.lua | 1 + tests/lua/single.lua | 1 + tests/lua/template1.lua | 1 + 168 files changed, 362 insertions(+), 357 deletions(-) diff --git a/examples/lean/ex4.lean b/examples/lean/ex4.lean index e60f52f957..39106880e0 100644 --- a/examples/lean/ex4.lean +++ b/examples/lean/ex4.lean @@ -1,4 +1,5 @@ Import tactic +Import int Definition a : Nat := 10 (* Trivial indicates a "proof by evaluation" *) Theorem T1 : a > 0 := (by trivial) diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 437c481130..7d63e74463 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -68,9 +68,9 @@ endfunction() add_kernel_theory("kernel.lean" "${CMAKE_CURRENT_BINARY_DIR}/macros.lua") add_kernel_theory("nat.lean" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean") -add_kernel_theory("int.lean" "${CMAKE_CURRENT_BINARY_DIR}/nat.olean") -add_kernel_theory("real.lean" "${CMAKE_CURRENT_BINARY_DIR}/int.olean") +add_theory("int.lean" "${CMAKE_CURRENT_BINARY_DIR}/nat.olean") +add_theory("real.lean" "${CMAKE_CURRENT_BINARY_DIR}/int.olean") add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/real.olean") add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean") diff --git a/src/builtin/cast.olean b/src/builtin/cast.olean index 481d07bb3426069eef7473ca866aff3d611cc8e2..43144a7f9f51bc6f2aaf243d739ab0208157a50c 100644 GIT binary patch delta 10 RcmbQs-o`#bd!th{GXN7t13mx% delta 33 jcmZo;pUXZ$Tg)@JAit=DAv3Rp0m>{&P0ZP-6~hbwyT%J5 diff --git a/src/builtin/int.olean b/src/builtin/int.olean index e5a503925f20c0428244dcf4a89557288e2b2114..9af0cddce7e7b4684b84af33b131617545179b26 100644 GIT binary patch delta 18 ZcmX@bdxLj^BztyhQC?~e!$zSUYyd!)25$fW delta 10 Rcmcb?dy030KhQC?~egJ*6*eo+ZSUSbKuMxmK30GM?N+yDRo delta 10 RcmX@Yxteo=get_extension(g_lean_extension_initializer.m_extid); } -/** - \brief Import all definitions and notation. -*/ void init_frontend(environment const & env, io_state & ios, bool no_kernel) { ios.set_formatter(mk_pp_formatter(env)); - if (!no_kernel) - import_all(env); + if (!no_kernel) { + import_kernel(env); + import_nat(env); + } } -void init_frontend(environment const & env) { - io_state ios; +void init_full_frontend(environment const & env, io_state & ios) { init_frontend(env, ios); + import_int(env); + import_real(env); +} +void init_full_frontend(environment const & env) { + io_state ios; + init_full_frontend(env, ios); } void add_infix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) { diff --git a/src/frontends/lean/frontend.h b/src/frontends/lean/frontend.h index 9d73d22c06..ea687f411a 100644 --- a/src/frontends/lean/frontend.h +++ b/src/frontends/lean/frontend.h @@ -14,10 +14,16 @@ Author: Leonardo de Moura namespace lean { /** - \brief Import all definitions and notation. + \brief Load kernel, nat and set pretty printer. */ void init_frontend(environment const & env, io_state & ios, bool no_kernel = false); -void init_frontend(environment const & env); + +/* + \brief Load kernel, nat, int, real and set pretty printer. + It is used for testing. +*/ +void init_full_frontend(environment const & env, io_state & ios); +void init_full_frontend(environment const & env); /** @name Notation for parsing and pretty printing. diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 969d15c662..f8fb5bbb24 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1139,6 +1139,24 @@ static int environment_is_opaque(lua_State * L) { return 1; } +static int environment_import(lua_State * L) { + rw_shared_environment env(L, 1); + int nargs = lua_gettop(L); + if (nargs == 3) { + env->import(luaL_checkstring(L, 2), to_io_state(L, 3)); + } else { + io_state * ios = get_io_state(L); + if (ios) { + env->import(luaL_checkstring(L, 2), *ios); + } else { + io_state ios; + ios.set_options(get_global_options(L)); + env->import(luaL_checkstring(L, 2), ios); + } + } + return 0; +} + static const struct luaL_Reg environment_m[] = { {"__gc", environment_gc}, // never throws {"__tostring", safe_function}, @@ -1162,6 +1180,7 @@ static const struct luaL_Reg environment_m[] = { {"local_objects", safe_function}, {"set_opaque", safe_function}, {"is_opaque", safe_function}, + {"import", safe_function}, {0, 0} }; diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp index adb6dd827d..b50bd2c9ab 100644 --- a/src/tests/frontends/lean/parser.cpp +++ b/src/tests/frontends/lean/parser.cpp @@ -42,7 +42,7 @@ static void parse_error(environment const & env, io_state const & ios, char cons } static void tst1() { - environment env; io_state ios; init_frontend(env, ios); + environment env; io_state ios; init_full_frontend(env, ios); parse(env, ios, "Variable x : Bool Variable y : Bool Axiom H : x && y || x => x"); parse(env, ios, "Eval true && true"); parse(env, ios, "Show true && false Eval true && false"); @@ -63,7 +63,7 @@ static void check(environment const & env, io_state & ios, char const * str, exp } static void tst2() { - environment env; io_state ios; init_frontend(env, ios); + environment env; io_state ios; init_full_frontend(env, ios); env->add_var("x", Bool); env->add_var("y", Bool); env->add_var("z", Bool); @@ -80,7 +80,7 @@ static void tst2() { } static void tst3() { - environment env; io_state ios; init_frontend(env, ios); + environment env; io_state ios; init_full_frontend(env, ios); parse(env, ios, "Help"); parse(env, ios, "Help Options"); parse_error(env, ios, "Help Echo"); diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index bc90ab3706..e66f838e20 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -63,7 +63,7 @@ static void tst2() { static void tst3() { std::cout << "tst3\n"; - environment env; init_frontend(env); + environment env; init_full_frontend(env); try { env->add_definition("a", Int, Const("a")); lean_unreachable(); @@ -108,7 +108,7 @@ static void tst3() { static void tst4() { std::cout << "tst4\n"; - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_definition("a", Int, iVal(1), true); // add opaque definition expr t = iAdd(Const("a"), iVal(1)); std::cout << t << " --> " << normalize(t, env) << "\n"; @@ -121,7 +121,7 @@ static void tst4() { } static void tst5() { - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_definition("a", Int, iVal(1), true); // add opaque definition try { std::cout << type_check(iAdd(Const("a"), Int), env) << "\n"; @@ -132,7 +132,7 @@ static void tst5() { } static void tst6() { - environment env; init_frontend(env); + environment env; init_full_frontend(env); level u = env->add_uvar("u", level() + 1); level w = env->add_uvar("w", u + 1); env->add_var("f", mk_arrow(Type(u), Type(u))); @@ -159,7 +159,7 @@ static void tst6() { } static void tst7() { - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("a", Int); env->add_var("b", Int); expr t = If(Int, True, Const("a"), Const("b")); @@ -207,7 +207,7 @@ static void tst9() { static void tst10() { environment env; - init_frontend(env); + init_full_frontend(env); env->add_definition("a", Int, iVal(1)); lean_assert(env->get_object("a").get_weight() == 1); expr a = Const("a"); diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 85e4f2e5c7..440be37b61 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -546,7 +546,7 @@ static void tst26() { */ std::cout << "\ntst26\n"; environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; buffer up; type_checker checker(env); @@ -588,7 +588,7 @@ static void tst27() { */ std::cout << "\ntst27\n"; environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; buffer up; type_checker checker(env); diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index 8789912341..edc2f2fac4 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -191,7 +191,7 @@ static void tst2() { static void tst3() { environment env; - init_frontend(env); + init_full_frontend(env); env->add_var("a", Bool); expr t1 = Const("a"); expr t2 = Const("a"); @@ -219,7 +219,7 @@ static void tst5() { #if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) expr t = mk_big(18); environment env; - init_frontend(env); + init_full_frontend(env); env->add_var("f", Bool >> (Bool >> Bool)); env->add_var("a", Bool); normalizer proc(env); @@ -255,7 +255,7 @@ static void tst6() { static void tst7() { environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; expr m1 = menv->mk_metavar(); expr x = Const("x"); @@ -279,7 +279,7 @@ static void tst7() { static void tst8() { environment env; - init_frontend(env); + init_full_frontend(env); env->add_var("P", Int >> (Int >> Bool)); expr P = Const("P"); expr v0 = Var(0); @@ -307,7 +307,7 @@ static void tst9() { static void tst10() { environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; context ctx({{"x", Bool}, {"y", Bool}}); expr m = menv->mk_metavar(ctx); diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp index 6b420c1e66..66325400c5 100644 --- a/src/tests/kernel/threads.cpp +++ b/src/tests/kernel/threads.cpp @@ -26,7 +26,7 @@ expr norm(expr const & e, environment & env) { } static void mk(expr const & a) { - environment env; init_frontend(env); + environment env; init_full_frontend(env); expr b = Const("b"); for (unsigned i = 0; i < 100; i++) { expr h = Const("h"); diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index 532715d595..522657c151 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -78,7 +78,7 @@ static void tst2() { static void tst3() { environment env; - init_frontend(env); + init_full_frontend(env); expr f = Fun("a", Bool, Eq(Const("a"), True)); std::cout << type_check(f, env) << "\n"; lean_assert(type_check(f, env) == mk_arrow(Bool, Bool)); @@ -88,7 +88,7 @@ static void tst3() { static void tst4() { environment env; - init_frontend(env); + init_full_frontend(env); expr a = Eq(iVal(1), iVal(2)); expr pr = mk_lambda("x", a, Var(0)); std::cout << type_check(pr, env) << "\n"; @@ -96,7 +96,7 @@ static void tst4() { static void tst5() { environment env; - init_frontend(env); + init_full_frontend(env); env->add_var("P", Bool); expr P = Const("P"); expr H = Const("H"); @@ -114,7 +114,7 @@ static void tst5() { static void tst6() { environment env; - init_frontend(env); + init_full_frontend(env); expr A = Const("A"); expr f = Const("f"); expr x = Const("x"); @@ -129,7 +129,7 @@ static void tst6() { static void tst7() { environment env; - init_frontend(env); + init_full_frontend(env); expr A = Const(name{"foo", "bla", "bla", "foo"}); expr f = Const("f"); expr x = Const("x"); @@ -144,7 +144,7 @@ static void tst7() { static void tst8() { environment env; - init_frontend(env); + init_full_frontend(env); env->add_var("P", mk_arrow(Int, mk_arrow(Int, Bool))); env->add_var("x", Int); expr P = Const("P"); @@ -164,7 +164,7 @@ static void tst8() { static void tst9() { environment env; - init_frontend(env); + init_full_frontend(env); env->add_var("P", mk_arrow(Int, mk_arrow(Int, Bool))); env->add_var("x", Int); expr P = Const("P"); @@ -184,7 +184,7 @@ static void tst9() { static void tst10() { environment env; - init_frontend(env); + init_full_frontend(env); env->add_var("f", mk_arrow(Int, Int)); env->add_var("b", Int); expr f = Const("f"); @@ -201,7 +201,7 @@ static void tst10() { static void tst11() { environment env; - init_frontend(env); + init_full_frontend(env); env->add_var("f", Int >> (Int >> Int)); env->add_var("a", Int); unsigned n = 1000; @@ -232,7 +232,7 @@ static void tst12() { #if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) expr t = mk_big(18); environment env; - init_frontend(env); + init_full_frontend(env); env->add_var("f", Int >> (Int >> Int)); env->add_var("a", Int); type_checker checker(env); @@ -255,7 +255,7 @@ static void tst12() { static void tst13() { environment env; - init_frontend(env); + init_full_frontend(env); env->add_var("f", Type() >> Type()); expr f = Const("f"); std::cout << type_check(f(Bool), env) << "\n"; @@ -264,7 +264,7 @@ static void tst13() { static void tst14() { environment env; - init_frontend(env); + init_full_frontend(env); expr f = Const("f"); expr a = Const("a"); env->add_var("f", Int >> Int); @@ -282,7 +282,7 @@ static void tst14() { static void tst15() { environment env; - init_frontend(env); + init_full_frontend(env); context ctx1, ctx2; expr A = Const("A"); expr vec1 = Const("vec1"); @@ -350,7 +350,7 @@ static void f2(type_checker & tc, expr const & F) { static void tst17() { environment env; - init_frontend(env); + init_full_frontend(env); type_checker tc(env); expr A = Const("A"); expr F; @@ -374,7 +374,7 @@ static std::ostream & operator<<(std::ostream & out, buffer uc; type_inferer inferer(env); diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp index 5701a4c14c..27857663dd 100644 --- a/src/tests/library/arith.cpp +++ b/src/tests/library/arith.cpp @@ -16,7 +16,7 @@ using namespace lean; static void tst0() { environment env; - init_frontend(env); + init_full_frontend(env); normalizer norm(env); env->add_var("n", Nat); expr n = Const("n"); @@ -47,7 +47,7 @@ static void tst0() { static void tst1() { environment env; - init_frontend(env); + init_full_frontend(env); expr e = mk_int_value(mpz(10)); lean_assert(is_int_value(e)); lean_assert(type_check(e, env) == Int); @@ -56,7 +56,7 @@ static void tst1() { static void tst2() { environment env; - init_frontend(env); + init_full_frontend(env); expr e = iAdd(iVal(10), iVal(30)); std::cout << e << "\n"; std::cout << normalize(e, env) << "\n"; @@ -73,7 +73,7 @@ static void tst2() { static void tst3() { environment env; - init_frontend(env); + init_full_frontend(env); expr e = iMul(iVal(10), iVal(30)); std::cout << e << "\n"; std::cout << normalize(e, env) << "\n"; @@ -90,7 +90,7 @@ static void tst3() { static void tst4() { environment env; - init_frontend(env); + init_full_frontend(env); expr e = iSub(iVal(10), iVal(30)); std::cout << e << "\n"; std::cout << normalize(e, env) << "\n"; @@ -107,7 +107,7 @@ static void tst4() { static void tst5() { environment env; - init_frontend(env); + init_full_frontend(env); env->add_var(name("a"), Int); expr e = Eq(iVal(3), iVal(4)); std::cout << e << " --> " << normalize(e, env) << "\n"; diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp index 19437cda5d..b1943a4edb 100644 --- a/src/tests/library/elaborator/elaborator.cpp +++ b/src/tests/library/elaborator/elaborator.cpp @@ -20,7 +20,7 @@ using namespace lean; static void tst1() { environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; buffer ucs; type_checker checker(env); @@ -75,7 +75,7 @@ static void tst2() { ?m4 in { Id, nat2int, nat2real } */ environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; buffer ucs; type_checker checker(env); @@ -116,7 +116,7 @@ static void tst3() { ?m5 in { Id, int2real } */ environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; buffer ucs; type_checker checker(env); @@ -158,7 +158,7 @@ static void tst4() { ?m6 in { Id, int2real } */ environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; buffer ucs; type_checker checker(env); @@ -202,7 +202,7 @@ static void tst5() { ?m4 in { Id, int2real } */ environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; buffer ucs; type_checker checker(env); @@ -239,7 +239,7 @@ static void tst6() { Theorem T : (f a (f b b)) == a := Subst _ _ _ _ H1 H2 */ environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; buffer ucs; type_checker checker(env); @@ -307,7 +307,7 @@ static void unsolved(expr const & e, environment const & env) { static void tst7() { std::cout << "\nTST 7\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr A = Const("A"); expr B = Const("B"); expr F = Const("F"); @@ -328,7 +328,7 @@ static void tst7() { static void tst8() { std::cout << "\nTST 8\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr a = Const("a"); expr b = Const("b"); expr c = Const("c"); @@ -354,7 +354,7 @@ static void tst8() { static void tst9() { std::cout << "\nTST 9\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr Nat = Const("N"); env->add_var("N", Type()); env->add_var("vec", Nat >> Type()); @@ -386,7 +386,7 @@ static void tst9() { static void tst10() { std::cout << "\nTST 10\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr Nat = Const("N"); env->add_var("N", Type()); expr R = Const("R"); @@ -410,7 +410,7 @@ static void tst10() { static void tst11() { std::cout << "\nTST 11\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr A = Const("A"); expr B = Const("B"); expr a = Const("a"); @@ -428,7 +428,7 @@ static void tst11() { static void tst12() { std::cout << "\nTST 12\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr lst = Const("list"); expr nil = Const("nil"); expr cons = Const("cons"); @@ -449,7 +449,7 @@ static void tst12() { static void tst13() { std::cout << "\nTST 13\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr B = Const("B"); expr A = Const("A"); expr x = Const("x"); @@ -472,7 +472,7 @@ static void tst13() { static void tst14() { std::cout << "\nTST 14\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr A = Const("A"); expr B = Const("B"); expr f = Const("f"); @@ -513,7 +513,7 @@ static void tst14() { static void tst15() { std::cout << "\nTST 15\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr A = Const("A"); expr B = Const("B"); expr C = Const("C"); @@ -539,7 +539,7 @@ static void tst15() { static void tst16() { std::cout << "\nTST 16\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr a = Const("a"); expr b = Const("b"); expr c = Const("c"); @@ -560,7 +560,7 @@ static void tst16() { EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3))), env); environment env2; - init_frontend(env2); + init_full_frontend(env2); success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}}, EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3))), Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}}, @@ -577,7 +577,7 @@ static void tst16() { void tst17() { std::cout << "\nTST 17\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr A = Const("A"); expr B = Const("B"); expr a = Const("a"); @@ -592,7 +592,7 @@ void tst17() { void tst18() { std::cout << "\nTST 18\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr A = Const("A"); expr h = Const("h"); expr f = Const("f"); @@ -606,7 +606,7 @@ void tst18() { void tst19() { std::cout << "\nTST 19\n"; environment env; - init_frontend(env); + init_full_frontend(env); expr R = Const("R"); expr A = Const("A"); expr r = Const("r"); @@ -633,7 +633,7 @@ void tst19() { void tst20() { std::cout << "\nTST 20\n"; environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; expr N = Const("N1"); expr M = Const("M1"); @@ -666,7 +666,7 @@ void tst20() { void tst21() { std::cout << "\nTST 21\n"; environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; expr N = Const("N"); expr M = Const("M"); @@ -698,7 +698,7 @@ void tst21() { void tst22() { std::cout << "\nTST 22\n"; environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; expr N = Const("N"); env->add_var("N", Type()); @@ -733,7 +733,7 @@ void tst22() { void tst23() { std::cout << "\nTST 23\n"; environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; expr N = Const("N"); env->add_var("N", Type()); @@ -763,7 +763,7 @@ void tst23() { void tst24() { std::cout << "\nTST 24\n"; environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; expr N = Const("N"); env->add_var("N", Type()); @@ -783,7 +783,7 @@ void tst24() { void tst25() { std::cout << "\nTST 25\n"; environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; expr N = Const("N"); env->add_var("N", Type()); @@ -819,7 +819,7 @@ void tst26() { Axiom H : g _ a = a */ environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; buffer ucs; type_checker checker(env); @@ -849,7 +849,7 @@ void tst27() { fun f : _, eq _ ((g _ f) a) a */ environment env; - init_frontend(env); + init_full_frontend(env); metavar_env menv; buffer ucs; type_checker checker(env); diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp index 17812bc41c..840d0eecad 100644 --- a/src/tests/library/rewriter/rewriter.cpp +++ b/src/tests/library/rewriter/rewriter.cpp @@ -38,7 +38,7 @@ static void theorem_rewriter1_tst() { Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("a", Nat); env->add_var("b", Nat); env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z @@ -70,7 +70,7 @@ static void theorem_rewriter2_tst() { Eq(nAdd(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("a", Nat); env->add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 @@ -108,7 +108,7 @@ static void then_rewriter1_tst() { Eq(nAdd(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("a", Nat); env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z env->add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 @@ -164,7 +164,7 @@ static void then_rewriter2_tst() { Eq(nAdd(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("a", Nat); env->add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z @@ -223,7 +223,7 @@ static void orelse_rewriter1_tst() { Eq(nAdd(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("a", Nat); env->add_var("b", Nat); env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z @@ -270,7 +270,7 @@ static void orelse_rewriter2_tst() { Eq(nAdd(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("a", Nat); env->add_var("b", Nat); env->add_axiom("ADD_ASSOC", add_assoc_thm_type); @@ -319,7 +319,7 @@ static void try_rewriter1_tst() { Eq(nAdd(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("a", Nat); env->add_var("b", Nat); env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z @@ -370,7 +370,7 @@ static void try_rewriter2_tst() { Eq(nAdd(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("a", Nat); env->add_var("b", Nat); env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z @@ -416,7 +416,7 @@ static void app_rewriter1_tst() { Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("f1", Nat >> Nat); env->add_var("f2", Nat >> (Nat >> Nat)); env->add_var("f3", Nat >> (Nat >> (Nat >> Nat))); @@ -506,7 +506,7 @@ static void repeat_rewriter1_tst() { Eq(nAdd(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("a", Nat); env->add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z @@ -564,7 +564,7 @@ static void repeat_rewriter2_tst() { Eq(nAdd(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("a", Nat); env->add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z @@ -611,7 +611,7 @@ static void depth_rewriter1_tst() { Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("f1", Nat >> Nat); env->add_var("f2", Nat >> (Nat >> Nat)); env->add_var("f3", Nat >> (Nat >> (Nat >> Nat))); @@ -658,7 +658,7 @@ static void lambda_body_rewriter_tst() { Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); - environment env; init_frontend(env); + environment env; init_full_frontend(env); env->add_var("f1", Nat >> Nat); env->add_var("f2", Nat >> (Nat >> Nat)); env->add_var("f3", Nat >> (Nat >> (Nat >> Nat))); @@ -703,7 +703,7 @@ static void lambda_type_rewriter_tst() { // Result : fun (x : vec(Nat, b + a)), x cout << "=== lambda_type_rewriter_tst() ===" << std::endl; context ctx; - environment env; init_frontend(env); + environment env; init_full_frontend(env); expr a = Const("a"); // a : Nat env->add_var("a", Nat); expr b = Const("b"); // b : Nat diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index 6c02da31b9..80d3e0e43d 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -49,7 +49,7 @@ static void check_failure(tactic t, ro_environment const & env, io_state const & static void tst1() { environment env; io_state io(options(), mk_simple_formatter()); - init_frontend(env); + init_full_frontend(env); env->add_var("p", Bool); env->add_var("q", Bool); expr p = Const("p"); @@ -115,7 +115,7 @@ static void tst1() { static void tst2() { environment env; io_state io(options(), mk_simple_formatter()); - init_frontend(env); + init_full_frontend(env); env->add_var("p", Bool); env->add_var("q", Bool); env->add_var("r", Bool); diff --git a/tests/lean/abst.lean b/tests/lean/abst.lean index 2749544345..1a92e0f93f 100644 --- a/tests/lean/abst.lean +++ b/tests/lean/abst.lean @@ -1,3 +1,4 @@ +Import int. Axiom PlusComm(a b : Int) : a + b == b + a. Variable a : Int. Check (Abst (fun x : Int, (PlusComm a x))). diff --git a/tests/lean/abst.lean.expected.out b/tests/lean/abst.lean.expected.out index e6bf256f72..61cdb63b5b 100644 --- a/tests/lean/abst.lean.expected.out +++ b/tests/lean/abst.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: PlusComm Assumed: a Abst (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a) diff --git a/tests/lean/apply_tac1.lean b/tests/lean/apply_tac1.lean index b1a1c8af5c..60b387cf4c 100644 --- a/tests/lean/apply_tac1.lean +++ b/tests/lean/apply_tac1.lean @@ -1,4 +1,5 @@ -(** import("tactic.lua") **) +Import tactic. +Import int. Variable f : Int -> Int -> Bool Variable P : Int -> Int -> Bool diff --git a/tests/lean/apply_tac1.lean.expected.out b/tests/lean/apply_tac1.lean.expected.out index 0d8b2861be..659d834815 100644 --- a/tests/lean/apply_tac1.lean.expected.out +++ b/tests/lean/apply_tac1.lean.expected.out @@ -1,5 +1,7 @@ Set: pp::colors Set: pp::unicode + Imported 'tactic' + Imported 'int' Assumed: f Assumed: P Assumed: Ax1 diff --git a/tests/lean/arith1.lean b/tests/lean/arith1.lean index 800fd8db45..3c256c8006 100644 --- a/tests/lean/arith1.lean +++ b/tests/lean/arith1.lean @@ -1,3 +1,4 @@ +Import int. Check 10 + 20 Check 10 Check 10 - 20 diff --git a/tests/lean/arith1.lean.expected.out b/tests/lean/arith1.lean.expected.out index 3b75009ca2..59663ed3dd 100644 --- a/tests/lean/arith1.lean.expected.out +++ b/tests/lean/arith1.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' 10 + 20 : ℕ 10 : ℕ 10 - 20 : ℤ diff --git a/tests/lean/arith2.lean b/tests/lean/arith2.lean index 1f38da6113..4fc39b60db 100644 --- a/tests/lean/arith2.lean +++ b/tests/lean/arith2.lean @@ -1,3 +1,5 @@ +Import int. +Import real. Show 1/2 Eval 4/6 Show 3 div 2 diff --git a/tests/lean/arith2.lean.expected.out b/tests/lean/arith2.lean.expected.out index 43be10aad7..c1131b7209 100644 --- a/tests/lean/arith2.lean.expected.out +++ b/tests/lean/arith2.lean.expected.out @@ -1,5 +1,7 @@ Set: pp::colors Set: pp::unicode + Imported 'int' + Imported 'real' 1 / 2 2/3 3 div 2 diff --git a/tests/lean/arith3.lean b/tests/lean/arith3.lean index d805e61abf..e690463c3f 100644 --- a/tests/lean/arith3.lean +++ b/tests/lean/arith3.lean @@ -1,3 +1,4 @@ +Import int. Eval 8 mod 3 Eval 8 div 4 Eval 7 div 3 diff --git a/tests/lean/arith3.lean.expected.out b/tests/lean/arith3.lean.expected.out index 0b8a4b6523..9fe6e20805 100644 --- a/tests/lean/arith3.lean.expected.out +++ b/tests/lean/arith3.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' 2 2 2 diff --git a/tests/lean/arith6.lean b/tests/lean/arith6.lean index 2cb769c014..ed5b8f30a6 100644 --- a/tests/lean/arith6.lean +++ b/tests/lean/arith6.lean @@ -1,3 +1,4 @@ +Import int. SetOption pp::unicode false Show 3 | 6 Eval 3 | 6 diff --git a/tests/lean/arith6.lean.expected.out b/tests/lean/arith6.lean.expected.out index ce817104be..660e52f2b1 100644 --- a/tests/lean/arith6.lean.expected.out +++ b/tests/lean/arith6.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Set: pp::unicode 3 | 6 true diff --git a/tests/lean/arith7.lean b/tests/lean/arith7.lean index b004e422f8..63ab949b52 100644 --- a/tests/lean/arith7.lean +++ b/tests/lean/arith7.lean @@ -1,3 +1,4 @@ +Import int. Eval | -2 | (* Unfortunately, we can't write |-2|, because |- is considered a single token. diff --git a/tests/lean/arith7.lean.expected.out b/tests/lean/arith7.lean.expected.out index deeb4397ca..f79b61be16 100644 --- a/tests/lean/arith7.lean.expected.out +++ b/tests/lean/arith7.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' 2 3 Defined: x diff --git a/tests/lean/arith8.lean b/tests/lean/arith8.lean index 0accbcfe5c..22a5bda5e5 100644 --- a/tests/lean/arith8.lean +++ b/tests/lean/arith8.lean @@ -1,3 +1,4 @@ +Import real. Eval 10.3 Eval 0.3 Eval 0.3 + 0.1 diff --git a/tests/lean/arith8.lean.expected.out b/tests/lean/arith8.lean.expected.out index e69cc588dc..cef4f8920f 100644 --- a/tests/lean/arith8.lean.expected.out +++ b/tests/lean/arith8.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'real' 103/10 3/10 2/5 diff --git a/tests/lean/arrow.lean b/tests/lean/arrow.lean index 07e47330b5..89005dfc6d 100644 --- a/tests/lean/arrow.lean +++ b/tests/lean/arrow.lean @@ -1,3 +1,4 @@ +Import int. Show (Int -> Int) -> Int Show Int -> Int -> Int Show Int -> (Int -> Int) diff --git a/tests/lean/arrow.lean.expected.out b/tests/lean/arrow.lean.expected.out index ceac4337a9..7dfad3a3c0 100644 --- a/tests/lean/arrow.lean.expected.out +++ b/tests/lean/arrow.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' (ℤ → ℤ) → ℤ ℤ → ℤ → ℤ ℤ → ℤ → ℤ diff --git a/tests/lean/bad1.lean b/tests/lean/bad1.lean index fc28eb98ae..4c94b7da97 100644 --- a/tests/lean/bad1.lean +++ b/tests/lean/bad1.lean @@ -1,3 +1,4 @@ +Import int. Variable g : Pi A : Type, A -> A. Variables a b : Int Axiom H1 : g _ a > 0 diff --git a/tests/lean/bad1.lean.expected.out b/tests/lean/bad1.lean.expected.out index 2a7b11980a..25524d2b2a 100644 --- a/tests/lean/bad1.lean.expected.out +++ b/tests/lean/bad1.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: g Assumed: a Assumed: b diff --git a/tests/lean/bad2.lean b/tests/lean/bad2.lean index 9fa112edcf..c523d122fa 100644 --- a/tests/lean/bad2.lean +++ b/tests/lean/bad2.lean @@ -1,3 +1,4 @@ +Import int. Variable list : Type -> Type Variable nil {A : Type} : list A Variable cons {A : Type} (head : A) (tail : list A) : list A diff --git a/tests/lean/bad2.lean.expected.out b/tests/lean/bad2.lean.expected.out index 2432a53a9a..e3a0a357e9 100644 --- a/tests/lean/bad2.lean.expected.out +++ b/tests/lean/bad2.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: list Assumed: nil Assumed: cons diff --git a/tests/lean/bad3.lean b/tests/lean/bad3.lean index 4ed705aa5e..ff25fc2e23 100644 --- a/tests/lean/bad3.lean +++ b/tests/lean/bad3.lean @@ -1,3 +1,4 @@ +Import int. Variable list : Type -> Type Variable nil {A : Type} : list A Variable cons {A : Type} (head : A) (tail : list A) : list A diff --git a/tests/lean/bad3.lean.expected.out b/tests/lean/bad3.lean.expected.out index 9bb3aade89..a38207f3e6 100644 --- a/tests/lean/bad3.lean.expected.out +++ b/tests/lean/bad3.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: list Assumed: nil Assumed: cons diff --git a/tests/lean/bad4.lean b/tests/lean/bad4.lean index de6871cee5..df0c275942 100644 --- a/tests/lean/bad4.lean +++ b/tests/lean/bad4.lean @@ -1,3 +1,4 @@ +Import int. Variable f {A : Type} (a : A) : A Variable a : Int Definition tst : Bool := (fun x, (f x) > 10) a diff --git a/tests/lean/bad4.lean.expected.out b/tests/lean/bad4.lean.expected.out index 30c5d9ddd3..10b4871ef1 100644 --- a/tests/lean/bad4.lean.expected.out +++ b/tests/lean/bad4.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: f Assumed: a Defined: tst diff --git a/tests/lean/bad5.lean b/tests/lean/bad5.lean index f89a711d10..4454260c55 100644 --- a/tests/lean/bad5.lean +++ b/tests/lean/bad5.lean @@ -1,3 +1,4 @@ +Import int. Variable g {A : Type} (a : A) : A Variable a : Int Variable b : Int diff --git a/tests/lean/bad5.lean.expected.out b/tests/lean/bad5.lean.expected.out index b0e7ef6022..916d2534b5 100644 --- a/tests/lean/bad5.lean.expected.out +++ b/tests/lean/bad5.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: g Assumed: a Assumed: b diff --git a/tests/lean/bad6.lean b/tests/lean/bad6.lean index 94fc28ebec..bc5ae55e3d 100644 --- a/tests/lean/bad6.lean +++ b/tests/lean/bad6.lean @@ -1,3 +1,5 @@ +Import int. +Import real. Variable f {A : Type} (a : A) : A Variable a : Int Variable b : Real diff --git a/tests/lean/bad6.lean.expected.out b/tests/lean/bad6.lean.expected.out index f15b3bed76..1bfc1d4c7b 100644 --- a/tests/lean/bad6.lean.expected.out +++ b/tests/lean/bad6.lean.expected.out @@ -1,5 +1,7 @@ Set: pp::colors Set: pp::unicode + Imported 'int' + Imported 'real' Assumed: f Assumed: a Assumed: b diff --git a/tests/lean/bad7.lean b/tests/lean/bad7.lean index 5e6bb51497..d1ce288b44 100644 --- a/tests/lean/bad7.lean +++ b/tests/lean/bad7.lean @@ -1,3 +1,4 @@ +Import real. Variable f {A : Type} (a b : A) : Bool Variable a : Int Variable b : Real diff --git a/tests/lean/bad7.lean.expected.out b/tests/lean/bad7.lean.expected.out index 41c92bb775..51ea1b8ea9 100644 --- a/tests/lean/bad7.lean.expected.out +++ b/tests/lean/bad7.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'real' Assumed: f Assumed: a Assumed: b diff --git a/tests/lean/bad8.lean b/tests/lean/bad8.lean index b0179a29be..dfe4df70a5 100644 --- a/tests/lean/bad8.lean +++ b/tests/lean/bad8.lean @@ -1,3 +1,4 @@ +Import int. Variable list : Type → Type Variable nil {A : Type} : list A Variable cons {A : Type} (head : A) (tail : list A) : list A diff --git a/tests/lean/bad8.lean.expected.out b/tests/lean/bad8.lean.expected.out index ac31c75692..4c9a74bd46 100644 --- a/tests/lean/bad8.lean.expected.out +++ b/tests/lean/bad8.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: list Assumed: nil Assumed: cons diff --git a/tests/lean/cast1.lean b/tests/lean/cast1.lean index 051dd833bd..4cb4027ca5 100644 --- a/tests/lean/cast1.lean +++ b/tests/lean/cast1.lean @@ -1,4 +1,5 @@ -Import cast +Import cast. +Import int. Variable vector : Type -> Nat -> Type Axiom N0 (n : Nat) : n + 0 = n diff --git a/tests/lean/cast1.lean.expected.out b/tests/lean/cast1.lean.expected.out index 1ede023283..946946e7a2 100644 --- a/tests/lean/cast1.lean.expected.out +++ b/tests/lean/cast1.lean.expected.out @@ -1,13 +1,14 @@ Set: pp::colors Set: pp::unicode Imported 'cast' + Imported 'int' Assumed: vector Assumed: N0 Proved: V0 Assumed: f Assumed: m Assumed: v1 -Error (line: 14, pos: 6) type mismatch at application +Error (line: 15, pos: 6) type mismatch at application f m v1 Function type: Π (n : ℕ), vector ℤ n → ℤ diff --git a/tests/lean/conv.lean b/tests/lean/conv.lean index 15f4b22203..fe0397fe63 100644 --- a/tests/lean/conv.lean +++ b/tests/lean/conv.lean @@ -1,3 +1,4 @@ +Import int. Definition id (A : Type) : (Type U) := A. Variable p : (Int -> Int) -> Bool. Check fun (x : id Int), x. diff --git a/tests/lean/conv.lean.expected.out b/tests/lean/conv.lean.expected.out index 3884c52536..15f80493ea 100644 --- a/tests/lean/conv.lean.expected.out +++ b/tests/lean/conv.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Defined: id Assumed: p λ x : id ℤ, x : id ℤ → id ℤ diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index 14238efa62..a4e7d58963 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -2,111 +2,23 @@ Set: pp::unicode Assumed: f Failed to solve - ⊢ (?M::1 ≈ λ x : ℕ, x) ⊕ (?M::1 ≈ nat_to_int) ⊕ (?M::1 ≈ nat_to_real) - (line: 4: pos: 8) Coercion for - 10 - Failed to solve - ⊢ Bool ≺ ℕ - Substitution - ⊢ Bool ≺ ?M::0 - (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of + ⊢ Bool ≺ ℕ + Substitution + ⊢ Bool ≺ ?M::0 + (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of + @f + with arguments: + ?M::0 + 10 + ⊤ + Assignment + ⊢ ℕ ≺ ?M::0 + (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of @f with arguments: ?M::0 - ?M::1 10 + 10 ⊤ - Assignment - ⊢ ℕ ≺ ?M::0 - Substitution - ⊢ ?M::5[inst:0 (10)] ≺ ?M::0 - (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of - @f - with arguments: - ?M::0 - ?M::1 10 - ⊤ - Assignment - x : ℕ ⊢ ℕ ≈ ?M::5 - Destruct/Decompose - ⊢ ℕ → ℕ ≈ Π x : ?M::4, ?M::5 - Substitution - ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 - Function expected at - ?M::1 10 - Assignment - ⊢ ℕ → ℕ ≺ ?M::3 - Propagate type, ?M::1 : ?M::3 - Assignment - ⊢ ?M::1 ≈ λ x : ℕ, x - Assumption 0 - Failed to solve - ⊢ Bool ≺ ℤ - Substitution - ⊢ Bool ≺ ?M::0 - (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of - @f - with arguments: - ?M::0 - ?M::1 10 - ⊤ - Assignment - ⊢ ℤ ≺ ?M::0 - Substitution - ⊢ ?M::5[inst:0 (10)] ≺ ?M::0 - (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of - @f - with arguments: - ?M::0 - ?M::1 10 - ⊤ - Assignment - a : ℕ ⊢ ℤ ≈ ?M::5 - Destruct/Decompose - ⊢ ℕ → ℤ ≈ Π x : ?M::4, ?M::5 - Substitution - ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 - Function expected at - ?M::1 10 - Assignment - ⊢ ℕ → ℤ ≺ ?M::3 - Propagate type, ?M::1 : ?M::3 - Assignment - ⊢ ?M::1 ≈ nat_to_int - Assumption 1 - Failed to solve - ⊢ Bool ≺ ℝ - Substitution - ⊢ Bool ≺ ?M::0 - (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of - @f - with arguments: - ?M::0 - ?M::1 10 - ⊤ - Assignment - ⊢ ℝ ≺ ?M::0 - Substitution - ⊢ ?M::5[inst:0 (10)] ≺ ?M::0 - (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of - @f - with arguments: - ?M::0 - ?M::1 10 - ⊤ - Assignment - a : ℕ ⊢ ℝ ≈ ?M::5 - Destruct/Decompose - ⊢ ℕ → ℝ ≈ Π x : ?M::4, ?M::5 - Substitution - ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 - Function expected at - ?M::1 10 - Assignment - ⊢ ℕ → ℝ ≺ ?M::3 - Propagate type, ?M::1 : ?M::3 - Assignment - ⊢ ?M::1 ≈ nat_to_real - Assumption 2 Assumed: g Error (line: 7, pos: 8) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::1, type: Type diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out index 8cc99545fd..4a5ec12e3d 100644 --- a/tests/lean/elab4.lean.expected.out +++ b/tests/lean/elab4.lean.expected.out @@ -7,8 +7,6 @@ Set: lean::pp::implicit Import "kernel" Import "nat" -Import "int" -Import "real" Variable C {A B : Type} (H : @eq Type A B) (a : A) : B Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) : @eq Type A A' diff --git a/tests/lean/elab5.lean.expected.out b/tests/lean/elab5.lean.expected.out index 8cc99545fd..4a5ec12e3d 100644 --- a/tests/lean/elab5.lean.expected.out +++ b/tests/lean/elab5.lean.expected.out @@ -7,8 +7,6 @@ Set: lean::pp::implicit Import "kernel" Import "nat" -Import "int" -Import "real" Variable C {A B : Type} (H : @eq Type A B) (a : A) : B Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) : @eq Type A A' diff --git a/tests/lean/eq1.lean b/tests/lean/eq1.lean index ef8c66b17c..e5a79ef412 100644 --- a/tests/lean/eq1.lean +++ b/tests/lean/eq1.lean @@ -1,4 +1,4 @@ - +Import int. Variable i : Int Check i = 0 SetOption pp::coercion true diff --git a/tests/lean/eq1.lean.expected.out b/tests/lean/eq1.lean.expected.out index 53482faf20..76bcaf5080 100644 --- a/tests/lean/eq1.lean.expected.out +++ b/tests/lean/eq1.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: i i = 0 : Bool Set: lean::pp::coercion diff --git a/tests/lean/eq2.lean b/tests/lean/eq2.lean index 44f17718d2..76cba5b3a7 100644 --- a/tests/lean/eq2.lean +++ b/tests/lean/eq2.lean @@ -1,3 +1,4 @@ +Import int. Variable List : Type -> Type Variable nil {A : Type} : List A Variable cons {A : Type} (head : A) (tail : List A) : List A diff --git a/tests/lean/eq2.lean.expected.out b/tests/lean/eq2.lean.expected.out index 820bd4a472..8c4122fa14 100644 --- a/tests/lean/eq2.lean.expected.out +++ b/tests/lean/eq2.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: List Assumed: nil Assumed: cons diff --git a/tests/lean/exists1.lean b/tests/lean/exists1.lean index f5b9594dbb..5d58675a3d 100644 --- a/tests/lean/exists1.lean +++ b/tests/lean/exists1.lean @@ -1,3 +1,4 @@ +Import int. Variable a : Int Variable P : Int -> Int -> Bool Axiom H : P a a diff --git a/tests/lean/exists1.lean.expected.out b/tests/lean/exists1.lean.expected.out index 4f1a031ce3..45f9d48977 100644 --- a/tests/lean/exists1.lean.expected.out +++ b/tests/lean/exists1.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: a Assumed: P Assumed: H diff --git a/tests/lean/exists2.lean b/tests/lean/exists2.lean index 69985052b0..993c91f172 100644 --- a/tests/lean/exists2.lean +++ b/tests/lean/exists2.lean @@ -1,3 +1,4 @@ +Import int. Variable a : Int Variable P : Int -> Int -> Bool Variable f : Int -> Int -> Int diff --git a/tests/lean/exists2.lean.expected.out b/tests/lean/exists2.lean.expected.out index 5455cd9691..96903c385d 100644 --- a/tests/lean/exists2.lean.expected.out +++ b/tests/lean/exists2.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: a Assumed: P Assumed: f diff --git a/tests/lean/exists3.lean b/tests/lean/exists3.lean index 8db4891c2a..6c68ab0157 100644 --- a/tests/lean/exists3.lean +++ b/tests/lean/exists3.lean @@ -1,3 +1,4 @@ +Import int. Variable P : Int -> Int -> Bool Theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) := diff --git a/tests/lean/exists3.lean.expected.out b/tests/lean/exists3.lean.expected.out index 85637a8ab5..badf3dbabb 100644 --- a/tests/lean/exists3.lean.expected.out +++ b/tests/lean/exists3.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: P Proved: T1 Assumed: Ax diff --git a/tests/lean/exists6.lean b/tests/lean/exists6.lean index 35fe6579ae..7860365b47 100644 --- a/tests/lean/exists6.lean +++ b/tests/lean/exists6.lean @@ -1,3 +1,4 @@ +Import int. Variable P : Int -> Int -> Int -> Bool Axiom Ax1 : exists x y z, P x y z Axiom Ax2 : forall x y z, not (P x y z) diff --git a/tests/lean/exists6.lean.expected.out b/tests/lean/exists6.lean.expected.out index 6055c3fff6..fa7ca6c6bf 100644 --- a/tests/lean/exists6.lean.expected.out +++ b/tests/lean/exists6.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: P Assumed: Ax1 Assumed: Ax2 diff --git a/tests/lean/explicit.lean b/tests/lean/explicit.lean index 4b7a494d6a..4fabe13289 100644 --- a/tests/lean/explicit.lean +++ b/tests/lean/explicit.lean @@ -1,3 +1,4 @@ +Import int. Variable f {A : Type} : A -> A -> A Variable module::g {A : Type} : A -> A -> A Check @f diff --git a/tests/lean/explicit.lean.expected.out b/tests/lean/explicit.lean.expected.out index ad1470a27d..12e6050f4e 100644 --- a/tests/lean/explicit.lean.expected.out +++ b/tests/lean/explicit.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: f Assumed: module::g @f : Π (A : Type), A → A → A @@ -8,4 +9,4 @@ module::@g : Π (A : Type), A → A → A h::1::explicit : Π (A B : Type), A → B → A Assumed: @h Assumed: h -Error (line: 8, pos: 37) failed to mark implicit arguments for 'h', the frontend already has an object named '@h' +Error (line: 9, pos: 37) failed to mark implicit arguments for 'h', the frontend already has an object named '@h' diff --git a/tests/lean/forall1.lean b/tests/lean/forall1.lean index e398033579..eef7878005 100644 --- a/tests/lean/forall1.lean +++ b/tests/lean/forall1.lean @@ -1,3 +1,4 @@ +Import int. Variable P : Int -> Bool Axiom Ax (x : Int) : P x Check ForallIntro Ax \ No newline at end of file diff --git a/tests/lean/forall1.lean.expected.out b/tests/lean/forall1.lean.expected.out index 4c2b98211f..6253ea01f3 100644 --- a/tests/lean/forall1.lean.expected.out +++ b/tests/lean/forall1.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: P Assumed: Ax ForallIntro Ax : ∀ x : ℤ, P x diff --git a/tests/lean/ho.lean b/tests/lean/ho.lean index b756407ec9..ed254bf31e 100644 --- a/tests/lean/ho.lean +++ b/tests/lean/ho.lean @@ -1,3 +1,4 @@ +Import int. Variable g {A : Type} (a : A) : A Variable a : Int Variable b : Int diff --git a/tests/lean/ho.lean.expected.out b/tests/lean/ho.lean.expected.out index 1c6c2b2aba..995896fd43 100644 --- a/tests/lean/ho.lean.expected.out +++ b/tests/lean/ho.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: g Assumed: a Assumed: b diff --git a/tests/lean/implicit1.lean b/tests/lean/implicit1.lean index 575f9145a8..ac8f2912be 100644 --- a/tests/lean/implicit1.lean +++ b/tests/lean/implicit1.lean @@ -1,3 +1,5 @@ +Import int. +Import real. Variable f : Int -> Int -> Int Show forall a, f a a > 0 Show forall a b, f a b > 0 diff --git a/tests/lean/implicit1.lean.expected.out b/tests/lean/implicit1.lean.expected.out index 116f0f4d64..4a9335d380 100644 --- a/tests/lean/implicit1.lean.expected.out +++ b/tests/lean/implicit1.lean.expected.out @@ -1,5 +1,7 @@ Set: pp::colors Set: pp::unicode + Imported 'int' + Imported 'real' Assumed: f ∀ a : ℤ, f a a > 0 ∀ a b : ℤ, f a b > 0 diff --git a/tests/lean/implicit2.lean b/tests/lean/implicit2.lean index 4b168f6dda..5f1042efaa 100644 --- a/tests/lean/implicit2.lean +++ b/tests/lean/implicit2.lean @@ -1,3 +1,4 @@ +Import real. Variable f {A : Type} (x y : A) : A Check f 10 20 Check f 10 diff --git a/tests/lean/implicit2.lean.expected.out b/tests/lean/implicit2.lean.expected.out index 18d3cc1659..b0b119cc00 100644 --- a/tests/lean/implicit2.lean.expected.out +++ b/tests/lean/implicit2.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'real' Assumed: f f 10 20 : ℕ f 10 : ℕ → ℕ @@ -7,6 +8,6 @@ f 10 : ℕ → ℕ Assumed: g g 10 20 ⊤ : Bool → Bool let r : ℝ → ℝ → ℝ := g 10 20 in r : ℝ → ℝ → ℝ -Error (line: 10, pos: 0) invalid expression, unexpected token +Error (line: 11, pos: 0) invalid expression, unexpected token Set: lean::pp::implicit let r : ℝ → ℝ → ℝ := @g ℕ 10 20 ℝ in r : ℝ → ℝ → ℝ diff --git a/tests/lean/implicit3.lean b/tests/lean/implicit3.lean index a5b6722a5d..93f16d1423 100644 --- a/tests/lean/implicit3.lean +++ b/tests/lean/implicit3.lean @@ -1,3 +1,5 @@ +Import int. + Show 10 = 20 Variable f : Int -> Int -> Int Variable g : Int -> Int -> Int -> Int diff --git a/tests/lean/implicit3.lean.expected.out b/tests/lean/implicit3.lean.expected.out index 0e45087875..9135abfb24 100644 --- a/tests/lean/implicit3.lean.expected.out +++ b/tests/lean/implicit3.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' 10 = 20 Assumed: f Assumed: g diff --git a/tests/lean/implicit4.lean b/tests/lean/implicit4.lean index e30be51951..1a808b6579 100644 --- a/tests/lean/implicit4.lean +++ b/tests/lean/implicit4.lean @@ -1,3 +1,4 @@ +Import int. Variable f {A : Type} (a1 a2 : A) {B : Type} (b1 b2 : B) : A Variable g {A1 A2 : Type} (a1 : A1) (a2 : A2) {B : Type} (b : B) : A1 Variable p (a1 a2 : Int) {B : Type} (b1 b2 b3 : B) : B diff --git a/tests/lean/implicit4.lean.expected.out b/tests/lean/implicit4.lean.expected.out index f02614ad34..7ae1af6986 100644 --- a/tests/lean/implicit4.lean.expected.out +++ b/tests/lean/implicit4.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: f Assumed: g Assumed: p diff --git a/tests/lean/implicit5.lean b/tests/lean/implicit5.lean index 68c61dbc0f..f2d68691f7 100644 --- a/tests/lean/implicit5.lean +++ b/tests/lean/implicit5.lean @@ -1,3 +1,5 @@ +Import int. +Import real. Variable f {A : Type} (a1 a2 : A) : A Variable g : Int -> Int -> Int Variable h : Int -> Int -> Real -> Int diff --git a/tests/lean/implicit5.lean.expected.out b/tests/lean/implicit5.lean.expected.out index e4702275a5..15d3eca259 100644 --- a/tests/lean/implicit5.lean.expected.out +++ b/tests/lean/implicit5.lean.expected.out @@ -1,5 +1,7 @@ Set: pp::colors Set: pp::unicode + Imported 'int' + Imported 'real' Assumed: f Assumed: g Assumed: h diff --git a/tests/lean/implicit6.lean b/tests/lean/implicit6.lean index 683e3c5240..b13cb45267 100644 --- a/tests/lean/implicit6.lean +++ b/tests/lean/implicit6.lean @@ -1,3 +1,4 @@ +Import int. Variable f {A : Type} : A -> A -> A Infixl 65 + : f Show true + false diff --git a/tests/lean/implicit6.lean.expected.out b/tests/lean/implicit6.lean.expected.out index cda47b9b15..99d2d01119 100644 --- a/tests/lean/implicit6.lean.expected.out +++ b/tests/lean/implicit6.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: f ⊤ + ⊥ 10 + 20 diff --git a/tests/lean/interactive/t7.lean b/tests/lean/interactive/t7.lean index 4964d81280..9e7cd6efa6 100644 --- a/tests/lean/interactive/t7.lean +++ b/tests/lean/interactive/t7.lean @@ -1,3 +1,4 @@ +Import int. (** import("tactic.lua") **) Variable q : Int -> Int -> Bool. Variable p : Int -> Bool. diff --git a/tests/lean/interactive/t7.lean.expected.out b/tests/lean/interactive/t7.lean.expected.out index 62463fbd0e..665c6761fe 100644 --- a/tests/lean/interactive/t7.lean.expected.out +++ b/tests/lean/interactive/t7.lean.expected.out @@ -1,6 +1,7 @@ # Set: pp::colors Set: pp::unicode - Assumed: q + Imported 'int' +# Assumed: q # Assumed: p # Assumed: Ax # Assumed: a diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean index fb565b3d55..af210036f1 100644 --- a/tests/lean/let1.lean +++ b/tests/lean/let1.lean @@ -1,3 +1,4 @@ +Import int. Show let a : Nat := 10, b : Nat := 20, c : Nat := 30, d : Nat := 10 in a + b + c + d Show let a : Nat := 1000000000000000000, b : Nat := 20000000000000000000, c : Nat := 3000000000000000000, d : Nat := 4000000000000000000 in a + b + c + d diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out index 42e528381c..cd0099666c 100644 --- a/tests/lean/let1.lean.expected.out +++ b/tests/lean/let1.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' let a : ℕ := 10, b : ℕ := 20, c : ℕ := 30, d : ℕ := 10 in a + b + c + d let a : ℕ := 1000000000000000000, b : ℕ := 20000000000000000000, diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean index fcc1f87713..f9c252a343 100644 --- a/tests/lean/let3.lean +++ b/tests/lean/let3.lean @@ -1,3 +1,4 @@ +Import int. Variable magic : Pi (H : Bool), H diff --git a/tests/lean/let3.lean.expected.out b/tests/lean/let3.lean.expected.out index dfb689ad53..cee1e3d016 100644 --- a/tests/lean/let3.lean.expected.out +++ b/tests/lean/let3.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: magic Set: lean::pp::notation Set: lean::pp::coercion diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean index 68afeb5e30..d1acf53826 100644 --- a/tests/lean/let4.lean +++ b/tests/lean/let4.lean @@ -1,3 +1,4 @@ +Import int. Show let b := true, diff --git a/tests/lean/let4.lean.expected.out b/tests/lean/let4.lean.expected.out index 9233a3cdaa..12cbc7ccb1 100644 --- a/tests/lean/let4.lean.expected.out +++ b/tests/lean/let4.lean.expected.out @@ -1,23 +1,24 @@ Set: pp::colors Set: pp::unicode + Imported 'int' let b := ⊤, a : ℤ := b in a Assumed: vector Assumed: const let a := 10, v1 := const a ⊤, v2 := v1 in v2 : vector Bool 10 let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 : vector Bool 10 -Error (line: 31, pos: 26) type mismatch at definition 'v2', expected type +Error (line: 32, pos: 26) type mismatch at definition 'v2', expected type vector ℤ a Given type: vector Bool a Assumed: foo Coercion foo -Error (line: 40, pos: 26) type mismatch at definition 'v2', expected type +Error (line: 41, pos: 26) type mismatch at definition 'v2', expected type vector ℤ a Given type: vector Bool a Set: lean::pp::coercion -Error (line: 48, pos: 26) type mismatch at definition 'v2', expected type +Error (line: 49, pos: 26) type mismatch at definition 'v2', expected type vector ℤ a Given type: vector Bool a diff --git a/tests/lean/loop2.lean b/tests/lean/loop2.lean index ab763a1201..9761f15df9 100644 --- a/tests/lean/loop2.lean +++ b/tests/lean/loop2.lean @@ -1,3 +1,5 @@ +Import int. + (** function add_paren(code) return "(" .. "** " .. code .. " **" .. ")" diff --git a/tests/lean/loop2.lean.expected.out b/tests/lean/loop2.lean.expected.out index 2332420b1e..5838e6e297 100644 --- a/tests/lean/loop2.lean.expected.out +++ b/tests/lean/loop2.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Variable x : ℤ done diff --git a/tests/lean/lua1.lean b/tests/lean/lua1.lean index 6dbac0ce6d..980f774ca0 100644 --- a/tests/lean/lua1.lean +++ b/tests/lean/lua1.lean @@ -1,3 +1,4 @@ +Import int. Variable x : Int (** diff --git a/tests/lean/lua1.lean.expected.out b/tests/lean/lua1.lean.expected.out index c726c6226c..fa24a8e954 100644 --- a/tests/lean/lua1.lean.expected.out +++ b/tests/lean/lua1.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: x hello world from Lua Assumed: y diff --git a/tests/lean/lua11.lean b/tests/lean/lua11.lean index 2cf1f4ae52..347dd1a045 100644 --- a/tests/lean/lua11.lean +++ b/tests/lean/lua11.lean @@ -1,3 +1,4 @@ +Import int. (** local env = get_environment() diff --git a/tests/lean/lua11.lean.expected.out b/tests/lean/lua11.lean.expected.out index 8252f0cecc..75c4267295 100644 --- a/tests/lean/lua11.lean.expected.out +++ b/tests/lean/lua11.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Int::add BuiltinSet Nat::numeral 512 diff --git a/tests/lean/lua12.lean b/tests/lean/lua12.lean index f9a182c35a..680e38c7bd 100644 --- a/tests/lean/lua12.lean +++ b/tests/lean/lua12.lean @@ -1,3 +1,4 @@ +Import int. Variables x y z : Int (** diff --git a/tests/lean/lua12.lean.expected.out b/tests/lean/lua12.lean.expected.out index 34010c9358..a0f1cac6ba 100644 --- a/tests/lean/lua12.lean.expected.out +++ b/tests/lean/lua12.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: x Assumed: y Assumed: z diff --git a/tests/lean/lua13.lean b/tests/lean/lua13.lean index a5a89fdaf4..95405b15f4 100644 --- a/tests/lean/lua13.lean +++ b/tests/lean/lua13.lean @@ -1,3 +1,4 @@ +Import int. Variables x y z : Int Variable f : Int -> Int -> Int diff --git a/tests/lean/lua13.lean.expected.out b/tests/lean/lua13.lean.expected.out index 4c0ba3e269..d22371e910 100644 --- a/tests/lean/lua13.lean.expected.out +++ b/tests/lean/lua13.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: x Assumed: y Assumed: z diff --git a/tests/lean/lua14.lean b/tests/lean/lua14.lean index 2c172bc783..ddfd94ce7b 100644 --- a/tests/lean/lua14.lean +++ b/tests/lean/lua14.lean @@ -1,3 +1,4 @@ +Import int. Variables x y z : Int Variable f : Int -> Int -> Int diff --git a/tests/lean/lua14.lean.expected.out b/tests/lean/lua14.lean.expected.out index b490829b0e..9e86d93436 100644 --- a/tests/lean/lua14.lean.expected.out +++ b/tests/lean/lua14.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: x Assumed: y Assumed: z diff --git a/tests/lean/lua15.lean b/tests/lean/lua15.lean index 528e57ac36..b9be6a737e 100644 --- a/tests/lean/lua15.lean +++ b/tests/lean/lua15.lean @@ -1,3 +1,4 @@ +Import int. Variables i j : Int Variable p : Bool diff --git a/tests/lean/lua15.lean.expected.out b/tests/lean/lua15.lean.expected.out index ea0e434145..5864193f6a 100644 --- a/tests/lean/lua15.lean.expected.out +++ b/tests/lean/lua15.lean.expected.out @@ -1,154 +1,65 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: i Assumed: j Assumed: p elaborator exception Failed to solve - ⊢ (?M::0 ≈ Nat::add) ⊕ (?M::0 ≈ Int::add) ⊕ (?M::0 ≈ Real::add) + ⊢ (?M::0 ≈ Nat::add) ⊕ (?M::0 ≈ Int::add) Overloading at - (Real::add | Int::add | Nat::add) i p + (Int::add | Nat::add) i p Failed to solve - ⊢ (?M::1 ≈ λ x : ℤ, x) ⊕ (?M::1 ≈ int_to_real) - Coercion for - i - Failed to solve - ⊢ ℤ ≺ ℕ - Substitution - ⊢ ℤ ≺ ?M::6 - Substitution - ⊢ ?M::5[inst:0 i] ≺ ?M::6 - Type of argument 1 must be convertible to the expected type in the application of - ?M::0 - with arguments: - ?M::1 i - p - Assignment - x : ℤ ⊢ ℤ ≈ ?M::5 - Destruct/Decompose - ⊢ ℤ → ℤ ≈ Π x : ?M::4, ?M::5 - Substitution - ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 - Function expected at - ?M::1 i + ⊢ ℤ ≺ ℕ + Substitution + ⊢ ℤ ≺ ?M::2 + Type of argument 1 must be convertible to the expected type in the application of + ?M::0 + with arguments: + i + p + Assignment + ⊢ ℕ ≈ ?M::2 + Destruct/Decompose + ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::2, ?M::3 + Substitution + ⊢ ?M::1 ≈ Π x : ?M::2, ?M::3 + Function expected at + ?M::0 i p + Assignment + ⊢ ℕ → ℕ → ℕ ≺ ?M::1 + Propagate type, ?M::0 : ?M::1 Assignment - ⊢ ℤ → ℤ ≺ ?M::3 - Propagate type, ?M::1 : ?M::3 - Assignment - ⊢ ?M::1 ≈ λ x : ℤ, x - Assumption 1 - Assignment - ⊢ ℕ ≈ ?M::6 - Destruct/Decompose - ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 - Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 - Function expected at - ?M::0 (?M::1 i) p - Assignment - ⊢ ℕ → ℕ → ℕ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 - Assignment - ⊢ ?M::0 ≈ Nat::add - Assumption 0 - Failed to solve - ⊢ ℝ ≺ ℕ - Substitution - ⊢ ℝ ≺ ?M::6 - Substitution - ⊢ ?M::5[inst:0 i] ≺ ?M::6 - Type of argument 1 must be convertible to the expected type in the application of - ?M::0 - with arguments: - ?M::1 i - p - Assignment - a : ℤ ⊢ ℝ ≈ ?M::5 - Destruct/Decompose - ⊢ ℤ → ℝ ≈ Π x : ?M::4, ?M::5 - Substitution - ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 - Function expected at - ?M::1 i - Assignment - ⊢ ℤ → ℝ ≺ ?M::3 - Propagate type, ?M::1 : ?M::3 - Assignment - ⊢ ?M::1 ≈ int_to_real - Assumption 2 - Assignment - ⊢ ℕ ≈ ?M::6 - Destruct/Decompose - ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 - Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 - Function expected at - ?M::0 (?M::1 i) p - Assignment - ⊢ ℕ → ℕ → ℕ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 - Assignment - ⊢ ?M::0 ≈ Nat::add - Assumption 0 + ⊢ ?M::0 ≈ Nat::add + Assumption 0 Failed to solve ⊢ Bool ≺ ℤ Substitution - ⊢ Bool ≺ ?M::8 + ⊢ Bool ≺ ?M::4 Type of argument 2 must be convertible to the expected type in the application of ?M::0 with arguments: - ?M::1 i + i p Assignment - ⊢ ℤ ≈ ?M::8 + ⊢ ℤ ≈ ?M::4 Destruct/Decompose - ⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 + ⊢ ℤ → ℤ ≈ Π x : ?M::4, ?M::5 Substitution - ⊢ ?M::7[inst:0 (?M::1 i)] ≈ Π x : ?M::8, ?M::9 + ⊢ ?M::3[inst:0 i] ≈ Π x : ?M::4, ?M::5 Function expected at - ?M::0 (?M::1 i) p + ?M::0 i p Assignment - a : ℤ ⊢ ℤ → ℤ ≈ ?M::7 + a : ℤ ⊢ ℤ → ℤ ≈ ?M::3 Destruct/Decompose - ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 + ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::2, ?M::3 Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 + ⊢ ?M::1 ≈ Π x : ?M::2, ?M::3 Function expected at - ?M::0 (?M::1 i) p + ?M::0 i p Assignment - ⊢ ℤ → ℤ → ℤ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 + ⊢ ℤ → ℤ → ℤ ≺ ?M::1 + Propagate type, ?M::0 : ?M::1 Assignment ⊢ ?M::0 ≈ Int::add - Assumption 3 - Failed to solve - ⊢ Bool ≺ ℝ - Substitution - ⊢ Bool ≺ ?M::8 - Type of argument 2 must be convertible to the expected type in the application of - ?M::0 - with arguments: - ?M::1 i - p - Assignment - ⊢ ℝ ≈ ?M::8 - Destruct/Decompose - ⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 - Substitution - ⊢ ?M::7[inst:0 (?M::1 i)] ≈ Π x : ?M::8, ?M::9 - Function expected at - ?M::0 (?M::1 i) p - Assignment - a : ℝ ⊢ ℝ → ℝ ≈ ?M::7 - Destruct/Decompose - ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 - Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 - Function expected at - ?M::0 (?M::1 i) p - Assignment - ⊢ ℝ → ℝ → ℝ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 - Assignment - ⊢ ?M::0 ≈ Real::add - Assumption 5 + Assumption 1 diff --git a/tests/lean/lua16.lean b/tests/lean/lua16.lean index 1fddfc4876..924eae90fd 100644 --- a/tests/lean/lua16.lean +++ b/tests/lean/lua16.lean @@ -1,4 +1,4 @@ - +Import int. Variables a b : Int (** diff --git a/tests/lean/lua16.lean.expected.out b/tests/lean/lua16.lean.expected.out index 349b4275c7..ab6938574e 100644 --- a/tests/lean/lua16.lean.expected.out +++ b/tests/lean/lua16.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: a Assumed: b Int::add a b diff --git a/tests/lean/lua17.lean b/tests/lean/lua17.lean index d0c9c61d06..98775d91e9 100644 --- a/tests/lean/lua17.lean +++ b/tests/lean/lua17.lean @@ -1,4 +1,4 @@ - +Import int. Variables a b : Int Show Options (** diff --git a/tests/lean/lua17.lean.expected.out b/tests/lean/lua17.lean.expected.out index 10c8b08d4e..986562a0d8 100644 --- a/tests/lean/lua17.lean.expected.out +++ b/tests/lean/lua17.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: a Assumed: b ⟨pp::unicode ↦ true, pp::colors ↦ false⟩ diff --git a/tests/lean/lua18.lean b/tests/lean/lua18.lean index caf86afec7..a14f54c333 100644 --- a/tests/lean/lua18.lean +++ b/tests/lean/lua18.lean @@ -1,3 +1,4 @@ +Import int. (** macro("MyMacro", { macro_arg.Expr, macro_arg.Comma, macro_arg.Expr }, function (env, e1, e2) diff --git a/tests/lean/lua18.lean.expected.out b/tests/lean/lua18.lean.expected.out index 5c9da949e7..01b99113dd 100644 --- a/tests/lean/lua18.lean.expected.out +++ b/tests/lean/lua18.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' 10 + 20 + 20 0 10 + 20 + 30 + 40 diff --git a/tests/lean/lua3.lean b/tests/lean/lua3.lean index 2811ab391b..29a825fe36 100644 --- a/tests/lean/lua3.lean +++ b/tests/lean/lua3.lean @@ -1,4 +1,4 @@ - +Import int. Variable x : Int (** diff --git a/tests/lean/lua3.lean.expected.out b/tests/lean/lua3.lean.expected.out index c81c26f333..a5df5f33bc 100644 --- a/tests/lean/lua3.lean.expected.out +++ b/tests/lean/lua3.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: x hello Error (line: 4, pos: 0) executing external script (script.lua:4), attempt to call global 'prn' (a nil value) diff --git a/tests/lean/lua4.lean b/tests/lean/lua4.lean index 29d7fd6a6f..75709a36ed 100644 --- a/tests/lean/lua4.lean +++ b/tests/lean/lua4.lean @@ -1,3 +1,4 @@ +Import int. Variable x : Int (** diff --git a/tests/lean/lua4.lean.expected.out b/tests/lean/lua4.lean.expected.out index d0c5eef8c6..c13529d25e 100644 --- a/tests/lean/lua4.lean.expected.out +++ b/tests/lean/lua4.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: x type of x is ℤ x + y : ℤ diff --git a/tests/lean/lua5.lean b/tests/lean/lua5.lean index 7f5e209f5d..bc62483a1b 100644 --- a/tests/lean/lua5.lean +++ b/tests/lean/lua5.lean @@ -1,3 +1,4 @@ +Import int. Variable x : Int (** diff --git a/tests/lean/lua5.lean.expected.out b/tests/lean/lua5.lean.expected.out index 1276a3fece..899932d639 100644 --- a/tests/lean/lua5.lean.expected.out +++ b/tests/lean/lua5.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: x Variable x : ℤ Variable y_1 : ℤ diff --git a/tests/lean/lua6.lean b/tests/lean/lua6.lean index 7002dd78cb..cf814ab0f2 100644 --- a/tests/lean/lua6.lean +++ b/tests/lean/lua6.lean @@ -1,3 +1,4 @@ +Import int. Variable x : Int SetOption pp::notation false (** diff --git a/tests/lean/lua6.lean.expected.out b/tests/lean/lua6.lean.expected.out index eb0c7486b1..335fc205e3 100644 --- a/tests/lean/lua6.lean.expected.out +++ b/tests/lean/lua6.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: x Set: lean::pp::notation ⟨lean::pp::notation ↦ false, pp::unicode ↦ true, pp::colors ↦ false⟩ diff --git a/tests/lean/lua8.lean b/tests/lean/lua8.lean index b8344c7a7d..05cc45fa14 100644 --- a/tests/lean/lua8.lean +++ b/tests/lean/lua8.lean @@ -1,3 +1,4 @@ +Import int. Variable x : Int (** diff --git a/tests/lean/lua8.lean.expected.out b/tests/lean/lua8.lean.expected.out index 60b8c30f50..02abc2293d 100644 --- a/tests/lean/lua8.lean.expected.out +++ b/tests/lean/lua8.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: x x : ℤ, y : ℤ Variable x : ℤ diff --git a/tests/lean/lua9.lean b/tests/lean/lua9.lean index 5db4405649..cf7fcf8e57 100644 --- a/tests/lean/lua9.lean +++ b/tests/lean/lua9.lean @@ -1,3 +1,4 @@ +Import int. Variable x : Bool (** diff --git a/tests/lean/lua9.lean.expected.out b/tests/lean/lua9.lean.expected.out index 4a3f84000b..17c31876b5 100644 --- a/tests/lean/lua9.lean.expected.out +++ b/tests/lean/lua9.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: x Type ℤ → ℤ → ℤ diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean index c29d7e3926..cd822be8b1 100644 --- a/tests/lean/norm_tac.lean +++ b/tests/lean/norm_tac.lean @@ -1,3 +1,4 @@ +Import int Import tactic SetOption pp::implicit true SetOption pp::coercion true diff --git a/tests/lean/norm_tac.lean.expected.out b/tests/lean/norm_tac.lean.expected.out index bf964344d7..cf126996de 100644 --- a/tests/lean/norm_tac.lean.expected.out +++ b/tests/lean/norm_tac.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Imported 'tactic' Set: lean::pp::implicit Set: lean::pp::coercion diff --git a/tests/lean/overload2.lean b/tests/lean/overload2.lean index 2798b09906..968f9464aa 100644 --- a/tests/lean/overload2.lean +++ b/tests/lean/overload2.lean @@ -1,3 +1,5 @@ +Import int +Import real Show 1 + true Variable R : Type Variable T : Type diff --git a/tests/lean/overload2.lean.expected.out b/tests/lean/overload2.lean.expected.out index a771cf2b24..6913b85e53 100644 --- a/tests/lean/overload2.lean.expected.out +++ b/tests/lean/overload2.lean.expected.out @@ -1,14 +1,16 @@ Set: pp::colors Set: pp::unicode + Imported 'int' + Imported 'real' Failed to solve ⊢ (?M::0 ≈ Nat::add) ⊕ (?M::0 ≈ Int::add) ⊕ (?M::0 ≈ Real::add) - (line: 1: pos: 10) Overloading at + (line: 3: pos: 9) Overloading at (Real::add | Int::add | Nat::add) 1 ⊤ Failed to solve ⊢ Bool ≺ ℕ Substitution ⊢ Bool ≺ ?M::8 - (line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of + (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of ?M::0 with arguments: ?M::1 1 @@ -19,7 +21,7 @@ Failed to solve ⊢ ℕ → ℕ ≈ Π x : ?M::8, ?M::9 Substitution ⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9 - (line: 1: pos: 10) Function expected at + (line: 3: pos: 9) Function expected at ?M::0 (?M::1 1) ⊤ Assignment a : ℕ ⊢ ℕ → ℕ ≈ ?M::7 @@ -27,7 +29,7 @@ Failed to solve ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 Substitution ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 - (line: 1: pos: 10) Function expected at + (line: 3: pos: 9) Function expected at ?M::0 (?M::1 1) ⊤ Assignment ⊢ ℕ → ℕ → ℕ ≺ ?M::2 @@ -39,7 +41,7 @@ Failed to solve ⊢ Bool ≺ ℤ Substitution ⊢ Bool ≺ ?M::8 - (line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of + (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of ?M::0 with arguments: ?M::1 1 @@ -50,7 +52,7 @@ Failed to solve ⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 Substitution ⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9 - (line: 1: pos: 10) Function expected at + (line: 3: pos: 9) Function expected at ?M::0 (?M::1 1) ⊤ Assignment a : ℤ ⊢ ℤ → ℤ ≈ ?M::7 @@ -58,7 +60,7 @@ Failed to solve ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 Substitution ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 - (line: 1: pos: 10) Function expected at + (line: 3: pos: 9) Function expected at ?M::0 (?M::1 1) ⊤ Assignment ⊢ ℤ → ℤ → ℤ ≺ ?M::2 @@ -70,7 +72,7 @@ Failed to solve ⊢ Bool ≺ ℝ Substitution ⊢ Bool ≺ ?M::8 - (line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of + (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of ?M::0 with arguments: ?M::1 1 @@ -81,7 +83,7 @@ Failed to solve ⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 Substitution ⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9 - (line: 1: pos: 10) Function expected at + (line: 3: pos: 9) Function expected at ?M::0 (?M::1 1) ⊤ Assignment a : ℝ ⊢ ℝ → ℝ ≈ ?M::7 @@ -89,7 +91,7 @@ Failed to solve ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 Substitution ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 - (line: 1: pos: 10) Function expected at + (line: 3: pos: 9) Function expected at ?M::0 (?M::1 1) ⊤ Assignment ⊢ ℝ → ℝ → ℝ ≺ ?M::2 diff --git a/tests/lean/push.lean b/tests/lean/push.lean index 26280813f9..a01cf0879a 100644 --- a/tests/lean/push.lean +++ b/tests/lean/push.lean @@ -1,3 +1,4 @@ +Import int. Variable first : Bool diff --git a/tests/lean/push.lean.expected.out b/tests/lean/push.lean.expected.out index cabd0ba7d4..7042fefd6a 100644 --- a/tests/lean/push.lean.expected.out +++ b/tests/lean/push.lean.expected.out @@ -1,13 +1,14 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: first Assumed: a Assumed: b Assumed: c Assumed: f f a -Error (line: 10, pos: 5) unknown identifier 'f' +Error (line: 11, pos: 5) unknown identifier 'f' Variable first : Bool 10 ++ 20 : ℤ -Error (line: 19, pos: 9) unknown identifier '++' -Error (line: 21, pos: 0) main scope cannot be removed +Error (line: 20, pos: 9) unknown identifier '++' +Error (line: 22, pos: 0) main scope cannot be removed diff --git a/tests/lean/revapp.lean b/tests/lean/revapp.lean index 805736798b..e59a8d1ef5 100644 --- a/tests/lean/revapp.lean +++ b/tests/lean/revapp.lean @@ -1,3 +1,4 @@ +Import int. Definition revapp {A : (Type U)} {B : A -> (Type U)} (a : A) (f : Pi (x : A), B x) : (B a) := f a. Infixl 100 |> : revapp diff --git a/tests/lean/revapp.lean.expected.out b/tests/lean/revapp.lean.expected.out index ea0f1fe480..637b7cebf6 100644 --- a/tests/lean/revapp.lean.expected.out +++ b/tests/lean/revapp.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Defined: revapp -21 Defined: revcomp diff --git a/tests/lean/scope.lean b/tests/lean/scope.lean index 73d1887f35..8c33d5e732 100644 --- a/tests/lean/scope.lean +++ b/tests/lean/scope.lean @@ -1,3 +1,4 @@ +Import int. Scope Variable A : Type diff --git a/tests/lean/scope.lean.expected.out b/tests/lean/scope.lean.expected.out index bff042f3f4..743dda21e2 100644 --- a/tests/lean/scope.lean.expected.out +++ b/tests/lean/scope.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: A Assumed: B Assumed: f diff --git a/tests/lean/simple.lean b/tests/lean/simple.lean index 9238291bc8..d5e2bc4f45 100644 --- a/tests/lean/simple.lean +++ b/tests/lean/simple.lean @@ -1,2 +1,3 @@ +Import int. Variable x : Int Variable y : Int \ No newline at end of file diff --git a/tests/lean/simple.lean.expected.out b/tests/lean/simple.lean.expected.out index de83b08546..978f691205 100644 --- a/tests/lean/simple.lean.expected.out +++ b/tests/lean/simple.lean.expected.out @@ -1,4 +1,5 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: x Assumed: y diff --git a/tests/lean/single.lean b/tests/lean/single.lean index 99b96f4802..d56d466032 100644 --- a/tests/lean/single.lean +++ b/tests/lean/single.lean @@ -1,3 +1,4 @@ +Import int. Variables a b c : Int. Show a + b + c. Check a + b. diff --git a/tests/lean/single.lean.expected.out b/tests/lean/single.lean.expected.out index 4839be9f7b..2ba1a3926a 100644 --- a/tests/lean/single.lean.expected.out +++ b/tests/lean/single.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: a Assumed: b Assumed: c diff --git a/tests/lean/slow/deep.lean b/tests/lean/slow/deep.lean index 7a43d2f691..b5df706c42 100644 --- a/tests/lean/slow/deep.lean +++ b/tests/lean/slow/deep.lean @@ -1,3 +1,4 @@ +Import int. Definition f1 (f : Int -> Int) (x : Int) : Int := f (f (f (f x))) Definition f2 (f : Int -> Int) (x : Int) : Int := f1 (f1 (f1 (f1 f))) x Definition f3 (f : Int -> Int) (x : Int) : Int := f1 (f2 (f2 f)) x diff --git a/tests/lean/slow/deep.lean.expected.out b/tests/lean/slow/deep.lean.expected.out index f9b6810970..d291b19b9d 100644 --- a/tests/lean/slow/deep.lean.expected.out +++ b/tests/lean/slow/deep.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Defined: f1 Defined: f2 Defined: f3 diff --git a/tests/lean/slow/tactic1.lean b/tests/lean/slow/tactic1.lean index 8c1a4a45a7..1116ece284 100644 --- a/tests/lean/slow/tactic1.lean +++ b/tests/lean/slow/tactic1.lean @@ -1,3 +1,4 @@ +Import int. Definition double {A : Type} (f : A -> A) : A -> A := fun x, f (f x). Definition big {A : Type} (f : A -> A) : A -> A := (double (double (double (double (double (double (double f))))))). diff --git a/tests/lean/slow/tactic1.lean.expected.out b/tests/lean/slow/tactic1.lean.expected.out index f0583d578d..1bad314f40 100644 --- a/tests/lean/slow/tactic1.lean.expected.out +++ b/tests/lean/slow/tactic1.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Defined: double Defined: big Proved: T1 diff --git a/tests/lean/subst.lean b/tests/lean/subst.lean index dc7fa1e243..44a78ac957 100644 --- a/tests/lean/subst.lean +++ b/tests/lean/subst.lean @@ -1,3 +1,4 @@ +Import int. Variable a : Int Variable n : Nat Axiom H1 : a + a + a = 10 diff --git a/tests/lean/subst.lean.expected.out b/tests/lean/subst.lean.expected.out index 102ef03f7a..173671a2c6 100644 --- a/tests/lean/subst.lean.expected.out +++ b/tests/lean/subst.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: a Assumed: n Assumed: H1 diff --git a/tests/lean/tactic13.lean b/tests/lean/tactic13.lean index 19383f5dfb..9f8a7d03ac 100644 --- a/tests/lean/tactic13.lean +++ b/tests/lean/tactic13.lean @@ -1,3 +1,4 @@ +Import int. (** import("tactic.lua") **) Variable f : Int -> Int -> Int diff --git a/tests/lean/tactic13.lean.expected.out b/tests/lean/tactic13.lean.expected.out index 8d42b18eb1..1cc3c6b619 100644 --- a/tests/lean/tactic13.lean.expected.out +++ b/tests/lean/tactic13.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: f Proved: T1 Proved: T2 diff --git a/tests/lean/tactic14.lean b/tests/lean/tactic14.lean index 93a91da076..bcbd04a192 100644 --- a/tests/lean/tactic14.lean +++ b/tests/lean/tactic14.lean @@ -1,3 +1,4 @@ +Import int. (** -- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions diff --git a/tests/lean/tactic14.lean.expected.out b/tests/lean/tactic14.lean.expected.out index a87cba3f62..1bb79c3851 100644 --- a/tests/lean/tactic14.lean.expected.out +++ b/tests/lean/tactic14.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Proved: T1 Theorem T1 (a b : ℤ) (f : ℤ → ℤ) (assumption : a = b) : f (f a) = f (f b) := Congr (Refl f) (Congr (Refl f) assumption) diff --git a/tests/lean/tst14.lean b/tests/lean/tst14.lean index bc5ab03e28..8485eff915 100644 --- a/tests/lean/tst14.lean +++ b/tests/lean/tst14.lean @@ -1,3 +1,4 @@ +Import int. Show Int -> Int -> Int Variable f : Int -> Int -> Int Eval f 0 diff --git a/tests/lean/tst14.lean.expected.out b/tests/lean/tst14.lean.expected.out index 9e06456e90..8968f3ce0a 100644 --- a/tests/lean/tst14.lean.expected.out +++ b/tests/lean/tst14.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' ℤ → ℤ → ℤ Assumed: f f 0 diff --git a/tests/lean/tst8.lean b/tests/lean/tst8.lean index 7c1baff1ee..9d50db40cc 100644 --- a/tests/lean/tst8.lean +++ b/tests/lean/tst8.lean @@ -1,3 +1,4 @@ +Import int Check fun (A : Type) (a : A), let b := a in b diff --git a/tests/lean/tst8.lean.expected.out b/tests/lean/tst8.lean.expected.out index ef1e42c5db..b8d638fc75 100644 --- a/tests/lean/tst8.lean.expected.out +++ b/tests/lean/tst8.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'int' λ (A : Type) (a : A), let b := a in b : Π (A : Type), A → A Assumed: g Defined: f diff --git a/tests/lean/ty1.lean b/tests/lean/ty1.lean index c4c2907175..a23d17cd39 100644 --- a/tests/lean/ty1.lean +++ b/tests/lean/ty1.lean @@ -1,3 +1,4 @@ +Import int. Variable i : Int. Check fun x, x + i Check fun x, x + 1 diff --git a/tests/lean/ty1.lean.expected.out b/tests/lean/ty1.lean.expected.out index 41f10b63dc..8edec4fdf8 100644 --- a/tests/lean/ty1.lean.expected.out +++ b/tests/lean/ty1.lean.expected.out @@ -1,9 +1,10 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: i λ x : ℤ, x + i : ℤ → ℤ λ x : ℕ, x + 1 : ℕ → ℕ -Error (line: 4, pos: 10) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::0, type: +Error (line: 5, pos: 10) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::0, type: (Type U) λ x y : ℤ, y + i + 1 + x : ℤ → ℤ → ℤ (λ x : ℤ, x) i : ℤ diff --git a/tests/lean/vars1.lean b/tests/lean/vars1.lean index 09f2b75b9b..a6cd08a1a0 100644 --- a/tests/lean/vars1.lean +++ b/tests/lean/vars1.lean @@ -1,3 +1,4 @@ +Import int. Variables a b c : Int Variables d b e : Int Variables d e f : Int diff --git a/tests/lean/vars1.lean.expected.out b/tests/lean/vars1.lean.expected.out index 34ee1bb749..e7f68535e3 100644 --- a/tests/lean/vars1.lean.expected.out +++ b/tests/lean/vars1.lean.expected.out @@ -1,9 +1,10 @@ Set: pp::colors Set: pp::unicode + Imported 'int' Assumed: a Assumed: b Assumed: c -Error (line: 2, pos: 0) invalid object declaration, environment already has an object named 'b' +Error (line: 3, pos: 0) invalid object declaration, environment already has an object named 'b' Assumed: d Assumed: e Assumed: f diff --git a/tests/lua/coercion_bug1.lua b/tests/lua/coercion_bug1.lua index 2d37ce2c1f..99f003cd03 100644 --- a/tests/lua/coercion_bug1.lua +++ b/tests/lua/coercion_bug1.lua @@ -1,5 +1,5 @@ local env = environment() - +env:import("int") parse_lean_cmds([[ Variable f : Int -> Int -> Int Notation 20 _ +++ _ : f diff --git a/tests/lua/env4.lua b/tests/lua/env4.lua index 6d9122efe9..780eb26cb1 100644 --- a/tests/lua/env4.lua +++ b/tests/lua/env4.lua @@ -1,5 +1,6 @@ assert(not pcall(function() get_environment() end)) local env = environment() +env:import("int") env:add_uvar("Z", level(level("M"), 1)) assert(env:is_ge(level("Z"), level("M"))) local child = env:mk_child() diff --git a/tests/lua/front.lua b/tests/lua/front.lua index 7fe1ddcfbd..68d83f6e8a 100644 --- a/tests/lua/front.lua +++ b/tests/lua/front.lua @@ -1,5 +1,6 @@ import("util.lua") local env = environment() +env:import("int") print(get_options()) parse_lean_cmds([[ Variable f : Int -> Int -> Int @@ -21,6 +22,7 @@ parse_lean_cmds([[ ]], env) local env2 = environment() +env2:import("int") parse_lean_cmds([[ Variable f : Int -> Int -> Int Variables a b : Int diff --git a/tests/lua/hidden1.lua b/tests/lua/hidden1.lua index 4222bac495..d2a1e80073 100644 --- a/tests/lua/hidden1.lua +++ b/tests/lua/hidden1.lua @@ -1,4 +1,5 @@ local env = environment() +env:import("int") assert(env:is_opaque("and")) assert(env:is_opaque("or")) assert(env:is_opaque({"Int", "lt"})) diff --git a/tests/lua/single.lua b/tests/lua/single.lua index 7f687f55dd..eda80d268c 100644 --- a/tests/lua/single.lua +++ b/tests/lua/single.lua @@ -1,4 +1,5 @@ print("hello world") local env = environment() +env:import("int") parse_lean_cmds([[ Variables a b : Int ]], env) print(parse_lean([[a + b + 10]], env)) diff --git a/tests/lua/template1.lua b/tests/lua/template1.lua index 1b4312b493..510bbc097f 100644 --- a/tests/lua/template1.lua +++ b/tests/lua/template1.lua @@ -1,6 +1,7 @@ import("util.lua") import("template.lua") local env = environment() +env:import("int") parse_lean_cmds([[ Variables a b c : Int Variables f : Int -> Int