Extraction using a driver on the extracted file
I am trying to use why3extract
and a custom driver to extract a Why3 module that would partly depends on an OCaml implementation. I cannot manage to use the driver to change the extraction of this module with the driver.
My file a.mlw
is as follows:
module A
type a
val eq_elt (e1 e2: a) : bool
ensures { e1 = e2 <-> result}
end
I took the driver ocaml64.drv
which I copied (into driver/ocaml_ext.drv
and added the following at the end:
module a.A
syntax val eq_elt "TODO"
end
I tried to extract with the following command:
why3 extract --modular -D driver/ocaml_ext.drv a.mlw -o todo1
I first get:
Library file not found: a
So, I added the option "-L ." to workaround this problem then the driver is read with no problems but, during printing, I get:
Symbol eq_elt cannot be extracted
I looked in more details and it seems that in this case, the extraction reads the file a.mlw
twice: once as a library which is used to fill the syntax map during the driver parsing; and once during the printing of the file a.mlw
. This leads to the element eq_elt
being generated twice and the extraction using the second one instead of the first when trying to query the syntax map.
I have a solution which would ensures that this cannot happen by calling both the file and the libraries with the same memoized call (Env.read_library
) but I am not sure this is how the code was intended.
So, is there currently a way to do what I tried ? If not, is it something that should be allowed ? If yes, a solution is to read all files with read_library (seems to register its result) instead of read_file (seems not to register its result). Does this look like a good enough solution ?
PS: I looked at 1-2 examples that use why3 extract but they do not seem to need this kind of extraction.