Fix detection of loop headers

[Lysxia]

Fixes #164

We desugar all loops using loop, we put a noop marker right before the loop keywords, and the invariants right after. We search for the loop header backwards from the invariants and stop when we hit a marker, in which case the invariants become assertions.

In hindsight this should work just as well with the invariants before loop and the marker after it, but the implementation turns out to be slightly more convenient this way because it lets us search for the marker block by block instead of statement by statement.

[jhjourdan]

What is the plan for handling for loop? In the case of for loops, the environment can be different from the environment before the loop (and hence shadow variables), and some mutation happen just before the place where the invariant is inserted. But still, the invariant should be interpreted in the outer scope.

[Lysxia]

I had to change the invariant_moves test case because the curly braces in the RHS of while let Some(_) = { ... } are not allowed in let .... else ......

[jhjourdan]

I had to change the invariant_moves test case because the curly braces in the RHS of while let Some(_) = { ... } are not allowed in let .... else ......

That's not very satisfying. Why isn't this syntax allowed? What if we add a pair of parentheses ?

Why didn't you use if let ... { ... } else { break } instead?

[Lysxia]

if let works better indeed!

[jhjourdan]

if let works better indeed!

Great!

It's weird, though, that "let else" does not support this.

What's happening if the pattern is irrefutable? Does rustc complain about dead code?

[Lysxia]

What's happening if the pattern is irrefutable? Does rustc complain about dead code?

Yes it does. Good catch. I added an attribute to disable the warning.

I fixed the desugaring of variants, which was the last change to pass tests. I noticed that loop variants don't seem to do anything at the moment (unlike variants for recursive functions), there is just one not very meaningful test case for it. To handle that test case I had to merge the desugaring of variants and invariants; the result is not super pretty but it will be easier to clean this code when loop variants are actually implemented to know what it's meant to do.