The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Sat, 7 May 2011 01:47:47 +0200,
Alexandre Pilkiewicz 
<alexandre.pilkiewicz AT polytechnique.org>
 a écrit :

> Dear list
> 
> I'm trying report some errors in my code by adding things like
> 
> Parameter error_badly_masked: unit -> unit.
> Extract Constant error_badly_masked => "Errors.error_badly_masked".
> 
> 
> Definition .....
>    let tt := error_badly_masked tt in
>    ....
> 
> But the extraction removes this call
> 
> Is it possible to forbid the extraction to remove call to parameters?
> 
> Thanks in advance
> 
> Alexandre

I suggest you to deactivate optimizations of the extractor:

Unset Extraction Optimize.

If you use "tt" in the rest of the code, that should do the trick,
else, you have to destructure it, to force the dependence to your
function call:

 Definition .....
    let tt := error_badly_masked tt in
    let () := tt in
    ....

But do you really need to perform some "Extraction constant ..."?
As P. Letouzey wrote in this list, it is an "unsafe" feature, you
really need some extra care if you want your code to be really correct.

As I guess you "error_badly_masked" is an exception raiser, you may
consider using an error monad. I am currently writting a short tutorial
on extraction that I hope to post on the cocorico wiki. I guess I am
not good at it, but it may be shorter for you (when it will be done)
than having a look at the Compcert Project (since it is a big project).

Here is a link if you want to take a look at this project on how to
manage errors.
http://compcert.inria.fr/doc/html/Errors.html