The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Ah, it's clear now; thanks, I will try.

Sincerely,
Kirill Taran

On Sat, Feb 22, 2014 at 5:25 PM, Rui Baptista <rpgcbaptista AT gmail.com> wrote:

Yes, you need to substitute [Parameter] with [Parameter Inline] for every parameter you want to inline. Some examples are at http://coq.inria.fr/stdlib/Coq.Structures.OrderedTypeEx.html.

Regards

On Sat, Feb 22, 2014 at 11:32 AM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

Cedric,

I am not sure. I tried that, but there are lines like Prelude.error "AXIOM TO BE REALIZED" in extracted code.
Maybe I haven't provided all module types with instances. I will check it.

Rui,

Have I type Parameter Inline for every parameter I want to inline?
(I didn't find manual page for this.)

Sincerely,
Kirill Taran

On Fri, Feb 21, 2014 at 5:29 PM, Cedric Auger <sedrikov AT gmail.com> wrote:

If I remember correctly, extraction to Haskell does not produce modules (mainly because there is no module Type equivalent in Haskell), so if you do not really care of the target language, you might exploit it.

2014-02-21 14:05 GMT+01:00 Rui Baptista <rpgcbaptista AT gmail.com>:

Hi,

Is [Parameter Inline] what you're looking for?

Regards, Rui Baptista

On Fri, Feb 21, 2014 at 12:56 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

Hello.

Is it possible to configure extraction such way that all modules will be eliminated from extracted code and parameters of them will be replaced with explicit extra arguments to functions?

E.g. this:

Module Type T.

Parameter P : Set.

End M.

(* In one file: *)

Module N := T nat. Import N.

Definition f : P := 1.
(* In other file: *)

Module B := T bool. Import N.

Definition f : P := true.

must become this:

(* In one file: *)

Definition f : nat := 1.
(* In other file: *)

Definition f : bool := true.

Sincerely,
Kirill Taran

--
.../Sedrikov\...