Patrick Nicodemus (Apr 04 2023 at 17:25): Patrick Nicodemus (Apr 04 2023 at 17:25):With Coq's auto you can pass a list of databases to a tactic. How can I do something similar with Elpi? Is it possible to have a tactic take a list of databases as an input, so that the tactic can accumulate all those databases dynamically?
Patrick Nicodemus (Apr 04 2023 at 17:27):If I write
Elpi Tactic mytac.
Elpi Accumulate Db abc.db.
it seems to make that database abc.db available to mytac at all other points.
On the other hand the coq.elpi.accumulate relation seems to be only for adding new contents of to a database.
Patrick Nicodemus (Apr 04 2023 at 17:32):There is just accumulate xyz but that seems only for files.
Enrico Tassi (Apr 05 2023 at 12:26):You are correct, there is no notion of accumulation akin to the one of Coq. You have to implement it yourself.
One option, maybe not the fastest one but conceptually simple, is to add an argument to each hint, eg
pred hint i:string, ....
solve (goal .... [str DB]) :- hint DB ....
Another option is to use modules to make rules in scope, eg
Module H1. Elpi Accumulate Db foo.db lp:{{ hint }}. End H1.
tac. (* no hint *)
Import H1. tac. (* hint available *)
If you give me more context I may suggest other options...
Last updated: Oct 13 2024 at 01:02 UTC