Michael Soegtrop (Oct 11 2022 at 16:34): Michael Soegtrop (Oct 11 2022 at 16:34):Another question: say I have a huge term of unknown structure and it contains applications of a constructor MyConstr. Is it easy in elpi to get a list of all the arguments of the application of MyConstr without duplicates - the arguments are all ground terms?
In the examples (pred quote in example_reflexive_tactic.v) I see how to reify a term with a well known structure, but what would I do if I don't know much about the term except that it has leaves as described? I don't see facilities in Elpi which would allow me to iterate over any term (as kind in Ltac2).
In Ltac2 I wrote a fold function for coq terms based on kind - with this it is quite simple. But it is not that fast if the result list is large cause there is no hashing or order of idents, so there is no efficient way to remove the duplicates in the list - something which wouldn't be that hard to fix, of course. I guess this part would be easier in a Prolog.
Another issue I have with porting such a concept is that I don't see a function argument to a "fold_coq_term" predicate would work.
Well I guess I shouldn't think about porting Ltac2 to Elpi but rather look for an idiomatic way to do it - but I don't see it yet.
Enrico Tassi (Oct 11 2022 at 18:53):I'll write a sketch tomorrow. look in coq-lib.elpi for fold-term and in elpi-builtin for std.set and cmp_term.
Enrico Tassi (Oct 11 2022 at 18:55):a test case would help, so that I can make another POC
Michael Soegtrop (Oct 11 2022 at 19:00):@Enrico Tassi : thanks - I found a fold-map which looks very promising ...
Enrico Tassi (Oct 11 2022 at 19:08):yeah, that one, I did not recall the name.
It does more than what you need. Btw, do you only need to collect constant names? or any argument?
Enrico Tassi (Oct 11 2022 at 19:10):in the former case, coq.gref.set is the most effective datastructure you can get.
Michael Soegtrop (Oct 11 2022 at 19:36):I need to collect specic arguments of specific constructors - the arguments are definitions - I need the names of these definitions (for the cbv delta list).
Enrico Tassi (Oct 12 2022 at 12:15):Here the APIs you need and a little example: https://github.com/LPCIC/coq-elpi/pull/395
There is still some work to do in order to obtain what you want, but you should have all the pieces.
The only caveat that may hit you is that, in the example, elpi has no way to leave in the proof term a, say, vmcast (the _ <: _ thingy) for Qed to call vmcompute. If this is a problem, it is surely fixable, and the usual workaround is in a comment.
Enrico Tassi (Oct 12 2022 at 12:26):Also, the example does not use it, but I've added coq.env.term-dependencies which may be helpful (and it was trivial to code in OCaml).
Michael Soegtrop (Oct 12 2022 at 12:54):@Enrico Tassi : thanks I will have a look right away. I sent you an example via email - it took a bit to put everything together.
Enrico Tassi (Oct 12 2022 at 12:56):Thanks, but I won't have time for it today, but I'll look into it.
Michael Soegtrop (Oct 12 2022 at 12:57):I say thank you for the support!
Enrico Tassi (Oct 12 2022 at 12:59):you are welcome
Last updated: Apr 19 2024 at 18:01 UTC