The Coq mailing list

[Fran�ois Armand <armand AT iie.cnam.fr>]

Hello Coq ml,

I have a problem with the Coq extraction of a module and its signature.
I try to extract this code in OCaml :

<-- code extraxt_error.v -->
Module Type SIG.
  Parameters (T1 T2  : Set).
  Record R : Set := mkr {
    r1 : T1 ;
    r2 : T2  }.
End SIG.

Module Impl <: SIG.
  Definition T1 := nat.
  Definition T2 := nat.
  Record R : Set := mkr {
    r1 : T1 ;
    r2 : T1  }.
End Impl.

Extraction "extract_error.ml" Impl.
<-- end code -->

The extraction seems to work fine, and I obtain two files :
"extract_error.ml" and "extract_error.mli".
But when I try to compile extract_error.ml, ocamlc returns this error :
<-- ocamlc error msg -->
The implementation extract_error.ml
does not match the interface extract_error.cmi:
Modules do not match:
  sig
    type coq_T1 = nat
    and coq_T2 = nat
    and coq_R = Impl.coq_R = { r1 : coq_T1; r2 : coq_T1; }
    val coq_R_rect : (coq_T1 -> coq_T1 -> 'a) -> coq_R -> 'a
    val coq_R_rec : (coq_T1 -> coq_T1 -> 'a) -> coq_R -> 'a
    val r1 : coq_R -> coq_T1
    val r2 : coq_R -> coq_T1
  end
is not included in
  sig
    type coq_T1 = nat
    and coq_T2 = nat
    and coq_R = Coq_mkr of coq_T1 * coq_T1
    val coq_R_rect : (coq_T1 -> coq_T1 -> 'a) -> coq_R -> 'a
    val coq_R_rec : (coq_T1 -> coq_T1 -> 'a) -> coq_R -> 'a
    val r1 : coq_R -> coq_T1
    val r2 : coq_R -> coq_T1
  end
Type declarations do not match:
  type coq_R = Impl.coq_R = { r1 : coq_T1; r2 : coq_T1; }
is not included in
  type coq_R = Coq_mkr of coq_T1 * coq_T1
<--- end ocamlc error msg-->

The problem seem to be linked with the extraction of R in the signature
: R becomes a pair while it's supposed to be a record.

What I am supposed to do to have my extracted code to compile ?

These are the files produced by extraction :

<-- extract_error.mli -->
type nat =
  | O
  | S of nat

module Impl :
 sig
  type coq_T1 = nat
  type coq_T2 = nat
  type coq_R =
    | Coq_mkr of coq_T1 * coq_T1

  val coq_R_rect : (coq_T1 -> coq_T1 -> 'a1) -> coq_R -> 'a1
  val coq_R_rec : (coq_T1 -> coq_T1 -> 'a1) -> coq_R -> 'a1
  val r1 : coq_R -> coq_T1
  val r2 : coq_R -> coq_T1
 end
<-- end extract_error.mli -->
<-- extract_error.ml -->
type nat =
  | O
  | S of nat

module Impl =
 struct
  type coq_T1 = nat

  type coq_T2 = nat

  type coq_R = { r1 : coq_T1; r2 : coq_T1 }

  (** val coq_R_rect : (coq_T1 -> coq_T1 -> 'a1) -> coq_R -> 'a1 **)

  let coq_R_rect f = function
    | { r1 = x; r2 = x0 } -> f x x0

  (** val coq_R_rec : (coq_T1 -> coq_T1 -> 'a1) -> coq_R -> 'a1 **)

  let coq_R_rec f = function
    | { r1 = x; r2 = x0 } -> f x x0

  (** val r1 : coq_R -> coq_T1 **)

  let r1 x = x.r1

  (** val r2 : coq_R -> coq_T1 **)

  let r2 x = x.r2
 end
<-- end extract_error.ml -->