LPCIC / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
131 stars 48 forks source link

Db sharing between synterp and interp #622

Open trilis opened 3 months ago

trilis commented 3 months ago

Suppose I have some "common utils" Db that I want to use both in interp and synterp code:

Elpi Db utils lp:{{
    pred f i:string.
    f S :- coq.say S.
}}.

I would expect that I will be able to accumulate it like this:

Elpi Command ElpiTest.
Elpi Accumulate Db utils.
#[synterp] Elpi Accumulate lp:{{
    main _ :- f "a".
}}.
Elpi Accumulate lp:{{
    main _ :- f "a".
}}.
Elpi Typecheck.
Elpi Export ElpiTest.

However, this command fails in synterp, not being able to find f. The solution I found is to make two copies of utils, one with #[synterp] tag, and then accumulate them twice, again once with #[synterp]. This solution works, but it isn't pretty. Is it possible to implement Db sharing? If it's hard, then just allowing to copy Db will remove the need to duplicate code, something like:

Elpi Db interp-utils lp:{{
    pred f i:string.
    f S :- coq.say S.
}}.
#[synterp] Elpi Db synterp-utils Copies interp-utils.

Elpi Command ElpiTest.
Elpi Accumulate Db interp-utils.
#[synterp] Elpi Accumulate Db synterp-utils.
trilis commented 3 months ago

Well, for my particular usecase actually main-interp/main-synterp solution worked perfectly, but I still can imagine the situation when one needs actual common library. For example, as synterp code mainly works with strings, it would be useful to use string manipulation library both in interp and synterp. But main-interp/main-synterp probably should be great for most of usecases.

So on the second thought, while this feature still would be useful, I suppose it's low-priority.