michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/tactic/expr_to_tactic): remove 'by_plus' support

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-29 13:50:05 -08:00
parent fbe5188480
commit f54963bc3e
7 changed files with 3 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/frontends/lean/elaborator.cpp
View file

@ -374,8 +374,6 @@ expr elaborator::visit_expecting_type_of(expr const & e, expr const & t, constra
return visit_choice(e, some_expr(t), cs);
} else if (is_by(e)) {
return visit_by(e, some_expr(t), cs);
} else if (is_by_plus(e)) {
return visit_by_plus(e, some_expr(t), cs);
} else if (is_calc_annotation(e)) {
return visit_calc_proof(e, some_expr(t), cs);
} else {
@ -427,15 +425,6 @@ expr elaborator::visit_by(expr const & e, optional<expr> const & t, constraint_s
return m;
}
expr elaborator::visit_by_plus(expr const & e, optional<expr> const & t, constraint_seq & cs) {
lean_assert(is_by_plus(e));
expr tac = visit(get_by_plus_arg(e), cs);
expr m = m_context.mk_meta(t, e.get_tag());
register_meta(m);
m_local_tactic_hints.insert(mlocal_name(get_app_fn(m)), tac);
return m;
}
expr elaborator::visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs) {
lean_assert(is_calc_annotation(e));
info_manager * im = nullptr;
@ -1715,8 +1704,6 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) {
return visit_let_value(e, cs);
} else if (is_by(e)) {
return visit_by(e, none_expr(), cs);
} else if (is_by_plus(e)) {
return visit_by_plus(e, none_expr(), cs);
} else if (is_calc_annotation(e)) {
return visit_calc_proof(e, none_expr(), cs);
} else if (is_no_info(e)) {
@ -2404,7 +2391,7 @@ static expr translate_local_name(environment const & env,
*/
static expr translate(environment const & env, list<expr> const & ctx, expr const & e) {
auto fn = [&](expr const & e) {
if (is_placeholder(e) || is_by(e) || is_by_plus(e)) {
if (is_placeholder(e) || is_by(e)) {
return some_expr(e); // ignore placeholders
} else if (is_constant(e)) {
expr new_e = copy_tag(e, translate_local_name(env, ctx, const_name(e), e));

1
src/frontends/lean/elaborator.h
View file

@ -116,7 +116,6 @@ class elaborator : public coercion_info_manager {
expr visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs);
expr visit_choice(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_by(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_by_plus(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr add_implict_args(expr e, constraint_seq & cs);
pair<expr, expr> ensure_fun(expr f, constraint_seq & cs);

2
src/frontends/lean/parse_table.cpp
View file

@ -25,7 +25,7 @@ namespace notation {
3- Every other subterm is annotated with no_info.
*/
static expr annotate_macro_subterms(expr const & e, bool root = true) {
if (is_var(e) || is_no_info(e) || is_by(e) || is_by_plus(e))
if (is_var(e) || is_no_info(e) || is_by(e))
return e;
if (is_binding(e))
return update_binding(e,

8
src/frontends/lean/parser.cpp
View file

@ -300,12 +300,6 @@ expr parser::mk_by(expr const & t, pos_info const & pos) {
return save_pos(::lean::mk_by(t), pos);
}
expr parser::mk_by_plus(expr const & t, pos_info const & pos) {
if (!has_tactic_decls())
throw parser_error("invalid 'by+' expression, tactic module has not been imported", pos);
return save_pos(::lean::mk_by_plus(t), pos);
}
void parser::updt_options() {
m_verbose = get_verbose(m_ios.get_options());
m_show_errors = get_parser_show_errors(m_ios.get_options());
@ -1683,7 +1677,7 @@ expr parser::parse_backtick_expr_core() {
expr parser::parse_backtick_expr() {
auto p = pos();
expr type = parse_backtick_expr_core();
expr assump = mk_by_plus(save_pos(mk_constant(get_tactic_assumption_name()), p), p);
expr assump = mk_by(save_pos(mk_constant(get_tactic_assumption_name()), p), p);
return save_pos(mk_typed_expr(type, assump), p);
}

1
src/frontends/lean/parser.h
View file

@ -296,7 +296,6 @@ public:
bool has_tactic_decls();
expr mk_by(expr const & t, pos_info const & pos);
expr mk_by_plus(expr const & t, pos_info const & pos);
bool keep_new_thms() const { return m_keep_theorem_mode != keep_theorem_mode::DiscardAll; }

9
src/library/tactic/expr_to_tactic.cpp
View file

@ -348,23 +348,15 @@ void register_num_tac(name const & n, std::function<tactic(unsigned k)> f) {
}
static name * g_by_name = nullptr;
static name * g_by_plus_name = nullptr;
expr mk_by(expr const & e) { return mk_annotation(*g_by_name, e); }
bool is_by(expr const & e) { return is_annotation(e, *g_by_name); }
expr const & get_by_arg(expr const & e) { lean_assert(is_by(e)); return get_annotation_arg(e); }
expr mk_by_plus(expr const & e) { return mk_annotation(*g_by_plus_name, e); }
bool is_by_plus(expr const & e) { return is_annotation(e, *g_by_plus_name); }
expr const & get_by_plus_arg(expr const & e) { lean_assert(is_by_plus(e)); return get_annotation_arg(e); }
void initialize_expr_to_tactic() {
g_by_name = new name("by");
register_annotation(*g_by_name);
g_by_plus_name = new name("by+");
register_annotation(*g_by_plus_name);
g_map = new expr_to_tactic_map();
g_tactic_expr_type = new expr(mk_constant(get_tactic_expr_name()));
@ -457,6 +449,5 @@ void finalize_expr_to_tactic() {
delete g_map;
delete g_tactic_opcode;
delete g_by_name;
delete g_by_plus_name;
}
}

5
src/library/tactic/expr_to_tactic.h
View file

@ -67,11 +67,6 @@ bool is_by(expr const & t);
/** \see mk_by */
expr const & get_by_arg(expr const & t);
// Similar to mk_by, but instructs the elaborator to include the whole context
expr mk_by_plus(expr const & t);
bool is_by_plus(expr const & t);
expr const & get_by_plus_arg(expr const & t);
expr const & get_tactic_type();
expr const & get_and_then_tac_fn();
expr const & get_or_else_tac_fn();