如何从 coq 写入文件

Question

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

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

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

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

Answer 1

您可以使用RedirectwithEval来接近：

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来实现。