在编译时使用类型提供程序加载和存储文件答案

【问题标题】：Loading and storing a file at compile time with a type provider在编译时使用类型提供程序加载和存储文件
【发布时间】：2018-04-28 06:51:36
【问题描述】：

我想在编译时加载一个（二进制）文件并将其存储在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])

这里发生了什么以及如何在编译时加载文件的内容？

【问题讨论】：

标签： ffi compile-time type-providers idris

【解决方案1】：

idris_newbuffer 是 Data.Buffer 使用的 C 函数。来自docs to type providers：

如果我们想从解释代码（例如 REPL 或类型提供程序）中调用我们的外部函数，我们需要动态链接一个包含我们需要的符号的库。

所以每个使用 FFI 的函数都需要链接一个动态库。那是Data.Buffer 和Data.ByteArray。让我们专注于第一个，看看会出现什么问题：

所以Data.Buffer 需要%dynamic "idris_buffer.so"（而不仅仅是它目前拥有的%include C "idris_buffer.h"）。您可以复制 idris/rts/idris_buffer.(h|c) 并删除需要其他 rts-stuff 的功能。编译共享库运行：

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 参数会引起麻烦。这是因为 Idris 看到使用了 openFile（另一个 C 函数）并且 transforms it in a Haskell call。一方面这很好，因为在编译期间我们正在解释 Idris 代码，这使得像readLineC/JS/Node/...这样的函数是不可知的。但在这种情况下很不幸，因为 Haskell 后端不支持returned file handle for FFI calls。所以我们可以编写另一个 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) 这样的中间格式。

I made a short example 可以在main 中访问List Bits8。 Buffer 基本上是 Data.Buffer 包括 _openFile 和 Pnt 而不是 ManagedPtr。我希望这对您有所帮助，但也许一些编译器的人可以提供更多背景。

【讨论】：