haskell - 象牙色 : how to use the ivory-hw package

Question

我正在尝试使用 Ivory ( http://ivorylang.org 、 https://github.com/GaloisInc/ivory )并使用 ivory-hw 模块来操作微 Controller 中的一些寄存器。

cmain :: Def ('[] :-> ())
cmain  = voidProc "main" $ body $ do
  setReg regFoo $ do
    clearBit foo_bitbar
    setBit foo_bitbaz
  forever $ return ()

main_module :: Module
main_module = package "main" $ do
  incl cmain

main :: IO ()
main = runCompiler [ main_module ] [] (initialOpts {constFold = True, 
                                                    outDir = Just "out"})

构建和运行给出:

$ exe
*** Procedure main
    ERROR: [ No location available ]:
             Unbound value: 'ivory_hw_io_write_u32'
exe: Sanity-check failed!

将选项 scErrors = False 添加到 runCompiler 会关闭健全性检查，代码将运行至完成生成源。

但是，main.c 包含对 ivory_hw_io_write_u32 的调用，但该函数未在任何地方定义(也许可以解释该错误)。浏览 github，我可以找到包含文件 ivory_hw_prim.h 的示例。

经过一些实验，我可以通过添加硬件模块来包含它，然后将其作为依赖项添加到我的 main_module 中:

hw_module :: Module
hw_module = package "ivory_hw_prim" hw_moduledef

main_module :: Module
main_module = package "main" $ do
  depend hw_module
  incl cmain

并调用runCompiler并添加hw_artifacts来生成 header :

main = runCompiler [ main_module ] hw_artifacts (initialOpts {scErrors = False, 
                                                              constFold = True, 
                                                              outDir = Just "out"})

这会将 ivory_hw_prim.h 添加到生成的文件集合中，并在 main.h 中包含必要的包含内容。

但是，这只能通过保留 runCompiler 的 scErrors = False 选项来实现，这表明我仍然没有正确执行此操作。

因此，我的问题是:使用 Ivory 的硬件包的正确方法是什么？

Answer 1

解决方案是在包中包含hw_moduledef:

main_module :: Module
main_module = package "main" $
  incl cmain >> hw_moduledef

(depend 函数仅包含 header 。)在包 "main" 中包含 hw_moduledef 使其定义对理智可见 -检查器。

顺便说一句，Ivory 模块系统将来可能会得到改进，以便 Ivory 在编译时计算依赖项，从而使程序员不必进行显式包含。