通过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您正在查看的函数不是读取文件的函数,而是计算读取文件操作生成的跟踪的函数.

我们在夸克(及其后续项目Reflex http://goto.ucsd.edu/reflex)中解决这个问题的方法是对这些有效的行为进行公理化,例如参见https://github.com/UCSD-PL/kraken/ blob/master/reflex/coq/ReflexIO.v来自第323行的axiomatized类型的基元.

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

这显然会增加您可信赖的计算基础,因为您需要确保您的原语完全按照您的公理化而不再进行.

总而言之,我们无法在Gallina本身执行有效的操作,因此我们对这些操作进行公理化,并且只能使用提取的OCaml代码执行它们.

我不知道任何技术可以让你在Gallina内部使用丰富的类型.