I wonder if it is possible to derive the enclosing file level module name of a module. I guess I can see if the module can be required or if the parent module (with the kernel path shortened by one) exists, but what I am missing here is a reverse of
coq.modpath->path to construct the shortened module path.
I'd rather add an API like https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L718 but for the current library (which is the module corresponding to the file name).
It should amount to
where Safe_typing.current_modpath is replaced by Safe_typing.current_dirpath (to be tested)
I am not sure we are talking about the same thing. I need this for the functions which create delta reduction symbol lists from enumerating modules. I am creating Coq files for Ltac2 from this (to get around the mutual fixpoint issue) and there I need to figure out the require statement I need for symbols in the module.
Here is an example for such a generated file. In essence I need to create from the lengthy reference lists the Require command list at the top of the file. Right now I am using a manually created table for the (rare) case of not file level modules. See (https://github.com/PrincetonUniversity/VST/blob/a0484526e3a48f8817e1590f5f969bf893ab6e40/elpi/cbv_symbol_lists_generator.v#L16).
P.S.: I would appreciate some feedback on if the code in the VST PR mentioned above is reasonably ideomatic Elpi.
Ah, I see, so it would be
coq.modpath->library i:modpath, o:modpath. I guess.
Yes, this would be it.
Last updated: Feb 05 2023 at 15:03 UTC