The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

On Thu, Sep 11, 2008 at 10:56:01AM +0200, AUGER Cédric wrote:
> I had some problem with Extraction function,
> Records are known to be non-recursive in Coq,
> but in CaML, we can use recursive records such as:
> 
> type foo = Foo | Foobar of bar
> and bar = {x : foo; y : bool}
> 
> this type is "inductively" correct, as "proven" in the Coq term:
> 
> Require Import Bool.
> 
> Inductive foo : Set :=
> | Foo : foo
> | Foobar : bar -> a
> with bar : Set :=
> | Build_bidule : foo -> bool -> bar
> .
> 
> but the extracted type is not a Record (hopefully, since
> we didn't provided the field names), and I want it to be
> a Record, so a mechanism such as:
> 
> Require Import Bool.
> 
> Inductive foo : Set :=
> | Foo : foo
> | Foobar : bar -> a
> with bar : Set :=
> | Build_bidule : foo -> bool -> bar
> as Record [ x y ]
> .
> would be usefull to change easily the status of an Inductive type
> 
> (maybe not as readable as
> 
> Inductive foo : Set :=
> | Foo : foo
> | Foobar : bar -> a
> with bar : Set :=
> | Build_bidule : {x : foo; y : bool} as Record
> .
> or so...)
> 
> I do not really know what problems can be encountered;
> I believe this is just a flag to set in Coq to be extracted
> as record type.
> 
> For other languages, such as Haskell, as I don't know them,
> I don't know if it is problematic.
> 
> Am I wrong and have to do without those Record or could it
> be implemented and added to Coq features?

At first view, your proposition is feasible. You may wish to fill a
feature wish at https://logical.futurs.inria.fr/coq-bugs, if ever some
developer has time to work on it. Alternatively, I wonder whether
cocorico may host a "feature wish" section that, compared to coq-bugs,
would have a better visibility and provide better opportunities for
elaboration (as suggested in May 29 "Coq Feature Requests" mail to this
list).

Hugo Herbelin