ocaml - Ocaml 库中的 string_dec 和字符串

Question

我有文件：

• String0.ml提取自String.v（来自 Coq 库）

• String.ml：是Ocaml的字符串库

将我的测试文件从 Coq 提取到 Ocaml 后，我想String.ml在 Ocaml 的库中使用，所以我编写了一个替换命令将所有替换String0为String.

问题出在文件test.v中，我使用了以下定义之一：

Definition beq_string := beq_dec string_dec.

string_decOcaml 的库中没有这个函数，但 Coq 的字符串库中有

所以我编译的时候出错了test.ml

open String
let beq_string = beq_dec string_dec

错误：未绑定的值 string_dec

我想将 Ocaml 的字符串库用于我的所有提取文件。我怎样才能编译string_dec？

Answer 1

也提取string_dec函数。

beq_string如果您愿意稍微信任 OCaml 库，通过提取以使用字符串的内置相等性，您将获得更好的性能：

Extract Constant beq_string => "((=) : string->string->bool)".

Answer 2

创建一个 MyString.ml 模块，其中包含：

module String0 = struct
  include String
  let string_dec = function ... (* the definition of string_dec *)
end

在 Coq 生成的所有文件中，从

open MyString

然后，您无需重命名String0为String，它将使用 String 模块中定义的string_dec函数，以及您定义的函数。