Exec-stmt-while
Execute a while statement.
- Signature
(exec-stmt-while test body compst fenv limit)
→
(mv result new-compst)
- Arguments
- test — Guard (exprp test).
- body — Guard (stmtp body).
- compst — Guard (compustatep compst).
- fenv — Guard (fun-envp fenv).
- limit — Guard (natp limit).
- Returns
- result — Type (value-option-resultp result).
- new-compst — Type (compustatep new-compst).
First, we execute the test.
If it yields a 0 scalar, we return a nil value result,
because it means that the loop completes,
and execution can proceed with any code after the loop.
Otherwise, we recursively execute the body.
If the body returns a result,
we return it from this ACL2 function without continuing the loop.
If the body returns no result,
we re-execute the loop,
by calling this ACL2 function recursively.
