Gordon Stewart (May 22 2024 at 16:19): Gordon Stewart (May 22 2024 at 16:19):Is there already an Elpi API for calling Search?
If not, is there a reason why such an API doesn't make sense? Would it be difficult to add?
Enrico Tassi (May 22 2024 at 16:31):Nobody asked for it. Depending on how many features you want it may require some plumbing, for example it supports patterns but the ocaml datatype may not be one for which we have a conversion function. Other than that I see no problem.
Michael Soegtrop (May 22 2024 at 16:31):Elpi has an API to enumerate the contents of modules, so you can write a search function in Elpi - say enumerate all lemmas which match an Elpi predicate. I use this frequently to create symbol lists for delta reductions.
Gordon Stewart (May 22 2024 at 16:40):A version that supported Search <gref> (no patterns) would probably sufficient for the use case I have in mind.
@Michael Soegtrop
Elpi has an API to enumerate the contents of modules, so you can write a search function in Elpi - say enumerate all lemmas which match an Elpi predicate.
It's a little unclear to me how you'd know which modules to enumerate. All those in scope?
Michael Soegtrop (May 23 2024 at 08:15):In my application of computing delta symbol lists I know the root modules upfront and enumerate sub modules from there. I would assume that in most cases of program driven searches this is the case - probably excluding AI applications. I am not sure Elpi has an API to enumerate all modules in scope, but I guess this would be easy to add.
But the main question to answer is if we want/need a dedicated search API or if it is better to be able to enumerate contents in a structured way and filter it with custom Elpi predicates, so that search is more an extensible library.
Enrico Tassi (May 23 2024 at 08:20):@Gordon Stewart please tell us which is your use case. I don't have any opposition to binding search, but the more we know the better we can advise.
No, there is no API to know the list of modules in scope.
Michael Soegtrop (May 23 2024 at 08:46):IMHO it would be better to have the equivalent of Search implemented in Elpi based on more fundamental APIs - this would be an excellent starting point for developing whatever search functionality one needs. A dedicated Search API might make sense for performance reasons, but only if it is really faster. @Gordon Stewart : do you share this view or do you have other arguments?
Gordon Stewart (May 23 2024 at 13:41):@Enrico Tassi Our application is related to ML-assisted proof and specification inference. Binding Search would give us a way to produce relevant context for queries (e.g., potentially applicable lemmas).
Concretely, I'd imagine that an interface like the following might make sense:
kind search-result type.
type search-result gref -> term /*gref's type*/ -> search-result.
pred coq.env.search i:gref, o:list search-result.
Note that this interface doesn't support patterns. The argument type could be generalized to make the interface forward compatible with a future generalization to patterns:
kind search-arg type.
type search-arg.gref gref -> search-arg.
type search-arg.pattern string -> search-arg.
...
@Michael Soegtrop
But the main question to answer is if we want/need a dedicated search API or if it is better to be able to enumerate contents in a structured way and filter it with custom Elpi predicates, so that search is more an extensible library.
I'm not at all opposed to an Elpi library implementation. But it's probably not necessary for the applications we have currently (described briefly above). The counter-argument is that directly binding Search gives a level of compatibility with existing Coq commands, which could be useful. The binding implementation is probably less work as well.
Last updated: Oct 13 2024 at 01:02 UTC