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
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:
RawQuerylets you build
extra_clause => goal, that is like adding
extra_clauseto the original program
Compile.unitwhich is a bit of a backdoor, but is what is currently used in Coq-Elpi to implement the
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: Feb 04 2023 at 01:03 UTC