The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Fri, 4 Jun 2004, François Armand wrote:

...
>      and coq_R = Impl.coq_R = { r1 : coq_T1; r2 : coq_T1; }
...
> is not included in
...
>      and coq_R = Coq_mkr of coq_T1 * coq_T1

First, thanks for the bug report. This is in fact a known problem about
extraction of records. The issue is that records, after their definition,
are seen by the Coq system as regular inductive types. The fact that they
have been defined as records is only stored in one particular table, and
that table is not very module-friendly for the moment.

As a consequence, in the Module, the extraction is able to conclude
that R has been defined as a record, hence the coq_R = { ... }.
But in the Module Type, the extraction isn't able to see that R is a
record, hence the coq_R = Coq_mkr of ...

The problem is even more general that this question of record detection.
The following code is legal in Coq:

------------------------------------------------------------------------
Module Type S.
 Inductive T : Set := Build_T : nat -> nat -> T.
End S.

Module M:S.
 Record T : Set := { A : nat; B : nat}.
End M.
------------------------------------------------------------------------

If the extraction still relies on the "Inductive" vs. "Record" annotation,
it will generate wrong code, with a mismatch between signature and
implementation.

As long as records are syntactic sugar in Coq whereas they aren't in
Ocaml, it will not be possible to find a satisfactory solution to the
record extraction problem. I have a plan to add a "tag" to the coq
inductive types structure to store the "Record or Non-Record" status, in
the same way as there is a "tag" to store the "Infinite (CoInductive) or
Finite (Inductive)" status. But this change will have consequences outside
the extraction domain, so it needs to be discussed first.

I will inform you when the problem has been solved. In the meanwhile, you
can avoid the problem by disactivating the record detection and extraction.
In Coq source file contrib/extraction/extraction.ml, at line 345, remove
for example the "if l = [] then", leaving only the "raise (I Standard);",
and recompile Coq.

Pierre Letouzey