c++ - 如何将数组从 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++ 数组。