Stream: Elpi users & devs

Topic: Adding a clause with a body to the context


view this post on Zulip Enzo Crance (Feb 27 2023 at 10:09):

Hello. I want to perform a substitution with copy, where the clause added to the context has a body to compute stuff. Up to management of the scope of variables, it would look like this:

(copy X Y :- p1 X Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 Y) => copy T T'

What do I need to add? (quantifiers / which variables / what order)
Until now I have only used single line copy instances added to the context, where the output is directly linked to the input, without further computations.

Intuitively, for the more complex case, I did the following but it doesn't seem to work:

(pi x y\ sigma Tmp1 Tmp2\ copy x y :- p1 x Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 y) => copy T T'

(sigma for all variables local to the body, pi so that the clause behaves like a top-level clause)
Did I make a mistake somewhere else, or is this code incorrect?

view this post on Zulip Enrico Tassi (Feb 27 2023 at 10:29):

(pi x y\ copy x y :- sigma Tmp1 Tmp2\ p1 x Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 y) => copy T T'

or

(pi x y Tmp1 Tmp2\ copy x y :- p1 x Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 y) => copy T T'

(the latter is faster)

view this post on Zulip Enrico Tassi (Feb 27 2023 at 10:30):

The order of abstractions does not matter

view this post on Zulip Enzo Crance (Feb 27 2023 at 11:10):

Thanks a lot! :smile:


Last updated: Jun 17 2024 at 22:01 UTC