Stream: Elpi users & devs

Topic: Derive the name of the enclosing file level module


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Nov 24 2022 at 14:36):

Ah, I see, so it would be coq.modpath->library i:modpath, o:modpath. I guess.

view this post on Zulip Michael Soegtrop (Nov 24 2022 at 14:53):

Yes, this would be it.

view this post on Zulip Enrico Tassi (Nov 24 2022 at 14:57):

https://github.com/LPCIC/coq-elpi/pull/406


Last updated: Mar 28 2024 at 21:01 UTC