2

我使用从 Coq 到 OCaml 的提取，其中我有 type Z, N,positive

我不用来提取它int不习惯从 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 类型，但 Coqstring与 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的提取在哪里。coqN_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？

4

1 回答 1

3

对于字符串，最简单的做法可能是ExtrOcamlString在提取文件中导入标准库模块，这将导致 Coq 将它们作为char listOCaml 中的 a 提取。然后，您可以使用自定义代码在char list和 native之间进行转换。string例如查看CompCertlib/Camlcoq.v发行版中的文件、函数和.camlstring_of_coqstringcoqstring_of_camlstring

于 2014-09-02T12:15:40.640 回答