Session API should export `merge_file_section`
The use case is using Why3 API to build sessions in a context where the parsing of source files is not done by the internal language mechanism. Currently the function merge_file
of Session_itp
is calling Env.read_file
, making impossible to workaround the internal language mechanism.
A possible solution would be to export the function merge_file_section
in the interface, so that the user could feed it with another set of theories coming from its own source.
Another possibility to investigate would be to make merge_files
more generic by allowing the caller to provide its own function to produce theories.
Yet a problem is that currently a so-called "file" in a session is something identified with a path name (relative to the session directory). In a general context this might be too restrictive. For example one may want to consider that in a session each "file" section correspond to a particular function in a source file. A more general point of view would be to replace this notion of file with a notion of "package" identified with a qualified identifier, which could be interpreted at will, say like dir1.dir2.filename.Package.Module.function
. The current mechanism enforcing the path name to be relative to the session dir should be relaxed though.