From bcfaeaceabb832a3459d2994322293a623cc42a4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Feb 2020 14:11:29 -0800
Subject: [PATCH] feat: change `ite` and `dite` argument order

Motivation: make sure `propagateExpectedType` heuristic is applied in
the new frontend when processing them.
---
 src/Init/Core.lean                 | 6 +++---
 src/Init/Data/Repr.lean            | 4 +++-
 src/Init/Data/ToString.lean        | 5 +++--
 src/library/app_builder.cpp        | 2 +-
 stage0/src/library/app_builder.cpp | 2 +-
 tests/lean/run/doNotation1.lean    | 2 +-
 tests/lean/run/elabIte.lean        | 4 ++++
 7 files changed, 16 insertions(+), 9 deletions(-)
 create mode 100644 tests/lean/run/elabIte.lean

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 6530fda4bb..cf4a5fce69 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -849,12 +849,12 @@ isFalse notFalse
 
 -- We use "dependent" if-then-else to be able to communicate the if-then-else condition
 -- to the branches
-@[macroInline] def dite (c : Prop) [h : Decidable c] {α : Sort u} : (c → α) → (¬ c → α) → α :=
+@[macroInline] def dite {α : Sort u} (c : Prop) [h : Decidable c] : (c → α) → (¬ c → α) → α :=
 fun t e => Decidable.casesOn h e t
 
 /- if-then-else -/
 
-@[macroInline] def ite (c : Prop) [h : Decidable c] {α : Sort u} (t e : α) : α :=
+@[macroInline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
 Decidable.casesOn h (fun hnc => e) (fun hc => t)
 
 namespace Decidable
@@ -1717,7 +1717,7 @@ match (propDecidable (Nonempty α)) with
 
 noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop)
   (h : Nonempty α) : {x : α // Exists (fun (y : α) => p y) → p x} :=
-@dite (Exists (fun (x : α) => p x)) (propDecidable _) _
+@dite _ (Exists (fun (x : α) => p x)) (propDecidable _)
   (fun (hp : Exists (fun (x : α) => p x)) =>
     show {x : α // Exists (fun (y : α) => p y) → p x} from
     let xp := indefiniteDescription _ hp;
diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index cd068e4f21..118c3f4851 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -24,7 +24,9 @@ instance : HasRepr Bool :=
 ⟨fun b => cond b "true" "false"⟩
 
 instance {p : Prop} : HasRepr (Decidable p) :=
-⟨fun b => @ite p b _ "true" "false"⟩
+⟨fun h => match h with
+  | Decidable.isTrue _  => "true"
+  | Decidable.isFalse _ => "false"⟩
 
 protected def List.reprAux {α : Type u} [HasRepr α] : Bool → List α → String
 | b,     []    => ""
diff --git a/src/Init/Data/ToString.lean b/src/Init/Data/ToString.lean
index 5eca7af4ac..a24b120bec 100644
--- a/src/Init/Data/ToString.lean
+++ b/src/Init/Data/ToString.lean
@@ -34,8 +34,9 @@ instance : HasToString Bool :=
 ⟨fun b => cond b "true" "false"⟩
 
 instance {p : Prop} : HasToString (Decidable p) :=
--- Remark: type class inference will not consider local instance `b` in the new Elaborator
-⟨fun b => @ite p b _ "true" "false"⟩
+⟨fun h => match h with
+  | Decidable.isTrue _  => "true"
+  | Decidable.isFalse _ => "false"⟩
 
 protected def List.toStringAux {α : Type u} [HasToString α] : Bool → List α → String
 | b,     []    => ""
diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index bfb4da4e48..dfec0773fe 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -963,7 +963,7 @@ expr mk_ite(type_context_old & ctx, expr const & c, expr const & t, expr const &
     expr t_type   = ctx.infer(t);
     level u       = get_level(ctx, t_type);
     return mk_app(mk_constant(get_ite_name(), {u}),
-                  {c, *dec_c_val, t_type, t, e});
+                  {t_type, c, *dec_c_val, t, e});
 }
 
 expr mk_id(type_context_old & ctx, expr const & type, expr const & h) {
diff --git a/stage0/src/library/app_builder.cpp b/stage0/src/library/app_builder.cpp
index bfb4da4e48..dfec0773fe 100644
--- a/stage0/src/library/app_builder.cpp
+++ b/stage0/src/library/app_builder.cpp
@@ -963,7 +963,7 @@ expr mk_ite(type_context_old & ctx, expr const & c, expr const & t, expr const &
     expr t_type   = ctx.infer(t);
     level u       = get_level(ctx, t_type);
     return mk_app(mk_constant(get_ite_name(), {u}),
-                  {c, *dec_c_val, t_type, t, e});
+                  {t_type, c, *dec_c_val, t, e});
 }
 
 expr mk_id(type_context_old & ctx, expr const & type, expr const & h) {
diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean
index 234a8f3c78..1b806481ab 100644
--- a/tests/lean/run/doNotation1.lean
+++ b/tests/lean/run/doNotation1.lean
@@ -99,7 +99,7 @@ def pred2 (x : Nat) : IO Bool :=
 pure $ x > 0
 
 def tst5 (x : Nat) : IO (Option Nat) :=
-if x > 10 then pure x else pure (x-1)
+if x > 10 then pure x else pure none
 
 syntax [doHash] "#":max : term
 
diff --git a/tests/lean/run/elabIte.lean b/tests/lean/run/elabIte.lean
new file mode 100644
index 0000000000..88c619a3b5
--- /dev/null
+++ b/tests/lean/run/elabIte.lean
@@ -0,0 +1,4 @@
+new_frontend
+
+def f (x y : Nat) : Option Nat :=
+if x > y then x else none