ocaml - Coqの抽出メカニズムを使用して、CoqのファンクターをOCamlに抽出します

Question

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

Definition PolyInterpretation := forall f : Sig, poly (arity f).

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

Module Type TPolyInt.
  Parameter sig : Signature.
  Parameter trsInt : PolyInterpretation sig.
  Parameter trsInt_wm : PolyWeakMonotone trsInt.
End TPolyInt.

Module PolyInt (Export PI : TPolyInt).

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

Module TPolyInt_imp.
 Variable arity : symbol -> nat.
 Variable l : list {g : symbol & poly (arity f).
 Definition sig := Sig arity.
 Definition trsInt f := fun_of_pairs_list f l.
 ...
End TPolyInt_imp.

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

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

Module Export P := PolyInt TPolyInt_imp.

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

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

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

Extraction Language Ocaml.
Set Extraction Optimize.
Set Extraction AccessOpaque.
Separate Extraction rainbow.P.

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

抽出後のコードはこちら

module TPolyInt_imp = 
 struct 
  (** val arity : symbol -> int **)
  
  let arity =
    failwith "AXIOM TO BE REALIZED"
  
  (** val l : (symbol, poly) sigT list **)
  
  let l =
    failwith "AXIOM TO BE REALIZED"
  
  (** val coq_sig : coq_Signature **)
  
  let coq_sig =
    coq_Sig arity
  
  (** val trsInt : symbol -> poly **)
  
  let trsInt f =
    fun_of_pairs_list arity f l
 end

module P = PolyInt(TPolyInt_imp)

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

Module Type Arity.
 Variable arity : symbol -> nat.
 Variable l : list {g : symbol & poly (arity g)}.
End Arity.

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

Module S (Import A: Arity).

  Module TPolyInt_imp.
    Definition sig := Sig arity.
    Definition trsInt f := fun_of_pairs_list f l.
    ...
  End TPolyInt_imp.

  Module P := PolyInt TPolyInt_imp.

End S.

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

Extraction Language Ocaml.
Set Extraction Optimize.
Set Extraction AccessOpaque.
Separate Extraction S.

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

Error: Signature mismatch:
       ...
       Values do not match:
         val trsInt : Cpf0.symbol -> Polynom.poly
       is not included in
         val trsInt : APolyInt.coq_PolyInterpretation
       File "rainbow.ml", line 534, characters 8-14: Actual declaration

抽出後のコード:

module type Arity = 
 sig 
  val arity : symbol -> int
  val l : (symbol, poly) sigT list
 end

module S = 
 functor (A:Arity) ->
 struct 
  module TPolyInt_imp = 
   struct 
    (** val coq_sig : coq_Signature **)
    
    let coq_sig =
      coq_Sig A.arity
    
    (** val trsInt : symbol -> poly **)
    
    let trsInt f =
      fun_of_pairs_list A.arity f A.l
   end
  
  module P = PolyInt(TPolyInt_imp)
  

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

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

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