Можете ли вы автоматически добавлять операторы импорта Haskell при извлечении из Coq?

Question

Я делаю извлечение из Coq в Haskell, которое требует импорта нескольких модулей на конец Haskell. Есть ли какая-либо функция извлечения Coq, которая позволяет делать это автоматически? Я знаю, что мог бы просто написать сценарий для этого, но я бы предпочел не изобретать велосипед в случае необходимости.

Answer 1

Нет, и это очень грустно.

Мы решили эту проблему с помощью скрипта Python, который добавляет несколько импортов ( fiximports.py), но для этого необходимо использовать препроцессор Haskell (вы используете его, передавая -F -pgmF fiximports.py в ghc) и приводит к неиспользованным предупреждениям об импорте, и не очень элегантно.

Я думаю, что проблема заключается в том, что этот импорт не нужен для извлечения OCaml, а функция не была разработана и реализована для извлечения на Haskell.