Allow "use ghost Foo"
It might happen that one wants to use a module for specification and ghost code, but not for actual code (and a fortiori extraction). A good example is
int.Int which is ubiquitous in WhyML programs but not necessarily in extracted programs.
It would be good to have a way in the surface language to express and enforce that such a module is not meant to be actually used. Proposed syntax:
use ghost int.Int. This would also make the extraction a lot less adhoc with respect to these modules.
A possible implementation would be to flag the corresponding scopes as being restricted. Any symbol accessed through such a scope would be forbidden to occur in non-ghost code. The change in
Why3extract.use_fold would be trivial.
- what if the user do both
- what if the user do
use ghoston a module with toplevel side effects?