coq - 如何从 coq 写入文件

Question

这可能是一个奇怪的问题，因为 Coq 应该是一种纯函数式语言，但是 Extraction存在并且它显然有副作用，所以我假设可能有一个更基本的命令来输出一个字符串或一些常量到一个文件，像这样:

Extraction "file.txt" "hello"%string.

这可能吗？是否需要编写自定义提取器(我什至不知道这是否可能)？

这个问题的实际原因与 Coq 中已经存在的提取机制的动机有关，但假设我想输出 C 代码或其他当前不支持的代码。我仍然可以在 Coq 中编写函数 extract : Expr -> string对于我在归纳类型中形式化的自定义语法 Expr .我怎样才能把这个字符串放到一个文件中？

Answer 1

您可以使用 Redirect与 Eval接近:

Require Import String.
Open Scope string_scope.

Redirect "file.txt" Eval compute in "hello".

(* file.txt.out now contains:
     = "hello"
     : string
*)

或者，编写您的函数 extract在 Coq 中，然后使用提取机制提取 extract e一些 e感兴趣，最后编写一个 OCaml 程序，导入这个(字符串)常量并打印它。走这条路的原因是在 Coq 中构建字符串太慢以至于你可能无法运行 Eval compute extract e但是你也许可以在 OCaml 中运行它。然后，您还可以(以未经验证的方式)用 OCaml 原生字符串替换 Coq 字符串，这样这个过程实际上是有效的；通过导入 ExtrOcamlString 很容易做到这一点在提取前的 Coq 中。