From 881589fc4602f160e26a58b3169fa4aa039737b0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 9 Jul 2022 16:25:30 -0700
Subject: [PATCH] chore: remove parser workarounds

---
 src/Init/Tactics.lean                |  8 ++++++--
 src/Init/Util.lean                   |  6 +++---
 tests/lean/getElem.lean              | 22 ++++++++++++++++++++++
 tests/lean/getElem.lean.expected.out |  8 ++++++++
 4 files changed, 39 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/getElem.lean
 create mode 100644 tests/lean/getElem.lean.expected.out

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 3eede15cac..f0296142cf 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -434,8 +434,12 @@ macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| decide)
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| assumption)
 
-macro "get_elem_tactic" : tactic => `(get_elem_tactic_trivial) -- TODO: add error message
+macro "get_elem_tactic" : tactic =>
+  `(first
+    | get_elem_tactic_trivial
+    | fail "failed to prove index is valid, possible solutions:\n  - Use `have`-expressions to prove the index is valid\n  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid\n  - Use `a[i]?` notation instead, result is an `Option` type\n  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid"
+   )
 
-macro:max (priority := high) x:term noWs "[" i:term "]" : term => `(getElem $x $i (by get_elem_tactic))
+macro:max x:term noWs "[" i:term "]" : term => `(getElem $x $i (by get_elem_tactic))
 
 macro x:term noWs "[" i:term "]'" h:term:max : term => `(getElem $x $i $h)
diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index 0016caae32..2902ce9586 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -59,10 +59,10 @@ def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () =
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k 0
 
 @[inline] def getElem! [GetElem Cont Idx Elem Dom] [Inhabited Elem] (xs : Cont) (i : Idx) [Decidable (Dom xs i)] : Elem :=
-  if h : _ then getElem xs i h else unreachable!
+  if h : _ then getElem xs i h else panic! "index out of bounds"
 
 @[inline] def getElem? [GetElem Cont Idx Elem Dom] (xs : Cont) (i : Idx) [Decidable (Dom xs i)] : Option Elem :=
   if h : _ then some (getElem xs i h) else none
 
-macro:max (priority := high) x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i) -- TODO: remove priority
-macro:max (priority := high) x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i) -- TODO: remove priority
+macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
+macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
diff --git a/tests/lean/getElem.lean b/tests/lean/getElem.lean
new file mode 100644
index 0000000000..242ed2cbd4
--- /dev/null
+++ b/tests/lean/getElem.lean
@@ -0,0 +1,22 @@
+def f1 (a : Array Nat) (i : Nat) :=
+  a[i]
+
+def f2 (a : Array Nat) (i : Fin a.size) :=
+  a[i] -- Ok
+
+def f3 (a : Array Nat) (h : n ≤ a.size) (i : Fin n) :=
+  a[i] -- Ok
+
+opaque a : Array Nat
+opaque n : Nat
+axiom n_lt_a_size : n < a.size
+
+def f4 (i : Nat) (h : i < n) :=
+  have : i < a.size := Nat.lt_trans h n_lt_a_size
+  a[i]
+
+def f5 (i : Nat) (h : i < n) :=
+  a[i]'(Nat.lt_trans h n_lt_a_size)
+
+def f6 (i : Nat) :=
+  a[i]!
diff --git a/tests/lean/getElem.lean.expected.out b/tests/lean/getElem.lean.expected.out
new file mode 100644
index 0000000000..b731036abf
--- /dev/null
+++ b/tests/lean/getElem.lean.expected.out
@@ -0,0 +1,8 @@
+getElem.lean:2:2-2:6: error: failed to prove index is valid, possible solutions:
+  - Use `have`-expressions to prove the index is valid
+  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
+  - Use `a[i]?` notation instead, result is an `Option` type
+  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
+a : Array Nat
+i : Nat
+⊢ i < Array.size a