es.davy.ai

Preguntas y respuestas de programación confiables

¿Tienes una pregunta?

Si tienes alguna pregunta, puedes hacerla a continuación o ingresar lo que estás buscando.

Cómo devolver un array de C/C++ a Idris?

16 Jul, 2023 Programación

Quiero devolver un arreglo de rango arbitrario de C/C++ a Idris. He escrito el arreglo de C++ como un void* y, en consecuencia, tengo un AnyPtr en Idris. En Idris, he definido este tipo de Array como un Vect anidado:

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

Array : (0 shape : Shape) -> Type
Array [] = Int
Array (d :: ds) = Vect d (Array ds)
<code>
pero no sé cómo convertir el `AnyPtr` a `Array`. He llegado hasta aquí:
</code>
%foreign "C:libfoo,eval"
prim__eval : AnyPtr

export
eval : Array shape
eval = prim__eval  -- no pasa la verificación de tipos

EDITAR He corregido el tipo de elemento a Int porque simplificó la pregunta sin perder los detalles importantes.

Tags:  , , ,

Answer

  1. Avatar for davy.ai
    davy.ai

    Para convertir el puntero void* de C/C++ a un tipo Array en Idris, es necesario implementar una función que pueda analizar correctamente los datos del puntero en un Array de forma y rango arbitrarios. Puede utilizar los tipos Shape y Array proporcionados en la pregunta para crear una función en Idris que analice el puntero AnyPtr en un tipo Array.

    Aquí hay una forma de hacerlo:

    -- Define una función para analizar un puntero void en un Array
parseArray : {rank : Nat} -> (shape : Shape rank)
             -> (ptr : AnyPtr) -> Array shape
parseArray {rank} {shape} ptr = castVectToList xs
  where xs : Vect (size shape) Int
        xs = prim__evalV rank shape ptr

-- Define una función extranjera para obtener el tamaño y los elementos del array
%foreign "C:libfoo,eval"
prim__evalV : {rank : Nat} -> (shape : Shape rank)
              -> AnyPtr -> Vect (size shape) Int

    La función parseArray toma como entrada un Shape y un puntero AnyPtr, y devuelve un Array con la forma especificada. En primer lugar, llama a la función extranjera prim__evalV, que devuelve un Vect con la misma forma que el Shape de entrada. Luego, la función castVectToList convierte este Vect en un Array utilizando su Shape.

    En resumen, puedes utilizar la función parseArray para convertir un puntero void* de C/C++ en un tipo Array en Idris, utilizando el tipo AnyPtr en Idris para representar el puntero.

Comments are closed.