(+Iterator do +Body)
iterator, must be nonvar
callable, must be nonvar
This control structure reduces the need to write auxiliary predicates performing simple iterations. A iterator is a term of one of the following forms:
Iterate Body starting with In=First until Out=Last. In and Out are local variables in Body.
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.
Iterate Body with X ranging over all arguments of Struct and I ranging over the argument number, 1-based. X and I are local variable in Body. Cannot be used for constructing a term.
Iterate Body with I ranging over integers from Min up to Max. I is a local variable in Body. Can be used for controlling iteration as well as counting, i.e. Max can be a variable.
Iterate Body with I ranging over integers from Min to Max. I is a local variable in Body. Min and Max can be arithmetic expressions. Can be used only for controlling iteration, i.e. Max cannot be uninstantiated.
For declaring variables in Body global, ie shared with the context. X can be a single variable, or a list of them.
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. When multiple
iteration specifiers are given in this way, typically not all of them
will impose a termination condition on the loop (e.g.
foreach with an
uninstantiated list and count with an uninstantiated maximum do not
impose a termination condition), but at least one of them should do
so. If several specifiers impose termination conditions, then these
conditions must coincide, i.e. specify the same number of iterations.
Call errors (see ref-sem-exc).