From aee1c6d3f38edb83a6af8146d3cf16cfc9e349b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 28 Dec 2013 17:31:35 -0800 Subject: [PATCH] feat(kernel): export/import (.olean) binary files Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 2 + src/frontends/lean/frontend.cpp | 28 +-- src/frontends/lean/frontend.h | 6 - src/frontends/lean/notation.cpp | 190 +++++++-------- src/frontends/lean/parser.cpp | 33 ++- src/frontends/lean/pp.cpp | 33 ++- src/frontends/lean/pp.h | 2 + src/kernel/builtin.cpp | 136 +++++------ src/kernel/environment.cpp | 119 +++++++++- src/kernel/environment.h | 19 +- src/kernel/kernel_exception.h | 2 +- src/kernel/object.cpp | 3 +- src/kernel/object.h | 4 + src/library/arith/int.cpp | 52 ++-- src/library/arith/nat.cpp | 30 +-- src/library/arith/real.cpp | 56 +++-- src/library/arith/special_fn.cpp | 48 ++-- src/library/basic_thms.cpp | 396 ++++++++++++++++--------------- src/shell/CMakeLists.txt | 2 - src/shell/lean.cpp | 34 ++- src/util/lean_path.cpp | 8 +- src/util/lean_path.h | 3 + src/{shell => }/version.h.in | 0 23 files changed, 699 insertions(+), 507 deletions(-) rename src/{shell => }/version.h.in (100%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d763bab8c..b578483dc 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -189,6 +189,8 @@ FOREACH(FILE ${LEANLIB}) ENDFOREACH(FILE) include_directories(${LEAN_SOURCE_DIR}) +configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h") +include_directories("${LEAN_BINARY_DIR}") add_subdirectory(util) set(LEAN_LIBS ${LEAN_LIBS} util) diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index f16ca5057..44de14d63 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -78,19 +78,9 @@ struct lean_extension : public environment_extension { coercion_map m_coercion_map; // mapping from (given_type, expected_type) -> coercion coercion_set m_coercion_set; // Set of coercions expr_to_coercions m_type_coercions; // mapping type -> list (to-type, function) - unsigned m_initial_size; // size of the environment after init_frontend was invoked name_set m_explicit_names; // set of explicit version of constants with implicit parameters lean_extension() { - m_initial_size = 0; - } - - void set_initial_size(unsigned sz) { - m_initial_size = sz; - } - - unsigned get_initial_size() const { - return m_initial_size; } lean_extension const * get_parent() const { @@ -373,11 +363,14 @@ struct lean_extension : public environment_extension { m_implicit_table[n] = mk_pair(v, explicit_version); expr body = mk_explicit_definition_body(type, n, 0, num_args); m_explicit_names.insert(explicit_version); - if (obj.is_axiom() || obj.is_theorem()) { - env->add_theorem(explicit_version, type, body); - } else { - env->add_definition(explicit_version, type, body); - } + env->add_neutral_object(new mark_implicit_command(n, sz, implicit)); + env->auxiliary_section([&]() { + if (obj.is_axiom() || obj.is_theorem()) { + env->add_theorem(explicit_version, type, body); + } else { + env->add_definition(explicit_version, type, body); + } + }); } bool has_implicit_arguments(name const & n) const { @@ -530,11 +523,6 @@ void init_frontend(environment const & env, io_state & ios) { ios.set_formatter(mk_pp_formatter(env)); import_all(env); init_builtin_notation(env, ios); - to_ext(env).set_initial_size(env->get_num_objects(false)); -} - -unsigned get_initial_size(ro_environment const & env) { - return to_ext(env).get_initial_size(); } 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 57730eb34..d3177bc96 100644 --- a/src/frontends/lean/frontend.h +++ b/src/frontends/lean/frontend.h @@ -18,12 +18,6 @@ namespace lean { */ void init_frontend(environment const & env, io_state & ios); -/** - \brief Return the environment size after init_frontend invocation. - Return 0 if \c init_frontend was not invoked for this environment. -*/ -unsigned get_initial_size(ro_environment const & env); - /** @name Notation for parsing and pretty printing. */ diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp index cd71faf0c..2256d560e 100644 --- a/src/frontends/lean/notation.cpp +++ b/src/frontends/lean/notation.cpp @@ -19,106 +19,108 @@ void add_alias(environment const & env, name const & n, name const & m) { \brief Initialize builtin notation. */ void init_builtin_notation(environment const & env, io_state & ios) { - if (!env->mark_builtin_imported("lean_notation")) - return; - add_infix(env, ios, "=", 50, mk_homo_eq_fn()); - mark_implicit_arguments(env, mk_homo_eq_fn(), 1); - mark_implicit_arguments(env, mk_if_fn(), 1); + env->import_builtin( + "lean_notation", + [&]() { + add_infix(env, ios, "=", 50, mk_homo_eq_fn()); + mark_implicit_arguments(env, mk_homo_eq_fn(), 1); + mark_implicit_arguments(env, mk_if_fn(), 1); - add_prefix(env, ios, "\u00ac", 40, mk_not_fn()); // "¬" - add_infixr(env, ios, "&&", 35, mk_and_fn()); // "&&" - add_infixr(env, ios, "/\\", 35, mk_and_fn()); // "/\" - add_infixr(env, ios, "\u2227", 35, mk_and_fn()); // "∧" - add_infixr(env, ios, "||", 30, mk_or_fn()); // "||" - add_infixr(env, ios, "\\/", 30, mk_or_fn()); // "\/" - add_infixr(env, ios, "\u2228", 30, mk_or_fn()); // "∨" - add_infixr(env, ios, "=>", 25, mk_implies_fn()); // "=>" - add_infixr(env, ios, "\u21D2", 25, mk_implies_fn()); // "⇒" - add_infixr(env, ios, "<=>", 25, mk_iff_fn()); // "<=>" - add_infixr(env, ios, "\u21D4", 25, mk_iff_fn()); // "⇔" + add_prefix(env, ios, "\u00ac", 40, mk_not_fn()); // "¬" + add_infixr(env, ios, "&&", 35, mk_and_fn()); // "&&" + add_infixr(env, ios, "/\\", 35, mk_and_fn()); // "/\" + add_infixr(env, ios, "\u2227", 35, mk_and_fn()); // "∧" + add_infixr(env, ios, "||", 30, mk_or_fn()); // "||" + add_infixr(env, ios, "\\/", 30, mk_or_fn()); // "\/" + add_infixr(env, ios, "\u2228", 30, mk_or_fn()); // "∨" + add_infixr(env, ios, "=>", 25, mk_implies_fn()); // "=>" + add_infixr(env, ios, "\u21D2", 25, mk_implies_fn()); // "⇒" + add_infixr(env, ios, "<=>", 25, mk_iff_fn()); // "<=>" + add_infixr(env, ios, "\u21D4", 25, mk_iff_fn()); // "⇔" - add_infixl(env, ios, "+", 65, mk_nat_add_fn()); - add_infixl(env, ios, "-", 65, mk_nat_sub_fn()); - add_prefix(env, ios, "-", 75, mk_nat_neg_fn()); - add_infixl(env, ios, "*", 70, mk_nat_mul_fn()); - add_infix(env, ios, "<=", 50, mk_nat_le_fn()); - add_infix(env, ios, "\u2264", 50, mk_nat_le_fn()); // ≤ - add_infix(env, ios, ">=", 50, mk_nat_ge_fn()); - add_infix(env, ios, "\u2265", 50, mk_nat_ge_fn()); // ≥ - add_infix(env, ios, "<", 50, mk_nat_lt_fn()); - add_infix(env, ios, ">", 50, mk_nat_gt_fn()); - add_mixfixc(env, ios, {"|", "|"}, 55, mk_nat_id_fn()); // absolute value for naturals is the identity function + add_infixl(env, ios, "+", 65, mk_nat_add_fn()); + add_infixl(env, ios, "-", 65, mk_nat_sub_fn()); + add_prefix(env, ios, "-", 75, mk_nat_neg_fn()); + add_infixl(env, ios, "*", 70, mk_nat_mul_fn()); + add_infix(env, ios, "<=", 50, mk_nat_le_fn()); + add_infix(env, ios, "\u2264", 50, mk_nat_le_fn()); // ≤ + add_infix(env, ios, ">=", 50, mk_nat_ge_fn()); + add_infix(env, ios, "\u2265", 50, mk_nat_ge_fn()); // ≥ + add_infix(env, ios, "<", 50, mk_nat_lt_fn()); + add_infix(env, ios, ">", 50, mk_nat_gt_fn()); + add_mixfixc(env, ios, {"|", "|"}, 55, mk_nat_id_fn()); // absolute value for naturals is the identity function - add_infixl(env, ios, "+", 65, mk_int_add_fn()); - add_infixl(env, ios, "-", 65, mk_int_sub_fn()); - add_prefix(env, ios, "-", 75, mk_int_neg_fn()); - add_infixl(env, ios, "*", 70, mk_int_mul_fn()); - add_infixl(env, ios, "div", 70, mk_int_div_fn()); - add_infixl(env, ios, "mod", 70, mk_int_mod_fn()); - add_infix(env, ios, "|", 50, mk_int_divides_fn()); - add_mixfixc(env, ios, {"|", "|"}, 55, mk_int_abs_fn()); - add_infix(env, ios, "<=", 50, mk_int_le_fn()); - add_infix(env, ios, "\u2264", 50, mk_int_le_fn()); // ≤ - add_infix(env, ios, ">=", 50, mk_int_ge_fn()); - add_infix(env, ios, "\u2265", 50, mk_int_ge_fn()); // ≥ - add_infix(env, ios, "<", 50, mk_int_lt_fn()); - add_infix(env, ios, ">", 50, mk_int_gt_fn()); + add_infixl(env, ios, "+", 65, mk_int_add_fn()); + add_infixl(env, ios, "-", 65, mk_int_sub_fn()); + add_prefix(env, ios, "-", 75, mk_int_neg_fn()); + add_infixl(env, ios, "*", 70, mk_int_mul_fn()); + add_infixl(env, ios, "div", 70, mk_int_div_fn()); + add_infixl(env, ios, "mod", 70, mk_int_mod_fn()); + add_infix(env, ios, "|", 50, mk_int_divides_fn()); + add_mixfixc(env, ios, {"|", "|"}, 55, mk_int_abs_fn()); + add_infix(env, ios, "<=", 50, mk_int_le_fn()); + add_infix(env, ios, "\u2264", 50, mk_int_le_fn()); // ≤ + add_infix(env, ios, ">=", 50, mk_int_ge_fn()); + add_infix(env, ios, "\u2265", 50, mk_int_ge_fn()); // ≥ + add_infix(env, ios, "<", 50, mk_int_lt_fn()); + add_infix(env, ios, ">", 50, mk_int_gt_fn()); - add_infixl(env, ios, "+", 65, mk_real_add_fn()); - add_infixl(env, ios, "-", 65, mk_real_sub_fn()); - add_prefix(env, ios, "-", 75, mk_real_neg_fn()); - add_infixl(env, ios, "*", 70, mk_real_mul_fn()); - add_infixl(env, ios, "/", 70, mk_real_div_fn()); - add_mixfixc(env, ios, {"|", "|"}, 55, mk_real_abs_fn()); - add_infix(env, ios, "<=", 50, mk_real_le_fn()); - add_infix(env, ios, "\u2264", 50, mk_real_le_fn()); // ≤ - add_infix(env, ios, ">=", 50, mk_real_ge_fn()); - add_infix(env, ios, "\u2265", 50, mk_real_ge_fn()); // ≥ - add_infix(env, ios, "<", 50, mk_real_lt_fn()); - add_infix(env, ios, ">", 50, mk_real_gt_fn()); + add_infixl(env, ios, "+", 65, mk_real_add_fn()); + add_infixl(env, ios, "-", 65, mk_real_sub_fn()); + add_prefix(env, ios, "-", 75, mk_real_neg_fn()); + add_infixl(env, ios, "*", 70, mk_real_mul_fn()); + add_infixl(env, ios, "/", 70, mk_real_div_fn()); + add_mixfixc(env, ios, {"|", "|"}, 55, mk_real_abs_fn()); + add_infix(env, ios, "<=", 50, mk_real_le_fn()); + add_infix(env, ios, "\u2264", 50, mk_real_le_fn()); // ≤ + add_infix(env, ios, ">=", 50, mk_real_ge_fn()); + add_infix(env, ios, "\u2265", 50, mk_real_ge_fn()); // ≥ + add_infix(env, ios, "<", 50, mk_real_lt_fn()); + add_infix(env, ios, ">", 50, mk_real_gt_fn()); - add_coercion(env, mk_nat_to_int_fn()); - add_coercion(env, mk_int_to_real_fn()); - add_coercion(env, mk_nat_to_real_fn()); + add_coercion(env, mk_nat_to_int_fn()); + add_coercion(env, mk_int_to_real_fn()); + add_coercion(env, mk_nat_to_real_fn()); - // implicit arguments for builtin axioms - mark_implicit_arguments(env, mk_mp_fn(), 2); - mark_implicit_arguments(env, mk_discharge_fn(), 2); - mark_implicit_arguments(env, mk_refl_fn(), 1); - mark_implicit_arguments(env, mk_subst_fn(), 4); - add_alias(env, "Subst", "SubstP"); - mark_implicit_arguments(env, "SubstP", 3); - mark_implicit_arguments(env, mk_eta_fn(), 2); - mark_implicit_arguments(env, mk_abst_fn(), 4); - mark_implicit_arguments(env, mk_imp_antisym_fn(), 2); - mark_implicit_arguments(env, mk_hsymm_fn(), 4); - mark_implicit_arguments(env, mk_htrans_fn(), 6); + // implicit arguments for builtin axioms + mark_implicit_arguments(env, mk_mp_fn(), 2); + mark_implicit_arguments(env, mk_discharge_fn(), 2); + mark_implicit_arguments(env, mk_refl_fn(), 1); + mark_implicit_arguments(env, mk_subst_fn(), 4); + add_alias(env, "Subst", "SubstP"); + mark_implicit_arguments(env, "SubstP", 3); + mark_implicit_arguments(env, mk_eta_fn(), 2); + mark_implicit_arguments(env, mk_abst_fn(), 4); + mark_implicit_arguments(env, mk_imp_antisym_fn(), 2); + mark_implicit_arguments(env, mk_hsymm_fn(), 4); + mark_implicit_arguments(env, mk_htrans_fn(), 6); - // implicit arguments for basic theorems - mark_implicit_arguments(env, mk_absurd_fn(), 1); - mark_implicit_arguments(env, mk_double_neg_elim_fn(), 1); - mark_implicit_arguments(env, mk_mt_fn(), 2); - mark_implicit_arguments(env, mk_contrapos_fn(), 2); - mark_implicit_arguments(env, mk_eq_mp_fn(), 2); - mark_implicit_arguments(env, mk_not_imp1_fn(), 2); - mark_implicit_arguments(env, mk_not_imp2_fn(), 2); - mark_implicit_arguments(env, mk_conj_fn(), 2); - mark_implicit_arguments(env, mk_conjunct1_fn(), 2); - mark_implicit_arguments(env, mk_conjunct2_fn(), 2); - mark_implicit_arguments(env, mk_disj1_fn(), 1); - mark_implicit_arguments(env, mk_disj2_fn(), 1); - mark_implicit_arguments(env, mk_disj_cases_fn(), 3); - mark_implicit_arguments(env, mk_refute_fn(), 1); - mark_implicit_arguments(env, mk_symm_fn(), 3); - mark_implicit_arguments(env, mk_trans_fn(), 4); - mark_implicit_arguments(env, mk_eqt_elim_fn(), 1); - mark_implicit_arguments(env, mk_eqt_intro_fn(), 1); - mark_implicit_arguments(env, mk_congr1_fn(), 4); - mark_implicit_arguments(env, mk_congr2_fn(), 4); - mark_implicit_arguments(env, mk_congr_fn(), 6); - mark_implicit_arguments(env, mk_forall_elim_fn(), 2); - mark_implicit_arguments(env, mk_forall_intro_fn(), 2); - mark_implicit_arguments(env, mk_exists_elim_fn(), 3); - mark_implicit_arguments(env, mk_exists_intro_fn(), 2); + // implicit arguments for basic theorems + mark_implicit_arguments(env, mk_absurd_fn(), 1); + mark_implicit_arguments(env, mk_double_neg_elim_fn(), 1); + mark_implicit_arguments(env, mk_mt_fn(), 2); + mark_implicit_arguments(env, mk_contrapos_fn(), 2); + mark_implicit_arguments(env, mk_eq_mp_fn(), 2); + mark_implicit_arguments(env, mk_not_imp1_fn(), 2); + mark_implicit_arguments(env, mk_not_imp2_fn(), 2); + mark_implicit_arguments(env, mk_conj_fn(), 2); + mark_implicit_arguments(env, mk_conjunct1_fn(), 2); + mark_implicit_arguments(env, mk_conjunct2_fn(), 2); + mark_implicit_arguments(env, mk_disj1_fn(), 1); + mark_implicit_arguments(env, mk_disj2_fn(), 1); + mark_implicit_arguments(env, mk_disj_cases_fn(), 3); + mark_implicit_arguments(env, mk_refute_fn(), 1); + mark_implicit_arguments(env, mk_symm_fn(), 3); + mark_implicit_arguments(env, mk_trans_fn(), 4); + mark_implicit_arguments(env, mk_eqt_elim_fn(), 1); + mark_implicit_arguments(env, mk_eqt_intro_fn(), 1); + mark_implicit_arguments(env, mk_congr1_fn(), 4); + mark_implicit_arguments(env, mk_congr2_fn(), 4); + mark_implicit_arguments(env, mk_congr_fn(), 6); + mark_implicit_arguments(env, mk_forall_elim_fn(), 2); + mark_implicit_arguments(env, mk_forall_intro_fn(), 2); + mark_implicit_arguments(env, mk_exists_elim_fn(), 3); + mark_implicit_arguments(env, mk_exists_intro_fn(), 2); + }); } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index c9a459697..8342d9c7c 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2140,7 +2140,7 @@ class parser::imp { /** \brief Return true iff \c obj is an object that should be ignored by the Show command */ bool is_hidden_object(object const & obj) const { - return obj.is_definition() && is_explicit(m_env, obj.get_name()); + return (obj.is_definition() && is_explicit(m_env, obj.get_name())) || !supported_by_pp(obj); } /** \brief Parse @@ -2155,7 +2155,8 @@ class parser::imp { name opt_id = curr_name(); next(); if (opt_id == g_env_kwd) { - unsigned beg = get_initial_size(m_env); + buffer to_display; + bool all = false; unsigned end = m_env->get_num_objects(false); unsigned i; if (curr_is_nat()) { @@ -2163,20 +2164,30 @@ class parser::imp { } else if (curr_is_identifier() && curr_name() == "all") { next(); i = std::numeric_limits::max(); - beg = 0; + all = true; } else { i = std::numeric_limits::max(); } - unsigned it = end; - while (it != beg && i != 0) { + unsigned it = end; + unsigned num_imports = 0; + while (it != 0 && i != 0) { --it; - if (!is_hidden_object(m_env->get_object(it, false))) - --i; - } - for (; it != end; ++it) { auto obj = m_env->get_object(it, false); - if (!is_hidden_object(obj)) - regular(m_io_state) << obj << endl; + if (is_begin_import(obj)) { + lean_assert(num_imports > 0); + num_imports--; + } else if (is_end_import(obj)) { + num_imports++; + } else if (is_hidden_object(obj)) { + // skip + } else if (num_imports == 0 || all) { + to_display.push_back(obj); + --i; + } + } + std::reverse(to_display.begin(), to_display.end()); + for (auto obj : to_display) { + regular(m_io_state) << obj << endl; } } else if (opt_id == g_options_kwd) { regular(m_io_state) << pp(m_io_state.get_options()) << endl; diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index dac5ee049..1e7526d90 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -154,6 +154,18 @@ expr replace_var_with_name(expr const & a, name const & n) { }); } +bool is_notation_decl(object const & obj) { + return dynamic_cast(obj.cell()); +} + +bool is_coercion_decl(object const & obj) { + return dynamic_cast(obj.cell()); +} + +bool supported_by_pp(object const & obj) { + return obj.kind() != object_kind::Neutral || is_notation_decl(obj) || is_coercion_decl(obj); +} + /** \brief Functional object for pretty printing expressions */ class pp_fn { typedef scoped_map aliases; @@ -1375,9 +1387,9 @@ public: case object_kind::Builtin: return pp_postulate(obj, opts); case object_kind::BuiltinSet: return pp_builtin_set(obj, opts); case object_kind::Neutral: - if (dynamic_cast(obj.cell())) { + if (is_notation_decl(obj)) { return pp_notation_decl(obj, opts); - } else if (dynamic_cast(obj.cell())) { + } else if (is_coercion_decl(obj)) { return pp_coercion_decl(obj, opts); } else { // If the object is not notation or coercion @@ -1392,13 +1404,16 @@ public: virtual format operator()(ro_environment const & env, options const & opts) { format r; bool first = true; - std::for_each(env->begin_objects(), - env->end_objects(), - [&](object const & obj) { - check_interrupted(); - if (first) first = false; else r += line(); - r += operator()(obj, opts); - }); + auto it = env->begin_objects(); + auto end = env->end_objects(); + for (; it != end; ++it) { + check_interrupted(); + auto obj = *it; + if (supported_by_pp(obj)) { + if (first) first = false; else r += line(); + r += operator()(obj, opts); + } + } return r; } diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 8f652e1da..d007c247a 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -14,4 +14,6 @@ class frontend; class environment; formatter mk_pp_formatter(ro_environment const & env); std::ostream & operator<<(std::ostream & out, frontend const & fe); +/** \brief Return true iff the given object is supported by this pretty printer. */ +bool supported_by_pp(object const & obj); } diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 133b32f24..cc6349b6e 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -220,91 +220,93 @@ MK_CONSTANT(htrans_fn, name("HTrans")); MK_CONSTANT(hsymm_fn, name("HSymm")); void import_basic(environment const & env) { - if (!env->mark_builtin_imported("basic")) - return; - env->add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION); - env->add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION); + env->import_builtin + ("basic", + [&]() { + env->add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION); + env->add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION); - expr p1 = Bool >> Bool; - expr p2 = Bool >> p1; - expr f = Const("f"); - expr g = Const("g"); - expr a = Const("a"); - expr b = Const("b"); - expr c = Const("c"); - expr x = Const("x"); - expr y = Const("y"); - expr A = Const("A"); - expr A_pred = A >> Bool; - expr B = Const("B"); - expr C = Const("C"); - expr q_type = Pi({A, TypeU}, A_pred >> Bool); - expr piABx = Pi({x, A}, B(x)); - expr A_arrow_u = A >> TypeU; - expr P = Const("P"); - expr H = Const("H"); - expr H1 = Const("H1"); - expr H2 = Const("H2"); + expr p1 = Bool >> Bool; + expr p2 = Bool >> p1; + expr f = Const("f"); + expr g = Const("g"); + expr a = Const("a"); + expr b = Const("b"); + expr c = Const("c"); + expr x = Const("x"); + expr y = Const("y"); + expr A = Const("A"); + expr A_pred = A >> Bool; + expr B = Const("B"); + expr C = Const("C"); + expr q_type = Pi({A, TypeU}, A_pred >> Bool); + expr piABx = Pi({x, A}, B(x)); + expr A_arrow_u = A >> TypeU; + expr P = Const("P"); + expr H = Const("H"); + expr H1 = Const("H1"); + expr H2 = Const("H2"); - env->add_builtin(mk_bool_type()); - env->add_builtin(mk_bool_value(true)); - env->add_builtin(mk_bool_value(false)); - env->add_builtin(mk_if_fn()); + env->add_builtin(mk_bool_type()); + env->add_builtin(mk_bool_value(true)); + env->add_builtin(mk_bool_value(false)); + env->add_builtin(mk_if_fn()); - // implies(x, y) := if x y True - env->add_opaque_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True))); + // implies(x, y) := if x y True + env->add_opaque_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True))); - // iff(x, y) := x = y - env->add_opaque_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y))); + // iff(x, y) := x = y + env->add_opaque_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y))); - // not(x) := if x False True - env->add_opaque_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True))); + // not(x) := if x False True + env->add_opaque_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True))); - // or(x, y) := Not(x) => y - env->add_opaque_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y))); + // or(x, y) := Not(x) => y + env->add_opaque_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y))); - // and(x, y) := Not(x => Not(y)) - env->add_opaque_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y))))); + // and(x, y) := Not(x => Not(y)) + env->add_opaque_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y))))); - // forall : Pi (A : Type u), (A -> Bool) -> Bool - env->add_opaque_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True)))); - // TODO(Leo): introduce epsilon - env->add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x))))))); - // Aliases for forall and exists - env->add_definition(Forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Forall(A, P))); - env->add_definition(Exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Exists(A, P))); + // forall : Pi (A : Type u), (A -> Bool) -> Bool + env->add_opaque_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True)))); + // TODO(Leo): introduce epsilon + env->add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x))))))); + // Aliases for forall and exists + env->add_definition(Forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Forall(A, P))); + env->add_definition(Exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Exists(A, P))); - // homogeneous equality - env->add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y))); + // homogeneous equality + env->add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y))); - // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b - env->add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b)); + // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b + env->add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b)); - // Discharge : Pi (a b : Bool) (H : a -> b), a => b - env->add_axiom(discharge_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a >> b}}, Implies(a, b))); + // Discharge : Pi (a b : Bool) (H : a -> b), a => b + env->add_axiom(discharge_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a >> b}}, Implies(a, b))); - // Case : Pi (P : Bool -> Bool) (H1 : P True) (H2 : P False) (a : Bool), P a - env->add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a))); + // Case : Pi (P : Bool -> Bool) (H1 : P True) (H2 : P False) (a : Bool), P a + env->add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a))); - // Refl : Pi (A : Type u) (a : A), a = a - env->add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a))); + // Refl : Pi (A : Type u) (a : A), a = a + env->add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a))); - // Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b - env->add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b))); + // Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b + env->add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b))); - // Eta : Pi (A : Type u) (B : A -> Type u), f : (Pi x : A, B x), (Fun x : A => f x) = f - env->add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f))); + // Eta : Pi (A : Type u) (B : A -> Type u), f : (Pi x : A, B x), (Fun x : A => f x) = f + env->add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f))); - // ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b - env->add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b))); + // ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b + env->add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b))); - // Abst : Pi (A : Type u) (B : A -> Type u), f g : (Pi x : A, B x), H : (Pi x : A, (f x) = (g x)), f = g - env->add_axiom(abst_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi(x, A, Eq(f(x), g(x)))}}, Eq(f, g))); + // Abst : Pi (A : Type u) (B : A -> Type u), f g : (Pi x : A, B x), H : (Pi x : A, (f x) = (g x)), f = g + env->add_axiom(abst_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi(x, A, Eq(f(x), g(x)))}}, Eq(f, g))); - // HSymm : Pi (A B : Type u) (a : A) (b : B) (H1 : a = b), b = a - env->add_axiom(hsymm_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {H1, Eq(a, b)}}, Eq(b, a))); + // HSymm : Pi (A B : Type u) (a : A) (b : B) (H1 : a = b), b = a + env->add_axiom(hsymm_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {H1, Eq(a, b)}}, Eq(b, a))); - // HTrans : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c - env->add_axiom(htrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c))); + // HTrans : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c + env->add_axiom(htrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c))); + }); } } diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 3abce2d35..08e460c51 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -8,10 +8,13 @@ Author: Leonardo de Moura #include #include #include +#include +#include #include "util/thread.h" #include "util/safe_arith.h" #include "util/realpath.h" #include "util/sstream.h" +#include "util/lean_path.h" #include "kernel/for_each_fn.h" #include "kernel/find_fn.h" #include "kernel/kernel_exception.h" @@ -19,6 +22,7 @@ Author: Leonardo de Moura #include "kernel/threadsafe_environment.h" #include "kernel/type_checker.h" #include "kernel/normalizer.h" +#include "version.h" namespace lean { class set_opaque_command : public neutral_object_cell { @@ -37,6 +41,45 @@ static void read_set_opaque(environment const & env, io_state const &, deseriali } static object_cell::register_deserializer_fn set_opaque_ds("SetOpaque", read_set_opaque); +class import_command : public neutral_object_cell { + std::string m_mod_name; +public: + import_command(std::string const & n):m_mod_name(n) {} + virtual ~import_command() {} + virtual char const * keyword() const { return "Import"; } + virtual void write(serializer & s) const { s << "Import" << m_mod_name; } +}; +static void read_import(environment const & env, io_state const & ios, deserializer & d) { + std::string n = d.read_string(); + env->import(n, ios); +} +static object_cell::register_deserializer_fn import_ds("Import", read_import); + +class end_import_mark : public neutral_object_cell { +public: + end_import_mark() {} + virtual ~end_import_mark() {} + virtual char const * keyword() const { return "EndImport"; } + virtual void write(serializer &) const {} +}; + +// For Importing builtin modules +class begin_import_mark : public neutral_object_cell { +public: + begin_import_mark() {} + virtual ~begin_import_mark() {} + virtual char const * keyword() const { return "BeginImport"; } + virtual void write(serializer &) const {} +}; + +bool is_begin_import(object const & obj) { + return dynamic_cast(obj.cell()) || dynamic_cast(obj.cell()); +} + +bool is_end_import(object const & obj) { + return dynamic_cast(obj.cell()); +} + static name g_builtin_module("builtin_module"); class extension_factory { std::vector m_makers; @@ -461,8 +504,80 @@ bool environment_cell::mark_imported(char const * fname) { return mark_imported_core(name(realpath(fname))); } -bool environment_cell::mark_builtin_imported(char const * id) { - return mark_imported_core(name(g_builtin_module, id)); +void environment_cell::auxiliary_section(std::function fn) { + add_neutral_object(new begin_import_mark()); + try { + fn(); + add_neutral_object(new end_import_mark()); + } catch (...) { + add_neutral_object(new end_import_mark()); + throw; + } +} + +void environment_cell::import_builtin(char const * id, std::function fn) { + if (mark_imported_core(name(g_builtin_module, id))) { + auxiliary_section(fn); + } +} + +static char const * g_olean_header = "oleanfile"; +static char const * g_olean_end_file = "EndFile"; +void environment_cell::export_objects(std::string const & fname) { + std::ofstream out(fname); + serializer s(out); + s << g_olean_header << LEAN_VERSION_MAJOR << LEAN_VERSION_MINOR; + auto it = begin_objects(); + auto end = end_objects(); + unsigned num_imports = 0; + for (; it != end; ++it) { + object const & obj = *it; + if (dynamic_cast(obj.cell())) { + if (num_imports == 0) + obj.write(s); + num_imports++; + } else if (dynamic_cast(obj.cell())) { + lean_assert(num_imports > 0); + num_imports--; + } else if (dynamic_cast(obj.cell())) { + num_imports++; + } else if (num_imports == 0) { + obj.write(s); + } + } + s << g_olean_end_file; +} + +bool environment_cell::import(std::string const & fname, io_state const & ios) { + std::string full_fname = realpath(find_file(fname, {".olean"}).c_str()); + if (mark_imported_core(full_fname)) { + std::ifstream in(fname); + deserializer d(in); + std::string header; + d >> header; + if (header != g_olean_header) + throw exception(sstream() << "file '" << full_fname << "' does not seem to be a valid object Lean file"); + unsigned major, minor; + // Perhaps we should enforce the right version number + d >> major >> minor; + try { + add_neutral_object(new import_command(fname)); + while (true) { + std::string k; + d >> k; + if (k == g_olean_end_file) { + add_neutral_object(new end_import_mark()); + return true; + } + read_object(env(), ios, k, d); + } + } catch (...) { + add_neutral_object(new end_import_mark()); + throw; + } + } else { + return false; + } } environment_cell::environment_cell(): diff --git a/src/kernel/environment.h b/src/kernel/environment.h index dd30e6429..60fb1b868 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include #include +#include #include "util/lua.h" #include "util/shared_mutex.h" #include "util/name_map.h" @@ -314,11 +315,18 @@ public: It will also mark the file as imported. */ bool mark_imported(char const * fname); + + void import_builtin(char const * id, std::function fn); + + void export_objects(std::string const & fname); + + bool import(std::string const & fname, io_state const & ios); + /** - \brief Return true iff the given builtin id was not already marked as imported. - It will also mark the id as imported. + \brief Execute function \c fn. Any object created by \c fn + is not exported by the environment. */ - bool mark_builtin_imported(char const * id); + void auxiliary_section(std::function fn); }; /** @@ -382,4 +390,9 @@ public: environment_cell const * operator->() const { return m_ptr.get(); } environment_cell const & operator*() const { return *(m_ptr.get()); } }; + +/** \brief Return true iff the given object marks the begin of the of a sequence of imported objects. */ +bool is_begin_import(object const & obj); +/** \brief Return true iff the given object marks the end of the of a sequence of imported objects. */ +bool is_end_import(object const & obj); } diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index a5a5e6e99..f7aa1f431 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -73,7 +73,7 @@ public: already_declared_exception(ro_environment const & env, name const & n):kernel_exception(env), m_name(n) {} virtual ~already_declared_exception() noexcept {} name const & get_name() const { return m_name; } - virtual char const * what() const noexcept { return "invalid object declaration, environment already has an object the given name"; } + virtual char const * what() const noexcept { return "invalid object declaration, environment already has an object with the given name"; } virtual format pp(formatter const & fmt, options const & opts) const; virtual exception * clone() const { return new already_declared_exception(m_env, m_name); } virtual void rethrow() const { throw *this; } diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp index 81eb4627d..e09715efb 100644 --- a/src/kernel/object.cpp +++ b/src/kernel/object.cpp @@ -22,8 +22,7 @@ void object_cell::register_deserializer(std::string const & k, reader rd) { lean_assert(readers.find(k) == readers.end()); readers[k] = rd; } -static void read_object(environment const & env, io_state const & ios, deserializer & d) { - auto k = d.read_string(); +void read_object(environment const & env, io_state const & ios, std::string const & k, deserializer & d) { object_readers & readers = get_object_readers(); auto it = readers.find(k); lean_assert(it != readers.end()); diff --git a/src/kernel/object.h b/src/kernel/object.h index ec0d52fa3..329e4c998 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -139,6 +139,8 @@ public: bool is_builtin_set() const { return m_ptr->is_builtin_set(); } bool in_builtin_set(expr const & e) const { return m_ptr->in_builtin_set(e); } + void write(serializer & s) const { m_ptr->write(s); } + object_cell const * cell() const { return m_ptr; } }; @@ -155,6 +157,8 @@ object mk_axiom(name const & n, expr const & t); object mk_var_decl(name const & n, expr const & t); inline object mk_neutral(neutral_object_cell * c) { lean_assert(c->get_rc() == 1); return object(c); } +void read_object(environment const & env, io_state const & ios, std::string const & k, deserializer & d); + /** \brief Helper function whether we should unfold an definition or not. diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index 22aef59fd..d3dc4302b 100644 --- a/src/library/arith/int.cpp +++ b/src/library/arith/int.cpp @@ -164,34 +164,36 @@ MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"})); MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"})); void import_int(environment const & env) { - if (!env->mark_builtin_imported("int")) - return; - import_nat(env); - expr i_i = Int >> Int; - expr ii_b = Int >> (Int >> Bool); - expr ii_i = Int >> (Int >> Int); - expr x = Const("x"); - expr y = Const("y"); + env->import_builtin( + "int", + [&]() { + import_nat(env); + expr i_i = Int >> Int; + expr ii_b = Int >> (Int >> Bool); + expr ii_i = Int >> (Int >> Int); + expr x = Const("x"); + expr y = Const("y"); - env->add_builtin(Int); - env->add_builtin_set(iVal(0)); - env->add_builtin(mk_int_add_fn()); - env->add_builtin(mk_int_mul_fn()); - env->add_builtin(mk_int_div_fn()); - env->add_builtin(mk_int_le_fn()); - env->add_builtin(mk_nat_to_int_fn()); + env->add_builtin(Int); + env->add_builtin_set(iVal(0)); + env->add_builtin(mk_int_add_fn()); + env->add_builtin(mk_int_mul_fn()); + env->add_builtin(mk_int_div_fn()); + env->add_builtin(mk_int_le_fn()); + env->add_builtin(mk_nat_to_int_fn()); - env->add_opaque_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y)))); - env->add_opaque_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x))); - env->add_opaque_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y))))); - env->add_opaque_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0)))); - env->add_opaque_definition(int_ge_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, iLe(y, x))); - env->add_opaque_definition(int_lt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x)))); - env->add_opaque_definition(int_gt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y)))); - env->add_opaque_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x)))); + env->add_opaque_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y)))); + env->add_opaque_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x))); + env->add_opaque_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y))))); + env->add_opaque_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0)))); + env->add_opaque_definition(int_ge_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, iLe(y, x))); + env->add_opaque_definition(int_lt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x)))); + env->add_opaque_definition(int_gt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y)))); + env->add_opaque_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x)))); - env->add_opaque_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y)))); - env->add_opaque_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x)))); + env->add_opaque_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y)))); + env->add_opaque_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x)))); + }); } static int mk_int_value(lua_State * L) { diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp index 5a43b1d2c..f2f5b2b45 100644 --- a/src/library/arith/nat.cpp +++ b/src/library/arith/nat.cpp @@ -123,22 +123,24 @@ MK_CONSTANT(nat_gt_fn, name({"Nat", "gt"})); MK_CONSTANT(nat_id_fn, name({"Nat", "id"})); void import_nat(environment const & env) { - if (!env->mark_builtin_imported("nat")) - return; - expr nn_b = Nat >> (Nat >> Bool); - expr x = Const("x"); - expr y = Const("y"); + env->import_builtin( + "nat", + [&]() { + expr nn_b = Nat >> (Nat >> Bool); + expr x = Const("x"); + expr y = Const("y"); - env->add_builtin(Nat); - env->add_builtin_set(nVal(0)); - env->add_builtin(mk_nat_add_fn()); - env->add_builtin(mk_nat_mul_fn()); - env->add_builtin(mk_nat_le_fn()); + env->add_builtin(Nat); + env->add_builtin_set(nVal(0)); + env->add_builtin(mk_nat_add_fn()); + env->add_builtin(mk_nat_mul_fn()); + env->add_builtin(mk_nat_le_fn()); - env->add_opaque_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x))); - env->add_opaque_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x)))); - env->add_opaque_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y)))); - env->add_opaque_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x)); + env->add_opaque_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x))); + env->add_opaque_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x)))); + env->add_opaque_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y)))); + env->add_opaque_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x)); + }); } static int mk_nat_value(lua_State * L) { diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp index 78680f240..241af1cdd 100644 --- a/src/library/arith/real.cpp +++ b/src/library/arith/real.cpp @@ -150,27 +150,29 @@ MK_CONSTANT(real_lt_fn, name({"Real", "lt"})); MK_CONSTANT(real_gt_fn, name({"Real", "gt"})); void import_real(environment const & env) { - if (!env->mark_builtin_imported("real")) - return; - expr rr_b = Real >> (Real >> Bool); - expr rr_r = Real >> (Real >> Real); - expr r_r = Real >> Real; - expr x = Const("x"); - expr y = Const("y"); + env->import_builtin( + "real", + [&]() { + expr rr_b = Real >> (Real >> Bool); + expr rr_r = Real >> (Real >> Real); + expr r_r = Real >> Real; + expr x = Const("x"); + expr y = Const("y"); - env->add_builtin(Real); - env->add_builtin_set(rVal(0)); - env->add_builtin(mk_real_add_fn()); - env->add_builtin(mk_real_mul_fn()); - env->add_builtin(mk_real_div_fn()); - env->add_builtin(mk_real_le_fn()); + env->add_builtin(Real); + env->add_builtin_set(rVal(0)); + env->add_builtin(mk_real_add_fn()); + env->add_builtin(mk_real_mul_fn()); + env->add_builtin(mk_real_div_fn()); + env->add_builtin(mk_real_le_fn()); - env->add_opaque_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y)))); - env->add_opaque_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(rVal(-1), x))); - env->add_opaque_definition(real_abs_fn_name, r_r, Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x)))); - env->add_opaque_definition(real_ge_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, rLe(y, x))); - env->add_opaque_definition(real_lt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(y, x)))); - env->add_opaque_definition(real_gt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(x, y)))); + env->add_opaque_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y)))); + env->add_opaque_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(rVal(-1), x))); + env->add_opaque_definition(real_abs_fn_name, r_r, Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x)))); + env->add_opaque_definition(real_ge_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, rLe(y, x))); + env->add_opaque_definition(real_lt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(y, x)))); + env->add_opaque_definition(real_gt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(x, y)))); + }); } class int_to_real_value : public const_value { @@ -191,14 +193,16 @@ static register_deserializer_fn int_to_real_ds("int_to_real", read_int_to_real); MK_CONSTANT(nat_to_real_fn, name("nat_to_real")); void import_int_to_real_coercions(environment const & env) { - if (!env->mark_builtin_imported("real_coercions")) - return; - import_int(env); - import_real(env); + env->import_builtin( + "real_coercions", + [&]() { + import_int(env); + import_real(env); - env->add_builtin(mk_int_to_real_fn()); - expr x = Const("x"); - env->add_opaque_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x)))); + env->add_builtin(mk_int_to_real_fn()); + expr x = Const("x"); + env->add_opaque_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x)))); + }); } static int mk_real_value(lua_State * L) { diff --git a/src/library/arith/special_fn.cpp b/src/library/arith/special_fn.cpp index 8dbed647b..223ff2a80 100644 --- a/src/library/arith/special_fn.cpp +++ b/src/library/arith/special_fn.cpp @@ -29,32 +29,34 @@ MK_CONSTANT(sech_fn, name("sech")); MK_CONSTANT(csch_fn, name("csch")); void import_special_fn(environment const & env) { - if (!env->mark_builtin_imported("special_fn")) - return; - import_real(env); + env->import_builtin( + "special_fn", + [&]() { + import_real(env); - expr r_r = Real >> Real; - expr x = Const("x"); + expr r_r = Real >> Real; + expr x = Const("x"); - env->add_var(exp_fn_name, r_r); - env->add_var(log_fn_name, r_r); + env->add_var(exp_fn_name, r_r); + env->add_var(log_fn_name, r_r); - env->add_var(real_pi_name, Real); - env->add_definition(name("pi"), Real, mk_real_pi()); // alias for pi - env->add_var(sin_fn_name, r_r); - env->add_opaque_definition(cos_fn_name, r_r, Fun({x, Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2)))))); - env->add_opaque_definition(tan_fn_name, r_r, Fun({x, Real}, rDiv(Sin(x), Cos(x)))); - env->add_opaque_definition(cot_fn_name, r_r, Fun({x, Real}, rDiv(Cos(x), Sin(x)))); - env->add_opaque_definition(sec_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cos(x)))); - env->add_opaque_definition(csc_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sin(x)))); + env->add_var(real_pi_name, Real); + env->add_definition(name("pi"), Real, mk_real_pi()); // alias for pi + env->add_var(sin_fn_name, r_r); + env->add_opaque_definition(cos_fn_name, r_r, Fun({x, Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2)))))); + env->add_opaque_definition(tan_fn_name, r_r, Fun({x, Real}, rDiv(Sin(x), Cos(x)))); + env->add_opaque_definition(cot_fn_name, r_r, Fun({x, Real}, rDiv(Cos(x), Sin(x)))); + env->add_opaque_definition(sec_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cos(x)))); + env->add_opaque_definition(csc_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sin(x)))); - env->add_opaque_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))), - rMul(rVal(2), Exp(rNeg(x)))))); - env->add_opaque_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))), - rMul(rVal(2), Exp(rNeg(x)))))); - env->add_opaque_definition(tanh_fn_name, r_r, Fun({x, Real}, rDiv(Sinh(x), Cosh(x)))); - env->add_opaque_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x)))); - env->add_opaque_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x)))); - env->add_opaque_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x)))); + env->add_opaque_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))), + rMul(rVal(2), Exp(rNeg(x)))))); + env->add_opaque_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))), + rMul(rVal(2), Exp(rNeg(x)))))); + env->add_opaque_definition(tanh_fn_name, r_r, Fun({x, Real}, rDiv(Sinh(x), Cosh(x)))); + env->add_opaque_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x)))); + env->add_opaque_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x)))); + env->add_opaque_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x)))); + }); } } diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp index b9c16997b..c8d4a6d15 100644 --- a/src/library/basic_thms.cpp +++ b/src/library/basic_thms.cpp @@ -47,241 +47,243 @@ MK_CONSTANT(exists_elim_fn, name("ExistsElim")); MK_CONSTANT(exists_intro_fn, name("ExistsIntro")); void import_basic_thms(environment const & env) { - if (!env->mark_builtin_imported("basic_thms")) - return; - expr A = Const("A"); - expr a = Const("a"); - expr b = Const("b"); - expr c = Const("c"); - expr H = Const("H"); - expr H1 = Const("H1"); - expr H2 = Const("H2"); - expr H3 = Const("H3"); - expr B = Const("B"); - expr f = Const("f"); - expr g = Const("g"); - expr h = Const("h"); - expr x = Const("x"); - expr y = Const("y"); - expr z = Const("z"); - expr P = Const("P"); - expr A1 = Const("A1"); - expr B1 = Const("B1"); - expr a1 = Const("a1"); - expr R = Const("R"); + env->import_builtin( + "basic_thms", + [&]() { + expr A = Const("A"); + expr a = Const("a"); + expr b = Const("b"); + expr c = Const("c"); + expr H = Const("H"); + expr H1 = Const("H1"); + expr H2 = Const("H2"); + expr H3 = Const("H3"); + expr B = Const("B"); + expr f = Const("f"); + expr g = Const("g"); + expr h = Const("h"); + expr x = Const("x"); + expr y = Const("y"); + expr z = Const("z"); + expr P = Const("P"); + expr A1 = Const("A1"); + expr B1 = Const("B1"); + expr a1 = Const("a1"); + expr R = Const("R"); - expr A_pred = A >> Bool; - expr q_type = Pi({A, TypeU}, A_pred >> Bool); - expr piABx = Pi({x, A}, B(x)); - expr A_arrow_u = A >> TypeU; + expr A_pred = A >> Bool; + expr q_type = Pi({A, TypeU}, A_pred >> Bool); + expr piABx = Pi({x, A}, B(x)); + expr A_arrow_u = A >> TypeU; - // Trivial : True - env->add_theorem(trivial_name, True, Refl(Bool, True)); + // Trivial : True + env->add_theorem(trivial_name, True, Refl(Bool, True)); - // True_neq_False : Not(True = False) - env->add_theorem(true_neq_false_name, Not(Eq(True, False)), Trivial); + // True_neq_False : Not(True = False) + env->add_theorem(true_neq_false_name, Not(Eq(True, False)), Trivial); - // EM : Pi (a : Bool), Or(a, Not(a)) - env->add_theorem(em_fn_name, Pi({a, Bool}, Or(a, Not(a))), - Fun({a, Bool}, Case(Fun({x, Bool}, Or(x, Not(x))), Trivial, Trivial, a))); + // EM : Pi (a : Bool), Or(a, Not(a)) + env->add_theorem(em_fn_name, Pi({a, Bool}, Or(a, Not(a))), + Fun({a, Bool}, Case(Fun({x, Bool}, Or(x, Not(x))), Trivial, Trivial, a))); - // FalseElim : Pi (a : Bool) (H : False), a - env->add_theorem(false_elim_fn_name, Pi({{a, Bool}, {H, False}}, a), - Fun({{a, Bool}, {H, False}}, Case(Fun({x, Bool}, x), Trivial, H, a))); + // FalseElim : Pi (a : Bool) (H : False), a + env->add_theorem(false_elim_fn_name, Pi({{a, Bool}, {H, False}}, a), + Fun({{a, Bool}, {H, False}}, Case(Fun({x, Bool}, x), Trivial, H, a))); - // Absurd : Pi (a : Bool) (H1 : a) (H2 : Not a), False - env->add_theorem(absurd_fn_name, Pi({{a, Bool}, {H1, a}, {H2, Not(a)}}, False), - Fun({{a, Bool}, {H1, a}, {H2, Not(a)}}, - MP(a, False, H2, H1))); + // Absurd : Pi (a : Bool) (H1 : a) (H2 : Not a), False + env->add_theorem(absurd_fn_name, Pi({{a, Bool}, {H1, a}, {H2, Not(a)}}, False), + Fun({{a, Bool}, {H1, a}, {H2, Not(a)}}, + MP(a, False, H2, H1))); - // EqMP : Pi (a b: Bool) (H1 : a = b) (H2 : a), b - env->add_theorem(eq_mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, b), - Fun({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, - Subst(Bool, a, b, Fun({x, Bool}, x), H2, H1))); + // EqMP : Pi (a b: Bool) (H1 : a = b) (H2 : a), b + env->add_theorem(eq_mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, b), + Fun({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, + Subst(Bool, a, b, Fun({x, Bool}, x), H2, H1))); - // DoubleNeg : Pi (a : Bool), Eq(Not(Not(a)), a) - env->add_theorem(double_neg_fn_name, Pi({a, Bool}, Eq(Not(Not(a)), a)), - Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Not(Not(x)), x)), Trivial, Trivial, a))); + // DoubleNeg : Pi (a : Bool), Eq(Not(Not(a)), a) + env->add_theorem(double_neg_fn_name, Pi({a, Bool}, Eq(Not(Not(a)), a)), + Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Not(Not(x)), x)), Trivial, Trivial, a))); - // DoubleNegElim : Pi (P : Bool) (H : Not (Not P)), P - env->add_theorem(double_neg_elim_fn_name, Pi({{P, Bool}, {H, Not(Not(P))}}, P), - Fun({{P, Bool}, {H, Not(Not(P))}}, - EqMP(Not(Not(P)), P, DoubleNeg(P), H))); + // DoubleNegElim : Pi (P : Bool) (H : Not (Not P)), P + env->add_theorem(double_neg_elim_fn_name, Pi({{P, Bool}, {H, Not(Not(P))}}, P), + Fun({{P, Bool}, {H, Not(Not(P))}}, + EqMP(Not(Not(P)), P, DoubleNeg(P), H))); - // ModusTollens : Pi (a b : Bool) (H1 : a => b) (H2 : Not(b)), Not(a) - env->add_theorem(mt_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, Not(a)), - Fun({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, - Discharge(a, False, Fun({H, a}, - Absurd(b, MP(a, b, H1, H), H2))))); + // ModusTollens : Pi (a b : Bool) (H1 : a => b) (H2 : Not(b)), Not(a) + env->add_theorem(mt_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, Not(a)), + Fun({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, + Discharge(a, False, Fun({H, a}, + Absurd(b, MP(a, b, H1, H), H2))))); - // Contrapositive : Pi (a b : Bool) (H : a => b), (Not(b) => Not(a)) - env->add_theorem(contrapos_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, Implies(Not(b), Not(a))), - Fun({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, - Discharge(Not(b), Not(a), Fun({H1, Not(b)}, MT(a, b, H, H1))))); + // Contrapositive : Pi (a b : Bool) (H : a => b), (Not(b) => Not(a)) + env->add_theorem(contrapos_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, Implies(Not(b), Not(a))), + Fun({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, + Discharge(Not(b), Not(a), Fun({H1, Not(b)}, MT(a, b, H, H1))))); - // FalseImpliesAny : Pi (a : Bool), False => a - env->add_theorem(false_imp_any_fn_name, Pi({a, Bool}, Implies(False, a)), - Fun({a, Bool}, Case(Fun({x, Bool}, Implies(False, x)), Trivial, Trivial, a))); + // FalseImpliesAny : Pi (a : Bool), False => a + env->add_theorem(false_imp_any_fn_name, Pi({a, Bool}, Implies(False, a)), + Fun({a, Bool}, Case(Fun({x, Bool}, Implies(False, x)), Trivial, Trivial, a))); - // AbsurdImpliesAny : Pi (a c : Bool) (H1 : a) (H2 : Not a), c - env->add_theorem(absurd_imp_any_fn_name, Pi({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, c), - Fun({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, - MP(False, c, FalseImpAny(c), Absurd(a, H1, H2)))); + // AbsurdImpliesAny : Pi (a c : Bool) (H1 : a) (H2 : Not a), c + env->add_theorem(absurd_imp_any_fn_name, Pi({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, c), + Fun({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, + MP(False, c, FalseImpAny(c), Absurd(a, H1, H2)))); - // NotImp1 : Pi (a b : Bool) (H : Not(Implies(a, b))), a - env->add_theorem(not_imp1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, a), - Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, - EqMP(Not(Not(a)), a, - DoubleNeg(a), - Discharge(Not(a), False, - Fun({H1, Not(a)}, - Absurd(Implies(a, b), - Discharge(a, b, - Fun({H2, a}, - FalseElim(b, Absurd(a, H2, H1)))), - H)))))); + // NotImp1 : Pi (a b : Bool) (H : Not(Implies(a, b))), a + env->add_theorem(not_imp1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, a), + Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, + EqMP(Not(Not(a)), a, + DoubleNeg(a), + Discharge(Not(a), False, + Fun({H1, Not(a)}, + Absurd(Implies(a, b), + Discharge(a, b, + Fun({H2, a}, + FalseElim(b, Absurd(a, H2, H1)))), + H)))))); - // NotImp2 : Pi (a b : Bool) (H : Not(Implies(a, b))), Not(b) - env->add_theorem(not_imp2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, Not(b)), - Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, - Discharge(b, False, - Fun({H1, b}, - Absurd(Implies(a, b), - // a => b - Discharge(a, b, Fun({H2, a}, H1)), - H))))); + // NotImp2 : Pi (a b : Bool) (H : Not(Implies(a, b))), Not(b) + env->add_theorem(not_imp2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, Not(b)), + Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, + Discharge(b, False, + Fun({H1, b}, + Absurd(Implies(a, b), + // a => b + Discharge(a, b, Fun({H2, a}, H1)), + H))))); - // Conj : Pi (a b : Bool) (H1 : a) (H2 : b), And(a, b) - env->add_theorem(conj_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, And(a, b)), - Fun({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, - Discharge(Implies(a, Not(b)), False, Fun({H, Implies(a, Not(b))}, - Absurd(b, H2, MP(a, Not(b), H, H1)))))); + // Conj : Pi (a b : Bool) (H1 : a) (H2 : b), And(a, b) + env->add_theorem(conj_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, And(a, b)), + Fun({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, + Discharge(Implies(a, Not(b)), False, Fun({H, Implies(a, Not(b))}, + Absurd(b, H2, MP(a, Not(b), H, H1)))))); - // Conjunct1 : Pi (a b : Bool) (H : And(a, b)), a - env->add_theorem(conjunct1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, a), - Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}}, - NotImp1(a, Not(b), H))); + // Conjunct1 : Pi (a b : Bool) (H : And(a, b)), a + env->add_theorem(conjunct1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, a), + Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}}, + NotImp1(a, Not(b), H))); - // Conjunct2 : Pi (a b : Bool) (H : And(a, b)), b - env->add_theorem(conjunct2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, b), - Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}}, - EqMP(Not(Not(b)), b, DoubleNeg(b), NotImp2(a, Not(b), H)))); + // Conjunct2 : Pi (a b : Bool) (H : And(a, b)), b + env->add_theorem(conjunct2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, b), + Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}}, + EqMP(Not(Not(b)), b, DoubleNeg(b), NotImp2(a, Not(b), H)))); - // Disj1 : Pi (a b : Bool) (H : a), Or(a, b) - env->add_theorem(disj1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a}}, Or(a, b)), - Fun({{a, Bool}, {b, Bool}, {H, a}}, - Discharge(Not(a), b, Fun({H1, Not(a)}, - FalseElim(b, Absurd(a, H, H1)))))); + // Disj1 : Pi (a b : Bool) (H : a), Or(a, b) + env->add_theorem(disj1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a}}, Or(a, b)), + Fun({{a, Bool}, {b, Bool}, {H, a}}, + Discharge(Not(a), b, Fun({H1, Not(a)}, + FalseElim(b, Absurd(a, H, H1)))))); - // Disj2 : Pi (b a : Bool) (H : b), Or(a, b) - env->add_theorem(disj2_fn_name, Pi({{b, Bool}, {a, Bool}, {H, b}}, Or(a, b)), - Fun({{b, Bool}, {a, Bool}, {H, b}}, - Discharge(Not(a), b, Fun({H1, Not(a)}, H)))); + // Disj2 : Pi (b a : Bool) (H : b), Or(a, b) + env->add_theorem(disj2_fn_name, Pi({{b, Bool}, {a, Bool}, {H, b}}, Or(a, b)), + Fun({{b, Bool}, {a, Bool}, {H, b}}, + Discharge(Not(a), b, Fun({H1, Not(a)}, H)))); - // DisjCases : Pi (a b c: Bool) (H1 : Or(a, b)) (H2 : a -> c) (H3 : b -> c), c */ - env->add_theorem(disj_cases_fn_name, Pi({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, c), - Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, - EqMP(Not(Not(c)), c, DoubleNeg(c), - Discharge(Not(c), False, - Fun({H, Not(c)}, - Absurd(c, - MP(b, c, Discharge(b, c, H3), - MP(Not(a), b, H1, - // Not(a) - MT(a, c, Discharge(a, c, H2), H))), - H)))))); + // DisjCases : Pi (a b c: Bool) (H1 : Or(a, b)) (H2 : a -> c) (H3 : b -> c), c */ + env->add_theorem(disj_cases_fn_name, Pi({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, c), + Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, + EqMP(Not(Not(c)), c, DoubleNeg(c), + Discharge(Not(c), False, + Fun({H, Not(c)}, + Absurd(c, + MP(b, c, Discharge(b, c, H3), + MP(Not(a), b, H1, + // Not(a) + MT(a, c, Discharge(a, c, H2), H))), + H)))))); - // Refute : Pi {a : Bool} (H : not a -> false), a */ - env->add_theorem(refute_fn_name, Pi({{a, Bool}, {H, Not(a) >> False}}, a), - Fun({{a, Bool}, {H, Not(a) >> False}}, - DisjCases(a, Not(a), a, EM(a), Fun({H1, a}, H1), Fun({H1, Not(a)}, FalseElim(a, H(H1)))))); + // Refute : Pi {a : Bool} (H : not a -> false), a */ + env->add_theorem(refute_fn_name, Pi({{a, Bool}, {H, Not(a) >> False}}, a), + Fun({{a, Bool}, {H, Not(a) >> False}}, + DisjCases(a, Not(a), a, EM(a), Fun({H1, a}, H1), Fun({H1, Not(a)}, FalseElim(a, H(H1)))))); - // Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a - env->add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)), - Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, - Subst(A, a, b, Fun({x, A}, Eq(x, a)), Refl(A, a), H))); + // Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a + env->add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)), + Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, + Subst(A, a, b, Fun({x, A}, Eq(x, a)), Refl(A, a), H))); - // Trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c - env->add_theorem(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)), - Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, - Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2))); + // Trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c + env->add_theorem(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)), + Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, + Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2))); - // EqTElim : Pi (a : Bool) (H : a = True), a - env->add_theorem(eqt_elim_fn_name, Pi({{a, Bool}, {H, Eq(a, True)}}, a), - Fun({{a, Bool}, {H, Eq(a, True)}}, - EqMP(True, a, Symm(Bool, a, True, H), Trivial))); + // EqTElim : Pi (a : Bool) (H : a = True), a + env->add_theorem(eqt_elim_fn_name, Pi({{a, Bool}, {H, Eq(a, True)}}, a), + Fun({{a, Bool}, {H, Eq(a, True)}}, + EqMP(True, a, Symm(Bool, a, True, H), Trivial))); - // EqTIntro : Pi (a : Bool) (H : a), a = True - env->add_theorem(eqt_intro_fn_name, Pi({{a, Bool}, {H, a}}, Eq(a, True)), - Fun({{a, Bool}, {H, a}}, - ImpAntisym(a, True, - Discharge(a, True, Fun({H1, a}, Trivial)), - Discharge(True, a, Fun({H2, True}, H))))); + // EqTIntro : Pi (a : Bool) (H : a), a = True + env->add_theorem(eqt_intro_fn_name, Pi({{a, Bool}, {H, a}}, Eq(a, True)), + Fun({{a, Bool}, {H, a}}, + ImpAntisym(a, True, + Discharge(a, True, Fun({H1, a}, Trivial)), + Discharge(True, a, Fun({H2, True}, H))))); - env->add_theorem(name("OrIdempotent"), Pi({a, Bool}, Eq(Or(a, a), a)), - Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Or(x, x), x)), Trivial, Trivial, a))); + env->add_theorem(name("OrIdempotent"), Pi({a, Bool}, Eq(Or(a, a), a)), + Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Or(x, x), x)), Trivial, Trivial, a))); - env->add_theorem(name("OrComm"), Pi({{a, Bool}, {b, Bool}}, Eq(Or(a, b), Or(b, a))), - Fun({{a, Bool}, {b, Bool}}, - Case(Fun({x, Bool}, Eq(Or(x, b), Or(b, x))), - Case(Fun({y, Bool}, Eq(Or(True, y), Or(y, True))), Trivial, Trivial, b), - Case(Fun({y, Bool}, Eq(Or(False, y), Or(y, False))), Trivial, Trivial, b), - a))); + env->add_theorem(name("OrComm"), Pi({{a, Bool}, {b, Bool}}, Eq(Or(a, b), Or(b, a))), + Fun({{a, Bool}, {b, Bool}}, + Case(Fun({x, Bool}, Eq(Or(x, b), Or(b, x))), + Case(Fun({y, Bool}, Eq(Or(True, y), Or(y, True))), Trivial, Trivial, b), + Case(Fun({y, Bool}, Eq(Or(False, y), Or(y, False))), Trivial, Trivial, b), + a))); - env->add_theorem(name("OrAssoc"), Pi({{a, Bool}, {b, Bool}, {c, Bool}}, Eq(Or(Or(a, b), c), Or(a, Or(b, c)))), - Fun({{a, Bool}, {b, Bool}, {c, Bool}}, - Case(Fun({x, Bool}, Eq(Or(Or(x, b), c), Or(x, Or(b, c)))), - Case(Fun({y, Bool}, Eq(Or(Or(True, y), c), Or(True, Or(y, c)))), - Case(Fun({z, Bool}, Eq(Or(Or(True, True), z), Or(True, Or(True, z)))), Trivial, Trivial, c), - Case(Fun({z, Bool}, Eq(Or(Or(True, False), z), Or(True, Or(False, z)))), Trivial, Trivial, c), b), - Case(Fun({y, Bool}, Eq(Or(Or(False, y), c), Or(False, Or(y, c)))), - Case(Fun({z, Bool}, Eq(Or(Or(False, True), z), Or(False, Or(True, z)))), Trivial, Trivial, c), - Case(Fun({z, Bool}, Eq(Or(Or(False, False), z), Or(False, Or(False, z)))), Trivial, Trivial, c), b), a))); + env->add_theorem(name("OrAssoc"), Pi({{a, Bool}, {b, Bool}, {c, Bool}}, Eq(Or(Or(a, b), c), Or(a, Or(b, c)))), + Fun({{a, Bool}, {b, Bool}, {c, Bool}}, + Case(Fun({x, Bool}, Eq(Or(Or(x, b), c), Or(x, Or(b, c)))), + Case(Fun({y, Bool}, Eq(Or(Or(True, y), c), Or(True, Or(y, c)))), + Case(Fun({z, Bool}, Eq(Or(Or(True, True), z), Or(True, Or(True, z)))), Trivial, Trivial, c), + Case(Fun({z, Bool}, Eq(Or(Or(True, False), z), Or(True, Or(False, z)))), Trivial, Trivial, c), b), + Case(Fun({y, Bool}, Eq(Or(Or(False, y), c), Or(False, Or(y, c)))), + Case(Fun({z, Bool}, Eq(Or(Or(False, True), z), Or(False, Or(True, z)))), Trivial, Trivial, c), + Case(Fun({z, Bool}, Eq(Or(Or(False, False), z), Or(False, Or(False, z)))), Trivial, Trivial, c), b), a))); - // Congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi (x : A) B x) (a : A) (H : f = g), f a = g a - env->add_theorem(congr1_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, Eq(f(a), g(a))), - Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, - Subst(piABx, f, g, Fun({h, piABx}, Eq(f(a), h(a))), Refl(B(a), f(a)), H))); + // Congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi (x : A) B x) (a : A) (H : f = g), f a = g a + env->add_theorem(congr1_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, Eq(f(a), g(a))), + Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, + Subst(piABx, f, g, Fun({h, piABx}, Eq(f(a), h(a))), Refl(B(a), f(a)), H))); - // Congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b - env->add_theorem(congr2_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}}, Eq(f(a), f(b))), - Fun({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}}, - Subst(A, a, b, Fun({x, A}, Eq(f(a), f(x))), Refl(B(a), f(a)), H))); + // Congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b + env->add_theorem(congr2_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}}, Eq(f(a), f(b))), + Fun({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}}, + Subst(A, a, b, Fun({x, A}, Eq(f(a), f(x))), Refl(B(a), f(a)), H))); - // Congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b - env->add_theorem(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))), - Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, - HTrans(B(a), B(b), B(b), f(a), f(b), g(b), - Congr2(A, B, a, b, f, H2), Congr1(A, B, f, g, b, H1)))); + // Congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b + env->add_theorem(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))), + Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, + HTrans(B(a), B(b), B(b), f(a), f(b), g(b), + Congr2(A, B, a, b, f, H2), Congr1(A, B, f, g, b, H1)))); - // ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a - env->add_theorem(forall_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)), - Fun({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, - EqTElim(P(a), Congr1(A, Fun({x, A}, Bool), P, Fun({x, A}, True), a, H)))); + // ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a + env->add_theorem(forall_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)), + Fun({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, + EqTElim(P(a), Congr1(A, Fun({x, A}, Bool), P, Fun({x, A}, True), a, H)))); - // ForallIntro : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P) - env->add_theorem(forall_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P)), - Fun({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, - Trans(A_pred, P, Fun({x, A}, P(x)), Fun({x, A}, True), - Symm(A_pred, Fun({x, A}, P(x)), P, Eta(A, Fun({x, A}, Bool), P)), // P == fun x : A, P x - Abst(A, Fun({x, A}, Bool), Fun({x, A}, P(x)), Fun({x, A}, True), Fun({x, A}, EqTIntro(P(x), H(x))))))); + // ForallIntro : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P) + env->add_theorem(forall_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P)), + Fun({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, + Trans(A_pred, P, Fun({x, A}, P(x)), Fun({x, A}, True), + Symm(A_pred, Fun({x, A}, P(x)), P, Eta(A, Fun({x, A}, Bool), P)), // P == fun x : A, P x + Abst(A, Fun({x, A}, Bool), Fun({x, A}, P(x)), Fun({x, A}, True), Fun({x, A}, EqTIntro(P(x), H(x))))))); - // ExistsElim : Pi (A : Type U) (P : A -> Bool) (B : Bool) (H1 : exists x : A, P x) (H2 : Pi (a : A) (H : P a), B) : B := - env->add_theorem(exists_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}}, B), - Fun({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}}, - Refute(B, Fun({R, Not(B)}, - Absurd(mk_forall(A, Fun({x, A}, Not(P(x)))), - ForallIntro(A, Fun({x, A}, Not(P(x))), Fun({a, A}, MT(P(a), B, Discharge(P(a), B, Fun({H, P(a)}, H2(a, H))), R))), - H1))))); + // ExistsElim : Pi (A : Type U) (P : A -> Bool) (B : Bool) (H1 : exists x : A, P x) (H2 : Pi (a : A) (H : P a), B) : B := + env->add_theorem(exists_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}}, B), + Fun({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}}, + Refute(B, Fun({R, Not(B)}, + Absurd(mk_forall(A, Fun({x, A}, Not(P(x)))), + ForallIntro(A, Fun({x, A}, Not(P(x))), Fun({a, A}, MT(P(a), B, Discharge(P(a), B, Fun({H, P(a)}, H2(a, H))), R))), + H1))))); - // ExistsIntro : Pi (A : Type u) (P : A -> bool) (a : A) (H : P a), exists A P - env->add_theorem(exists_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}}, mk_exists(A, P)), - Fun({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}}, - Discharge(mk_forall(A, Fun({x, A}, Not(P(x)))), False, - Fun({H2, mk_forall(A, Fun({x, A}, Not(P(x))))}, - Absurd(P(a), H, ForallElim(A, Fun({x, A}, Not(P(x))), H2, a)))))); + // ExistsIntro : Pi (A : Type u) (P : A -> bool) (a : A) (H : P a), exists A P + env->add_theorem(exists_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}}, mk_exists(A, P)), + Fun({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}}, + Discharge(mk_forall(A, Fun({x, A}, Not(P(x)))), False, + Fun({H2, mk_forall(A, Fun({x, A}, Not(P(x))))}, + Absurd(P(a), H, ForallElim(A, Fun({x, A}, Not(P(x))), H2, a)))))); + }); } } diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index a520acd77..38a17ad01 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -7,8 +7,6 @@ add_custom_target(githash DEPENDS ${LEAN_BINARY_DIR}/githash.h ${LEAN_SOURCE_DIR}/../.git/HEAD ${LEAN_SOURCE_DIR}/../.git/index ) -configure_file("${LEAN_SOURCE_DIR}/shell/version.h.in" "${LEAN_BINARY_DIR}/version.h") -include_directories("${LEAN_BINARY_DIR}") add_executable(lean lean.cpp) add_dependencies(lean githash) target_link_libraries(lean ${EXTRA_LIBS}) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 93b708d90..819231c73 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -36,7 +36,7 @@ using lean::notify_assertion_violation; using lean::environment; using lean::io_state; -enum class input_kind { Unspecified, Lean, Lua }; +enum class input_kind { Unspecified, Lean, OLean, Lua }; static void on_ctrl_c(int ) { lean::request_interrupt(); @@ -51,12 +51,15 @@ static void display_help(std::ostream & out) { std::cout << "Input format:\n"; std::cout << " --lean use parser for Lean default input format for files,\n"; std::cout << " with unknown extension (default)\n"; + std::cout << " --olean use parser for Lean binary input format for files\n"; + std::cout << " with unknown extension\n"; std::cout << " --lua use Lua parser for files with unknown extension\n"; std::cout << "Miscellaneous:\n"; std::cout << " --help -h display this message\n"; std::cout << " --version -v display version number\n"; std::cout << " --githash display the git commit hash number used to build this binary\n"; std::cout << " --path display the path used for finding Lean libraries and extensions\n"; + std::cout << " --output=file -o save the final environment in binary format in the given file\n"; std::cout << " --luahook=num -c how often the Lua interpreter checks the interrupted flag,\n"; std::cout << " it is useful for interrupting non-terminating user scripts,\n"; std::cout << " 0 means 'do not check'.\n"; @@ -83,10 +86,12 @@ static struct option g_long_options[] = { {"version", no_argument, 0, 'v'}, {"help", no_argument, 0, 'h'}, {"lean", no_argument, 0, 'l'}, + {"olean", no_argument, 0, 'b'}, {"lua", no_argument, 0, 'u'}, {"path", no_argument, 0, 'p'}, {"luahook", required_argument, 0, 'c'}, {"githash", no_argument, 0, 'g'}, + {"output", required_argument, 0, 'o'}, #if defined(LEAN_USE_BOOST) {"tstack", required_argument, 0, 's'}, #endif @@ -96,9 +101,11 @@ static struct option g_long_options[] = { int main(int argc, char ** argv) { lean::save_stack_info(); lean::register_modules(); + bool export_objects = false; + std::string output; input_kind default_k = input_kind::Lean; // default while (true) { - int c = getopt_long(argc, argv, "lupgvhc:012s:012", g_long_options, NULL); + int c = getopt_long(argc, argv, "lupgvhc:012s:012o:", g_long_options, NULL); if (c == -1) break; // end of command line switch (c) { @@ -117,6 +124,9 @@ int main(int argc, char ** argv) { case 'u': default_k = input_kind::Lua; break; + case 'b': + default_k = input_kind::OLean; + break; case 'c': script_state::set_check_interrupt_freq(atoi(optarg)); break; @@ -126,6 +136,10 @@ int main(int argc, char ** argv) { case 's': lean::set_thread_stack_size(atoi(optarg)*1024); break; + case 'o': + output = optarg; + export_objects = true; + break; default: std::cerr << "Unknown command line option\n"; display_help(std::cerr); @@ -146,7 +160,10 @@ int main(int argc, char ** argv) { init_frontend(env, ios); script_state S; shell sh(env, &S); - return sh() ? 0 : 1; + int status = sh() ? 0 : 1; + if (export_objects) + env->export_objects(output); + return status; } else { lean_assert(default_k == input_kind::Lua); script_state S; @@ -164,6 +181,8 @@ int main(int argc, char ** argv) { if (ext) { if (strcmp(ext, "lean") == 0) { k = input_kind::Lean; + } else if (strcmp(ext, "olean") == 0) { + k = input_kind::OLean; } else if (strcmp(ext, "lua") == 0) { k = input_kind::Lua; } @@ -176,6 +195,13 @@ int main(int argc, char ** argv) { } if (!parse_commands(env, ios, in, &S, false, false)) ok = false; + } else if (k == input_kind::OLean) { + try { + env->import(std::string(argv[i]), ios); + } catch (lean::exception & ex) { + std::cerr << "Failed to load binary file '" << argv[i] << "': " << ex.what() << "\n"; + ok = false; + } } else if (k == input_kind::Lua) { try { S.dofile(argv[i]); @@ -187,6 +213,8 @@ int main(int argc, char ** argv) { lean_unreachable(); // LCOV_EXCL_LINE } } + if (export_objects) + env->export_objects(output); return ok ? 0 : 1; } } diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index 15346eccc..0fd7c0ad5 100644 --- a/src/util/lean_path.cpp +++ b/src/util/lean_path.cpp @@ -155,7 +155,7 @@ std::string name_to_file(name const & fname) { return fname.to_string(g_sep_str.c_str()); } -std::string find_file(std::string fname) { +std::string find_file(std::string fname, std::initializer_list const & extensions) { bool is_known = is_known_file_ext(fname); fname = normalize_path(fname); for (auto path : g_lean_path_vector) { @@ -163,7 +163,7 @@ std::string find_file(std::string fname) { if (auto r = check_file(path, fname)) return *r; } else { - for (auto ext : { ".olean", ".lean", ".lua" }) { + for (auto ext : extensions) { if (auto r = check_file(path, fname, ext)) return *r; } @@ -172,6 +172,10 @@ std::string find_file(std::string fname) { throw exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH"); } +std::string find_file(std::string fname) { + return find_file(fname, {".olean", ".lean", ".lua"}); +} + char const * get_lean_path() { return g_lean_path.c_str(); } diff --git a/src/util/lean_path.h b/src/util/lean_path.h index 786cf301e..81caef57e 100644 --- a/src/util/lean_path.h +++ b/src/util/lean_path.h @@ -18,6 +18,9 @@ char const * get_lean_path(); */ std::string find_file(std::string fname); +std::string find_file(std::string fname, std::initializer_list const & exts); + + /** \brief Return true iff fname ends with ".lean" */ bool is_lean_file(std::string const & fname); /** \brief Return true iff fname ends with ".olean" */ diff --git a/src/shell/version.h.in b/src/version.h.in similarity index 100% rename from src/shell/version.h.in rename to src/version.h.in