OCaml的串和串Coq的（提取Coq的至OCaml的）

我用从Coq的至OCaml的，其中I有Z类型，N提取，positiveOCaml的串和串Coq的（提取Coq的至OCaml的）

我不使用，以提取它OCaml中的int。

然后我提取后具有的类型是：

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

我试着写在勒柯克的功能，然后用于提取得到OCaml的类型，但勒柯克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其中从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？

来源

2014-09-02 Quyen

对于字符串，最容易做的事情可能是在提取文件中导入标准库模块ExtrOcamlString，这会导致Coq在OCaml中将它们提取为char list。然后，您可以使用自定义代码在char list和原生string之间进行转换。看看lib/Camlcoq.v中的CompCert分布，功能camlstring_of_coqstring和coqstring_of_camlstring。

来源

2014-09-02 12:15:40

OCaml的串和串Coq的（提取Coq的至OCaml的）

回答

相关问题