From dc9626ceabc7cae55da7d058368cb7f4795ce759 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Sep 2020 18:10:06 -0700 Subject: [PATCH] feat: try to improve weird error message @Kha Before this commit, we were producing the error "expected command" at the `let` token ```lean check id let x := 1; x ``` The new error is "expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term". The example above looks artificial, but it will happen all the time as users start to define their own notation. --- src/Lean/Parser/Basic.lean | 19 +++++++++++++++---- src/Lean/Parser/Module.lean | 8 +++++++- src/Lean/Parser/Term.lean | 8 +++----- tests/lean/precissues.lean | 2 ++ tests/lean/precissues.lean.expected.out | 4 +++- 5 files changed, 30 insertions(+), 11 deletions(-) diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 2ec988c507..3bd6ca879b 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -88,6 +88,7 @@ input.get (input.next pos) Note that nothing prevents users from using a higher precedence, but we strongly discourage them from doing it. -/ def maxPrec : Nat := 1024 +def leadPrec := maxPrec - 1 abbrev Token := String @@ -351,6 +352,13 @@ instance hasAndthen : HasAndthen Parser := { info := nodeInfo n p.info, fn := nodeFn n p.fn } +def errorFn (msg : String) : ParserFn := +fun _ s => s.mkUnexpectedError msg + +@[inline] def error (msg : String) : Parser := +{ info := epsilonInfo, + fn := errorFn msg } + /- Succeeds if `c.prec <= prec` -/ def checkPrecFn (prec : Nat) : ParserFn := fun c s => @@ -399,14 +407,14 @@ checkPrec prec >> trailingNodeAux n p @[inline] def group (p : Parser) : Parser := node nullKind p -def mergeOrElseErrors (s : ParserState) (error1 : Error) (iniPos : Nat) : ParserState := +def mergeOrElseErrors (s : ParserState) (error1 : Error) (iniPos : Nat) (mergeErrors : Bool) : ParserState := match s with | ⟨stack, pos, cache, some error2⟩ => - if pos == iniPos then ⟨stack, pos, cache, some (error1.merge error2)⟩ + if pos == iniPos then ⟨stack, pos, cache, some (if mergeErrors then error1.merge error2 else error2)⟩ else s | other => other -@[inline] def orelseFn (p q : ParserFn) : ParserFn +@[inline] def orelseFnCore (p q : ParserFn) (mergeErrors : Bool) : ParserFn | c, s => let iniSz := s.stackSize; let iniPos := s.pos; @@ -414,11 +422,14 @@ match s with match s.errorMsg with | some errorMsg => if s.pos == iniPos then - mergeOrElseErrors (q c (s.restore iniSz iniPos)) errorMsg iniPos + mergeOrElseErrors (q c (s.restore iniSz iniPos)) errorMsg iniPos mergeErrors else s | none => s +@[inline] def orelseFn (p q : ParserFn) : ParserFn := +orelseFnCore p q true + @[noinline] def orelseInfo (p q : ParserInfo) : ParserInfo := { collectTokens := p.collectTokens ∘ q.collectTokens, collectKinds := p.collectKinds ∘ q.collectKinds, diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index 71e39b7912..792460dc71 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -70,6 +70,12 @@ match s.errorMsg with | some _ => pos + 1 | none => s.pos +def topLevelCommandParserFn : ParserFn := +orelseFnCore + commandParser.fn + (andthenFn (lookaheadFn termParser.fn) (errorFn "expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term")) + false /- do not merge errors -/ + partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleParserState → MessageLog → Syntax × ModuleParserState × MessageLog | s@{ pos := pos, recovering := recovering }, messages => if inputCtx.input.atEnd pos then @@ -78,7 +84,7 @@ partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleP let c := mkParserContext env inputCtx; let s := { cache := initCacheForInput c.input, pos := pos : ParserState }; let s := whitespace c s; - let s := (commandParser : Parser).fn c s; + let s := topLevelCommandParserFn c s; match s.errorMsg with | none => let stx := s.stxStack.back; diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index e15d2d541a..28266684df 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -41,8 +41,6 @@ checkPrec prec >> unicodeSymbol sym asciiSym >> termParser (prec+1) def infixL (sym : String) (prec : Nat) : TrailingParser := checkPrec prec >> symbol sym >> termParser (prec+1) -def leadPrec := maxPrec - 1 - /- Built-in parsers -/ @[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.indentedNonEmptySeq @@ -52,8 +50,8 @@ def leadPrec := maxPrec - 1 @[builtinTermParser] def num : Parser := checkPrec maxPrec >> numLit @[builtinTermParser] def str : Parser := checkPrec maxPrec >> strLit @[builtinTermParser] def char : Parser := checkPrec maxPrec >> charLit -@[builtinTermParser] def type := parser! "Type" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec) -@[builtinTermParser] def sort := parser! "Sort" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec) +@[builtinTermParser] def type := parser! "Type" >> optional (checkWsBefore "" >> checkPrec leadPrec >> levelParser maxPrec) +@[builtinTermParser] def sort := parser! "Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> levelParser maxPrec) @[builtinTermParser] def prop := parser! "Prop" @[builtinTermParser] def hole := parser! "_" @[builtinTermParser] def syntheticHole := parser! "?" >> (ident <|> hole) @@ -135,7 +133,7 @@ def funBinder : Parser := funImplicitBinder <|> instBinder <|> termParser maxPre def optExprPrecedence := optional (try ":" >> termParser maxPrec) @[builtinTermParser] def «parser!» := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser @[builtinTermParser] def «tparser!» := parser!:leadPrec "tparser! " >> optExprPrecedence >> termParser -@[builtinTermParser] def borrowed := parser! "@&" >> termParser (maxPrec - 1) +@[builtinTermParser] def borrowed := parser! "@&" >> termParser leadPrec @[builtinTermParser] def quotedName := parser! nameLit -- NOTE: syntax quotations are defined in Init.Lean.Parser.Command @[builtinTermParser] def «match_syntax» := parser!:leadPrec "match_syntax" >> termParser >> " with " >> matchAlts diff --git a/tests/lean/precissues.lean b/tests/lean/precissues.lean index 4cc4bbc3e6..d91a5302e6 100644 --- a/tests/lean/precissues.lean +++ b/tests/lean/precissues.lean @@ -14,6 +14,8 @@ def f (x : Nat) (g : Nat → Nat) := g x #check id have True from ⟨⟩; this -- should fail +#check id let x := 10; x + #check 1 #check id (have True from ⟨⟩; this) diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out index 30eb0c26e7..6ffeab106d 100644 --- a/tests/lean/precissues.lean.expected.out +++ b/tests/lean/precissues.lean.expected.out @@ -4,7 +4,9 @@ f 1 fun (x : Nat) => x : Nat 0 : Nat f 1 fun (x : Nat) => x : Nat id : ?m → ?m -precissues.lean:15:10: error: expected command +precissues.lean:15:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term +id : ?m → ?m +precissues.lean:17:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term 1 : Nat id ((fun (this : True) => this) True.intro) : True 0 = (fun (this : Nat) => this) 1 : Prop