LPCIC / elpi

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

CHR: add unique non instantiable key instead of [_] #253

Open FissoreD opened 4 months ago

FissoreD commented 4 months ago

[_] is used typically to retrieve all the goals suspended for a given predicate. The use of [_] can lead to goal resolution issue if the _ is accidentally instantiated. For example, the following code raise a failure:

pred p i:int.
pred trig.

% this extends the previous constraint
constraint p trig {
  rule \ trig (p A) <=> (false).
}

main :-
  % declare_constraint (p 4) [_], not (declare_constraint trig [_]).
  std.spy-do![declare_constraint (p 4) [_], not (declare_constraint trig [_])].

The premise with the spy-do! fails, whereas the same premise without the spy-do! succeeds

gares commented 4 months ago

Thanks for opening the issue. I think the desired solution is to use some constant, say the-key, instead of _, eg declare_constraint (p X) [X,the-key] to get it resumed when X materializes and combined via CHR rules with all the other constraints about X or about the-key.

https://github.com/LPCIC/elpi/blob/4cac107eab2acb7aaad5390e9b32eb5ef139323d/src/runtime.ml#L3402