====================================================================
leave in loops
====================================================================

The leave keyword is often more useful in terminating a loop. A
leave causes control to transfer to the expression immediately following
the loop. As loops always return the unique value of Void, you cannot
return a value with leave. That is, leave takes no argument.

  f() ==
    i := 1
    repeat
      if factorial(i) > 1000 then leave
      i := i + 1
    i
                      Type: Void

This example is a modification of the last example in the previous
section. Instead of using return we'll use leave.

  f()
   7
                      Type: PositiveInteger

The loop terminates when factorial(i) gets big enough. The last line
of the function evaluates to the corresponding "good" value of i
and the function terminates, returning that value.

You can only use leave to terminate the evaluation of one loop. Lets
consider a loop within a loop, that is, a loop with a nested loop. 
First, we initialize two counter variables.

  (i,j) := (1,1)
   1
                      Type: PositiveInteger

  repeat
    repeat
      if (i + j) > 10 then leave
      j := j + 1
    if (i + j) > 10 then leave
    i := i + 1
                      Type: Void

Nested loops must have multiple leave expressions at the appropriate
nesting level. How would you rewrite this so (i + j) > 10 is only
evaluated once?

====================================================================
leave vs => in loop bodies
====================================================================

Compare the following two loops:

  i := 1                      i := 1
  repeat                      repeat
    i := i + 1                  i := i + 1
    i > 3 => i                  if i > 3 then leave
    output(i)                   output(i)

In the example on the left, the values 2 and 3 for i are displayed but
then the "=>" does not allow control to reach the call to output again.
The loop will not terminate until you run out of space or interrupt the
execution. The variable i will continue to be incremented because the
"=>" only means to leave the block, not the loop.

In the example on the right, upon reaching 4, the leave will be executed,
and both the block and the loop will terminate. This is one of the reasons
why both "=>" and leave are provided. Using a while clase with the "=>"
lets you simulate the action of leave.

