2

Coq から OCaml への抽出を使用しまし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 type を使用する関数がいくつかある 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

convert 関数 :string -> coq_Nとstring -> coq_Zを書く方法を教えてくださいstring -> positive。

4

1 に答える 1

3

文字列の場合、おそらく最も簡単な方法はExtrOcamlString、抽出ファイルに標準ライブラリ モジュールをインポートすることです。これにより、Coq は文字列char listを OCaml として抽出します。その後、カスタム コードを使用してchar listとネイティブの間で変換できます。stringたとえばlib/Camlcoq.v、CompCertディストリビューションのファイル、関数camlstring_of_coqstring、および を見てくださいcoqstring_of_camlstring。

于 2014-09-02T12:15:40.640 に答える