OCaml字符串和Coq字符串(从Coq提取到OCaml)

Question

我使用了从Coq到OCaml的提取，其中有Z、N、positive类型。

我不需要在int of OCaml中提取它。

那么提取后的类型是：

type positive =
| Coq_xI of positive
| Coq_xO of positive
| Coq_xH

type coq_N =
| N0
| Npos of positive

type coq_Z =
| Z0
| Zpos of positive
| Zneg of positive

我在OCaml中有一个程序，其中一些函数使用OCaml类型的string。

在我的OCaml程序中，我需要编写一些转换类型的函数：string -> coq_N、string -> coq_Z、string -> positive

我尝试用Coq编写函数，然后使用提取来获得OCaml类型，但是Coq string与OCaml string不同。

例如：

open Ascii
open BinNums
open Datatypes

type string =
| EmptyString
| String of ascii * string

let string_of_coqN (s: string): coq_N =
  match s with
    | EmptyString -> N0
    | String (a, _) -> (coq_N_of_ascii a);;

其中coq_N_of_ascii是从coq函数N_of_ascii中提取的。

例如，当我应用函数string_of_coqN时：

let test (x: string) = string_of_N x;;

我接到的投诉是

Error: This expression has type string but an expression was expected of type
         String0.string

您能帮我找到一种编写转换函数的方法吗：string -> coq_N、string -> coq_Z和string -> positive。

Answer 1

对于字符串，最简单的方法可能是在提取文件中导入标准库模块ExtrOcamlString，这将导致Coq在OCaml中将它们提取为char list。然后可以使用自定义代码在char list和本机string之间进行转换。例如，查看CompCert发行版、函数camlstring_of_coqstring和coqstring_of_camlstring中的文件camlstring_of_coqstring。