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.
Open questions:
- what if the user do both
use
anduse ghost
? - what if the user do
use ghost
on a module with toplevel side effects?