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

Question

我用從Coq的至OCaml的，其中I有Z類型，N提取，positive

我不使用，以提取它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？

Answer 1

對於字符串，最容易做的事情可能是在提取文件中導入標準庫模塊ExtrOcamlString，這會導致Coq在OCaml中將它們提取爲char list。然後，您可以使用自定義代碼在char list和原生string之間進行轉換。看看lib/Camlcoq.v中的CompCert分佈，功能camlstring_of_coqstring和coqstring_of_camlstring。