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

fix(frontends/lean/parser): reachable code

Browse source 
The new test nbug1.lean exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-08 15:22:16 -08:00
parent 8add5571f1
commit 68c2e5cc7d
3 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1822,6 +1822,7 @@ class parser::imp {
'Notation' [Num] parts ':' ID
*/
void parse_notation_decl() {
auto p = pos();
next();
unsigned prec = parse_precedence();
bool first = true;
@ -1844,7 +1845,7 @@ class parser::imp {
if (curr_is_colon()) {
next();
if (parts.size() == 0) {
throw parser_error("invalid notation declaration, it must have at least one identifier", pos());
throw parser_error("invalid notation declaration, it must have at least one identifier", p);
}
name name_id = check_identifier_next("invalid notation declaration, identifier expected");
expr d = mk_constant(name_id);
@ -1859,7 +1860,7 @@ class parser::imp {
// prefix: ID _
m_frontend.add_prefix(parts[0], prec, d);
} else {
lean_unreachable(); // LCOV_EXCL_LINE
throw parser_error("invalid notation declaration, at least one placeholder expected", p);
}
} else {
if (first_placeholder && prev_placeholder) {

1
tests/lean/nbug1.lean Normal file
View file

@ -0,0 +1 @@
Notation 100 ++ : and

3
tests/lean/nbug1.lean.expected.out Normal file
View file

@ -0,0 +1,3 @@
Set: pp::colors
Set: pp::unicode
Error (line: 1, pos: 1) invalid notation declaration, at least one placeholder expected