Exec-for-iterations
Execute the iterations of a loop statement.
- Signature
(exec-for-iterations test update body cstate funenv limit)
→
outcome
- Arguments
- test — Guard (expressionp test).
- update — Guard (blockp update).
- body — Guard (blockp body).
- cstate — Guard (cstatep cstate).
- funenv — Guard (funenvp funenv).
- limit — Guard (natp limit).
- Returns
- outcome — Type (soutcome-resultp outcome).
We execute the test, ensuring it returns one value.
As also explained for if (see exec-statement),
we consider 0 to be false and any non-0 value to be true.
If the test is false, we terminate regularly.
If the test is true, we first execute the body.
If it terminates with break,
we turn that into a regular termination:
we break out of the loop gracefully, no more iterations will happen.
If the body terminates with leave,
we terminate in the same way.
If the body terminates with continue or regularly,
we continue the iteration,
by executing the update block.
If the update block terminates with leave,
we terminate the loop in the same way.
If the update block terminates with break or continue,
we defensively return an error.
If the update block terminates regularly,
we recursively call this ACL2 function,
to continue iterating.
