where is `reshapeEquiv` function?

[Seasawher]

Thank you for creating awesome library and document!

I'm reading this document and find a following description:

The reshape function is also a concrete instance of the more general function reshapeEquiv, which reshapes an array of size I to an array of size J by an arbitrary equivalence I ≃ J:

def reshapeEquiv (x : Float^[I]) (ι : I ≃ J) : Float^[J] := ...

This function allows you to reshape an array and perform various permutations of its data.

The reshape function is implemented with the reshapeEquiv function via the natural equivalence between two index types I and J, where you first convert i : I to a flat index toFin i : Fin (card I) and then convert it back to a structured index J by fromFin (toFin i) : J.

at: https://lecopivo.github.io/scientific-computing-lean/working-with-arrays/basics.html#reshaping-arrays

but I can't find reshapeEquiv function in the sciLean repository.

[lecopivo]

I wrote some parts without the code existing and working :) I didn't fix this yet and I should rewrite the section.

It could be defined as:

variable {I J : Type} [IndexType I] [IndexType J]
def reshapeEquiv (x : Float^[I]) (eq : I ≃ J) : Float^[J] := ⊞ j => x[eq.symm j]

but I don't think this is a good definition as it allocates new memory. Ideally I should create a view on the old memory that just recomputes the index on the fly.

I should define type synonym:

def ArrayView (C : Type) {Elem I J} [ArrayType C I Elem] (eq : I ≃ J) := C

with instance

instance (C : Type) {Elem I J} [ArrayType C I Elem] (eq : I ≃ J) : ArrayType (ArrayView C eq) J Elem := ...

i.e. assuming you have an array c : C with indices I and elements Elem you can view it as array with indices J if you provide a bijection between the index types eq : I ≃ J . Then the function reshapeEquiv would be

variable {I J : Type} [IndexType I] [IndexType J]
def reshapeEquiv (x : Float^[I]) (eq : I ≃ J) : ArrayView (Float^[I]) eq := x