Stream: Elpi users & devs

Topic: Elpi API

Janno (Feb 18 2022 at 10:00):

I am exploring the elpi API and I am wondering if there is an analogue to the RawQuery module but for program input, not queries. Something that would probably be called RawProgram?

Enrico Tassi (Feb 18 2022 at 13:03):

No, but you are the second one asking or it, so there should be one.

One difficulty is that RawProgram would be very powerful, in the sense that a program is not only made by clauses but also types and modes declarations, and so on. I currently don't have a concrete use case for it.

If you want to just create a clause and add it to an existing program, then there are two ways:

• RawQuery lets you build extra_clause => goal, that is like adding extra_clause to the original program
• Utils.clause_of_term + Compile.unit which is a bit of a backdoor, but is what is currently used in Coq-Elpi to implement the coq.elpi.accumulate API

Do you have a concrete use case for building a program programmatically (without going trough text)?
In any case, thanks for the feedback, if you have more I'm all ears!

Last updated: Oct 13 2024 at 01:02 UTC