Can you automatically add Haskell import statements when extracting from Coq?

Question

I'm doing an extraction from Coq to Haskell that requires importing a couple of modules on the Haskell end. Is there any Coq extraction feature that allows you to do this automatically? I know I could just write a script to do this but I'd prefer to not reinvent the wheel if necessary.

Answer 1

There isn't, and it's very sad.

We've solved this problem with a Python script that adds several imports (fiximports.py), but this requires using the Haskell preprocessor (you use it by passing -F -pgmF fiximports.py to ghc) and results in unused imports warnings, and isn't terribly elegant.

I think the issue is that these imports are unnecessary for OCaml extraction, and the feature hasn't been designed and implemented for Haskell extraction.