From 5a19430f60edae37a03c08da0a382fc04bad385d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 23 May 2017 10:33:31 +0200 Subject: [PATCH] fix(frontends/lean/scanner): wrong upos after field projection --- src/frontends/lean/scanner.cpp | 3 +-- tests/lean/field_proj_pos.lean | 2 ++ tests/lean/field_proj_pos.lean.expected.out | 7 +++++++ 3 files changed, 10 insertions(+), 2 deletions(-) create mode 100644 tests/lean/field_proj_pos.lean create mode 100644 tests/lean/field_proj_pos.lean.expected.out diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index 237a7eca4a..0994440556 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -523,7 +523,7 @@ auto scanner::read_key_cmd_id() -> token_kind { break; } } - move_back(cs.size() - id_sz, num_utfs - 1); + move_back(cs.size() - id_sz, 1); cs.shrink(id_sz); cs.push_back(0); m_name_val = name(cs.data()); @@ -531,7 +531,6 @@ auto scanner::read_key_cmd_id() -> token_kind { } } } else if (is_id_first(cs, 0)) { - id_sz = cs.size(); while (true) { id_sz = cs.size(); id_utf_sz = num_utfs; diff --git a/tests/lean/field_proj_pos.lean b/tests/lean/field_proj_pos.lean new file mode 100644 index 0000000000..ef6386ba83 --- /dev/null +++ b/tests/lean/field_proj_pos.lean @@ -0,0 +1,2 @@ +example (h : true ∨ true) : true := +by exact (h).elim _ _ diff --git a/tests/lean/field_proj_pos.lean.expected.out b/tests/lean/field_proj_pos.lean.expected.out new file mode 100644 index 0000000000..30485bd47f --- /dev/null +++ b/tests/lean/field_proj_pos.lean.expected.out @@ -0,0 +1,7 @@ +field_proj_pos.lean:2:18: error: don't know how to synthesize placeholder +context: +h : true ∨ true +⊢ true → true +state: +h : true ∨ true +⊢ true