-
Notifications
You must be signed in to change notification settings - Fork 61
Open
Description
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.
Metadata
Metadata
Assignees
Labels
No labels