Open rudihorn opened 4 years ago
Thanks for the detailed report.
Constraints are resumed only when any of the variables they are keyd on gets assigned. That would be the list you pass to declare_constraint. This API is not very nice and high level, since you have to check which arguments of tr are variables, using var for example, and pass them to the constraint API.
I'm sorry the doc is so slim, I'm working on it.
Hi gares,
thanks for your help.
I've tried the following example now, which seems to work for the purpose. I assume it woludn't work for variables in predicates though (e.g. updating X
for a suspended constraint tr (pre X) Y
). Is there a builtin function to recover all the vars / a nicer way to do things or is this WIP? Was thinking of something like tr X Y :- declare_constraint (tr X Y) (fv X ++ fv Y)
.
mode (tr i i).
type tr int -> int -> prop.
tr X Y :- var X, var Y, declare_constraint (tr X Y) [X, Y].
tr X Y :- var X, declare_constraint (tr X Y) [X].
tr X Y :- var Y, declare_constraint (tr X Y) [Y].
tr X Y :- declare_constraint (tr X Y) [].
constraint tr {
rule \ (tr X 0) <=> (X = 0).
}
Great, I had no time to try it out myself. Glad it works.
No, there is no such a builtin, mainly because it does not work "well" with binders (the higher order case, when a variable is under a binder it is unclear how to pull it out). But what could work is to have declare_constraint
take a list of terms (rather than just variables) and key the constraint on all the variables contained in the given terms. In this way the problem above is not visible, since you don't have to represent that "list" of variables.
The CHR part of the language is still a bit rough (see for example #71), I'm very open to suggestions.
In this very specific case I would try something like this, but it is not a general solution (also untested)
tr X Y :- std.filter [X,Y] var VS, declare_constraint (tr X Y) VS.
I've been trying to experiment with constraint handling rules with ELPI, and as far as I can tell the CHR behaviour does not match that of SWI. Specifically the SWI CHR manual (https://www.swi-prolog.org/pldoc/man?section=SyntaxAndSemantics) states:
Example
To demonstrate the behaviour I have written a small application in SWI and ELPI.
Correct Behaviour (SWI)
Program:
Running
swipl simple.pl <<< "tr(X, Y), tr(Y, 0)."
: Output:Execution: SWI starts with
tr(X,Y)
and tries to match it with any rule. As this doesn't happen,tr(X,Y)
is suspended and SWI considers the next ruletr(Y,0)
as active. This second rule matches thetr1
rule, and updatesY=0
. As the variableY
is used bytr(X,Y)
, this rule becomes active again and tries to matchtr(X,0)
which matchestr1
, settingX=0
.Incorrect Behaviour (ELPI)
Program:
Running
elpi simple.elpi <<< "tr X Y, tr Y 0."
: Output:Execution: ELPI similarly starts with the rule
tr X Y
, which does not match any rules, suspending it. It next tries the ruletr Y 0
, which matches the equivalent oftr1
, settingY=0
. Thetr X0 0
rule is left suspended, even though it could be matched withtr1
, eliminating it and settingX=0
.Comment
I'm not sure if I've misunderstood Elpi in some form or another. I have also noticed there is a small bug in the GCD example, where the line
should be: