Stream: Elpi users & devs

Topic: Dependencies between databases

Gordon Stewart (Feb 17 2024 at 22:33):

Let's say I have a bunch of elpi databases that depend upon each other: C.db -> B.db -> A.db and then a command C that depends directly only on C.db but only transitively on B.db and A.db.

Currently, I seem to have to accumulate the transitive closure of dependencies when defining C, as in:

Elpi Command C.
Elpi Accumulate Db A.db.
Elpi Accumulate Db B.db.
Elpi Accumulate Db C.db.
Elpi Accumulate lp:{{
...
}}.
Elpi Typecheck. (*predicates from C.db that mention predicates from B.db (that perhaps mention predicates from A.db) won't typecheck unless I also accumulate A.db and B.db*)
Elpi Export C.

This doesn't scale very well. Is there some obvious feature of elpi that I'm missing? What's the recommended way to handle dependencies among databases? Should I instead be using .elpi files and have those files locally accumulate their dependencies?

Enrico Tassi (Feb 18 2024 at 07:40):

Nope, the language to build Elpi programs in Coq is very simplistic and has no notion of dependency that could be exploited.

Enrico Tassi (Feb 18 2024 at 07:43):

Using accumulate inside a .elpi file is not recommend, since thes dependencies are inlined and you may risk loading the same rule twice

Enrico Tassi (Feb 18 2024 at 07:44):

I'm not against adding a notion of dependency, but I do not have a design in mind either.

Gordon Stewart (Feb 20 2024 at 15:30):

Thanks, Enrico. Sorry for the slightly delayed response (yesterday was a US holiday).

Here's a proposal:

Elpi Db A.db. (*declare A.db*)
(*no dependencies*)
Elpi Db A.db Accumulate lp:{{
  pred A : ...
  A X :- ...
}}.
Elpi End A.db. (*end direct accumulation phase; can still accumulate clauses via `coq.elpi.accumulate`?*)

Elpi Db B.db.
Elpi Db B.db Require Db A.db.
Elpi Db B.db Require File F. (*defines predicate F*)
Elpi Db B.db Accumulate lp:{{
  pred B : ...
  B X : A X, F X, ...
}}.
Elpi End B.db.

Elpi Db C.db.
Elpi Db C.db Require Db B.db. (*direct dependency on B, transitive on A and F*)
Elpi Db C.db Accumulate lp:{{
  pred C : ...
  C X : B X, ...
}}.
Elpi End C.db.

Last updated: Oct 13 2024 at 01:02 UTC