Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Db sharing between synterp and interp #622

Open
trilis opened this issue Apr 17, 2024 · 1 comment
Open

Db sharing between synterp and interp #622

trilis opened this issue Apr 17, 2024 · 1 comment

Comments

@trilis
Copy link
Contributor

trilis commented Apr 17, 2024

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
Copy link
Contributor Author

trilis commented Apr 17, 2024

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant