From 60e4f4fee13ec6bc564e7331a34c24e9c99aa04f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Oct 2020 17:01:10 -0700 Subject: [PATCH] feat: improve `notFollowedBy` error messages --- src/Lean/Parser/Basic.lean | 11 +++++++---- src/Lean/Parser/Command.lean | 2 +- src/Lean/Parser/Do.lean | 3 ++- src/Lean/Parser/Extension.lean | 4 ++-- src/Lean/Parser/Tactic.lean | 5 +++-- src/Lean/Parser/Term.lean | 2 +- 6 files changed, 16 insertions(+), 11 deletions(-) diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index c1567ba751..184dc85be8 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -488,7 +488,7 @@ fun c s => { info := p.info, fn := lookaheadFn p.fn } -@[inline] def notFollowedByFn (p : ParserFn) : ParserFn := +@[inline] def notFollowedByFn (p : ParserFn) (msg : String) : ParserFn := fun c s => let iniSz := s.stackSize; let iniPos := s.pos; @@ -497,10 +497,10 @@ fun c s => s.restore iniSz iniPos else let s := s.restore iniSz iniPos; - s.mkError "notFollowedBy" + s.mkUnexpectedError ("unexpected " ++ msg) -@[inline] def notFollowedBy (p : Parser) : Parser := -{ fn := notFollowedByFn p.fn } +@[inline] def notFollowedBy (p : Parser) (msg : String) : Parser := +{ fn := notFollowedByFn p.fn msg } @[specialize] partial def manyAux (p : ParserFn) : ParserFn | c, s => @@ -1035,6 +1035,9 @@ let sym := sym.trim; { info := symbolInfo sym, fn := symbolFn sym } +abbrev notSymbol (s : String) : Parser := +notFollowedBy (symbol s) s + /-- Check if the following token is the symbol _or_ identifier `sym`. Useful for parsing local tokens that have not been added to the token table (but may have been so by some unrelated code). diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 4c3efb6026..4b3b8ead2e 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -87,7 +87,7 @@ def openOnly := parser! try (ident >> "(") >> many1 ident >> ")" def openSimple := parser! many1 ident @[builtinCommandParser] def «open» := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple) -@[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notFollowedBy «end» >> commandParser) >> "end" +@[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notSymbol "end" >> commandParser) >> "end" @[builtinCommandParser] def «initialize» := parser! "initialize " >> optional («try» (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq @[builtinCommandParser] def «in» := tparser! " in " >> commandParser diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index 9a86848f75..f6fe09f6b2 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -25,7 +25,8 @@ def doSeqIndent := parser! many1Indent $ group (doElemParser >> optional "; " def doSeqBracketed := parser! "{" >> withoutPosition (many1 (group (doElemParser >> optional "; "))) >> "}" def doSeq := doSeqBracketed <|> doSeqIndent -def notFollowedByRedefinedTermToken := notFollowedBy ("if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "assert!") +def notFollowedByRedefinedTermToken := + notFollowedBy ("if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "assert!") "token at 'do' element" @[builtinDoElemParser] def doLet := parser! "let " >> letDecl @[builtinDoElemParser] def doLetRec := parser! group ("let " >> nonReservedSymbol "rec ") >> letRecDecls diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 7855c6a790..5634b13532 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -203,7 +203,7 @@ partial def compileParserDescr (env : Environment) (categories : ParserCategorie | ParserDescr.optional d => optional <$> compileParserDescr d | ParserDescr.lookahead d => lookahead <$> compileParserDescr d | ParserDescr.try d => try <$> compileParserDescr d -| ParserDescr.notFollowedBy d => notFollowedBy <$> compileParserDescr d +| ParserDescr.notFollowedBy d => do p ← compileParserDescr d; pure $ notFollowedBy p "element" -- TODO allow user to set msg at ParserDescr | ParserDescr.many d => many <$> compileParserDescr d | ParserDescr.many1 d => many1 <$> compileParserDescr d | ParserDescr.sepBy d₁ d₂ => sepBy <$> compileParserDescr d₁ <*> compileParserDescr d₂ @@ -487,7 +487,7 @@ fun ctx s => | some (Syntax.atom _ sym) => if ctx.insideQuot && sym == "$" then s else match cat.tables.leadingTable.find? (mkNameSimple sym) with - | some _ => s.mkError "notFollowedByCategoryToken" + | some _ => s.mkUnexpectedError (toString catName) | _ => s | _ => s diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index dc23d924f5..b07d85f2ae 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ import Lean.Parser.Term +import Lean.Parser.Command namespace Lean namespace Parser @@ -25,7 +26,7 @@ fun c s => def ident' : Parser := ident <|> underscore -@[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> notFollowedBy "|" >> many (checkColGt >> termParser maxPrec) +@[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> notSymbol "|" >> many (checkColGt >> termParser maxPrec) @[builtinTacticParser] def «intros» := parser! nonReservedSymbol "intros " >> many (checkColGt >> ident') @[builtinTacticParser] def «revert» := parser! nonReservedSymbol "revert " >> many1 (checkColGt >> ident) @[builtinTacticParser] def «clear» := parser! nonReservedSymbol "clear " >> many1 (checkColGt >> ident) @@ -55,7 +56,7 @@ def location := parser! "at " >> (locationWildcard <|> locationTarget <| def rwRule := parser! optional (unicodeSymbol "←" "<-") >> termParser def rwRuleSeq := parser! "[" >> sepBy1 rwRule ", " true >> "]" -@[builtinTacticParser] def «rewrite» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> notFollowedBy "[" >> rwRule >> optional location +@[builtinTacticParser] def «rewrite» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> notSymbol "[" >> rwRule >> optional location @[builtinTacticParser] def «rewriteSeq» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRuleSeq >> optional location def majorPremise := parser! optional (try (ident >> " : ")) >> termParser diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 94de00b299..ddd8e7dccf 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -157,7 +157,7 @@ def letIdDecl := node `Lean.Parser.Term.letIdDecl $ try (letIdLhs >> " := ") def letPatDecl := node `Lean.Parser.Term.letPatDecl $ try (termParser >> pushNone >> optType >> " := ") >> termParser def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts false -- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl` -def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") >> (letIdDecl <|> letPatDecl <|> letEqnsDecl)) +def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl)) @[builtinTermParser] def «let» := parser!:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser @[builtinTermParser] def «let!» := parser!:leadPrec withPosition ("let! " >> letDecl) >> optSemicolon termParser @[builtinTermParser] def «let*» := parser!:leadPrec withPosition ("let* " >> letDecl) >> optSemicolon termParser