Ivory: как использовать пакет слоновой кости hw

Question

Я экспериментирую с Ivory (http://ivorylang.org, https://github.com/GaloisInc/ivory) и с помощью модуля ivory-hw для управления некоторыми регистрами в микроконтроллере.

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.

После нескольких экспериментов я могу включить это, добавив модуль для Hw материала, а затем, добавив, что в зависимости от моего 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 добавил генерировать заголовок:

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

ivory_hw_prim.h Это добавляет к коллекции файлов, созданных и включает в себя необходимые включают в main.h.

Однако это работает только при сохранении опции scErrors = False до runCompiler, которая предполагает, что я все еще не делаю этого правильно.

Мой вопрос заключается в следующем: Каков правильный способ использования пакета HW от Ivory?

Answer 1

Решение состоит в том, чтобы включить hw_moduledef в пакете:

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

(. depend функция включает в себя только заголовок) Включая hw_moduledef в пакете "main" делает ее определения видимым для здравомыслия-проверки.

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