問題タブ [coq-extraction]

tmpcoq から ocaml に抽出した後に生成されるフォルダーがあります。

main.mlで 1 つの関数を呼び出すために使用するファイルですcpf0。

Cpf0.proofバインドされていないというエラーが表示されました。使用しようとしました: (proofに存在しCpf0ます)。

同じエラーが発生しました。

Ocaml リンク:ocamlc -I tmp -c main.ml

受け入れない理由がわかりませんCpf0か？

しかし、open Cpf0;;単独では、リンクしてもエラーは発生しません。の別のファイルでテストしましたtmpが、そのファイルのすべての機能を使用できます。

私はファイルを持っています：

• String0.mlから抽出しましたString.v（Coqライブラリからです）

• String.ml: Ocamlの文字列ライブラリです

テストファイルを Coq から Ocaml に展開した後、Ocaml のライブラリで使用したいので、すべてをString.mlに置き換える置換コマンドを作成します。String0String

問題はファイルtest.vにあります。定義の1つを使用しました：

関数string_decは Ocaml のライブラリにはありませんが、Coq の文字列ライブラリにはあります

そのため、コンパイル時にエラーが発生しますtest.ml

エラー: バインドされていない値 string_dec

すべての抽出ファイルに Ocaml の文字列ライブラリを使用したいと考えています。どうすればコンパイルできますstring_decか?

私は抽出変換natを行っていますbig_int

ライブラリを使用したとき: ExtrOcamlNatBigInt、正しい型を返しませbig_intんOcaml

nat_caseだから私はそれを修正します（ファイルExtrOcamlNatBigInt）が、Ocamlのライブラリには function がないため、関数を定義する方法が見つかりBig_intませんnat_case。

nat_casebyの 2 番目の定義を定義しようとしています。

2 番目の定義を使用した後の結果を次に示します。

n次の行でエラーが発生しましたelse f0 (n - one):

ファイル "Datatypes.ml"、68 行目、51 ～ 52 文字目: エラー: この式には Big_int.big_int 型がありますが、int 型の式が予期されていました

minus( -) のせいだと思います。

minus抽出も変更します：

nat_caseの関数を定義するのを手伝ってくれませんBig_intか? どうもありがとうございました。

こんにちは、Coq から Ocaml への抽出を書いています。型を変換したいと思います。

しかし、私はタイプを維持したいZですint

これらの条件を抽出するために私が行っているコードは次のとおりです。

Coq のライブラリ ( BinInt.v )でZ -> int定義されているため、保持することはできません。Z

エラーが発生しました: (function coq_Zdouble_plus_one)

ファイル「BinInt.ml」、38 行目、4 ～ 5 文字目:

エラー: この式は int 型ですが、式は int32 型である必要があります

を抽出すればZ -> int32OKですが、私が望むものではありません。

このモジュール内にモジュール構造があり、内部の関数の変数の使用を宣言していますmodule A。

次に、抽出メカニズムを使用します。

あるいは単に

「抽出されたコードでは、次の公理を実現する必要があります: Aa」という警告付きのコードが生成されました。

ここaで、failwith "AXIOM TO BE REALIZED" I could't run my function success due to thisを受け取りましたfailwith

aモジュール内で変数を使用する必要があるためです。failwith抽出後に生成されないモジュールを定義する方法はありますか? failwithまたは、この関数を生成しない抽出と関係がありますか?

関数がありますPolyInterpretation（http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt.html）

およびモジュール署名TPolyInt( http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt_MA.html )

次に、私のファイルで、ファンクターを使用rainbow.vするモジュールのTPolyInt_imp目的を定義しますPolyInt

タイプがある場所fun_of_pairs_list:forall f: Cpf0.symbol, list {g : symbol & poly (arity g)} -> poly (arity f)

次に、モジュールを定義しますP。

証明アシスタントは上記Coqの定義を受け入れましたP。

次に、抽出を使用してに抽出しましたOCaml。

私はそれを別のファイルに書きます：extraction.v

それは正常に動作します。

抽出後のコードはこちら

ファンクター内にTPolyInt_impを含めVariableて生成したfailwith AXIOMため、これらすべての変数を含む新しい署名を定義することにしました。

Arity次に、( ) をパラメーターとして取る新しいファンクターを定義します。そして、このファンクター内でモジュールを定義しますTPolyInt_imp(TPolyInt_imp以前と同様)。

次に、抽出を使用してに抽出しOcamlます。

次に、次のようなエラーが表示されました。

抽出後のコード:

抽出の何が問題になっていますか？そして、彼らがこのエラーを抱えている理由は? 抽出後に正常にコンパイルできるようにコードを修正するにはどうすればよいですか?

また、署名を実装する新しいモジュールを定義したくありませんArity。

私のコードにタイプがなく、コンパイルできないことをとても残念に思っています。私は自分の問題の考えを伝えようとしています。

foo関数をファイルCoqに抽出したい。OCaml私の実際の関数は を使用する必要があるためRecursive Extraction、プログラムを実行すると、抽出された OCaml コードが に出力されますcmd。しかし、たとえば次のようにファイルに出力したいと思います。foo.ml

私が試したとき：

またRecursive Extraction foo "foo.ml"

エラーが発生しました：Syntax error: "." expected after [vernac:command] (in [vernac_aux]).

私の質問は次のとおりです。構文fooを使用して関数をファイルに抽出できますか? Recursive Extractionご協力ありがとうございました。

Coq から OCaml への抽出を使用しましZたN。positive

int私はOCamlでそれを抽出するために使用しません。

次に、抽出後のタイプは次のとおりです。

OCaml type を使用する関数がいくつかある OCaml のプログラムがありstringます。

私の OCaml プログラムでは、型を変換するいくつかの関数を書く必要があります: string -> coq_N, string -> coq_Z,string -> positive

Coq で関数を書き込もうとして、抽出を使用して OCaml 型を取得しましたが、Coqstringは OCaml とは異なりstringます。

例えば：

関数coq_N_of_asciiからの抽出はどこにありますか。coqN_of_ascii

string_of_coqNたとえば、関数を適用したとき：

という苦情が来ました

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