|
|
|---|
|
|
|
|---|
Execute the iterations of a
(exec-for-loop-iterations name bound body env limit) → value?+denv
We first check whether the loop has ended, with a separate ACL2 function. If it does, we pop the top scope; note that this top scope contains exactly the loop counter, initially pushed by init-for-loop, and preserved by exec-block. Besides popping this top scope, we return no value, because the loop has ended without returning a value. If the loop has not ended, we execute the loop body as a block. Note that this immediately pushes a new scope for the block, which is why the preceding scope, as noted above, only contains the loop counter. It would be a mistake to not push a new scope here, because the loop may declare new variables and constants at each iteration. If the loop body returns a value, we return it and end the loop. Otherwise, we increment the loop counter, and recursively call this ACL2 function to loop back.