Combination of with/then and given/yields

[bobismijnnaam]

What should the rules be around combining with/then/given/yields? Can they be interleaved arbitrarily, and if so, what are the evaluation rules? Or do we only allow a chain of withs, followed by one given, one yields, and one or more thens? Are there other options we should consider?

Related: #907

[pieter-bos]

Some invariants we should consider:

• All given arguments must be evaluated before the annotated expression
• All yields values are available after evaluation of the annotated expression
• By definition, we would like with to occur before evaluation of the annotated expression
• By definition, we would like `then to occur after evaluation of the annotated expression

This implies that the sequence must be {with, given} happens-before {annotated expression} happens-before {then, yields}. We can choose the order among with, given and then, yields.

Please note that if we want to support intermixing with, given and/or then, yields, this will be somewhat inconvenient to implement, since non-invocations may also have with/then annotations, but no given/yields annotations. Furthermore, given and yields parameters are stored inside the invocation from an early point, whereas with and then explicitly surround expressions.

[bobismijnnaam]

To give my personal opinion:

• No intermixing of with/given and then/yields
• Only 1 given/yields

Mostly because I don't see the direct benefit of being much more flexible than this, but I'm open to being convinced otherwise. Upside to being restrictive is that it's easy to explain. Abbreviating those points with improvised regex syntax:

(with statement;)+ m(args) given { assigns+ } yields { assigns+ } (then statement;)+

In terms of evaluation order, I'd prefer if it followed the syntactical order from above left-to-right. (With the exception of computation of the targets of the yields assignments - these go before the annotated expression, if I understand the current implementation intention correctly).

Afaict, this is all compatible with what Pieter stated above.