constraint iter[i, j] A(x){i} * A(y){j} -> P(x, y, i, j);
cannot AFAIK be represented in Starling because then the pattern match A(x){i} * A(y){j} <- A(z){n} generates an unbounded possible set of patterns (i=n j=0; i=n-1 j=1; …; i=0 j=n).
Instead, what we could do is add a new downclosure check where any such pattern must be of the form x != y => blah. I think (but could be wrong) the logical equivalent would be x == y || P(x, y, i, j) <=> P(x, y, i, j).
This would, I think, allow us to pattern match iterated views in the usual way, ie. we match the two sides of the * against two separate atoms in the view.
Motivating example is the sense barrier and Dimitrios barrier.
The general case
cannot AFAIK be represented in Starling because then the pattern match
A(x){i} * A(y){j} <- A(z){n}generates an unbounded possible set of patterns (i=n j=0; i=n-1 j=1; …; i=0 j=n).Instead, what we could do is add a new downclosure check where any such pattern must be of the form
x != y => blah. I think (but could be wrong) the logical equivalent would bex == y || P(x, y, i, j) <=> P(x, y, i, j).This would, I think, allow us to pattern match iterated views in the usual way, ie. we match the two sides of the * against two separate atoms in the view.
Motivating example is the sense barrier and Dimitrios barrier.