From 90d920b7c97d7c0fc5438c05cfb079c887d7f3ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Jul 2016 01:57:43 +0100 Subject: [PATCH] chore(frontends/lean,library/explicit): remove dead code --- src/frontends/lean/builtin_exprs.cpp | 12 ------------ src/frontends/lean/old_elaborator.cpp | 8 +------- src/frontends/lean/pp.cpp | 5 +---- src/library/explicit.cpp | 8 -------- src/library/explicit.h | 10 ---------- src/library/head_map.cpp | 2 -- 6 files changed, 2 insertions(+), 43 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 056c5beca7..8341334b44 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -476,18 +476,6 @@ static expr parse_partial_explicit_expr(parser & p, unsigned, expr const *, pos_ } } -static expr parse_consume_args_expr(parser & p, unsigned, expr const *, pos_info const & pos) { - expr e = p.parse_expr(get_Max_prec()); - if (is_choice(e)) { - buffer new_choices; - for (unsigned i = 0; i < get_num_choices(e); i++) - new_choices.push_back(p.save_pos(mk_consume_args(get_choice(e, i)), pos)); - return p.save_pos(mk_choice(new_choices.size(), new_choices.data()), pos); - } else { - return p.save_pos(mk_consume_args(e), pos); - } -} - static expr parse_sorry(parser & p, unsigned, expr const *, pos_info const & pos) { return p.mk_sorry(pos); } diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp index 9c04eb148f..6fad4b64b2 100644 --- a/src/frontends/lean/old_elaborator.cpp +++ b/src/frontends/lean/old_elaborator.cpp @@ -220,7 +220,7 @@ void old_elaborator::save_type_data(expr const & e, expr const & r) { // std::cout << ">> infom: " << infom() << ", pip: " << pip() << "\n"; if (!m_no_info && infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e) || is_as_atomic(e) || - is_consume_args(e) || is_notation_info(e))) { + is_notation_info(e))) { if (auto p = pip()->get_pos_info(e)) { expr t = m_tc->infer(r).first; m_pre_info_data.add_type_info(p->first, p->second, t); @@ -1720,9 +1720,6 @@ expr old_elaborator::visit_core(expr const & e, constraint_seq & cs) { } else if (is_as_atomic(e)) { // ignore annotation return visit_core(get_as_atomic_arg(e), cs); - } else if (is_consume_args(e)) { - // ignore annotation - return visit_core(get_consume_args_arg(e), cs); } else if (is_explicit_or_partial_explicit(e)) { // ignore annotation return visit_core(get_explicit_or_partial_explicit_arg(e), cs); @@ -1818,9 +1815,6 @@ pair old_elaborator::visit(expr const & e) { r = get_as_atomic_arg(e); if (is_explicit_or_partial_explicit(r)) r = get_explicit_or_partial_explicit_arg(r); r = visit_core(r, cs); - } else if (is_consume_args(e)) { - consume_args = true; - r = visit_core(get_consume_args_arg(e), cs); } else { r = visit_core(e, cs); } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index ac92c96f9b..e6013a294d 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1079,9 +1079,6 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer> & a } else if (is_app(e)) { buffer p_args, e_args; expr p_fn = get_app_args(p, p_args); - bool consume = is_consume_args(p_fn); - if (consume) - p_fn = get_consume_args_arg(p_fn); expr e_fn = get_app_args(e, e_args); if (!match(p_fn, e_fn, args)) return false; @@ -1103,7 +1100,7 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer> & a return false; expr const & body = binding_body(fn_type); binder_info const & info = binding_info(fn_type); - if ((!consume || closed(body)) && is_explicit(info)) { + if ((closed(body)) && is_explicit(info)) { if (j >= p_args.size()) return false; if (!match(p_args[j], e_args[i], args)) diff --git a/src/library/explicit.cpp b/src/library/explicit.cpp index 5cc4c013bd..9dcc67f3b3 100644 --- a/src/library/explicit.cpp +++ b/src/library/explicit.cpp @@ -13,7 +13,6 @@ static name * g_explicit_name = nullptr; static name * g_partial_explicit_name = nullptr; static name * g_as_atomic_name = nullptr; static name * g_as_is_name = nullptr; -static name * g_consume_args_name = nullptr; expr mk_explicit(expr const & e) { return mk_annotation(*g_explicit_name, e); } bool is_explicit(expr const & e) { return is_annotation(e, *g_explicit_name); } @@ -36,22 +35,16 @@ expr mk_as_atomic(expr const & e) { return mk_annotation(*g_as_atomic_name, e); bool is_as_atomic(expr const & e) { return is_annotation(e, *g_as_atomic_name); } expr const & get_as_atomic_arg(expr const & e) { lean_assert(is_as_atomic(e)); return get_annotation_arg(e); } -expr mk_consume_args(expr const & e) { return mk_annotation(*g_consume_args_name, e); } -bool is_consume_args(expr const & e) { return is_annotation(e, *g_consume_args_name); } -expr const & get_consume_args_arg(expr const & e) { lean_assert(is_consume_args(e)); return get_annotation_arg(e); } - void initialize_explicit() { g_explicit_name = new name("@@"); g_partial_explicit_name = new name("@"); g_as_atomic_name = new name("as_atomic"); g_as_is_name = new name("as_is"); - g_consume_args_name = new name("!"); register_annotation(*g_explicit_name); register_annotation(*g_partial_explicit_name); register_annotation(*g_as_atomic_name); register_annotation(*g_as_is_name); - register_annotation(*g_consume_args_name); } void finalize_explicit() { @@ -59,6 +52,5 @@ void finalize_explicit() { delete g_as_atomic_name; delete g_partial_explicit_name; delete g_explicit_name; - delete g_consume_args_name; } } diff --git a/src/library/explicit.h b/src/library/explicit.h index b112bc5713..4720cd2996 100644 --- a/src/library/explicit.h +++ b/src/library/explicit.h @@ -59,16 +59,6 @@ bool is_as_atomic(expr const & e); */ expr const & get_as_atomic_arg(expr const & e); -/** \brief Create the expression '! e'. - This only affects the elaborator behavior. - It instructs the elaborator to keep adding '_' - for \c e arguments. -*/ -expr mk_consume_args(expr const & e); -/** \brief Return true iff \c e is an '!f' expression. */ -bool is_consume_args(expr const & e); -expr const & get_consume_args_arg(expr const & e); - void initialize_explicit(); void finalize_explicit(); } diff --git a/src/library/head_map.cpp b/src/library/head_map.cpp index 8a785f89a7..dac3500b35 100644 --- a/src/library/head_map.cpp +++ b/src/library/head_map.cpp @@ -15,8 +15,6 @@ head_index::head_index(expr const & e) { f = get_app_fn(get_as_atomic_arg(f)); else if (is_explicit(f)) f = get_explicit_arg(f); - else if (is_consume_args(f)) - f = get_consume_args_arg(f); else break; }