从Coq中提取时,您能自动添加Haskell导入语句吗？

Question

我正在从Coq提取到Haskell,需要在Haskell端导入几个模块.是否有任何Coq提取功能允许您自动执行此操作？我知道我可以写一个脚本来做这件事,但我宁愿不必重新发明轮子.

Answer 1

没有，这是非常可悲的。

我们通过添加多个导入 ( fiximports.py ) 的 Python 脚本解决了这个问题，但这需要使用 Haskell 预处理器（通过传递-F -pgmF fiximports.pyto来使用它ghc）并导致未使用的导入警告，而且不是很优雅。

我认为问题在于这些导入对于 OCaml 提取来说是不必要的，并且该功能尚未针对 Haskell 提取进行设计和实现。