6

I have a function PolyInterpretation (http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt.html)

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

and a module signature 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).

Then in my file rainbow.v, I define a module TPolyInt_imp purpose to use functor 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.

Where fun_of_pairs_list has type: forall f: Cpf0.symbol, list {g : symbol & poly (arity g)} -> poly (arity f)

Then I define a module P:

Module Export P := PolyInt TPolyInt_imp.

The Coqproof assistant accepted the definition P above.

Then I used extraction to extract to OCaml.

I write it in another file: extraction.v

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

It works fine.

Here is the code after the extraction

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)

Because inside the functor TPolyInt_imp they included Variable and generate the failwith AXIOMthen I decided to define a new signature to contain all those variables.

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

Then define a new functor taking (Arity) as a parameter. And inside this functor I define module TPolyInt_imp (like TPolyInt_imp before).

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.

Then I use the extraction to extract it to Ocaml.

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

Then I got an error saying that:

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

The code after the extraction:

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)

What is wrong with the extraction? and the reason why they have this error? How can I correct my code that I can get the success compile after the extraction?

Also I do not want to define a new module that implement the signature Arity.

I am so sorry for my code lacking of type and not able to compile. I am trying to give the idea of my problem.

ghilesZ
  • 1,502
  • 1
  • 18
  • 30
Quyen
  • 1,363
  • 1
  • 11
  • 21
  • What is the definition of `Sig` (used in your `TPolyInt_imp` module)? – Arthur Azevedo De Amorim Mar 23 '13 at 14:15
  • Record Signature : Type := mkSignature { symbol :> Type; beq_symb : symbol -> symbol -> bool; beq_symb_ok : forall x y, beq_symb x y = true <-> x = y }. Definition Sig (arity:symbol -> nat) := mkSignature arity beq_symbol_ok. (http://color.inria.fr/doc/CoLoR.Term.Varyadic.VSignature.html#Signature) – Quyen Mar 23 '13 at 15:52
  • OK... How was the definition of `PolyInterpretation` extracted? It seems that erasure is causing the two types not to be unifiable anymore, even though that shouldn't happen... – Arthur Azevedo De Amorim Mar 24 '13 at 15:49
  • type coq_PolyInterpretation = symbol -> poly; module type TPolyInt = sig val coq_sig : coq_Signature val trsInt : coq_PolyInterpretation end – Quyen Mar 25 '13 at 01:45

0 Answers0