0

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

Module A.

  Variable a : nat.   

End A.

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

Extraction Language Ocaml.   
Set Extraction Optimize.
Set Extraction AccessOpaque.
Extraction A.

あるいは単に

Extraction A.

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

type nat =
| O
| S of nat

module A = 
 struct 
  (** val a : nat **)

  let a =
    failwith "AXIOM TO BE REALIZED"
 end

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

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

4

1 に答える 1

1

ある時点で、 の値を指定する必要がありますA.a。Aに関して抽象化したい場合a、最も便利な方法は、OCaml で直接変換されているファンクタを使用することだと思います。

Module Type Param.
  Variable x: nat.
End Param.

Module A (Import P: Param).

  Definition a:=P.x.   

End A.

Extraction Language Ocaml.   
Set Extraction Optimize.
Set Extraction AccessOpaque.

Extraction "test.ml" A.

(もちろん、A計算を実行するには、結果の OCaml ファンクターをインスタンス化する必要があります)。

于 2013-03-07T08:45:15.400 に答える