How to return an array from C/C++ to Idris?

I want to return an array of arbitrary rank from C/C++ to Idris. I've typed the C++ array as a void*, and correspondingly have an AnyPtr in Idris. In Idris, I've defined such an Array type as a nested Vect:

Shape : {0 rank: Nat} -> Type
Shape = Vect rank Nat

Array : (0 shape : Shape) -> Type
Array [] = Int
Array (d :: ds) = Vect d (Array ds)

but I don't know how to convert the AnyPtr to the Array. I've got as far as

%foreign "C:libfoo,eval"
prim__eval : AnyPtr

export
eval : Array shape
eval = prim__eval  -- doesn't type check

EDIT I fixed the element type to Int because it simplified the question without losing the important details.

Solution

Note: Assumes the array shape is accessible in Idris.

To get an array

We can return an AnyPtr which points to the beginning of the array, then write a function that recurses over the array getting the elements at each point.

For example (warning - not well tested),

-- we index with Int not Nat because we can't use Nat in FFI
%foreign "C:libfoo,index_int32"
indexInt : AnyPtr -> Int -> Int

%foreign "C:libfoo,index_void_ptr")
indexArray : AnyPtr -> Int -> AnyPtr

%foreign "C:libfoo,get_array"
getArray : AnyPtr

%foreign "C:libfoo,get_int32"
getInt : Int

rangeTo : (n : Nat) -> Vect n Nat
rangeTo Z = []
rangeTo (S n) = snoc (rangeTo n) (S n)

build_array : (shape : Shape {rank=S _}) -> AnyPtr -> Array shape
build_array [n] ptr = map (indexInt ptr . cast . pred) (rangeTo n)
build_array (n :: r :: est) ptr =
    map ((build_array (r :: est)) . (indexArray ptr . cast . pred)) (rangeTo n)

eval : {shape : _} -> Array shape
eval {shape=[]} = getInt
eval {shape=n :: rest} = map (build_array (n :: rest)) getArray

with

extern "C" {  // if we're in C++
    int32 index_i32(void* ptr, int32 idx) {
        return ((int32*) ptr)[idx];
    }

    void* index_void_ptr(void** ptr, int32 idx) {
        return ptr[idx];
    }

    int32 get_int32();
    void* get_array();
}

To pass an array

You can create an array of the appropriate size in C/C++, return a pointer to that array, then do the same as above, recursively assigning each element of the Idris array to the C/C++ array.