From a5502e652c38d112dd74ab4ff42dbe1cdd9d69be Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Sep 2021 19:48:14 -0700
Subject: [PATCH] chore: activate builtin `if-then-else` elaborator

---
 src/Init/Notation.lean             |  4 +--
 src/Lean/Elab/BuiltinNotation.lean | 39 ++++++++++++++++++++++++------
 2 files changed, 34 insertions(+), 9 deletions(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 0266342b14..bd9aa5ba9a 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -137,12 +137,12 @@ 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) ppGroup(ppDedent("if " ident " : " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
+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) => ``(dite $c (fun $h:ident => $t) (fun $h:ident => $e))
 
-syntax (name := termIfThenElse) ppGroup(ppDedent("if " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
+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) => ``(ite $c $t $e)
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 20b36818b7..02471f84bd 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -50,13 +50,38 @@ open Meta
     | none => throwError "invalid constructor ⟨...⟩, expected type must be known"
   | _ => throwUnsupportedSyntax
 
-/-
-@[builtinMacro Lean.Parser.Term.if] def expandIf : Macro := fun stx =>
-  match_syntax stx with
-  | `(if $h : $cond then $t else $e) => `(dite $cond (fun $h:ident => $t) (fun $h:ident => $e))
-  | `(if $cond then $t else $e)      => `(ite $cond $t $e)
-  | _                                => Macro.throwUnsupported
--/
+
+@[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]
+  let newStx ←
+    if stx[1].isNone then
+      `(ite $c $t $e)
+    else
+      let h := stx[1][0]
+      `(dite $c (fun $h:ident => $t) (fun $h:ident => $e))
+  withMacroExpansion stx newStx <| elabTerm newStx expectedType?
+
+-- TODO: delete
+@[builtinTermElab termDepIfThenElse] def elabIfOld1 : TermElab := fun stx expectedType? => do
+  /- "if " ident " : " term " then" term "else" term -/
+  let h := stx[1]
+  let c := stx[3]
+  let t := stx[5]
+  let e := stx[7]
+  let newStx ← `(dite $c (fun $h:ident => $t) (fun $h:ident => $e))
+  withMacroExpansion stx newStx <| elabTerm newStx expectedType?
+
+-- TODO: delete
+@[builtinTermElab termIfThenElse] def elabIfOld2 : TermElab := fun stx expectedType? => do
+  /- "if " term " then" term "else" term -/
+  let c := stx[1]
+  let t := stx[3]
+  let e := stx[5]
+  let newStx ← `(ite $c $t $e)
+  withMacroExpansion stx newStx <| elabTerm newStx expectedType?
 
 @[builtinTermElab borrowed] def elabBorrowed : TermElab := fun stx expectedType? =>
   match stx with