Loop$
Iteration with an analogue of the Common Lisp loop macro
Loop$ is the ACL2 analogue of the Common Lisp's iteration
primitive, loop. This topic introduces the two classes of ACL2
loop$ expressions, FOR loop$s and DO loop$s; see
for-loop$ and do-loop$ (respectively) for their full
documentation.
Loop$ was introduced into ACL2 in Version 8.2 (May, 2019), over 20
years after ACL2 was first released. So there are many experienced ACL2 users
who have never used loop$. The Loop$ Primer, see loop$-primer, is textbook-style introduction, meant to be read linearly and
may be a good starting place for you. The primer follows a “monkey-see
monkey-do” approach, showing lots of examples. Sample proofs are worked
out in detail and then the reader is challenged to apply those lessons to
exercises. Solutions to the exercises are provided in books among the
Community Books. Depending on your preferred learning style and familiarity
with loop$ and ACL2 in general, you might want to work your way through
the primer (see loop$-primer) instead of bouncing around the hypertext
user's manual.
The Introduction below is followed by a discussion of types and guards.
For a discussion of how to state effective lemmas about loop$s and how to
prove inductive theorems about loop$s see stating-and-proving-lemmas-about-loop$s. Also, for a summary of how the
rewriter handles apply$, ev$, and loop$ scions, see
rewriting-calls-of-apply$-ev$-and-loop$-scions.
But before we get started we emphasize a few key points.
Introduction to loop$
As noted above, there are two classes of loop$ expressions. These are
identified as follows.
- FOR loop$ expressions:
(loop$ FOR ...)
- DO loop$ expressions:
(loop$ WITH ... DO ...)
Below we introduce these two classes of loop$ expressions. For full
documentation see the topic for each class: see for-loop$ for FOR
loop$s and do-loop$ for DO loop$s. In particular
various restrictions are discussed in those topics, but for now we mention
just the following. While FOR loop$ expressions are often more
convenient to use than DO loop$ expressions, their UNTIL,
WHEN, and body expressions are not permitted to reference state
or stobjs, and they always return a single value. DO loop$
expressions do not have these restrictions, but they may not use the idioms of
FOR loop$s, like ``FOR x IN ...'' or ``UNTIL p''.
ACL2's loop$ is considerably more restrictive than Common Lisp's
loop, but when an ACL2 loop$ expression is translated without error
it has the same meaning as the corresponding Common Lisp loop.
Loop$ supports :guard expressions (discussed below) in
certain places and these are ignored by Common Lisp.
Next we present some FOR loop$ examples. They illustrate the
three supported forms of FOR loop$ iteration: the use of IN, to
iterate over elements of a list; the use of ON, to iterate over the
non-empty tails of a list; and the use of FROM .. TO, to iterate over a
range of integers (optionally with BY to specify the increment at each
step). These examples also illustrate the use of WHEN to restrict which
iterations are considered and the use of UNTIL to terminate early.
Additional keywords illustrated are OF-TYPE to specify types and AS
to specify additional iteration variables. They also illustrate some of the
operations permitted at each iteration, such as SUM and COLLECT.
ACL2 !>(loop$ for x in '(1 2 3) sum (* x x))
14
ACL2 !>(loop$ for x in '(1 2 3) collect (* x x))
(1 4 9)
ACL2 !>(loop$ for x on '(1 2 3) collect x)
((1 2 3) (2 3) (3))
ACL2 !>(loop$ for x of-type integer from -10 to 10 by 2 collect x)
(-10 -8 -6 -4 -2 0 2 4 6 8 10)
ACL2 !>(loop$ for i from 1 to 10
as x in '(a b c d e f g)
collect (cons i x))
((1 . A)
(2 . B)
(3 . C)
(4 . D)
(5 . E)
(6 . F)
(7 . G))
ACL2 !>(loop$ for i from 1 to 10
as x in '(a b c d e f g)
until (> i 6)
collect (cons i x))
((1 . A)
(2 . B)
(3 . C)
(4 . D)
(5 . E)
(6 . F))
ACL2 !>(loop$ for i from 1 to 10
as x in '(a b c d e f g)
until (> i 6)
when (evenp i)
collect (cons i x))
((2 . B) (4 . D) (6 . F))
Finally we present two DO loop$ examples. We explore them
further in the documentation specific to DO loop$ expressions; see
do-loop$.
Our first DO loop$ example shows iteration with the indicated
initial values for local variables x and y. They are modified at
each iteration through the loop until x is empty, at which point the
value of y is returned. (See do-loop$ for more thorough
explanations.)
ACL2 !>(loop$ with x = '(a b c)
with y = nil
do (cond ((consp x)
(progn (setq y (cons (car x) y))
(setq x (cdr x))))
(t (return y))))
(C B A)
ACL2 !>
Our second example of a DO loop$ expression illustrates more
features than the first. Also, it illustrates the use of a loop$
expression inside a definition, which is allowed for both FOR loop$s
and DO loop$s. We see here that stobjs and multiple-value returns are allowed for DO loop$s, where the
:VALUES keyword specifies the shape of the return. We also see here the
use of the optional :GUARD keyword of a loop$ expression (legal for
both classes of loop$s, as discussed further below) and the optional
:MEASURE keyword of a DO loop$ expression.
But notice the defwarrant events below! They are required because
the functions fld and update-fld are not system primitives. They
are introduced by the user's defstobj event below. This is in
contrast to the DO loop$ in our first example above where no
warrants are required because all the functions in that example are
primitive.
The semantics of loop$ involve apply$ and thus loop$s
inherit the restrictions imposed on apply$ and its scions. Among
those restrictions are that (a) unwarranted :logic mode functions cannot
be apply$'d in the top-level read-eval-print loop and (b) proofs about
the applications of unwarranted functions are impossible. Restriction (a)
means you cannot even execute a :logic mode loop$ containing
unwarranted functions. Restriction (b) means you can't verify the guards of such loop$. This last point obviates the main reason for
using loop$: its fast execution as a Common Lisp loop once guards are
verified.
Now here is our second example.
(defstobj st fld)
(include-book "projects/apply/top" :dir :system) ; needed for defwarrant
(defwarrant fld)
(defwarrant update-fld)
(defun test-loop$ (i0 max st)
(declare (xargs :guard (and (natp i0) (natp max))
:stobjs st))
(loop$ with i of-type (satisfies natp) = i0
with cnt of-type integer = 0
do
:measure (nfix (- max i))
:guard (and (natp max)
(natp cnt)
(stp st))
:values (nil st) ; shape of return; can be omitted when it's (nil)
(if (>= i max)
(loop-finish)
(progn (setq st (update-fld i st))
(mv-setq (cnt i)
(mv (+ 1 cnt) (+ 1 i)))))
finally
:guard (stp st)
(return
(mv (list 'from i0 'to max 'is cnt 'steps 'and 'fld '= (fld st))
st))))
ACL2 !>(test-loop$ 3 8 st)
((FROM 3 TO 8 IS 5 STEPS AND FLD = 7)
<st>)
ACL2 !>
Both classes of loop$ expressions (FOR and DO loop$s)
rely heavily on the ACL2 built-in function, apply$: in each iteration
through the loop, a lambda object based on the body of the loop$
is given as the function argument of apply$. Similarly, the UNTIL
and WHEN clauses of FOR loop$s and the :measure and
FINALLY clauses of DO loop$s are translated into lambda
objects. The functions in all those lambda objects must be warranted to
evaluate the loop$ and/or prove its properties (including its guards)
because logically the application of an unwarranted function is
undefined. (However, recall from guarantees-of-the-top-level-loop that
:program mode functions do not need warrants, just badges, for execution
in the evaluation theory.)
The documentation for apply$ illustrates a simple defun that
is inadmissible because the measure theorem cannot be proved without a warrant
and warrants cannot be assumed during the proofs of the measure conjectures.
The same issue arises when one of the functions critically involved in a
measure conjecture is defined using a loop$ whose body involves a
user-defined function. For a simple example of this issue and how to work
around it, see community-book
books/demos/measure-and-warrant.lisp.
Types and guards in loop$ expressions
In this section we document basic aspects of the OF-TYPE and
:GUARD keywords in loop$ expressions. See for-loop$ and
do-loop$ for detailed documentation on guards for FOR and DO
loop$ expressions, respectively.
Loop$ expressions execute fastest when they are guard
verified. But the loop$ body raises interesting guard verification
problems, as do the UNTIL and WHEN tests of a FOR loop$,
because they are executed for many different values of the iteration
variables. The FINALLY clause of a DO loop$ raises a similar
concern, since the values of its variables may be modified repeatedly by
execution of the loop$ body. It may be necessary to provide type
information or even stronger invariants to verify guards for loop$s. We
now provide a few examples illustrating the handling of guards in
loop$.
The first example below is an acceptable loop$ expression but cannot
be guard verified, as would be necessary if it appeared in a defun
that was to be guard verified. The problem is that (+ 1 x) requires
x to be numeric and, in general, we don't know anything about the value
of x here. (Actually, because the target range is just a constant below,
ACL2 could deduce information about each value x takes on, but it
doesn't.) The second example can be guard verified and has the advantage of
being standard Common Lisp, so compilers might optimize the handing of (+ 1
x). The third example can also be guard verified but since the :GUARD
directive used here is ignored by Common Lisp it does not inform the compiler,
so this example might execute more slowly than the previous one. The last
example shows the syntax and use of the ACL2-specific addition to loop$:
the :GUARD directive protecting, in this case, the loop$ body.
:GUARD is useful when you wish to add more guard information than can be
expressed with the Common Lisp OF-TYPE directive. The OF-TYPE and
:GUARD directives are conjoined to form the actual guard protecting the
loop$ body.
ACL2 !>(loop$ for x in '(1 2 3) collect (+ 1 x))
(2 3 4)
ACL2 !>(loop$ for x of-type integer in '(1 2 3) collect (+ 1 x))
(2 3 4)
ACL2 !>(loop$ for x in '(1 2 3) collect :guard (integerp x) (+ 1 x))
(2 3 4)
ACL2 !>(let ((max 10))
(loop$ for x of-type integer in '(1 2 3)
collect
:guard (and (integerp max) (< x max))
(- max x)))
(9 8 7)
The guard on the (- max x) above is (and (integerp x) (integerp
max) (< x max)) and the compiler is informed that x is an integer by
the OF-TYPE.
The examples just above are of FOR loop$s. Here is a DO
loop$ example that illustrates types and guards.
ACL2 !>(loop$ with i of-type integer = 7
with ans = nil
do
:guard (true-listp ans)
(progn (setq ans (cons i ans))
(setq i (- i 2))
(if (< i 0) (loop-finish) t))
finally
:guard (true-listp ans)
(return (reverse ans)))
(7 5 3 1)
ACL2 !>
Neither :GUARD is necessary in order for this execution to complete.
However, if this loop$ is put into a definition — (defun foo ()
(loop$ ...)) — then both :GUARD expressions are necessary in
order for the definition to be guard-verified.
As suggested above, when a loop$ expression occurs in the body of a
guard-verified function, it will be executed as a Common Lisp
loop expression, which can be much more efficient than executing without
such guard verification. This efficiency can also be gained in top-level
loop$ expressions if the tau-system completes (silently) the
necessary guard verification. See print-cl-cache.
Subtopics
- Loop$-primer
- Primer for using loop$
- Do-loop$
- Iteration with loop$ using local variables and stobjs
- For-loop$
- Iteration with loop$ over an interval of integers or a list
- Loop$-recursion
- Defining functions that recur from within FOR loop$ expressions
- Stating-and-proving-lemmas-about-loop$s
- Stating and proving theorems about loop$s
- Loop$-recursion-induction
- Advice on inductive theorems about loop$-recursive functions
- Do$
- Definition of do$
