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.

I'll write a sketch tomorrow. look in coq-lib.elpi for fold-term and in elpi-builtin for std.set and cmp_term.

a test case would help, so that I can make another POC

@Enrico Tassi : thanks - I found a `fold-map`

which looks very promising ...

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?

in the former case, coq.gref.set is the most effective datastructure you can get.

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).

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.

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).

@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.

Thanks, but I won't have time for it today, but I'll look into it.

I say thank you for the support!

you are welcome

Last updated: Feb 04 2023 at 02:03 UTC