The Coq mailing list

[Trevor Elliott <awesomelyawesome AT gmail.com>]

Hi Pierre,

>> 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.
>
> One more time, this sounds quite right. The semantic of Extract Constant
> is to change the _body_ of the concerned constant, but not the call sites:

I think that my description failed a bit here :)

When doing recursive extraction, I see no mention of (*) or (+), and
the full bodies of mult and plus added to my resulting program.  It's
fine with me if this is the expected behavior, my only problem is the
difference between the OCaml and Haskell extractions.  When extracting
to OCaml, i get something like this:

> let rec mult = (*)

whereas when extracting to Haskell, I get the following, even when I
have Extract Constant mult => "(*)":

> mult :: Prelude.Int -> Prelude.Int -> Prelude.Int
> mult n m =
>  (\f0 fS n -> if n Prelude.<= 0 then f0 () else fS (n Prelude.- 1))
>    (\_ -> 0)
>    (\p -> plus m (mult p m))
>    n

--trevor