Извлечь функтор из Coq в Ocaml, используя механизм извлечения Coq

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,

Мне очень жаль, что в моем коде отсутствует тип и я не могу его скомпилировать. Я пытаюсь дать представление о моей проблеме.