Skip to content

Db sharing between synterp and interp #622

@trilis

Description

@trilis

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

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions