io - 通过 ynot 在 Coq 中进行文件 I/O

Question

有没有人有一小段代码可以在 Coq 中从文件中读取字符串(ynot 库似乎可以做到这一点，但我无法弄清楚)？

Ynot 可以在这里找到:http://ynot.cs.harvard.edu/该发行版在示例中包含一个 IO 目录，其中包括定义如下内容的 FS.v:

Fixpoint ReadFile (fm : fd_model) (ms : list mode) (fd : File fm ms) (str : string) {struct str} : Trace :=  
   match str with  
       | EmptyString => Read fd None :: nil  
       | String a b => (ReadFile fd b) ++ (Read fd (Some a) :: nil)  
   end.

但我不知道如何调用它。

我试过这样的事情:

Eval compute in ReadFile (File (FileModel "demo.txt") [R]).  
                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^  
Error: The term "File (FileModel "demo.txt") [R]" has type "Set" while it is expected to have type "File ?16 ?17".

类似地，Quark 项目 ( http://goto.ucsd.edu/quark/ ) 定义了具有替代机制的 VCRIO.v。

如有任何帮助，我们将不胜感激!

Answer 1

一般来说，您将无法直接在 Coq 中执行文件 I/O，原因很简单，因为底层语言 Gallina 是纯粹而完整的。

特别是，您正在查看的函数 ReadFile 不是一个读取文件的函数，而是一个计算由读取文件的操作生成的跟踪的函数。

我们在 Quark(及其后继项目 Reflex http://goto.ucsd.edu/reflex)中解决这个问题的方法是将这些有效的行为公理化，例如参见 https://github.com/UCSD-PL/kraken/blob/master/reflex/coq/ReflexIO.v来自第 323 行，用于我们原语的公理化类型。

因此，在 Coq 方面，我们推断使用这种一元有效类型，然后一旦代码被提取，这些公理就会用适当类型的 OCaml 函数实现，请参见此处 https://github.com/UCSD-PL/kraken/blob/master/reflex/ml/primitives/ReflexImpl.ml第 111 行。

这显然增加了您的可信计算基础，因为您需要确保您的原语完全按照您公理化的方式行事，而不是更多。

---

回顾一下，我们无法在 Gallina 本身中执行有效的操作，因此我们将这些操作公理化，只能使用提取的 OCaml 代码真正执行它们。

我不知道有什么技术可以让您在 Gallina 中使用丰富的类型来执行这些操作。