From c24cd877c8c0fcdf6be7b3ee0ed12bf3b46dfd1b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Oct 2021 17:30:06 -0700
Subject: [PATCH] chore: define `if-then-else` again as a macro

We can do it using the new auxiliary notation `let_mvar%` and
`wait_if_type_mvar%`.
---
 src/Init/Notation.lean             | 10 ++++++++++
 src/Lean/Elab/BuiltinNotation.lean | 29 -----------------------------
 src/Lean/Parser/Term.lean          |  2 --
 3 files changed, 10 insertions(+), 31 deletions(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 0060cc0bcd..d85a7a0284 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -137,6 +137,16 @@ infixr:100 " <$> " => Functor.map
 macro_rules | `($x <|> $y) => `(binop_lazy% HOrElse.hOrElse $x $y)
 macro_rules | `($x >> $y)  => `(binop_lazy% HAndThen.hAndThen $x $y)
 
+syntax (name := termDepIfThenElse) (priority := high) ppGroup(ppDedent("if " ident " : " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
+
+macro_rules
+  | `(if $h:ident : $c then $t:term else $e:term) => `(let_mvar% ?m := $c; wait_if_type_mvar% ?m; dite ?m (fun $h:ident => $t) (fun $h:ident => $e))
+
+syntax (name := termIfThenElse) (priority := high) ppGroup(ppDedent("if " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
+
+macro_rules
+  | `(if $c then $t:term else $e:term) => `(let_mvar% ?m := $c; wait_if_type_mvar% ?m; ite ?m $t $e)
+
 macro "if " "let " pat:term " := " d:term " then " t:term " else " e:term : term =>
   `(match $d:term with | $pat:term => $t | _ => $e)
 
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index ac867aa391..526925315b 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -50,35 +50,6 @@ open Meta
     | none => throwError "invalid constructor ⟨...⟩, expected type must be known"
   | _ => throwUnsupportedSyntax
 
-@[builtinTermElab Lean.Parser.Term.if] def elabIf : TermElab := fun stx expectedType? => do
-  /- "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser -/
-  let c := stx[2]
-  let t := stx[4]
-  let e := stx[6]
-  if !stx[1].isNone then
-    -- TODO: add special support for dependent ite
-    let h := stx[1][0]
-    let stxNew ← `(dite $c (fun $h:ident => $t) (fun $h:ident => $e))
-    withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
-  else if let some c ← isLocalIdent? c then
-    let cType ← inferType c
-    -- Postpone if the type of the condition is not available
-    tryPostponeIfMVar cType
-    let localDecl ← getLocalDecl c.fvarId!
-    -- If `c` is auxiliary let-decl created by this elaborator, then expand it (see "else" branch of this method)
-    let c ←
-      if localDecl.userName.eraseMacroScopes ==  `_if_cond then
-        instantiateMVars localDecl.value
-      else
-        pure c
-    elabAppArgs (← mkConst `ite) #[] #[Arg.expr c, Arg.stx t, Arg.stx e] expectedType? (explicit := false) (ellipsis := false)
-  else
-    -- If condition is not a free variable, then add an auxiliary let-decl.
-    let cNew ← `(_if_cond)
-    let iteNew := stx.setArg 2 cNew
-    let stxNew ← `(let_tmp _if_cond := $c; $iteNew)
-    withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
-
 @[builtinTermElab borrowed] def elabBorrowed : TermElab := fun stx expectedType? =>
   match stx with
   | `(@& $e) => return markBorrowed (← elabTerm e expectedType?)
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 556bccc158..03f060740e 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -269,8 +269,6 @@ def macroLastArg   := macroDollarArg <|> macroArg
 
 @[builtinTermParser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> incQuotDepth (parserOfStack 1) >> ")"
 
-@[builtinTermParser] def «if» := leading_parser:leadPrec ppGroup $ ppDedent $ "if " >> optIdent >> termParser >> " then" >> ppSpace >> termParser >> ppDedent (ppSpace >> "else") >> ppSpace >> termParser
-
 end Term
 
 @[builtinTermParser default+1] def Tactic.quot    : Parser := leading_parser "`(tactic|" >> incQuotDepth tacticParser >> ")"