max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(frontends/lean,library/explicit): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-02 01:57:43 +01:00
parent 97719a4c5f
commit 90d920b7c9
6 changed files with 2 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/frontends/lean/builtin_exprs.cpp
View file

@ -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<expr> 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);
}

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

@ -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<expr, constraint_seq> 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);
}

5
src/frontends/lean/pp.cpp
View file

@ -1079,9 +1079,6 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
} else if (is_app(e)) {
buffer<expr> 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<optional<expr>> & 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))

8
src/library/explicit.cpp
View file

@ -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;
}
}

10
src/library/explicit.h
View file

@ -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();
}

2
src/library/head_map.cpp
View file

@ -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;
}