missing `Array.insert`

Stream: general

[Asei Inoue]

I think this function is missing in the libraries.
PR welcome?

variable {α : Type}

/--
By swapping elements of the array one by one,
move `xs[old_idx]` to the position `xs[new_idx]`
while preserving the relative order of all other elements.
-/
def Array.insert (xs : Array α) (old_idx new_idx : Nat) (hold: old_idx < xs.size := by decide) (hnew : new_idx < xs.size := by decide) : Array α := Id.run do
  let mut vec := xs.toVector
  if old_idx > new_idx then
    for hi : i in 0...(old_idx - new_idx) do
      vec := vec.swap (old_idx - i) (old_idx - i - 1)
  if old_idx < new_idx then
    for hi : i in 0...(new_idx - old_idx) do
      vec := vec.swap (old_idx + i) (old_idx + i + 1)
  return vec.toArray

#guard #[3, 1, 4, 15, 9, 2].insert 5 2 = #[3, 1, 2, 4, 15, 9]
#guard #[3, 1, 4, 15, 9, 2].insert 1 4 = #[3, 4, 15, 9, 1, 2]

[Shreyas Srinivas]

If we had this function, we would also have Array.push. Both would be O(n) operations.

[Henrik Böving]

We have Array.push?

[Shreyas Srinivas]

sorry. I wanted to say Vector.push. Same issue.

[Shreyas Srinivas]

I saw vector operations in the code

[Robin Arnez]

I suppose you mean something different because we do have docs#Vector.push​?

[Shreyas Srinivas]

When I wrote Vector, we decided not to add push

[Shreyas Srinivas]

The reasoning was that Vector and Array are meant to provide efficient API and we should not let users footgun themselves

[Shreyas Srinivas]

I am guessing that line of reasoning is not valid anymore

[Robin Arnez]

Uhh Array.push and Vector.push is O(1), do you mean "Array.cons" / "Vector.cons"?

[Shreyas Srinivas]

Right sorry cons.

[Shreyas Srinivas]

I apologise, I am a bit scatter-brained right now

[Asei Inoue]

The insert function is something that is needed when trying to implement insertion sort on arrays, and I think it is also useful as a building block for other functions. Having this function and its properties available in the library would be valuable, even if it is not particularly efficient.

[Shreyas Srinivas]

then maybe you want to make cslib PR? But yeah I can also see some uses for this function. Another place to make this PR might be batteries

[Asei Inoue]

I think Batteries is better

[Robin Arnez]

I'll just note that the name Array.insert gives me more an impression that you insert a new element but really, you're only moving the values around. So a better name would probably be something like Array.move (which I suppose would be a more efficient way to do (xs.eraseIdx old_idx).insertIdx new_idx xs[old_idx]?)

[cmlsharp]

Do any other languages have an operation like this in their standard libraries?

The closest I can think of is std::rotate in C++ which I think(?) is a generalization of this? Edit: Rust vectors also have rotate_left and rotate _right.

[Eric Wieser]

std::rotate was also what came to mind for me

[Eric Wieser]

Would a signature like

def SubArray.rotate (a : Subarray X) (i : Nat) : Subarray X

make sense, where the underlying docs#Subarray.array contains the updated value?

[cmlsharp]

I think the way a lot of Array functions currently work is that the primary method is defined on Array with optional start/stop index parameters, and then the subarray functions are defined in terms of those. My understanding (@Henrik Böving please correct me if I'm wrong) is that this is an API concession to ensure you can avoid allocating a 'Subarray' structure if you don't need to/if the compiler can't infer you don't need to.

So given that maybe something like

def Array.rotate (a : Array x) (i : Nat) (start := 0) (stop := a.size) : Array x

(which then SubArray.rotate is defined in terms of)
You could also consider making i an Int to let you write left and right rotations in an ergonomic way. (the actual implementation should probably select whichever direction leads to fewer swaps though). That's not necessary of course, but it's a bit nicer than stop - i