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.)
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.
so you miss something you need. Im reluctant to add functors, but better access to module types is OK.
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)
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: Oct 13 2024 at 01:02 UTC