Загрузка и хранение файла во время компиляции с поставщиком типов - PullRequest
Новая
       10

Загрузка и хранение файла во время компиляции с поставщиком типов

0 голосов
/ 28 апреля 2018

Я хотел бы загрузить (двоичный) файл во время компиляции и сохранить его в переменной верхнего уровня типа Bytes: 

module FileProvider

import Data.Bits
import Data.Bytes
import Data.Buffer

%default total

export
loadImage : String -> IO (Provider Bytes)
loadImage fileName = do
    Right file <- openFile fileName Read
      | Left err => pure (Error $ show err)
    Just buf <- newBuffer size
      | Nothing => pure (Error "allocation failed")
    readBufferFromFile file buf size
    Provide . dropPrefix 2 . pack <$> bufferData buf
  where
    size : Int
    size = 256 * 256 + 2

Кажется, что работает правильно во время выполнения: 

module Main

import FileProvider
import Data.Bits
import Data.Bytes

main : IO ()
main = do
     Provide mem <- loadImage "ram.mem"
       | Error err => putStrLn err
     printLn $ length mem

Однако, если я попытаюсь запустить его во время компиляции, произойдет сбой с таинственным сообщением с упоминанием FFI: 

module Main

import FileProvider
import Data.Bits
import Data.Bytes

%language TypeProviders
%provide (mem : Bytes) with loadImage "ram.mem"

main : IO ()
main = do
     printLn $ length mem

$ idris -p bytes -o SOMain SOMain.idr 
Symbol "idris_newBuffer" not found
idris: user error (Could not call foreign function "idris_newBuffer" with args [65538])

Что здесь происходит и как я могу загрузить содержимое файла во время компиляции?

1 Ответ

0 голосов
/ 28 апреля 2018

idris_newbuffer - это функция C, используемая Data.Buffer. От документов до поставщиков типа :

Если мы хотим вызывать наши сторонние функции из интерпретируемого кода (такого как REPL или поставщик типов), нам нужно динамически связать библиотеку, содержащую нужные нам символы.

Таким образом, каждая функция, использующая FFI, должна иметь связанную динамическую библиотеку. Это было бы Data.Buffer и Data.ByteArray. Давайте сосредоточимся на первом и посмотрим, какие проблемы возникают:

Так что Data.Buffer требуется %dynamic "idris_buffer.so" (и не только %include C "idris_buffer.h", который у него есть в настоящее время). Вы можете скопировать idris/rts/idris_buffer.(h|c) и удалить функцию, которая требует другого rts-материала. Чтобы скомпилировать общую библиотеку, запустите: 

cc -o idris_buffer.so -fPIC -shared idris_buffer.c

При использовании модифицированного Data.Buffer вы все равно получите ошибку: 

Could not use <<handle {handle: ram.mem}>> as FFI arg.

Вызов FFI: Data.Buffer.readBufferFromFile. Аргумент File вызывает проблемы. Это потому, что Идрис видит, что используется openFile (еще одна функция C) и преобразует его в вызов Haskell . С одной стороны, это хорошо, потому что во время компиляции мы интерпретируем код Idris, и это делает следующие функции вроде readLine C / JS / Node /… agnostic. Но в этом случае, к сожалению, бэкэнд на Haskell не поддерживает дескриптор возвращаемого файла для вызовов FFI . Таким образом, мы можем написать еще одну fopen : String -> String -> IO Ptr функцию, которая делает то же самое, но имеет другое имя, поэтому Ptr останется Ptr, как это можно использовать в вызовах FFI.

С этим сделано, есть еще одна ошибка благодаря встроенным модулям: 

Could not use prim__registerPtr (<<ptr 0x00000000009e2bf0>>) (65546) as FFI arg.

Data.Buffer использует ManagedPtr в своем бэкэнде. И да, это также не поддерживается в вызовах FFI. Поэтому вам нужно изменить их на Ptr. Думаю, оба этих могут поддерживаться в компиляторе.

Наконец все должно работать для действительного %provide (mem : Buffer). Но нет, потому что: 

Can't convert pointers back to TT after execution.

Несмотря на то, что Idris теперь может читать файл во время компиляции, он не может сделать Buffer или что-либо еще с Pnt доступным для выполнения - и это вполне разумно. Наличие всего лишь указателя на то, когда программа была скомпилирована, является случайной вещью во время выполнения. Поэтому вам нужно либо преобразовать данные в результат в поставщике, либо использовать промежуточный формат, например Provider (List Bits8).

Я сделал короткий пример , чтобы List Bits8 был доступен в main. Buffer в основном Data.Buffer с _openFile и Pnt вместо ManagedPtr. Я надеюсь, что это поможет вам как-то, но, возможно, некоторые из людей, которые занимаются компиляцией, могут дать больше информации.

...