ocaml - Ocaml ライブラリの string_dec と string

Question

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

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

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

Definition beq_string := beq_dec string_dec.

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

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

open String
let beq_string = beq_dec string_dec

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

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

score 3 · Accepted Answer

関数も抽出しstring_decます。

OCaml ライブラリを少し信頼しても構わないと思っている場合は、抽出beq_stringして文字列に組み込みの等価性を使用することで、パフォーマンスが大幅に向上します。

Extract Constant beq_string => "((=) : string->string->bool)".

score 2 · Accepted Answer

以下を含む MyString.ml モジュールを作成します。

module String0 = struct
  include String
  let string_dec = function ... (* the definition of string_dec *)
end

Coqによって生成されたすべてのファイルで、次のように開始します

open MyString

String0次に、名前をに変更する必要はありません。Stringこれは、String モジュールで定義された関数と、定義した関数を使用しstring_decます。

2 に答える 2