8

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.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
tlon
  • 413
  • 2
  • 6
  • I don't think there is. I looked for ages and couldn't find any and wrote a script for it myself. I really hope someone answers your question in the positive though. – Probie Apr 30 '18 at 14:56

1 Answers1

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.

Tej Chajed
  • 3,749
  • 14
  • 18
  • Is there a relevant issue on Coq's bugtracker? – Anton Trunov May 01 '18 at 21:52
  • I don't see such an issue. Feel free to open one, though! Note also https://github.com/coq/coq/blob/master/plugins/extraction/ExtrHaskellString.v#L11: `At the moment, Coq's extraction has no way to add extra import statements to the extracted Haskell code. You will have to manually add: [...]` – Jason Gross May 03 '18 at 04:29