Allow multiple iterators in an iterated constraint

[MattWindsor91]

For the sense barrier, we need to encode

constraint isBarrier(i) * isBarrier(j)  ->  i == j;

I think the easiest way to encode this, to keep iterated atoms separate from non-iterated atoms, would be as something like

constraint iter[n] isBarrier(i) * iter[m] isBarrier(j)  ->  i == j;

Working out how to support these sorts of constraint is another issue, but for now the biggest block is that the iterator works at the constraint level. IMO it should be at the atom level, as that's how iterators are attached in the internal representation.

This would need a change to downclosure, namely that downclosure is checked for each iterator instead of just the one.

[septract]

At the level of syntax, I'd prefer an extra 'field' on iterated atoms, eg something like:

constraint iter[n,m] isBarrier(i){n} * isBarrier(j){m} -> blah

To me that matched more the logical structure of the constraint.

[MattWindsor91]

Base downclosure might be difficult to generalise to multiple iterators. The strongest version would be something like saying constraint iter[n] A(x) * iter[m] B(y) -> P(n, m, x, y) must obey D(emp) => P(0, m, x, y) and D(emp) => P(m, 0, x, y). But this might be too restrictive.

A weaker (and much more difficult to prove!) version, though I'm not sure if it's sound, would be

• |_ A(x) _| => P(0, m, x, y)
• |_ B(y) _| => P(0, m, x, y)
• D(emp) => P(0, m, x, y)

[MattWindsor91]

I wish my Coq formalisation noodling around covered downclosure so I could actually check this :P But since it's currently a weekend project and hasn't really got anywhere then that kite doesn't fly