From 246923886aa2b9ef9f3064a84ec04984039917a2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 4 Nov 2022 10:10:49 +0100 Subject: [PATCH] fix: do not create choice nodes for failed parses --- src/Lean/Parser/Basic.lean | 3 +-- tests/lean/1760.lean | 3 +++ tests/lean/1760.lean.expected.out | 2 ++ 3 files changed, 6 insertions(+), 2 deletions(-) create mode 100644 tests/lean/1760.lean create mode 100644 tests/lean/1760.lean.expected.out diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index bb5dd98c33..7f9d34c9c9 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1389,8 +1389,7 @@ def keepPrevError (s : ParserState) (oldStackSize : Nat) (oldStopPos : String.Po def mergeErrors (s : ParserState) (oldStackSize : Nat) (oldError : Error) : ParserState := match s with | ⟨stack, lhsPrec, pos, cache, some err⟩ => - if oldError == err then s - else ⟨stack.shrink oldStackSize, lhsPrec, pos, cache, some (oldError.merge err)⟩ + ⟨stack.shrink oldStackSize, lhsPrec, pos, cache, if oldError == err then some err else some (oldError.merge err)⟩ | other => other def keepLatest (s : ParserState) (startStackSize : Nat) : ParserState := diff --git a/tests/lean/1760.lean b/tests/lean/1760.lean new file mode 100644 index 0000000000..806a155dcc --- /dev/null +++ b/tests/lean/1760.lean @@ -0,0 +1,3 @@ +-- should run in linear time +#check [[[[[[[[[[[[[[[[[[[[[[[[ +#check (((((((((((((((((((((((()))))))))))))))))))))))) diff --git a/tests/lean/1760.lean.expected.out b/tests/lean/1760.lean.expected.out new file mode 100644 index 0000000000..0472ebebd0 --- /dev/null +++ b/tests/lean/1760.lean.expected.out @@ -0,0 +1,2 @@ +1760.lean:3:0: error: expected ':', ']' or term +() : Unit