The Coq mailing list

[Trevor Elliott <awesomelyawesome AT gmail.com>]

Hi Wouter,

> Using the following commands produces pretty much what I'd expect to see:
>
>> Extraction Language Haskell.
>> Extract Inductive Datatypes.nat => "Integer" ["0" "succ"]
>>   "(\fO fS n -> if n==0 then fO () else fS (n-1))".
>> Extract Inlined Constant plus => "(+)".
>> Extract Inlined Constant mult => "(*)".
>> Extraction fact_body.
>> Extraction fact.

This extracts the right program, but I think that's because it's not
trying to do anything with plus and mult.

> But using "Recursive Extraction fact" seems to generate too much code:
> it also produces code for mult and plus, which is exactly what the
> Extract Inlined Constant commands should avoid... Is that the same
> behaviour you're seeing?

Yes, Recursive Extraction is what is generating additional code for
plus and mult.  I've tried using Extract Inlined Constant for plus and
mult, but that just performs a global renaming of plus and mult to (+)
and (*) respectively.  Additionally, if I just use Extract Constant
for plus and mult, the rhs is never used in my recursively extracted
program; the symbol mult is still used in fact_body.

--trevor