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

feat(frontends/lean): nested begin-end blocks

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-24 11:59:27 -08:00
parent 21e972e34a
commit 1ff6446a63
4 changed files with 103 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -143,7 +143,7 @@ static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
return p.mk_by(t, pos);
}
static expr parse_begin_end_core(parser & p, pos_info const & pos) {
static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & end_token, bool nested = false) {
if (!p.has_tactic_decls())
throw parser_error("invalid 'begin-end' expression, tactic module has not been imported", pos);
environment env = open_tactic_namespace(p);
@ -153,7 +153,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
optional<expr> pre_tac = get_begin_end_pre_tactic(env);
buffer<expr> tacs;
bool first = true;
while (!p.curr_is_token(get_end_tk())) {
while (!p.curr_is_token(end_token)) {
if (first) {
first = false;
} else {
@ -164,19 +164,27 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
tacs.push_back(mk_begin_end_element_annotation(info_tac));
}
}
if (p.curr_is_token(get_end_tk()))
if (p.curr_is_token(get_begin_tk())) {
auto pos = p.pos();
tacs.push_back(parse_begin_end_core(p, pos, get_end_tk(), true));
} else if (p.curr_is_token(get_lcurly_tk())) {
auto pos = p.pos();
tacs.push_back(parse_begin_end_core(p, pos, get_rcurly_tk(), true));
} else if (p.curr_is_token(end_token)) {
break;
bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) ||
p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
p.curr_is_token(get_fun_tk()));
auto pos = p.pos();
expr tac = p.parse_expr();
if (use_exact)
tac = p.mk_app(get_exact_tac_fn(), tac, pos);
if (pre_tac)
tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
tac = mk_begin_end_element_annotation(tac);
tacs.push_back(tac);
} else {
bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) ||
p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
p.curr_is_token(get_fun_tk()));
auto pos = p.pos();
expr tac = p.parse_expr();
if (use_exact)
tac = p.mk_app(get_exact_tac_fn(), tac, pos);
if (pre_tac)
tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
tac = mk_begin_end_element_annotation(tac);
tacs.push_back(tac);
}
}
auto end_pos = p.pos();
p.next();
@ -196,11 +204,15 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
for (unsigned i = 1; i < tacs.size(); i++) {
r = p.mk_app({get_and_then_tac_fn(), r, tacs[i]}, end_pos);
}
return p.mk_by(mk_begin_end_annotation(r), end_pos);
r = p.save_pos(mk_begin_end_annotation(r), end_pos);
if (nested)
return r;
else
return p.mk_by(r, end_pos);
}
static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) {
return parse_begin_end_core(p, pos);
return parse_begin_end_core(p, pos, get_end_tk());
}
static expr parse_proof_qed_core(parser & p, pos_info const & pos) {
@ -220,7 +232,7 @@ static expr parse_proof(parser & p, expr const & prop) {
return parse_proof_qed_core(p, pos);
} else if (p.curr_is_token(get_begin_tk())) {
auto pos = p.pos();
return parse_begin_end_core(p, pos);
return parse_begin_end_core(p, pos, get_end_tk());
} else if (p.curr_is_token(get_by_tk())) {
// parse: 'by' tactic
auto pos = p.pos();

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

@ -1536,6 +1536,9 @@ bool elaborator::try_using(substitution & subst, expr const & mvar, proof_state
static void extract_begin_end_tactics(expr pre_tac, buffer<expr> & pre_tac_seq) {
if (is_begin_end_element_annotation(pre_tac)) {
pre_tac_seq.push_back(get_annotation_arg(pre_tac));
} else if (is_begin_end_annotation(pre_tac)) {
// nested begin-end block
pre_tac_seq.push_back(pre_tac);
} else {
buffer<expr> args;
if (get_app_args(pre_tac, args) == get_and_then_tac_fn()) {
@ -1548,47 +1551,64 @@ static void extract_begin_end_tactics(expr pre_tac, buffer<expr> & pre_tac_seq)
}
}
void elaborator::try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac) {
bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac) {
lean_assert(is_begin_end_annotation(pre_tac));
buffer<expr> pre_tac_seq;
extract_begin_end_tactics(get_annotation_arg(pre_tac), pre_tac_seq);
for (expr ptac : pre_tac_seq) {
expr new_ptac = subst.instantiate_all(ptac);
if (auto tac = pre_tactic_to_tactic(new_ptac)) {
try {
proof_state_seq seq = (*tac)(env(), ios(), ps);
auto r = seq.pull();
if (!r) {
// tactic failed to produce any result
display_unsolved_proof_state(mvar, ps, "tactic failed", ptac);
return;
}
if (m_ctx.m_flycheck_goals) {
if (auto p = pip()->get_pos_info(ptac)) {
auto out = regular(env(), ios());
flycheck_information info(out);
if (info.enabled()) {
display_information_pos(out, pip()->get_file_name(), p->first, p->second);
out << " proof state:\n" << ps.pp(env(), ios()) << "\n";
if (is_begin_end_annotation(ptac)) {
goals gs = ps.get_goals();
if (!gs)
throw_elaborator_exception("invalid nested begin-end block, there are no goals to be solved", ptac);
goal g = head(gs);
expr mvar = g.get_mvar();
proof_state focus_ps(ps, goals(g));
if (!try_using_begin_end(subst, mvar, focus_ps, ptac))
return false;
substitution ps_new_subst = ps.get_subst();
name const & mvar_name = mlocal_name(mvar);
ps_new_subst.assign(mvar_name, *subst.get_expr(mvar_name));
ps = proof_state(ps, tail(gs), ps_new_subst);
} else {
expr new_ptac = subst.instantiate_all(ptac);
if (auto tac = pre_tactic_to_tactic(new_ptac)) {
try {
proof_state_seq seq = (*tac)(env(), ios(), ps);
auto r = seq.pull();
if (!r) {
// tactic failed to produce any result
display_unsolved_proof_state(mvar, ps, "tactic failed", ptac);
return false;
}
if (m_ctx.m_flycheck_goals) {
if (auto p = pip()->get_pos_info(ptac)) {
auto out = regular(env(), ios());
flycheck_information info(out);
if (info.enabled()) {
display_information_pos(out, pip()->get_file_name(), p->first, p->second);
out << " proof state:\n" << ps.pp(env(), ios()) << "\n";
}
}
}
ps = r->first;
} catch (tactic_exception & ex) {
display_tactic_exception(ex, ps, ptac);
return false;
}
ps = r->first;
} catch (tactic_exception & ex) {
display_tactic_exception(ex, ps, ptac);
return;
} else {
return false;
}
} else {
return;
}
}
if (!empty(ps.get_goals())) {
display_unsolved_proof_state(mvar, ps, "unsolved subgoals", pre_tac);
return false;
} else {
subst = ps.get_subst();
expr v = subst.instantiate(mvar);
subst.assign(mlocal_name(mvar), v);
return true;
}
}

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

@ -150,7 +150,7 @@ class elaborator : public coercion_info_manager {
optional<tactic> pre_tactic_to_tactic(expr const & pre_tac);
bool try_using(substitution & subst, expr const & mvar, proof_state const & ps,
expr const & pre_tac, tactic const & tac, bool show_failure);
void try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac);
bool try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac);
void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited);
expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited);
expr solve_unassigned_mvars(substitution & subst, expr const & e);

29
tests/lean/run/nested_begin_end.lean Normal file
View file

@ -0,0 +1,29 @@
example (p q : Prop) : p ∧ q ↔ q ∧ p :=
begin
apply iff.intro,
begin
intro H,
apply and.intro,
apply (and.elim_right H),
apply (and.elim_left H)
end,
begin
intro H,
apply and.intro,
apply (and.elim_right H),
apply (and.elim_left H)
end
end
example (p q : Prop) : p ∧ q ↔ q ∧ p :=
begin
apply iff.intro,
{intro H,
apply and.intro,
apply (and.elim_right H),
apply (and.elim_left H)},
{intro H,
apply and.intro,
apply (and.elim_right H),
apply (and.elim_left H)}
end