feat: indented do blocks

@Kha it is soooooo much nicer :)

src/Lean/Parser/Term.lean

@@ -159,8 +159,8 @@ 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  := sepBy1 doElem "; "
-def bracketedDoSeq := parser! "{" >> doSeq >> "}"
+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)
 

tests/lean/file_not_found.lean

@@ -4,13 +4,15 @@ new_frontend
 open IO.FS
 def usingIO {α} (x : IO α) := x
 #eval (discard $ IO.FS.Handle.mk "non-existent-file.txt" Mode.read : IO Unit)
-#eval usingIO do condM (IO.fileExists "readonly.txt")
-               (pure ())
-               (IO.FS.withFile "readonly.txt" Mode.write $ fun _ => pure ());
-         IO.setAccessRights "readonly.txt" { user := { read := true } };
-         (pure () : IO Unit)
+#eval usingIO do
+  condM (IO.fileExists "readonly.txt")
+    (pure ())
+    (IO.FS.withFile "readonly.txt" Mode.write $ fun _ => pure ());
+  IO.setAccessRights "readonly.txt" { user := { read := true } };
+  pure ()
 #eval (discard $ IO.FS.Handle.mk "readonly.txt" Mode.write : IO Unit)
-#eval usingIO do h ← IO.FS.Handle.mk "readonly.txt" Mode.read;
-         h.putStr "foo";
-         IO.println "foo";
-         (pure () : IO Unit)
+#eval usingIO do
+  h ← IO.FS.Handle.mk "readonly.txt" Mode.read;
+  h.putStr "foo";
+  IO.println "foo";
+  pure ()

tests/lean/file_not_found.lean.expected.out

@@ -3,7 +3,7 @@ file_not_found.lean:6:0: error: no such file or directory (error code: 2)
   file: non-existent-file.txt
 
 
-file_not_found.lean:12:0: error: permission denied (error code: 13)
+file_not_found.lean:13:0: error: permission denied (error code: 13)
   file: readonly.txt
 
-file_not_found.lean:13:0: error: invalid argument (error code: 9, bad file descriptor)
+file_not_found.lean:14:0: error: invalid argument (error code: 9, bad file descriptor)

tests/lean/run/IO_test.lean

@@ -17,17 +17,17 @@ unless (expected == actual) $ throw $ IO.userError $
 def test : IO Unit := do
 let xs : ByteArray := ⟨#[1,2,3,4]⟩;
 let fn := "foo.txt";
-withFile fn Mode.write $ fun h => do
-{ h.write xs;
+withFile fn Mode.write fun h => do
   h.write xs;
-  pure () };
+  h.write xs;
+  pure ();
 ys ← withFile "foo.txt" Mode.read $ fun h => h.read 10;
 check_eq "1" (xs.toList ++ xs.toList) ys.toList;
-withFile fn Mode.append $ fun h => do
-{ h.write ⟨#[5,6,7,8]⟩;
-  pure () };
-withFile "foo.txt" Mode.read $ fun h => do
-  { ys ← h.read 10;
+withFile fn Mode.append fun h => do
+  h.write ⟨#[5,6,7,8]⟩;
+  pure ();
+withFile "foo.txt" Mode.read fun h => do
+    ys ← h.read 10;
     check_eq "2" [1,2,3,4,1,2,3,4,5,6] ys.toList;
     ys ← h.read 2;
     check_eq "3" [7,8] ys.toList;
@@ -38,7 +38,7 @@ withFile "foo.txt" Mode.read $ fun h => do
     check_eq "5" [] ys.toList;
     b ← h.isEof;
     unless b
-      (throw $ IO.userError $ "wrong (6): ") };
+      (throw $ IO.userError $ "wrong (6): ");
 pure ()
 
 #eval test

tests/lean/run/meta2.lean

@@ -52,11 +52,10 @@ def tst3 : MetaM Unit :=
 do print "----- tst3 -----";
    let t   := mkLambda `x BinderInfo.default nat $ mkBVar 0;
    mvar ← mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
-   lambdaTelescope t $ fun xs _ => do {
+   lambdaTelescope t fun xs _ => do
      let x := xs.get! 0;
      check $ isExprDefEq (mkApp mvar x) (mkAppN add #[x, mkAppN add #[mkNatLit 10, x]]);
-     pure ()
-   };
+     pure ();
    v ← getAssignment mvar;
    print v;
    pure ()
@@ -66,7 +65,7 @@ do print "----- tst3 -----";
 def tst4 : MetaM Unit :=
 do print "----- tst4 -----";
    let t   := mkLambda `x BinderInfo.default nat $ mkBVar 0;
