Jason Gross (Dec 01 2021 at 02:12): Jason Gross (Dec 01 2021 at 02:12):Is there a way to access the body of a Qed-opaque proof in Elpi? (The use-case I have in mind, which seems like it might make a nice addition to the examples, is to take a module functor (such as Coq.Sorting.Mergesort.Sort), and replace each module type with a Record and each functor with a definition producing the corresponding thing, automatically (at least so long as no nested module shenanigans are going on). This requires abstracting opaque proof terms over module arguments.)
Enrico Tassi (Dec 01 2021 at 08:39):yes https://github.com/LPCIC/coq-elpi/blob/3d5a6521e3ed4c53377ed5ddf08b76ee908ce0ec/coq-builtin.elpi#L603 but support for modules is pretty barebone, eg module types are presented as a list of id https://github.com/LPCIC/coq-elpi/blob/3d5a6521e3ed4c53377ed5ddf08b76ee908ce0ec/coq-builtin.elpi#L623 rather than a list of global terms, and there are no functors.
Enrico Tassi (Dec 01 2021 at 08:40):so you miss something you need. Im reluctant to add functors, but better access to module types is OK.
Jason Gross (Dec 02 2021 at 22:33):Not having functors is not so bad (though it might be nice to have access to the list of module types a functor takes as arguments). Here's a hacky way of doing it without functors, though: Manually declare dummy modules for the parameters, instantiate the functor with the dummy module. Then the spec of the elpi program would be to take a module M + a list of pairs (module type, module of that type), declare record versions of all the module types as well one for the implicit module type of M, and then abstract M over the constants in the given list of modules so that it can be turned into a function of records. (It would be nice if the elpi function could also do the "declare dummy modules and instantiate functor" step, but it's not really that important.)
(Also, currently, this is more a curiosity for me than something I'm needing in a project, thought up as a thing that might solve an issue a colleague of mine is running into)
Enrico Tassi (Dec 03 2021 at 06:21):ok then please open an issue for a POC poi ting to this thread, I think I can write the module type to record part without too much struggle
Last updated: Apr 18 2024 at 07:02 UTC