search

LPCIC / elpi

Embeddable Lambda Prolog Interpreter
GNU Lesser General Public License v2.1
283 stars 35 forks source link

Mismatching fields in generated trace in case of CHR #147

Open jwintz opened 2 years ago

jwintz commented 2 years ago

Hi,

This issue concerns the trace-browser branch, the elaborator specifically.

https://github.com/LPCIC/elpi/blob/96c4d071194b4c7f20b9d09754c60a8e76922b07/tests/sources/trace_chr.elab.json#L170

I see a mismatch here, between the sibling goal_id and the goal_text fields.

It might very well be a misunderstanding of mine, but aren't they supposed to match the definition of the following step: https://github.com/LPCIC/elpi/blob/96c4d071194b4c7f20b9d09754c60a8e76922b07/tests/sources/trace_chr.elab.json#L422?

gares commented 2 years ago

Goal 10 is resumed because the variable it contains was assigned to s X.... If I understand the question, it is normal that the goal text is not exactly the same, the purpose is indeed to see the updated goal.

jwintz commented 2 years ago

Fine by me ! It was more a matter of understanding ... I just find it strange to click on such a text to end up on a step which is not named the same in the context of the browser (the display ). In the screenshot below, the sibling links to goal id 10, which actually is the one display in the second screenshot.

Screenshot 2022-06-05 at 17 43 04 Screenshot 2022-06-05 at 17 43 54

If only ergonomic questions remain, this issue can very well be closed for me.

Thanks.

gares commented 2 years ago

I don't know what is best to display, but I think the trace is correct: 7 (0|5) should have as event the resumption of goal 10, since it sets X0 to (s X1).

This phenomena is true in general, a new goal (p X) may become p (f Y) before it gets the chance to be handled. Maybe one could do a wdiff and color differently f Y, signaling that the goal at creation time was less instantiated. In a few cases it would help I guess. In general, I'm not so sure, since it is very frequent. It probably depends on the display of the differences. If it was "optional/no demand" then I think it would be good.