Ivory: how to use the ivory-hw package

Question

I'm experimenting with Ivory (http://ivorylang.org, https://github.com/GaloisInc/ivory) and using the ivory-hw module to manipulate some registers in a microcontroller.

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"})

Building and running gives:

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

Adding the option scErrors = False to runCompiler turns sanity checks off and the code runs to completion generating sources.

However, main.c contains a call to ivory_hw_io_write_u32 but this function is not defined anywhere (perhaps explaining the error). Poking about github, I can find examples that have a file ivory_hw_prim.h.

After some experimentation, I can include this by adding a module for the hw stuff and then adding that as a dependency to my 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

and calling the runCompiler with hw_artifacts added to generate the header:

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

This adds ivory_hw_prim.h to the collection of files generated and includes the necessary include in main.h.

However, this only works by retaining the scErrors = False option to runCompiler which suggests that I am still not doing this right.

My question is therefore: What is the correct way to use Ivory's HW package?

Answer 1

The solution is to include hw_moduledef in the package:

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

(The depend function just includes the header.) Including hw_moduledef in the package "main" makes its definitions visible to the sanity-checker.

By the way, the Ivory module system may be improved in the future, so that Ivory computes, at compile time, the dependencies, relieving the programmer from having to make explicit includes.