CODEWITHSUNDEEP
haskellcoqcoq-extraction
tlon
tlon

Reputation: 423

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

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.

Upvotes: 9

Views: 241

Answers (1)

Tej Chajed
Tej Chajed

Reputation: 3948

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.

Upvotes: 1

Related Questions