Enzo Crance (Jul 22 2021 at 10:21): Enzo Crance (Jul 22 2021 at 10:21):Hello. I have an elpi database I want to populate through a vernacular command (making the database grow a priori with static knowledge without a user having to touch elpi to add things manually) and a tactic (adding things to a database while solving a goal with Ltac). It looks like the command works but not the tactic. Let me show you a bit of the file architecture (along with a diagram).
Key: Green arrows mean that the file at the head of the arrow has a Require Export of the file at the source of the arrow. Red arrows mean Require Import. Grey arrows mean Elpi Accumulate File.
Enzo Crance (Jul 22 2021 at 10:22):
Enzo Crance (Jul 22 2021 at 10:22):So here is a short explanation. I have a Commands.v file containing both the command and the tactic. Both do the same thing, so they internally call a common predicate add written in an elpi file commands.elpi, that accumulates a clause to a x.db database. Both the command and the tactic need the initial DB and the elpi code to be defined. I think I had a bug once when the database wasn't sourced with Require Export, so I used green arrows when sourcing the DB, but that might be a reason for the current bug, idk.
I also have a Tactic.v file defining my main tactic which only uses the DB as information but does not push anything into it. Therefore, in the Test.v file, I have access to:
Add command imported from Commands.v which seems to work as well;add tactic imported from Commands.v which seems to have no effect on the database and I cannot see why.Do you have an idea? I hope I am as clear as possible and the diagram helps. Thanks in advance for your help.
Enrico Tassi (Jul 22 2021 at 10:38):Hum, I think the code should raise an error if you call coq.elpi.accumulate from a tactic (since it is not supported). I guess I forgot to add it.
Said that I'd like a little proof script example where you use add and then your tactic. There must be a way out without using a global db, in particular C => works like coq.elpi.accumulate (clause C) but does not have a persistent effect, so we should have all we need.
Enzo Crance (Jul 22 2021 at 10:57):Proof.
add T U.
main_tactic.
vs
Add T U.
Goal ...
Proof.
main_tactic.
Only the second one works. But I guess if we want to use => then the add tactic would have to take a sort of continuation as an argument, otherwise it does not know what to put at the right of the arrow.
Enzo Crance (Jul 22 2021 at 11:00):Or maybe we could put the arguments of add in a global variable that the main_tactic can access, thus consuming them and emptying this variable for next calls in the Coq file. But I do not know if that notion of global variable exists.
Enrico Tassi (Jul 22 2021 at 12:03):If T and U are "global", then you should use Add in the middle of the proof. Unfortuantely the addition will be global, and not local to the proof, but this is a general Coq problem.
Enrico Tassi (Jul 22 2021 at 12:05):Yes, I was thinking to something like main_tactic with U, V and internally do [caluase_for_U , clause_for_V] => usual_code
Enrico Tassi (Jul 22 2021 at 12:05):This works fine even if U and V are proof variables and not global terms.
Enrico Tassi (Jul 22 2021 at 12:06):No, there is no notion of global, mutable, variable. I could add one, I think it may be useful, but here it seems unnecessary.
Enzo Crance (Jul 22 2021 at 12:21):Enrico Tassi said:
Yes, I was thinking to something like
main_tactic with U, Vand internally do[clause_for_U , clause_for_V] => usual_code
I will try something like this. Thanks for the suggestion.
Enrico Tassi (Jul 22 2021 at 12:36):I think you should be able to do
Tactic Notation "mytac" "with" constr_list_sep(l, ",") := elpi main_tactic ltac_term_list:(l).
to get your tactic called with a list of term arguments as in
solve (goal _ _ _ _ [trm <the_term_for_U>, trm <the_term_for_V>]) _ :- ...
Hope it works.
Last updated: Oct 13 2024 at 01:02 UTC