feat: add if and for for do blocks

src/Lean/Parser/Do.lean

@@ -88,6 +88,43 @@ def doId   := parser! try (ident >> optType >> leftArrow) >> termParser
 def doPat  := parser! try (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
 @[builtinDoElemParser] def doAssign := notFollowedBy "let " >> (doId <|> doPat)
 @[builtinDoElemParser] def doHave   := parser! "have " >> Term.haveDecl
+/-
+In `do` blocks, we support `if` without an `else`. Thus, we use indentation to prevent examples such as
+```
+if c_1 then
+  if c_2 then
+    action_1
+else
+  action_2
+```
+from being parsed as
+```
+if c_1 then {
+  if c_2 then {
+    action_1
+  } else {
+    action_2
+  }
+}
+```
+We also have special support for `else if` because we don't want to write
+```
+if c_1 then
+  action_1
+else if c_2 then
+       action_2
+     else
+       action_3
+```
+-/
+@[builtinDoElemParser] def doIf := parser! withPosition fun pos =>
+  "if " >> termParser >> " then " >> doSeq
+  >> many (checkColGe pos.column "'else if' in 'do' must be indented" >> try (" else " >> " if ") >> termParser >> " then " >> doSeq)
+  >> optional (checkColGe pos.column "'else' in 'do' must be indented" >> " else " >> doSeq)
+@[builtinDoElemParser] def doFor := parser! "for " >> termParser >> " in " >> termParser maxPrec >> doSeq
+@[builtinDoElemParser] def «break» := parser! "break"
+@[builtinDoElemParser] def «continue» := parser! "continue"
+
 @[builtinDoElemParser] def doExpr   := parser! notFollowedBy "let " >> notFollowedBy "have " >> termParser
 
 @[builtinTermParser] def «do»  := parser!:maxPrec "do " >> doSeq

tests/lean/run/strInterpolation.lean

@@ -103,7 +103,8 @@ chunks.iterateM Syntax.missing fun i elem result => do
   elem ← match elem.isStrInterpolantStrLit? with
     | none     => mkElem elem
     | some str => mkElem (mkStxStrLit str);
-  if i.val == 0 then pure elem else mkAppend result elem
+  -- TODO: remove `(` after we write new elabDo
+  (if i.val == 0 then pure elem else mkAppend result elem)
 
 end Lean.Syntax