Используйте функции C в Idris

Question

Idris может компилировать .idr в C-код (JS, NodeJS).Можно ли сделать это в обратном направлении - скомпилировать C-код в формат Idris?Или, может быть, использовать функции C напрямую в коде Idris?

Answer 1

Конечно!Взгляните на интерфейс внешней функции (FFI) .Основываясь на вашей цели компиляции (например, C, JavaScript, ...), вы можете использовать встроенные функции, такие как этот пример вызова void *fileOpen(char *path, char *mode) внутри монады IO:

do_fopen : String -> String -> IO Ptr
do_fopen f m
   = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m