-   lambdaTelescope t $ fun xs _ => do {
+   lambdaTelescope t fun xs _ => do
      let x := xs.get! 0;
      mvar ← mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
      -- the following `isExprDefEq` fails because `x` is also in the context of `mvar`
@@ -74,8 +73,7 @@ do print "----- tst4 -----";
      check $ approxDefEq $ isExprDefEq (mkApp mvar x) (mkAppN add #[x, mkAppN add #[mkNatLit 10, x]]);
      v ← getAssignment mvar;
      print v;
-     pure ()
-   };
+     pure ();
    pure ()
 
 #eval tst4
@@ -199,7 +197,7 @@ do print "----- tst11 -----";
    check $ isType (mkArrow nat nat);
    check $ not <$> isType add;
    check $ not <$> isType (mkNatLit 1);
-   withLocalDeclD `x nat $ fun x => do {
+   withLocalDeclD `x nat fun x => do
      check $ not <$> isType x;
      check $ not <$> (mkLambdaFVars #[x] x >>= isType);
      check $ not <$> (mkLambdaFVars #[x] nat >>= isType);
@@ -207,15 +205,14 @@ do print "----- tst11 -----";
      (t, _) ← mkForallUsedOnly #[x] t;
      print t;
      check $ isType t;
-     pure ()
-   };
+     pure ();
    pure ()
 
 #eval tst11
 
 def tst12 : MetaM Unit :=
 do print "----- tst12 -----";
-   withLocalDeclD `x nat $ fun x => do {
+   withLocalDeclD `x nat $ fun x => do
      t ← mkEqRefl x >>= mkLambdaFVars #[x];
      print t;
      type ← inferType t;
@@ -223,8 +220,7 @@ do print "----- tst12 -----";
      isProofQuick t >>= fun b => print (toString b);
      isProofQuick nat >>= fun b => print (toString b);
      isProofQuick type >>= fun b => print (toString b);
-     pure ()
-   };
+     pure ();
    pure ()
 
 #eval tst12

tests/lean/run/nicerNestedDos.lean

@@ -0,0 +1,36 @@
+new_frontend
+
+def f (x : Nat) : IO Nat := do
+IO.println "hello";
+when (x > 5) do
+  IO.println ("x: " ++ toString x);
+  IO.println "done";
+pure (x + 1)
+
+#eval f 2
+#eval f 10
+
+def g (x : Nat) : StateT Nat Id Unit := do
+when (x > 10) do
+  s ← get;
+  set (s + x);
+pure ()
+
+theorem ex1 : (g 10).run 1 = ((), 1) :=
+rfl
+
+theorem ex2 : (g 20).run 1 = ((), 21) :=
+rfl
+
+def h (x : Nat) : StateT Nat Id Unit := do
+when (x > 10) do {
+  s ← get;
+set (s + x) -- we don't need to respect indentation when `{` `}` are used
+};
+pure ()
+
+theorem ex3 : (h 10).run 1 = ((), 1) :=
+rfl
+
+theorem ex4 : (h 20).run 1 = ((), 21) :=
+rfl

tests/lean/run/unif_issue.lean

@@ -3,8 +3,8 @@ new_frontend
 open Lean
 
 #eval toString $
-  Unhygienic.run $
-    do a ← `(Nat.one);
+  Unhygienic.run do
+    a ← `(Nat.one);
     let rhs_0 : _ := fun (a : Lean.Syntax) (b : Lean.Syntax) => pure Syntax.missing;
     let rhs_1 : _ := fun (_a : _) => pure Lean.Syntax.missing;
     let discr_2 : _ := a;
@@ -22,8 +22,8 @@ open Lean
 #check (let rhs := fun a => pure a; rhs 0 : Id Nat)
 
 #check toString $
-  Unhygienic.run $
-    do a ← `(Nat.one);
+  Unhygienic.run do
+    a ← `(Nat.one);
     let rhs_0 : _ := fun (a : Lean.Syntax) (b : Lean.Syntax) => pure Syntax.missing;
     let rhs_1 : _ := fun (_a : _) => pure Lean.Syntax.missing;
     let discr_2 : _ := a;