From 2d8506b7c66953b22ec2afa4fc8ba76ebabbea6d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Sep 2020 06:18:44 -0700
Subject: [PATCH] feat: add `doElem` parser category

---
 src/Lean/Parser.lean         |  1 +
 src/Lean/Parser/Command.lean |  1 +
 src/Lean/Parser/Do.lean      | 38 ++++++++++++++++++++++++++++++++++++
 src/Lean/Parser/Term.lean    | 11 -----------
 4 files changed, 40 insertions(+), 11 deletions(-)
 create mode 100644 src/Lean/Parser/Do.lean

diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean
index c263cde361..eaa56232b9 100644
--- a/src/Lean/Parser.lean
+++ b/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
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 8e041b9fe7..111e918b9d 100644
--- a/src/Lean/Parser/Command.lean
+++ b/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
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
new file mode 100644
index 0000000000..c33e8190ef
--- /dev/null
+++ b/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
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 28266684df..1825692c79 100644
--- a/src/Lean/Parser/Term.lean
+++ b/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