From d0996fb9450dc37230adea9d10ecfdf10330ef67 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 3 Apr 2021 11:56:26 +0200 Subject: [PATCH] chore: improve EOI error message --- src/Lean/Parser/Basic.lean | 32 +++++++++++++-------------- src/Lean/Parser/Module.lean | 2 +- src/Lean/PrettyPrinter/Formatter.lean | 2 +- tests/lean/eoi.lean | 1 + tests/lean/eoi.lean.expected.out | 2 ++ 5 files changed, 21 insertions(+), 18 deletions(-) create mode 100644 tests/lean/eoi.lean create mode 100644 tests/lean/eoi.lean.expected.out diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index d3d4ba8b86..afac3a92e0 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -248,12 +248,12 @@ def mkError (s : ParserState) (msg : String) : ParserState := match s with | ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack, lhsPrec, pos, cache, some { expected := [ msg ] }⟩ -def mkUnexpectedError (s : ParserState) (msg : String) : ParserState := +def mkUnexpectedError (s : ParserState) (msg : String) (expected : List String := []) : ParserState := match s with - | ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack, lhsPrec, pos, cache, some { unexpected := msg }⟩ + | ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack, lhsPrec, pos, cache, some { unexpected := msg, expected := expected }⟩ -def mkEOIError (s : ParserState) : ParserState := - s.mkUnexpectedError "end of input" +def mkEOIError (s : ParserState) (expected : List String := []) : ParserState := + s.mkUnexpectedError "unexpected end of input" expected def mkErrorAt (s : ParserState) (msg : String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState := match s, initStackSz? with @@ -1063,10 +1063,10 @@ private def updateCache (startPos : Nat) (s : ParserState) : ParserState := ⟨stack, lhsPrec, pos, { tokenCache := { startPos := startPos, stopPos := pos, token := tk } }, none⟩ | other => other -def tokenFn : ParserFn := fun c s => +def tokenFn (expected : List String := []) : ParserFn := fun c s => let input := c.input let i := s.pos - if input.atEnd i then s.mkEOIError + if input.atEnd i then s.mkEOIError expected else let tkc := s.cache.tokenCache if tkc.startPos == i then @@ -1079,7 +1079,7 @@ def tokenFn : ParserFn := fun c s => def peekTokenAux (c : ParserContext) (s : ParserState) : ParserState × Except ParserState Syntax := let iniSz := s.stackSize let iniPos := s.pos - let s := tokenFn c s + let s := tokenFn [] c s if let some e := s.errorMsg then (s.restore iniSz iniPos, Except.error s) else let stx := s.stxStack.back @@ -1102,7 +1102,7 @@ def rawIdentFn : ParserFn := fun c s => @[inline] def satisfySymbolFn (p : String → Bool) (expected : List String) : ParserFn := fun c s => let initStackSz := s.stackSize let startPos := s.pos - let s := tokenFn c s + let s := tokenFn expected c s if s.hasError then s else @@ -1141,7 +1141,7 @@ def checkTailNoWs (prev : Syntax) : Bool := def nonReservedSymbolFnAux (sym : String) (errorMsg : String) : ParserFn := fun c s => let initStackSz := s.stackSize let startPos := s.pos - let s := tokenFn c s + let s := tokenFn [errorMsg] c s if s.hasError then s else match s.stxStack.back with @@ -1247,7 +1247,7 @@ def numLitFn : ParserFn := fun c s => let initStackSz := s.stackSize let iniPos := s.pos - let s := tokenFn c s + let s := tokenFn ["numeral"] c s if !s.hasError && !(s.stxStack.back.isOfKind numLitKind) then s.mkErrorAt "numeral" iniPos initStackSz else s @[inline] def numLitNoAntiquot : Parser := { @@ -1259,7 +1259,7 @@ def scientificLitFn : ParserFn := fun c s => let initStackSz := s.stackSize let iniPos := s.pos - let s := tokenFn c s + let s := tokenFn ["scientific number"] c s if !s.hasError && !(s.stxStack.back.isOfKind scientificLitKind) then s.mkErrorAt "scientific number" iniPos initStackSz else s @[inline] def scientificLitNoAntiquot : Parser := { @@ -1270,7 +1270,7 @@ def scientificLitFn : ParserFn := def strLitFn : ParserFn := fun c s => let initStackSz := s.stackSize let iniPos := s.pos - let s := tokenFn c s + let s := tokenFn ["string literal"] c s if !s.hasError && !(s.stxStack.back.isOfKind strLitKind) then s.mkErrorAt "string literal" iniPos initStackSz else s @[inline] def strLitNoAntiquot : Parser := { @@ -1281,7 +1281,7 @@ def strLitFn : ParserFn := fun c s => def charLitFn : ParserFn := fun c s => let initStackSz := s.stackSize let iniPos := s.pos - let s := tokenFn c s + let s := tokenFn ["char literal"] c s if !s.hasError && !(s.stxStack.back.isOfKind charLitKind) then s.mkErrorAt "character literal" iniPos initStackSz else s @[inline] def charLitNoAntiquot : Parser := { @@ -1292,7 +1292,7 @@ def charLitFn : ParserFn := fun c s => def nameLitFn : ParserFn := fun c s => let initStackSz := s.stackSize let iniPos := s.pos - let s := tokenFn c s + let s := tokenFn ["Name literal"] c s if !s.hasError && !(s.stxStack.back.isOfKind nameLitKind) then s.mkErrorAt "Name literal" iniPos initStackSz else s @[inline] def nameLitNoAntiquot : Parser := { @@ -1303,7 +1303,7 @@ def nameLitFn : ParserFn := fun c s => def identFn : ParserFn := fun c s => let initStackSz := s.stackSize let iniPos := s.pos - let s := tokenFn c s + let s := tokenFn ["identifier"] c s if !s.hasError && !(s.stxStack.back.isIdent) then s.mkErrorAt "identifier" iniPos initStackSz else s @[inline] def identNoAntiquot : Parser := { @@ -1318,7 +1318,7 @@ def identFn : ParserFn := fun c s => def identEqFn (id : Name) : ParserFn := fun c s => let initStackSz := s.stackSize let iniPos := s.pos - let s := tokenFn c s + let s := tokenFn ["identifier"] c s if s.hasError then s else match s.stxStack.back with diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index cc5c45a974..9af05b31f4 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -64,7 +64,7 @@ def isExitCommand (s : Syntax) : Bool := private def consumeInput (c : ParserContext) (pos : String.Pos) : String.Pos := let s : ParserState := { cache := initCacheForInput c.input, pos := pos } - let s := tokenFn c s + let s := tokenFn [] c s match s.errorMsg with | some _ => pos + 1 | none => s.pos diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index c8463e146d..960a1a1305 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -243,7 +243,7 @@ def trailingNode.formatter (k : SyntaxNodeKind) (_ _ : Nat) (p : Formatter) : Fo categoryParser.formatter `foo def parseToken (s : String) : FormatterM ParserState := do - Parser.tokenFn { + Parser.tokenFn [] { input := s, fileName := "", fileMap := FileMap.ofString "", diff --git a/tests/lean/eoi.lean b/tests/lean/eoi.lean new file mode 100644 index 0000000000..8050e8d1aa --- /dev/null +++ b/tests/lean/eoi.lean @@ -0,0 +1 @@ +def foo : Nat diff --git a/tests/lean/eoi.lean.expected.out b/tests/lean/eoi.lean.expected.out new file mode 100644 index 0000000000..e3ece41a45 --- /dev/null +++ b/tests/lean/eoi.lean.expected.out @@ -0,0 +1,2 @@ +eoi.lean:2:0: error: unexpected end of input; expected ':=', 'where' or '|' +eoi.lean:1:0-1:13: error: declaration body is missing