如何将数组从 C/C++ 返回到 Idris？

Question

我想从 C/C++ 返回一个任意等级的数组给 Idris。我将 C++ 数组键入为 void*，并在 Idris 中相应地有一个 AnyPtr。在 Idris 中，我将这种 Array 类型定义为嵌套的 Vect：

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

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

但我不知道如何将AnyPtr 转换为Array。我已经到了

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

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

编辑我将元素类型固定为Int，因为它简化了问题而不会丢失重要的细节。

Answer 1

注意：假设数组形状可在 Idris 中访问。

获取一个数组

我们可以返回一个指向数组开头的AnyPtr，然后编写一个在数组上递归获取每个点的元素的函数。

例如（警告 - 未经过充分测试），

-- 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

与

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()
}

传递一个数组

您可以在 C/C++ 中创建一个适当大小的数组，返回指向该数组的指针，然后执行与上述相同的操作，递归地将 Idris 数组的每个元素分配给 C/C++ 数组。