From 3729c7ffb2edd6e9a5769be8e89dc051f4e298d0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Jun 2018 12:52:04 -0700 Subject: [PATCH] chore(kernel/expr): remove some old/legacy functions --- src/frontends/lean/builtin_exprs.cpp | 6 +++--- src/frontends/lean/notation_cmd.cpp | 8 ++++---- src/frontends/lean/user_notation.cpp | 2 +- src/kernel/expr.h | 4 ---- src/kernel/old_type_checker.cpp | 4 ++-- src/kernel/type_checker.cpp | 4 ++-- src/library/string.cpp | 16 ++++++++-------- src/library/type_context.cpp | 2 +- src/tests/kernel/max_sharing.cpp | 28 ++++++++++++++-------------- src/tests/library/deep_copy.cpp | 10 +++++----- src/tests/library/expr_lt.cpp | 28 ++++++++++++++-------------- src/tests/library/head_map.cpp | 8 ++++---- src/tests/library/occurs.cpp | 8 ++++---- 13 files changed, 62 insertions(+), 66 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 1607945f8a..df04a3c930 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -439,7 +439,7 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) expr prop = p.parse_expr(); p.check_token_next(get_comma_tk(), "invalid 'show' declaration, ',' expected"); expr proof = parse_proof(p); - expr b = p.save_pos(mk_lambda(get_this_tk(), prop, Var(0)), pos); + expr b = p.save_pos(mk_lambda(get_this_tk(), prop, mk_bvar(0)), pos); expr r = p.mk_app(b, proof, pos); return p.save_pos(mk_show_annotation(r), pos); } @@ -1090,8 +1090,8 @@ static expr parse_field(parser & p, unsigned, expr const * args, pos_info const parse_table init_led_table() { parse_table r(false); - r = r.add({transition("->", mk_expr_action(get_arrow_prec()-1))}, mk_arrow(Var(1), Var(1))); - r = r.add({transition("^.", mk_ext_action(parse_field))}, Var(0)); + r = r.add({transition("->", mk_expr_action(get_arrow_prec()-1))}, mk_arrow(mk_bvar(1), mk_bvar(1))); + r = r.add({transition("^.", mk_ext_action(parse_field))}, mk_bvar(0)); return r; } diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 381f1cc7a1..03bccdc10c 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -237,16 +237,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota #pragma GCC diagnostic ignored "-Wmaybe-uninitialized" #endif return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec), pp_tk)), - mk_app(f, Var(1), Var(0)), overload, priority, grp, parse_only), new_token); + mk_app(f, mk_bvar(1), mk_bvar(0)), overload, priority, grp, parse_only), new_token); case mixfix_kind::infixr: return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec), pp_tk)), - mk_app(f, Var(1), Var(0)), overload, priority, grp, parse_only), new_token); + mk_app(f, mk_bvar(1), mk_bvar(0)), overload, priority, grp, parse_only), new_token); case mixfix_kind::postfix: return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action(), pp_tk)), - mk_app(f, Var(0)), overload, priority, grp, parse_only), new_token); + mk_app(f, mk_bvar(0)), overload, priority, grp, parse_only), new_token); case mixfix_kind::prefix: return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec), pp_tk)), - mk_app(f, Var(0)), overload, priority, grp, parse_only), new_token); + mk_app(f, mk_bvar(0)), overload, priority, grp, parse_only), new_token); } } lean_unreachable(); // LCOV_EXCL_LINE diff --git a/src/frontends/lean/user_notation.cpp b/src/frontends/lean/user_notation.cpp index 73ced00bdf..a2228c07ba 100644 --- a/src/frontends/lean/user_notation.cpp +++ b/src/frontends/lean/user_notation.cpp @@ -83,7 +83,7 @@ static environment add_user_notation(environment const & env, name const & d, un throw formatted_exception(some(pos), ex.pp()); } } - }))}, Var(0), /* overload */ persistent, prio, notation_entry_group::Main, /* parse_only */ true), persist); + }))}, mk_bvar(0), /* overload */ persistent, prio, notation_entry_group::Main, /* parse_only */ true), persist); } struct user_notation_modification : public modification { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index b25d5283e9..e9320dc11a 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -334,15 +334,11 @@ inline expr mk_metavar(name const & n, expr const & t) { return mk_metavar(n, n, expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi); inline expr mk_local(name const & n, expr const & t) { return mk_local(n, n, t, mk_binder_info()); } inline expr mk_local(name const & n, expr const & t, binder_info bi) { return mk_local(n, n, t, bi); } -inline expr Local(name const & n, expr const & t, binder_info bi = mk_binder_info()) { return mk_local(n, t, bi); } inline name const & mlocal_name(expr const & e) { return static_cast(cnstr_obj_ref(e, 0)); } inline name const & mlocal_pp_name(expr const & e) { return static_cast(cnstr_obj_ref(e, 1)); } inline expr const & mlocal_type(expr const & e) { return static_cast(cnstr_obj_ref(e, 2)); } inline expr mk_constant(name const & n, levels const & ls) { return mk_const(n, ls); } inline expr mk_constant(name const & n) { return mk_constant(n, levels()); } -inline expr Const(name const & n) { return mk_constant(n); } -inline expr BVar(unsigned idx) { return mk_bvar(idx); } -inline expr Var(unsigned idx) { return mk_bvar(idx); } inline bool is_constant(expr const & e) { return is_const(e); } expr mk_quote(bool is_reflected, expr const & e); inline expr const & quote_value(expr const & e) { return static_cast(cnstr_obj_ref(e, 0)); } diff --git a/src/kernel/old_type_checker.cpp b/src/kernel/old_type_checker.cpp index 950711bb4f..7e985ce6b3 100644 --- a/src/kernel/old_type_checker.cpp +++ b/src/kernel/old_type_checker.cpp @@ -571,7 +571,7 @@ bool old_type_checker::try_eta_expansion_core(expr const & t, expr const & s) { expr s_type = whnf(infer_type(s)); if (!is_pi(s_type)) return false; - expr new_s = mk_lambda(binding_name(s_type), binding_domain(s_type), mk_app(s, Var(0)), binding_info(s_type)); + expr new_s = mk_lambda(binding_name(s_type), binding_domain(s_type), mk_app(s, mk_bvar(0)), binding_info(s_type)); if (!is_def_eq(t, new_s)) return false; return true; @@ -768,7 +768,7 @@ old_type_checker::~old_type_checker() {} void initialize_old_type_checker() { g_id_delta = new name("id_delta"); - g_dont_care = new expr(Const("dontcare")); + g_dont_care = new expr(mk_const("dontcare")); g_kernel_fresh = new name("_old_kernel_fresh"); register_name_generator_prefix(*g_kernel_fresh); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index f4a25e2e03..1d7a4f052c 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -604,7 +604,7 @@ bool type_checker::try_eta_expansion_core(expr const & t, expr const & s) { expr s_type = whnf(infer_type(s)); if (!is_pi(s_type)) return false; - expr new_s = mk_lambda(binding_name(s_type), binding_domain(s_type), mk_app(s, Var(0)), binding_info(s_type)); + expr new_s = mk_lambda(binding_name(s_type), binding_domain(s_type), mk_app(s, mk_bvar(0)), binding_info(s_type)); if (!is_def_eq(t, new_s)) return false; return true; @@ -891,7 +891,7 @@ certified_declaration certify_unchecked::certify_or_check(environment const & en void initialize_type_checker() { g_id_delta = new name("id_delta"); - g_dont_care = new expr(Const("dontcare")); + g_dont_care = new expr(mk_const("dontcare")); g_kernel_fresh = new name("_kernel_fresh"); register_name_generator_prefix(*g_kernel_fresh); } diff --git a/src/library/string.cpp b/src/library/string.cpp index 72644c92be..b114f06322 100644 --- a/src/library/string.cpp +++ b/src/library/string.cpp @@ -85,14 +85,14 @@ bool is_string_literal(expr const & e) { } void initialize_string() { - g_nat = new expr(Const(get_nat_name())); - g_char = new expr(Const(get_char_name())); - g_char_mk = new expr(Const(get_char_mk_name())); - g_char_of_nat = new expr(Const(get_char_of_nat_name())); - g_string = new expr(Const(get_string_name())); - g_empty = new expr(Const(get_string_empty_name())); - g_str = new expr(Const(get_string_str_name())); - g_fin_mk = new expr(Const(get_fin_mk_name())); + g_nat = new expr(mk_const(get_nat_name())); + g_char = new expr(mk_const(get_char_name())); + g_char_mk = new expr(mk_const(get_char_mk_name())); + g_char_of_nat = new expr(mk_const(get_char_of_nat_name())); + g_string = new expr(mk_const(get_string_name())); + g_empty = new expr(mk_const(get_string_empty_name())); + g_str = new expr(mk_const(get_string_str_name())); + g_fin_mk = new expr(mk_const(get_fin_mk_name())); } optional expand_string_literal(expr const & e) { diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 59ab891b5f..4dbc1ff21a 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -2562,7 +2562,7 @@ bool type_context_old::is_def_eq_eta(expr const & e1, expr const & e2) { // e2_type may not be a Pi because it is a stuck term. // We are ignoring this case and just failing. expr new_e2 = ::lean::mk_lambda(binding_name(e2_type), binding_domain(e2_type), - mk_app(e2, Var(0)), binding_info(e2_type)); + mk_app(e2, mk_bvar(0)), binding_info(e2_type)); scope s(*this); if (is_def_eq_core(e1, new_e2) && process_postponed(s)) { s.commit(); diff --git a/src/tests/kernel/max_sharing.cpp b/src/tests/kernel/max_sharing.cpp index 2e6eeccaec..cd5440c160 100644 --- a/src/tests/kernel/max_sharing.cpp +++ b/src/tests/kernel/max_sharing.cpp @@ -17,12 +17,12 @@ using namespace lean; static void tst1() { max_sharing_fn max_fn; - expr a1 = Const("a"); - expr a2 = Const("a"); - expr N = Const("N"); - expr x = Local("x", N); - expr y = Local("y", N); - expr f = Const("f"); + expr a1 = mk_const("a"); + expr a2 = mk_const("a"); + expr N = mk_const("N"); + expr x = mk_local("x", N); + expr y = mk_local("y", N); + expr f = mk_const("f"); expr F1, F2; F1 = mk_app(f, Fun(x, mk_app(f, x, x)), Fun(y, mk_app(f, y, y))); lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1))); @@ -35,9 +35,9 @@ static void tst1() { static void tst2() { max_sharing_fn max_fn1; max_sharing_fn max_fn2; - expr x = Const("x"); - expr f = Const("f"); - expr g = Const("g"); + expr x = mk_const("x"); + expr f = mk_const("f"); + expr g = mk_const("g"); expr t1 = max_fn2(max_fn1(mk_app(f, mk_app(g, x)))); expr t2 = max_fn2(mk_app(f, t1, mk_app(g, x))); expr arg1 = app_arg(app_arg(app_fn(t2))); @@ -47,11 +47,11 @@ static void tst2() { static void tst3() { max_sharing_fn max_fn; - expr a1 = Const("a"); - expr a2 = Const("a"); - expr a3 = Const("a"); - expr g = Const("g"); - expr f = Const("f"); + expr a1 = mk_const("a"); + expr a2 = mk_const("a"); + expr a3 = mk_const("a"); + expr g = mk_const("g"); + expr f = mk_const("f"); expr new_a1 = max_fn(a1); lean_assert(is_eqp(new_a1, a1)); expr t1 = max_fn(mk_app(f, a2)); diff --git a/src/tests/library/deep_copy.cpp b/src/tests/library/deep_copy.cpp index c1897ce61a..8e14a46b58 100644 --- a/src/tests/library/deep_copy.cpp +++ b/src/tests/library/deep_copy.cpp @@ -15,14 +15,14 @@ Author: Leonardo de Moura using namespace lean; static void tst1() { - expr f = Const("f"); - expr a = Const("a"); - expr x = Var(0); + expr f = mk_const("f"); + expr a = mk_const("a"); + expr x = mk_bvar(0); expr Type = mk_Type(); expr t = Type; - expr z = Const("z"); + expr z = mk_const("z"); expr m = mk_metavar("a", Type); - expr F = mk_pi("y", t, mk_lambda("x", t, mk_app(f, mk_app(f, mk_app(f, x, a), Const("10")), mk_app(f, x, m)))); + expr F = mk_pi("y", t, mk_lambda("x", t, mk_app(f, mk_app(f, mk_app(f, x, a), mk_const("10")), mk_app(f, x, m)))); expr G = deep_copy(F); lean_assert(F == G); lean_assert(!is_eqp(F, G)); diff --git a/src/tests/library/expr_lt.cpp b/src/tests/library/expr_lt.cpp index e9d8a0ce0b..993fe7ee3d 100644 --- a/src/tests/library/expr_lt.cpp +++ b/src/tests/library/expr_lt.cpp @@ -16,20 +16,20 @@ static void lt(expr const & e1, expr const & e2, bool expected) { } static void tst1() { - lt(Var(0), Var(0), false); - lt(Var(0), Var(1), true); - lt(Const("a"), Const("b"), true); - lt(Const("a"), Const("a"), false); - lt(Var(1), Const("a"), true); - lt(mk_app(Const("f"), Var(0)), mk_app(Const("f"), Var(0), Const("a")), true); - lt(mk_app(Const("f"), Var(0), Const("a"), Const("b")), mk_app(Const("f"), Var(0), Const("a")), false); - lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("g"), Var(0), Const("a")), true); - lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("f"), Var(1), Const("a")), true); - lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("f"), Var(0), Const("b")), true); - lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("f"), Var(0), Const("a")), false); - lt(mk_app(Const("g"), Var(0), Const("a")), mk_app(Const("f"), Var(0), Const("a")), false); - lt(mk_app(Const("f"), Var(1), Const("a")), mk_app(Const("f"), Var(0), Const("a")), false); - lt(mk_app(Const("f"), Var(0), Const("b")), mk_app(Const("f"), Var(0), Const("a")), false); + lt(mk_bvar(0), mk_bvar(0), false); + lt(mk_bvar(0), mk_bvar(1), true); + lt(mk_const("a"), mk_const("b"), true); + lt(mk_const("a"), mk_const("a"), false); + lt(mk_bvar(1), mk_const("a"), true); + lt(mk_app(mk_const("f"), mk_bvar(0)), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), true); + lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("a"), mk_const("b")), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), false); + lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), mk_app(mk_const("g"), mk_bvar(0), mk_const("a")), true); + lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), mk_app(mk_const("f"), mk_bvar(1), mk_const("a")), true); + lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), mk_app(mk_const("f"), mk_bvar(0), mk_const("b")), true); + lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), false); + lt(mk_app(mk_const("g"), mk_bvar(0), mk_const("a")), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), false); + lt(mk_app(mk_const("f"), mk_bvar(1), mk_const("a")), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), false); + lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("b")), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), false); } int main() { diff --git a/src/tests/library/head_map.cpp b/src/tests/library/head_map.cpp index 7852a39cdf..5100854806 100644 --- a/src/tests/library/head_map.cpp +++ b/src/tests/library/head_map.cpp @@ -15,11 +15,11 @@ using namespace lean; static void tst1() { head_map map; - expr a = Const("a"); - expr f = Const("f"); - expr b = Const("b"); + expr a = mk_const("a"); + expr f = mk_const("f"); + expr b = mk_const("b"); expr Prop = mk_Prop(); - expr x = Local("x", Prop); + expr x = mk_local("x", Prop); expr l1 = Fun(x, x); expr l2 = Fun(x, mk_app(f, x)); lean_assert(l1 != l2); diff --git a/src/tests/library/occurs.cpp b/src/tests/library/occurs.cpp index aa65d9c637..d9e22e6c8e 100644 --- a/src/tests/library/occurs.cpp +++ b/src/tests/library/occurs.cpp @@ -14,12 +14,12 @@ Author: Leonardo de Moura using namespace lean; static void tst1() { - expr f = Const("f"); - expr a = Const("a"); - expr b = Const("b"); + expr f = mk_const("f"); + expr a = mk_const("a"); + expr b = mk_const("b"); expr Type = mk_Type(); expr T = Type; - expr a1 = Local("a", T); + expr a1 = mk_local("a", T); lean_assert(occurs(f, f)); lean_assert(!occurs(a, f)); lean_assert(occurs(a, mk_app(f, a)));