feat: trailing ; in indented "do" sequences

cc @Kha

src/Lean/Elab/Do.lean

@@ -42,14 +42,14 @@ match expectedType? with
 
 private def getDoElems (stx : Syntax) : Array Syntax :=
 let arg := stx.getArg 1;
-if arg.getKind == `Lean.Parser.Term.doSeqBracketed then
-  let args := (arg.getArg 1).getArgs;
-  if args.back.isToken ";" then -- temporary hack
-    args.pop
-  else
-    args
+let args := if arg.getKind == `Lean.Parser.Term.doSeqBracketed then
+  (arg.getArg 1).getArgs
 else
-  arg.getArgs
+  arg.getArgs;
+if args.back.isToken ";" then -- temporary hack
+  args.pop
+else
+  args
 
 private partial def hasLiftMethod : Syntax → Bool
 | Syntax.node k args =>

src/Lean/Parser/Do.lean

@@ -21,7 +21,67 @@ namespace Term
 def leftArrow : Parser := unicodeSymbol " ← " " <- "
 @[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser
 
-def doSeqIndent    := withPosition fun pos => sepBy1 doElemParser (try ("; " >> checkColGe pos.column "do-elements must be indented"))
+/-
+  Trailing ';'s in indented "do" blocks are quite convenient, but
+  we have to use a few hacks to support them.
+  We can't simply set `allowTrailingSep` to `true` at the `sepBy1` parser.
+  For example, the parser
+  ```
+  withPosition fun pos =>
+    sepBy1 (checkColGe pos.column "do-elements must be indented" >> doElemParser) "; " true
+  ```
+  doesn't work because we may consume the ";" of another syntactic construct.
+  Example:
+  ```
+  def tst1 (a : Nat) : IO Unit :=
+  let f (x : Nat) : IO Unit := do
+    IO.println x;
+    pure ();  -- it would consume `;` of the let-expression
+  f a
+  ```
+  The following parser also doesn't work
+  ```
+  withPosition fun pos =>
+    sepBy1 doElemParser (try ("; " >> checkColGe pos.column "do-elements must be indented")) true
+  ```
+  because the next element after the trailing ';' would have to be indented. Otherwise, it would
+  fail the `checkColGe` indentation test.
+  ```
+    if a < 10 then do
+      pure a; -- syntax error here
+    else
+      IO.println "hello"
+  ```
+  There are two hacks:
+  1- We want a trailing `;` in a `do` sequence where the next element is a command.
+  ```
+  def foo := do
+  IO.println "hello";
+  IO.println "world";
+
+  def x := 10
+  ```
+  We considered using just `notFollowedBy commandParser` after `checkColGe`, but it is inconvenient in IDEs
+  since we keep getting a "expected term" error while we are typing the next command after the `do` sequence.
+  So, we avoid this problem by using `notFollowedByCommandToken` which fails if the next token is
+  the beggining of a command.
+
+  2- We use an `optional "; "` after the `sepBy` to consume the trailing `;` when the next element is not indented,
+  or it is a `commandParser`. To ensure we are not consuming the `;` of another syntactic element,
+  `notFollowedByTermToken >> notFollowedBy (ident <|> numLit <|> strLit <|> charLit <|> nameLit)`
+-/
+def doSeqIndent :=
+withPosition fun pos₁ =>
+  sepBy1
+    doElemParser
+    -- The separator for the indented `do`-block
+    ("; "
+     -- check indentation
+     >> checkColGe pos₁.column "do-elements must be indented"
+     -- no black lines between do-elements.
+     -- >> checkLineLe (pos₂.line+1) "no blank lines between do-elements"
+      >> notFollowedByCommandToken)
+  >> optional (try ("; " >> notFollowedByTermToken >> notFollowedBy (ident <|> numLit <|> strLit <|> charLit <|> nameLit)))
 def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
 def doSeq          := doSeqBracketed <|> doSeqIndent
 

src/Lean/Parser/Extension.lean

@@ -493,5 +493,8 @@ fun ctx s =>
 abbrev notFollowedByCommandToken : Parser :=
 notFollowedByCategoryToken `command
 
+abbrev notFollowedByTermToken : Parser :=
+notFollowedByCategoryToken `term
+
 end Parser
 end Lean

tests/compiler/termparsertest1.lean.expected.out

@@ -294,7 +294,8 @@ do
      ":="
      (Term.paren "(" [`b [(Term.tupleTail "," [`a])]] ")"))))
   ";"
-  (Term.doExpr (Term.app `pure [(Term.paren "(" [(Term.add `a "+" `b) []] ")")]))])
+  (Term.doExpr (Term.app `pure [(Term.paren "(" [(Term.add `a "+" `b) []] ")")]))]
+ [])
 do { x ← f a; pure $ a + a }
 (Term.do
  "do"

tests/lean/run/doNotation1.lean

@@ -21,7 +21,7 @@ a ← f;      -- liftM inserted here
 b ← g1 1;   -- liftM inserted here
 let x := g2 b;
 IO.println b;
-pure (s+a)
+pure (s+a);
 
 def myPrint {α} [HasToString α] (a : α) : IO Unit :=
 IO.println (">> " ++ toString a)
@@ -63,7 +63,7 @@ def tst1 : IO Unit := do
 a ← f;
 let x := a + 1;
 IO.println "hello";
-IO.println x
+IO.println x;
 
 def tst2 : IO Unit := do
 let x := ← g $ (←f) + (←f);
@@ -76,7 +76,7 @@ if (← g 1) > 0 then
 else do
   x ← f;
   y ← g x;
-  IO.println y
+  IO.println y;
 
 def pred (x : Nat) : IO Bool := do
 pure $ (← g x) > 0
@@ -103,7 +103,7 @@ partial def expandHash : Syntax → StateT Bool MacroM Syntax
   if k == `doHash then do set true; `(←MonadState.get)
   else do
     args ← args.mapM expandHash;
-    pure $ Syntax.node k args
+    pure $ Syntax.node k args;
 | stx => pure stx
 
 @[macro Lean.Parser.Term.do] def expandDo : Macro :=