feat: add doElem parser category

src/Lean/Parser.lean

@@ -10,6 +10,7 @@ import Lean.Parser.Tactic
 import Lean.Parser.Command
 import Lean.Parser.Module
 import Lean.Parser.Syntax
+import Lean.Parser.Do
 
 namespace Lean
 namespace PrettyPrinter

src/Lean/Parser/Command.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.Do
 
 namespace Lean
 namespace Parser

src/Lean/Parser/Do.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Parser.Term
+
+namespace Lean
+namespace Parser
+
+@[init] def regBuiltinDoElemParserAttr : IO Unit :=
+registerBuiltinParserAttribute `builtinDoElemParser `doElem
+
+@[init] def regDoElemParserAttribute : IO Unit :=
+registerBuiltinDynamicParserAttribute `doElemParser `doElem
+
+@[inline] def doElemParser (rbp : Nat := 0) : Parser :=
+categoryParser `doElem rbp
+
+namespace Term
+
+def leftArrow : Parser := unicodeSymbol " ← " " <- "
+def doLet  := parser! "let ">> letDecl
+def doId   := parser! try (ident >> optType >> leftArrow) >> termParser
+def doPat  := parser! try (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
+def doExpr := parser! termParser
+def doHave := parser! "have " >> Term.haveDecl
+
+def doElem := doLet <|> doId <|> doPat <|> doExpr
+def doSeq  := withPosition fun pos => sepBy1 doElem (try ("; " >> checkColGe pos.column "do-elements must be indented"))
+def bracketedDoSeq := parser! "{" >> sepBy1 doElem "; " >> "}"
+
+@[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser
+@[builtinTermParser] def «do»  := parser!:maxPrec "do " >> (bracketedDoSeq <|> doSeq)
+
+end Term
+end Parser
+end Lean

src/Lean/Parser/Term.lean

@@ -154,17 +154,6 @@ def attributes       := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
 @[builtinTermParser] def «letrec» :=
     parser!:leadPrec group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser
 
-def leftArrow : Parser := unicodeSymbol " ← " " <- "
-def doLet  := parser! "let ">> letDecl
-def doId   := parser! try (ident >> optType >> leftArrow) >> termParser
-def doPat  := parser! try (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
-def doExpr := parser! termParser
-def doElem := doLet <|> doId <|> doPat <|> doExpr
-def doSeq  := withPosition fun pos => sepBy1 doElem (try ("; " >> checkColGe pos.column "do-elements must be indented"))
-def bracketedDoSeq := parser! "{" >> sepBy1 doElem "; " >> "}"
-@[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser
-@[builtinTermParser] def «do»  := parser!:maxPrec "do " >> (bracketedDoSeq <|> doSeq)
-
 @[builtinTermParser] def nativeRefl   := parser! "nativeRefl! " >> termParser maxPrec
 @[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser maxPrec
 @[builtinTermParser] def decide       := parser! "decide! " >> termParser maxPrec