From 5fa8d9105e177f2af904a0d9cfb39e990c4f8d00 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Sep 2020 17:26:50 -0700
Subject: [PATCH] feat: add `if` and `for` for `do` blocks

---
 src/Lean/Parser/Do.lean              | 37 ++++++++++++++++++++++++++++
 tests/lean/run/strInterpolation.lean |  3 ++-
 2 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index fdf9c30793..92c2a7b327 100644
--- a/src/Lean/Parser/Do.lean
+++ b/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
diff --git a/tests/lean/run/strInterpolation.lean b/tests/lean/run/strInterpolation.lean
index 8531466488..958871a115 100644
--- a/tests/lean/run/strInterpolation.lean
+++ b/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