Stream: Elpi users & devs

Topic: declare_constraint does not carry the context

Enzo Crance (May 16 2023 at 10:12):

Hello. I just noticed an interesting behaviour with declare_constraint. It seems like the context at the moment of suspending the goal is not available in the CHR, but comes back when the goal is resumed. Here is a minimal example:

pred p o:int.
p X :- var X, !, declare_constraint (p X) [X].
p X :- if ctx (coq.say X) (coq.say "no").

constraint p {
  rule (p X) <=> (if ctx (X = 1) (X = 2)).
}

If I call ctx => p X, the rule does not see ctx, takes the second branch, gives X the value 2, and when the goal is resumed the second instance of p sees ctx and prints 2 on the screen.

Can you explain why it was implemented like this? Thanks!

PS: I noticed that because I am using a debug predicate triggering calls to coq.say only when debug is in the context, and in the CHR nothing was printed :laughing:

Enrico Tassi (May 16 2023 at 11:37):

It is available, but is reified. Try

constraint p {
  rule (C ?- p X) | (std.mem C ctx) <=> (X = 1).
  rule (p X) <=> (X = 2).
}

Enrico Tassi (May 16 2023 at 11:38):

Here a tiny bit of doc: https://github.com/LPCIC/elpi/blob/master/ELPI.md#example-of-higher-order-rules

Enrico Tassi (May 16 2023 at 11:44):

To sum up:

• a constraint is an actual sequent, you have the context and the goal
• the context is a list of prop, you access it by writing context ?- goal and goal means _ ?- goal
• the new goal is resumed in an empty context, unless you write somthing like C => g as the new goal
• if you match over multiple constraints that live under names generated by pi x\, then the CHR rule runs under a set of names which is the disjoint union, and it is up to you to make sense of it, e.g. by comparing the contexts. This is explained in the doc above, but does not play a role in your example

Enrico Tassi (May 16 2023 at 11:46):

Or, if you really want the test to be done in the regular level (instead at the meta level of CHR):

constraint p {
  rule (C ?- p X) <=> (C => if ctx (X = 1) (X = 2)).
}

but that seems less idiomatic to me

Last updated: Oct 13 2024 at 01:02 UTC