From c0f264ffe01ecbc0bb161b7eeb7cf4906970c3fe Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 19 Jan 2024 19:29:18 +0100
Subject: [PATCH] fix: reducing out-of-bounds swap! should return `a`, not
 `default` (#3197)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`Array.set!` and `Array.swap!` are fairly similar operations, both
modify an array, both take an index that it out of bounds.

But they behave different; all of these return `true`
```
#eval #[1,2].set! 2 42 == #[1,2]    -- with panic
#reduce #[1,2].set! 2 42 == #[1,2]  -- no panic

#eval #[1,2].swap! 0 2 == #[1,2]    -- with panic
#reduce #[1,2].swap! 0 2 == default -- no panic
```

The implementations are
```
@[extern "lean_array_set"]
def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
  Array.setD a i v
```
but
```
@[extern "lean_array_swap"]
def swap! (a : Array α) (i j : @& Nat) : Array α :=
  if h₁ : i < a.size then
  if h₂ : j < a.size then swap a ⟨i, h₁⟩ ⟨j, h₂⟩
  else panic! "index out of bounds"
  else panic! "index out of bounds"
```

It seems to be more consistent to unify the behaviors, and define
```
@[extern "lean_array_swap"]
def swap! (a : Array α) (i j : @& Nat) : Array α :=
  if h₁ : i < a.size then
  if h₂ : j < a.size then swap a ⟨i, h₁⟩ ⟨j, h₂⟩
  else a
  else a
```

Also adds docstrings.

Fixes #3196
---
 src/Init/Data/Array/Basic.lean | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index a86f99e561..217451a403 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -71,6 +71,12 @@ abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size =
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
   a.set ⟨i.toNat, h⟩ v
 
+/--
+Swaps two entries in an array.
+
+This will perform the update destructively provided that `a` has a reference
+count of 1 when called.
+-/
 @[extern "lean_array_fswap"]
 def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   let v₁ := a.get i
@@ -78,12 +84,18 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   let a'  := a.set i v₂
   a'.set (size_set a i v₂ ▸ j) v₁
 
+/--
+Swaps two entries in an array, or panics if either index is out of bounds.
+
+This will perform the update destructively provided that `a` has a reference
+count of 1 when called.
+-/
 @[extern "lean_array_swap"]
 def swap! (a : Array α) (i j : @& Nat) : Array α :=
   if h₁ : i < a.size then
   if h₂ : j < a.size then swap a ⟨i, h₁⟩ ⟨j, h₂⟩
-  else panic! "index out of bounds"
-  else panic! "index out of bounds"
+  else a
+  else a
 
 @[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
   let e := a.get i