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

fix(frontends/lean/parse_rewrite_tactic): fixes #691

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-28 11:28:05 -07:00
parent 869ad261c5
commit 4a4ef48344
3 changed files with 30 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/frontends/lean/parse_rewrite_tactic.cpp
View file

@ -36,19 +36,31 @@ static expr parse_rule(parser & p, bool use_paren) {
} }
} }
static void check_not_in_theorem_queue(parser & p, name const & n, pos_info const & pos) {
if (p.in_theorem_queue(n)) {
throw parser_error(sstream() << "invalid 'rewrite' tactic, cannot unfold '" << n << "' "
<< "which is still in the theorem queue. Use command 'reveal " << n << "' "
<< "to access its definition.", pos);
}
}
static expr parse_rewrite_unfold_core(parser & p) { static expr parse_rewrite_unfold_core(parser & p) {
buffer<name> to_unfold; buffer<name> to_unfold;
if (p.curr_is_token(get_lbracket_tk())) { if (p.curr_is_token(get_lbracket_tk())) {
p.next(); p.next();
while (true) { while (true) {
auto pos = p.pos();
to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier expected")); to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier expected"));
check_not_in_theorem_queue(p, to_unfold.back(), pos);
if (!p.curr_is_token(get_comma_tk())) if (!p.curr_is_token(get_comma_tk()))
break; break;
p.next(); p.next();
} }
p.check_token_next(get_rbracket_tk(), "invalid unfold rewrite step, ',' or ']' expected"); p.check_token_next(get_rbracket_tk(), "invalid unfold rewrite step, ',' or ']' expected");
} else { } else {
auto pos = p.pos();
to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier or '[' expected")); to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier or '[' expected"));
check_not_in_theorem_queue(p, to_unfold.back(), pos);
} }
location loc = parse_tactic_location(p); location loc = parse_tactic_location(p);
return mk_rewrite_unfold(to_list(to_unfold), loc); return mk_rewrite_unfold(to_list(to_unfold), loc);
@ -174,6 +186,7 @@ expr parse_unfold_tactic(parser & p) {
auto pos = p.pos(); auto pos = p.pos();
if (p.curr_is_identifier()) { if (p.curr_is_identifier()) {
name c = p.check_constant_next("invalid unfold tactic, identifier expected"); name c = p.check_constant_next("invalid unfold tactic, identifier expected");
check_not_in_theorem_queue(p, c, pos);
location loc = parse_tactic_location(p); location loc = parse_tactic_location(p);
elems.push_back(p.save_pos(mk_rewrite_unfold(to_list(c), loc), pos)); elems.push_back(p.save_pos(mk_rewrite_unfold(to_list(c), loc), pos));
} else if (p.curr_is_token(get_lbracket_tk())) { } else if (p.curr_is_token(get_lbracket_tk())) {

13
tests/lean/691.lean Normal file
View file

@ -0,0 +1,13 @@
theorem foo : Type₁ := unit
example : foo = unit :=
by unfold foo
example : foo = unit :=
by unfold [foo]
example : foo = unit :=
by rewrite [↑foo]
example : foo = unit :=
by rewrite [↑[foo] ]

4
tests/lean/691.lean.expected.out Normal file
View file

@ -0,0 +1,4 @@
691.lean:4:10: error: invalid 'rewrite' tactic, cannot unfold 'foo' which is still in the theorem queue. Use command 'reveal foo' to access its definition.
691.lean:7:11: error: invalid 'rewrite' tactic, cannot unfold 'foo' which is still in the theorem queue. Use command 'reveal foo' to access its definition.
691.lean:10:13: error: invalid 'rewrite' tactic, cannot unfold 'foo' which is still in the theorem queue. Use command 'reveal foo' to access its definition.
691.lean:13:14: error: invalid 'rewrite' tactic, cannot unfold 'foo' which is still in the theorem queue. Use command 'reveal foo' to access its definition.