Michael Soegtrop (Nov 24 2022 at 11:08): Michael Soegtrop (Nov 24 2022 at 11:08):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.
Enrico Tassi (Nov 24 2022 at 13:02):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).
Enrico Tassi (Nov 24 2022 at 13:06):It should amount to
https://github.com/LPCIC/coq-elpi/blob/master/src/coq_elpi_builtins.ml#L1720-L1724
where Safe_typing.current_modpath is replaced by Safe_typing.current_dirpath (to be tested)
Michael Soegtrop (Nov 24 2022 at 13:40):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.
Michael Soegtrop (Nov 24 2022 at 13:43):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).
Michael Soegtrop (Nov 24 2022 at 13:51):P.S.: I would appreciate some feedback on if the code in the VST PR mentioned above is reasonably ideomatic Elpi.
Enrico Tassi (Nov 24 2022 at 14:36):Ah, I see, so it would be coq.modpath->library i:modpath, o:modpath. I guess.
Michael Soegtrop (Nov 24 2022 at 14:53):Yes, this would be it.
Enrico Tassi (Nov 24 2022 at 14:57):https://github.com/LPCIC/coq-elpi/pull/406
Last updated: Oct 13 2024 at 01:02 UTC