(+Iterator do +Body)
iterator, must be nonvar
callable, must be nonvar
This control structure reduces the need to write auxiliary predicates performing simple iterations. It iterates Body until Iterator’s termination condition is true.
A iterator is a term of one of the following forms:
In the first iteration, In=First. In the n:th
iteration, In is the value that Out had at the end of the
(n-1):th iteration. In and Out are local variables in Body.
The termination condition is
Iterate Body with X ranging over all elements of
List. X is a local variable in Body. Can also be
used for constructing a list. The termination condition is
Tail = , where Tail is the suffix of List
that follows the elements that have been iterated over.
Iterate Body with X ranging over all arguments of Struct and I ranging over the argument number, 1-based. X and I are local variables in Body. Cannot be used for constructing a term. So the termination condition is true iff all arguments have been iterated over.
Iterate Body with I ranging over integers from Min,
which can be any arithmetic expression, whose value is coerced to an integer.
I is a local variable in Body. Is normally used for counting
the number of iterations. The termination condition is
I = Max,
i.e. Max can be and typically is a variable.
Iterate Body with I ranging over integers from Min
to Max inclusive, which can be any integer expressions, whose
values are coerced to integers. I is a local variable in
Body. The termination condition is
Max, i.e. Max cannot be a variable.
For declaring variables in Body global, i.e. shared with the context. X can be a single variable, or a list of them. The termination condition is true. Please note: By default, variables in Body have local scope.
The iterators are iterated synchronously; that is, they all take their first value for the first execution of Body, their second value for the second execution of Body, etc. The order in which they are written does not matter, and the set of local variables in Body is the union of those of the iterators. The termination condition is the conjunction of those of the iterators.
Call errors (see ref-sem-exc).