Do-loop$
Iteration with loop$ using local variables and stobjs
This topic assumes that you have read the introduction to
loop$ expressions in ACL2; see loop$. Here we give more complete
documentation on DO loop$ expressions, beginning with an informal
introduction based largely on examples and then continuing with detailed
syntax and semantics. For a discussion of proofs about loop$s, see stating-and-proving-lemmas-about-loop$s.
More examples of loop$ expressions, including DO loop$s,
may be found in community-book projects/apply/loop-tests.lisp.
INFORMAL INTRODUCTION
The most basic DO loop$ expressions have the following form.
(loop$ WITH v1 = a1
...
WITH vn = an
DO body)
A Basic Example
The example loop$ expression below initially stores the list (a b
c) in the variable x and nil in the variable y. Then it
iterates, repeatedly popping the first element of x onto y until
x is empty. Then it returns the final value of y.
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 !>
This example illustrates the basic operation of DO loop$
expressions.
- Initially, variables are initialized according to the WITH
clauses: for each binding WITH Vi = Ei, we say that Vi is a
WITH-bound variable, and Vi is initially bound to the value
of Ei.
- In this example, x is initially bound to the list (a b c)
and y is initially bound to nil.
- Then, the loop body — i.e., the term after the DO
keyword — is repeatedly evaluated. An update to WITH-bound
variable Vj occurs whenever an expression (setq Vj Ej) is
encountered while evaluating the loop body, binding Vj to the value of
Ej (which may reference the current values of WITH-bound variables).
- In this example, as long is x is a cons, y is assigned to
(cons (car x) y) and then x is assigned to the cdr of its
current value.
- Ultimately an expression (RETURN E) should be encountered, in which
case the value of E is returned — where as before, E may
reference the current values of WITH-bound variables.
- In this example, when x is not a cons (and hence is, in fact,
nil), the current value of y is returned as the value of the
loop$ expression. By this point each element of the initial value of
x has been pushed onto y, so the value (c b a) is
returned.
Note that progn is permitted as shown, to connect a sequence of
expressions. Indeed, that is how more than one assignment is accomplished;
unlike Common Lisp, the DO keyword is followed by exactly one expression,
so DO expr1 expr2 is illegal in ACL2 but DO (progn expr1 expr2) is
fine.
Also note that the WITH-bound variables are initialized sequentially:
later bindings may reference values of earlier ones, for example as
follows.
ACL2 !>(loop$ with x = (* 3 4) with y = (* 10 x) do (return (list y)))
(120)
ACL2 !>
See lp-section-14 of the Loop$ Primer for some exercises in
writing and executing DO Loop$s (with answers in a Community Book).
But remember to come back here when you get to the end of that section.
Parallel Assignment Using Mv-setq
ACL2 also supports parallel assignment to two or more variables, using
mv-setq. The following is equivalent to the example immediately
above.
ACL2 !>(loop$ with x = '(a b c)
with y = nil
do (cond ((consp x)
(mv-setq (x y)
(mv (cdr x) (cons (car x) y))))
(t (return y))))
(C B A)
ACL2 !>
Thus, the first argument of an mv-setq call is not evaluated, and is a
list of distinct variables of length at least 2. The second argument is any
expression that returns multiple values consistent with the first argument
— ``consistent'' in the sense that the number of values returned equals
the number of variables in the first argument and stobjs must match up. Thus,
the rules for (mv-setq vars expr) are the same as for (mv-let vars
expr ...).
The FINALLY Clause
We have seen the loop$ keywords WITH and DO. A third
loop$ keyword, FINALLY, is also supported. Here is a variant of the
preceding example that illustrates the use of FINALLY. The iteration
stops with the (loop-finish) form this time, rather than with a call of
return. Execution of (loop-finish) passes control to the
FINALLY clause, which is executed just like the DO body but with a
single pass, thus determining the value of the loop$ — in this
example, returning the final value of y.
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 (loop-finish)))
finally (return y))
(C B A)
ACL2 !>
This example illustrates that (loop-finish) terminates the iteration,
passing control to the FINALLY clause if there is one. The FINALLY
clause is evaluated under the current bindings of the WITH-bound
variables, just as a DO body is executed (but with a single pass rather
than iteration).
The value returned by a DO loop$ expression is nil when no
return expression is evaluated (or more generally, a suitable value
consistent with the :VALUES keyword discussed below). Here is an
example, which illustrates an error that may be easy to commit.
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 (loop-finish)))
finally (length y))
NIL
ACL2 !>
Presumably the intention was to return the length of y, which in this
case would be 3. But then the FINALLY clause should have been
(return (length y)).
The :VALUES Keyword
The :VALUES keyword is necessary for a loop$ expression that
returns a double-float, a stobj or multiple-values. When
the :VALUES keyword is used, the syntax is :VALUES (v0 ... vk),
where each vi is either nil, :df, or a stobj
name. :VALUES (nil) denotes return of a single ordinary value;
:VALUES (s) denotes return of a single value that is a stobj named
s; and :VALUES (v0 ... vk) for k > 0 denotes return of k+1
values, where vi is nil if the ith returned value is an ordinary
value, :DF if the ith returned value is a double-float, and otherwise
vi is the name of the stobj returned as the ith value. You may
recognize (v0 ... vk) as an output signature. If the measure supplied to
do$ fails to decrease on an iteration, an error is caused and the output
signature is used compute a ``default value,'' which is generally a list of
k+1 objects (but is a single object when k is 0). The ith object in the
default value is nil if vi is nil, is #d0.0 if vi is
:DF, and is the last latched value of the named stobj otherwise. No stobj
name may be duplicated, and :VALUES must appear between the DO loop
keyword and the DO body. Let's look at an example.
Below we introduce a stobj and add a warrant for its accessor
and updater. Warrants are necessary for functions called in DO bodies
and FINALLY clauses in order for those forms to be evaluated. See loop$ for a discussion of the necessity of such warrants. The two loop$
expressions are similar in nature to those above, first without and then with
a FINALLY clause; also see the discussion below. All forms below
complete successfully.
(include-book "projects/apply/top" :dir :system)
(defstobj st fld)
(defwarrant fld)
(defwarrant update-fld)
; Check that (fld st) is currently nil.
(assert-event (equal (fld st) nil))
(loop$ with x = '(1 2 3)
do
:values (st)
(cond ((endp x)
(return st))
(t (mv-setq (st x)
(let ((st (update-fld (cons (car x)
(fld st))
st)))
(mv st (cdr x)))))))
(assert-event (equal (fld st) '(3 2 1)))
(update-fld nil st)
(assert-event (equal (fld st) nil))
(loop$ with x = '(1 2 3)
do
:values (st)
(cond ((endp x)
(loop-finish))
(t (progn (setq st
(update-fld (cons (car x)
(fld st))
st))
(setq x (cdr x)))))
finally (return st))
(assert-event (equal (fld st) '(3 2 1)))
These loops are similar to those we saw earlier, but this time, when we pop
values from x they go into a stobj. Since we return that stobj, st,
the :VALUES is (st). The fifth argument of the call of do$
generated from these loop$s is '(st). One might expect :VALUES
to be st instead, but :VALUES is always a list; when a single value
is returned, :VALUES is a one-element list. Thus, the default for
:VALUES is (nil).
Notice that the examples above apply setq to st. This
illustrates that a variable assigned by setq or mv-setq must either
be declared in a WITH clause or be a known stobj. Of course, here
st is a known stobj. In fact, stobjs are not allowed to be declared in
WITH clauses (and that is not necessary for assigning to them).
The OF-TYPE Keyword
So far our examples have all involved loop$ expressions that are
evaluated directed at the ACL2 prompt. These do not require the OF-TYPE
keyword described in this section. But loop$ expressions may also appear
in definitions. When these definitions are to be guard-verified,
OF-TYPE keyword may be critical.
Consider the following example, which searches for an even number in a
given list of integers, returning t if one is found and else nil.
As usual, we start by including the usual book for reasoning about
loop$.
(include-book "projects/apply/top" :dir :system)
(defun has-evenp (x)
(declare (xargs :guard (integer-listp x)))
(loop$ with temp of-type (satisfies integer-listp) = x
do
(cond ((endp temp)
(return nil))
((evenp (car temp))
(return t))
(t
(setq temp (cdr temp))))))
We see that the expression immediately following OF-TYPE is a legal
type-spec, in this case expressing that (integer-listp temp) holds
for every value of temp during execution of the loop$. Let's see
why this use of OF-TYPE is necessary. When it is omitted, guard
verification fails with the following top-level checkpoints.
Subgoal 1.2
(IMPLIES (AND (ALISTP ALIST)
(NOT (CONSP (CDR (ASSOC-EQ-SAFE 'TEMP ALIST)))))
(NOT (CDR (ASSOC-EQ-SAFE 'TEMP ALIST))))
Subgoal 1.1
(IMPLIES (AND (ALISTP ALIST)
(CONSP (CDR (ASSOC-EQ-SAFE 'TEMP ALIST))))
(INTEGERP (CADR (ASSOC-EQ-SAFE 'TEMP ALIST))))
To understand these checkpoints we need to understand a bit about how ACL2
gives a semantics to DO loop$ expressions (as we explain in more
detail in the section on Semantics below). In the ACL2 logic, a DO
loop$ expression is represented as a transformation on an association
list, named alist, that assigns values to every variable in the
expression. This alist is transformed by each iteration through the loop.
The value of the variable temp in alist is (assoc-eq-safe
'temp alist), where assoc-eq-safe is just a variant of assoc
whose guard makes no requirements on the alist. The first checkpoint
above (Subgoal 1.2) thus says that if the value of temp is not a cons,
then it's nil. That requirement comes from the expression, (endp
temp), since the guard of endp is that its argument is a cons or
nil. The second checkpoint (Subgoal 1.1) says that if the value of
temp is a cons, then its car is an integer. That requirement comes
from the expression (evenp (car temp)), since the guard for evenp
requires its argument to be an integer.
When we add the restriction provided by the OF-TYPE keyword that
temp satisfies integer-listp, the checkpoints each get the added
hypothesis (integer-listp (cdr (assoc-eq-safe 'temp alist))). That
allows the guard proof to go through. This addition also imposes that same
requirement on the initial alist, but it is discharged because the guard for
has-evenp specifies (integer-listp x) and temp is initially
assigned to x. Importantly, use of the OF-TYPE keyword on a
variable imposes a guard proof obligation for every assignment to that
variable, that the new value of that variable also satisfies the given type.
In this case, this means that under the hypotheses that (endp temp) and
(evenp (car temp)) are false, and also assuming that temp satisfies
integer-listp — where here, temp is (cdr (assoc-eq-safe
'temp alist)) — then (cdr temp) satisfies integer-listp.
ACL2 discharges this requirement automatically.
The :GUARD Keyword
Consider the following definition, which is identical to the one for
has-evenp displayed above except that instead of using the OF-TYPE
keyword, it uses the :GUARD keyword.
(defun has-evenp (x)
(declare (xargs :guard (integer-listp x)))
(loop$ with temp = x
do
:guard (integer-listp temp)
(cond ((endp temp)
(return nil))
((evenp (car temp))
(return t))
(t
(setq temp (cdr temp))))))
This definition is accepted by ACL2 for much the same reason that the
preceding one was accepted. The difference is that while the OF-TYPE
keyword adds a requirement at every assignment of the variable, the
:GUARD imposes the invariant that when the guard holds entering the
loop$ body, it also holds when the loop$ body is next entered. Thus
we see the following in the Goal generated for the guard conjecture,
where new-alist is let-bound (not shown here) to the result of updating
alist after one iteration through the loop, and where (equal exit-flg
nil) indicates that another iteration is pending (because neither a
return nor a loop-finish was executed).
(IMPLIES (AND (AND (ALISTP ALIST)
(INTEGER-LISTP (CDR (ASSOC-EQ-SAFE 'TEMP ALIST))))
(EQUAL EXIT-FLG NIL))
(AND (ALISTP NEW-ALIST)
(INTEGER-LISTP (CDR (ASSOC-EQ-SAFE 'TEMP NEW-ALIST)))))
The :guard is generally ignored when it is within the definition's
body for a guard-verified or a :program-mode function. The
reason is that in these cases, the loop$ expression is converted to a
Common Lisp loop expression. (There are exceptions involving set-guard-checking and invariant-risk.) However, in other cases the
:guard is checked at runtime. Consider the following example.
(defun f (lst)
(loop$ with x = lst
do
:guard (consp x)
(cond ((consp x)
(setq x (cdr x)))
(t (return x)))))
Here we see a runtime guard violation.
ACL2 !>(f '(a b c d))
ACL2 Error [Evaluation] in TOP-LEVEL: The guard for a DO$ form,
(AND (ALISTP ALIST) (CONSP (CDR (ASSOC-EQ-SAFE 'X ALIST)))),
has been violated by the following alist:
((X)).
See :DOC do-loop$.
ACL2 !>
As noted in the preceding section (on “The OF-TYPE
Keyword”), a call of do$ transforms an alist with each iteration
through the loop. The alist initially binds the symbol X to the list
(A B C D), and each iteration modifies that binding by cdring the
value of X, until finally that value is nil — and then a guard
check fails for the value of X, i.e., (CONSP (CDR (ASSOC-EQ-SAFE 'X
ALIST))) is nil.
A more detailed explanation may be found in the final section,
“Semantics”.
The :MEASURE Keyword
The discussion above doesn't address the obvious possibility that a DO
loop$ may not terminate. Consider the following example, which not only
assumes that the usual book has been included as discussed above, but also
assumes that the form (defwarrant princ$) has been evaluated.
ACL2 !>(loop$ with x = '(100 200 300)
do
:values (state)
(setq state (princ$ (car x) *standard-co* state)))
ACL2 Error in TOP-LEVEL: No :MEASURE was provided after the DO operator
and we failed to find a likely measure. Please supply a :MEASURE in
(LOOP$ WITH X = '(100 200 300)
DO :VALUES (STATE)
(SETQ STATE
(PRINC$ (CAR X) *STANDARD-CO* STATE))).
See :DOC loop$.
ACL2 !>
As suggested by the error message, ACL2 has tried to guess a measure, i.e.,
a term whose value is expected to decrease on each successive iteration. This
notion of ``decrease'' is the expected one when the value of the measure is a
natural number: smaller in the sense of <. In general, the measure
decreases in the sense of L< when lex-fix is applied to each
argument; see L<.
Of course, no measure decreases in the example above, because the values of
the variables don't change with each iteration. We can see what happens when
we supply an explicit measure: the body is evaluated, as evidenced by the
appearance of 100 in the output, but then the measure is evaluated and is
seen not to have decreased from what it was at the start of the previous
iteration.
ACL2 !>(loop$ with x = '(100 200 300)
do
:values (state)
:measure (acl2-count x)
(setq state (princ$ (car x) *standard-co* state)))
100
HARD ACL2 ERROR in DO$: The measure, (ACL2-COUNT X), used in the do
loop$ statement
(LOOP$ WITH X = '(100 200 300)
DO :VALUES (STATE)
:MEASURE (ACL2-COUNT X)
(SETQ STATE
(PRINC$ (CAR X) *STANDARD-CO* STATE)))
failed to decrease! Recall that do$ tracks the values of do loop$
variables in an alist. The measure is computed using the values in
the alist from before and after execution of the body. We cannot print
the values of double floats and live stobjs, if any are found in the
alist, because they are raw Lisp objects, not ACL2 objects. We print
any double float as its corresponding rational and simply print the
name of any live stobj (as a string).
Before execution of the do body the alist was
((X 100 200 300) (STATE . "<state>")).
After the execution of the do body the alist was
((X 100 200 300) (STATE . "<state>")).
Before the execution of the body the measure was
603.
After the execution of the body the measure was
603.
Logically, in this situation the do$ returns the value of a term whose
output signature is (STATE), where the value of any component of type
:df is #d0.0 and the value of any stobj component is the last latched
value of that stobj.
ACL2 Error in TOP-LEVEL: Evaluation aborted. To debug see :DOC print-
gv, see :DOC trace, and see :DOC wet.
ACL2 !>
Presumably the following is what was intended.
ACL2 !>(loop$ with x = '(100 200 300)
do
:values (state)
:measure (acl2-count x)
(if (atom x)
(return state)
(progn
(setq state (princ$ (car x) *standard-co* state))
(setq x (cdr x)))))
100200300<state>
ACL2 !>
In fact, the :MEASURE can be omitted in this case; ACL2 is able to
guess (ACL2-COUNT X).
Guard verification requires a proof that the measure does indeed go
down in the sense of L<, after applying lex-fix to the arguments;
see L<. Fortunately, guard verification takes advantage of
information specified by OF-TYPE and :GUARD keywords. For example,
the following two definitions are admitted (after the usual initial
include-book form), even though termination would not be provable without
the OF-TYPE expression in the first and the DO body's :GUARD in the
second; consider the case that n is -1.
(defun foo (max)
(declare (xargs :guard (natp max)))
(loop$ with n of-type (satisfies natp) = max
do
(if (= n 0)
(return 'stop)
(setq n (- n 1)))))
(defun foo (max)
(declare (xargs :guard (natp max)))
(loop$ with n = max
do
:guard (natp n)
(if (= n 0)
(return 'stop)
(setq n (- n 1)))))
A More Complex Example
We conclude with an example presented in the documentation for loop$ that illustrates all the features above. Notice that the :GUARD
keyword may appear not only in the DO body but also in the FINALLY
clause, to specify that the indicated guard holds upon entry to the
FINALLY clause. Here we assume that we have already evaluated not only
the usual include-book form, but also the defstobj and
defwarrant forms above.
(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))))
Notice that any variables bound above the loop$ may appear in it, for
example, the formal parameters of this function. But only variables that are
WITH-bound or declared as stobjs may be assigned with setq or
mv-setq. The :GUARD of (stp st) is necessary, because ACL2
does not automatically infer that stobj recognizer calls hold inside
loop$ expressions the way it does in ordinary bodies of defun
forms.
We can evaluate the function above, as in the following example.
ACL2 !>(test-loop$ 3 8 st)
((FROM 3 TO 8 IS 5 STEPS AND FLD = 7)
<st>)
ACL2 !>
SYNTAX
General Form:
(LOOP$ WITH var1 OF-TYPE spec1 = init1 ; a WITH declaration
WITH var2 OF-TYPE spec2 = init2
...
DO
:measure m
:guard do-guard
:values v
do-body
FINALLY
:guard fin-guard
fin-body)
where much of that is optional: ``OF-TYPE speci'', ``=
initi'' (when ``OF-TYPE speci'' is present), ``:MEASURE m'', the
two ``:GUARD ...'' clauses, ``:VALUES v'', and ``FINALLY
fin-body''. If the :MEASURE is omitted, ACL2 tries to guess a likely
measure using the same heuristic it does with recursive defuns. If
:VALUES is omitted then v defaults to (nil); it indicates the
shape of the return value for the loop$ expression.
Do-body must be a cons, not an atom, as must each of the following
that is supplied: m, do-guard, v, fin-guard, and
fin-body.
All ACL2 function symbols in the measure m and the two bodies must be
badged so apply$ can handle them. Furthermore, they must be
warranted if proofs are to be done about them or if they are in logic mode and are called during evaluation.
The do-body and fin-body positions are to be what we call
``DO-body term''. These are not, in general, normal ACL2 terms! They
allow restricted uses of RETURN, PROGN, SETQ, MV-SETQ, and
LOOP-FINISH as described below. In the descriptions below we ignore
the distinctions between translated and untranslated terms; see term).
As usual, the restrictions on return values apply only to code, not to terms
occurring in theorem statements.
- Every ordinary term that returns a single, non-stobj value
- An IF call whose first argument is an ordinary term (which
necessarily returns a single, non-stobj value) and whose true and false
branches are DO-body terms
- A LET, LET*, or MV-LET expression, subject to the following
restrictions (unless the term is an ordinary term).
- The terms in the bindings are all ordinary terms.
- The body is a DO-body term.
- No variable bound in the bindings is WITH-bound, a known stobj, or a variable occurring free in the surrounding DO loop$
expression.
- (PROGN term1 term2 ... termk), where each termi is a DO-body
term; also (PROG2 term1 term2) in that case
- (RETURN term), where term is an ordinary term
- (LOOP-FINISH), but only in a DO body, not in a FINALLY
clause
- (SETQ var term), where the variable var is declared in a
WITH declaration or is a stobj name, and term is an ordinary term
that returns a single value, that value being a stobj of type var if
var is a stobj
- (MV-SETQ (var0 ... varn) term) for two or more distinct variables
vari, where each vari is declared in a WITH declaration or is a
stobj name, and term is an ordinary term that returns n+1 values, where
if vari is a stobj then the ith value returned is of that type
Notice that in code, where restrictions on return values are in force, no
stobj may be let-bound in a DO body or FINALLY clause. This is due
not only to the explicit restriction above for LET, LET*, and
MV-LET expressions, but also due to the first condition above, on
ordinary terms returning a single, non-stobj value.
We conclude this section by discussing some syntactic restrictions.
The following restriction applies to loop$ expressions meeting the
following two conditions: :VALUES specifies other than the default of
(NIL), and there is at least one loop-finish expression in the
loop$ body. In that case, there must be a FINALLY clause that ACL2
recognizes as always executing a return call. This makes sense, since in
Common Lisp, the value returned by a loop is nil when ``falling
through'' without executing a return; but nil would violate the
specified :VALUES in the case above.
As noted above, assignments with setq and mv-setq may only set
stobj variables and variables declared using WITH. This restriction
applies to the innermost loop$ that contains the assignment. The
following, for example, is illegal because the WITH declaration for
x is not in the loop$ immediately above the assignment to x
with setq.
(defun do-loop-nested-outer-with-var-bad (lst)
(loop$ with x = lst
do
(return
(loop$ with temp = '(1 2 3)
do
(cond ((endp temp)
(return (pairlis$ x x)))
(t (progn (setq x (cons (car temp) x))
(setq temp (cdr temp)))))))))
However, we expect it to be easy in general to work around this
restriction. The following definition, for example, accomplishes what was
presumably intended above and is accepted by ACL2.
(defun do-loop-nested-outer-with-var (lst)
(loop$ with x = lst
do
(return
(loop$ with temp = '(1 2 3)
with x = x
do
(cond ((endp temp)
(return (pairlis$ x x)))
(t (progn (setq x (cons (car temp) x))
(setq temp (cdr temp)))))))))
Every return expression in the DO body and (if present) FINALLY
clause must return a value or multiple-values consistent with what is
specified by the :VALUES keyword (by default, a single ordinary value).
Note that this requirement does not tolerate the replacement of a stobj by a
stobj that is congruent to it.
It is illegal for a loop$ expression to be in the scope of function
bindings of an flet or macrolet expression.
As noted above, the measure, body, and FINALLY clauses of a DO
loop$ must be fully badged.
In a function call, it is illegal for a LOOP$ expression to occur in a slot
whose ilk is not nil.
SEMANTICS
Consider again the initial example in the Informal Introduction above.
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 !>
We have seen that after initializing variables using WITH clauses,
each iteration of a DO loop$ updates those variables by evaluating
the body of the loop (i.e., the term after the DO keyword), until a
return expression is executed to return the current value of a term
— in this case, the current value of the term, y.
Of course, progn and return are not ACL2 functions! (Recall that
the word ``applicative'' is part of what ``ACL2'' abbreviates.) The following
term is essentially what is produced from the loop$ expression above. We
discuss it below.
(DO$ ; Measure Function
(LAMBDA$ (ALIST)
(LET ((X (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(Y (CDR (ASSOC-EQ-SAFE 'Y ALIST))))
(ACL2-COUNT X)))
; Initial Alist
(LIST (CONS 'X '(A B C))
(CONS 'Y NIL))
; Body Function
(LAMBDA$ (ALIST)
(LET ((X (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(Y (CDR (ASSOC-EQ-SAFE 'Y ALIST))))
(IF (CONSP X)
(LIST NIL
NIL ; irrelevant
(LIST (CONS 'X (CDR X))
(LIST* 'Y (CAR X) Y)))
(LIST :RETURN
Y
(LIST (CONS 'X X) (CONS 'Y Y))))))
... ; Other arguments are omitted here.
)
The display above is approximate; in particular, it hides some logically
irrelevant clutter such as declare forms and it shows only arguments
of do$ relevant to our discussion of the example above. Also, the
display employs user-level syntax (i.e., an untranslated term; see
term). See also the subsection of lambda$ entitled ``About
Lambda$s and Prover Output.''
The definition of do$ is given later in this topic, for those who care
to explore it, but this discussion is intended to be self-contained. Do$
operates by maintaining an alist that maps variables to values, for all
variables referenced in the loop$ expression — though only
variables that are declared in WITH clauses or are stobjs may be
modified. This alist is updated on each iteration by calling apply$
on the ``Body Function'' above, producing a 3-element list (exit-token val
new-alist). If exit-token is :RETURN then val is returned.
But if exit-token is nil, then do$ is called recursively with
new-alist as its alist argument.
To see do$ in action one can submit the following forms. Here the
body of f is just the loop$ expression shown above. Notice that
f is not guard-verified; after submitting (verify-guards f)
the loop$ expression is evaluated as a Common Lisp loop call rather
than using do$, so there would be no trace output. Don't worry
about having a precise understanding of the fancy calls of trace!; the
comments there should suffice.
(include-book "projects/apply/top" :dir :system)
(defun f ()
(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)))))
; Store the translated body function so that we can access it later
; with (@ my-body-fn):
(trace! (do$ :entry (f-put-global 'my-body-fn (nth 2 arglist) state)))
; Run f to store to my-body-fn as commented above.
(f)
; Trace do$ calls and trace calls of apply$ on the body function.
(trace! (do$ :notinline t ; include recursive calls
:cond (eq traced-fn 'do$) ; skip *1* call
:entry (list traced-fn alist))
(apply$ :cond (equal (car arglist) (@ my-body-fn))
:entry (list traced-fn
(cadr arglist) ; the alist
)))
(f)
Here is the trace output from the final call of f above; analysis
follows.
ACL2 !>(f)
1> (DO$ ((X A B C) (Y)))
2> (APPLY$ (((X A B C) (Y))))
<2 (APPLY$ (NIL NIL ((X B C) (Y A))))
2> (DO$ ((X B C) (Y A)))
3> (APPLY$ (((X B C) (Y A))))
<3 (APPLY$ (NIL NIL ((X C) (Y B A))))
3> (DO$ ((X C) (Y B A)))
4> (APPLY$ (((X C) (Y B A))))
<4 (APPLY$ (NIL NIL ((X) (Y C B A))))
4> (DO$ ((X) (Y C B A)))
5> (APPLY$ (((X) (Y C B A))))
<5 (APPLY$ (:RETURN (C B A) ((X) (Y C B A))))
<4 (DO$ (C B A))
<3 (DO$ (C B A))
<2 (DO$ (C B A))
<1 (DO$ (C B A))
(C B A)
ACL2 !>
First consider the calls of do$ above. You can see that X is
initially bound in the alist to (A B C), but on successive do$
calls, X is bound to successive cdrs of (A B C). Meanwhile,
the accumulator variable Y is initially bound to NIL but at each
call of do$, the next car of (A B C) is pushed onto the binding
of Y. Now consider the calls of apply$. Up until the last call,
apply$ing the body function results in a triple of the form (mv nil
nil new-alist), where new-alist is supplied as the alist argument for
the next do$ call. The last call of apply$ on the body function
gives the result (mv :RETURN (C B A) new-alist), where (C B A) is
the value returned by the calls of do$.
Now consider this variant of the above example, which was given above when
introducing FINALLY clauses.
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 (loop-finish)))
finally (return y))
(C B A)
ACL2 !>
The corresponding do$ call is similar to that of the preceding
example, but notice :LOOP-FINISH in place of :RETURN, and notice
that we show the fourth argument this time: the function corresponding to the
FINALLY clause.
(DO$ ; Measure Function
(LAMBDA$ (ALIST)
(LET ((X (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(Y (CDR (ASSOC-EQ-SAFE 'Y ALIST))))
(ACL2-COUNT X)))
; Initial Alist
(LIST (CONS 'X '(A B C))
(CONS 'Y NIL))
; Body Function
(LAMBDA$ (ALIST)
(LET ((X (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(Y (CDR (ASSOC-EQ-SAFE 'Y ALIST))))
(IF (CONSP X)
(LIST NIL
NIL ; irrelevant
(LIST (CONS 'X (CDR X))
(LIST* 'Y (CAR X) Y)))
(LIST :LOOP-FINISH
NIL ; irrelevant
(LIST (CONS 'X X) (CONS 'Y Y))))))
; FINALLY function
(LAMBDA$ (ALIST)
(LET ((X (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(Y (CDR (ASSOC-EQ-SAFE 'Y ALIST))))
(LIST :RETURN
Y
(LIST (CONS 'X X) (CONS 'Y Y)))))
; Values (output signature)
'(NIL)
... ; Last argument omitted here.
)
Above, we also took the opportunity to show the fifth argument of do$,
which is the output signature of the logical value to be returned should the
measure fail to decrease. That output signature is specified with the
:VALUES keyword in a do loop$. If omitted and the loop$
returns a single ordinary object, the output signature is (nil) as here.
The values argument to do$ is passed along unchanged as the function
iterates and, should the measure fail to decrease, the signature is used to
compute a default answer. However, that default answer is never relevant to
evaluations because a hard ACL2 error actually occurs. The default answer may
be relevant when reasoning about do$ calls. Since guard verification of
a do loop$ guarantees termination, the default answer is never
relevant when dealing with guard verified functions containing do
loop$s.
Here is the definition of do$.
Function: do$
(defun do$ (measure-fn alist do-fn finally-fn values dolia)
(declare (xargs :guard (and (apply$-guard measure-fn '(nil))
(apply$-guard do-fn '(nil))
(apply$-guard finally-fn '(nil))
(weak-dolia-p dolia))))
(let* ((triple (true-list-fix (apply$ do-fn (list alist))))
(exit-token (car triple))
(val (cadr triple))
(new-alist (caddr triple)))
(cond
((eq exit-token :return) val)
((eq exit-token :loop-finish)
(let*
((triple (true-list-fix (apply$ finally-fn (list new-alist))))
(exit-token (car triple))
(val (cadr triple)))
(if (eq exit-token :return) val nil)))
((l< (lex-fix (apply$ measure-fn (list new-alist)))
(lex-fix (apply$ measure-fn (list alist))))
(do$ measure-fn new-alist
do-fn finally-fn values dolia))
(t
(prog2$
(let
((all-stobj-names
(true-list-fix (access dolia dolia :all-stobj-names)))
(untrans-measure (access dolia dolia :untrans-measure))
(untrans-do-loop$ (access dolia dolia :untrans-do-loop$)))
(er
hard? 'do$
"The measure, ~x0, used in the do loop$ ~
statement~%~Y12~%failed to decrease! Recall that do$ tracks ~
the values of do loop$ variables in an alist. The measure is ~
computed using the values in the alist from before and after ~
execution of the body. We cannot print the values of double ~
floats and live stobjs, if any are found in the alist, ~
because they are raw Lisp objects, not ACL2 objects. We ~
print any double float as its corresponding rational and ~
simply print the name of any live stobj (as a ~
string).~%~%Before execution of the do body the alist ~
was~%~Y32.~|After the execution of the do body the alist ~
was~%~Y42.~|Before the execution of the body the measure ~
was~%~x5.~|After the execution of the body the measure ~
was~%~x6.~|~%Logically, in this situation the do$ returns the ~
value of a term whose output signature is ~x7, where the ~
value of any component of type :df is #d0.0 and the value of ~
any stobj component is the last latched value of that stobj."
untrans-measure untrans-do-loop$ nil
(eviscerate-do$-alist alist all-stobj-names)
(eviscerate-do$-alist new-alist all-stobj-names)
(apply$ measure-fn (list alist))
(apply$ measure-fn (list new-alist))
values))
(loop$-default-values values new-alist))))))
We conclude by returning to an earlier example that illustrates runtime
guard-checking. But this time we do some tracing, as indicated.
(defun f (lst)
(loop$ with x = lst
do
:guard (consp x)
(cond ((consp x)
(setq x (cdr x)))
(t (return x)))))
(trace! (do$ :entry (list traced-fn alist) :notinline t))
(trace$ do-body-guard-wrapper)
As before, we have a guard violation. The trace output is explained
below.
ACL2 !>(f '(a b c d))
1> (ACL2_*1*_ACL2::DO$ ((X A B C D)))
2> (DO$ ((X A B C D)))
3> (DO-BODY-GUARD-WRAPPER T NIL)
<3 (DO-BODY-GUARD-WRAPPER T)
3> (DO-BODY-GUARD-WRAPPER T NIL)
<3 (DO-BODY-GUARD-WRAPPER T)
3> (DO-BODY-GUARD-WRAPPER T NIL)
<3 (DO-BODY-GUARD-WRAPPER T)
3> (DO$ ((X B C D)))
4> (DO-BODY-GUARD-WRAPPER T NIL)
<4 (DO-BODY-GUARD-WRAPPER T)
4> (DO-BODY-GUARD-WRAPPER T NIL)
<4 (DO-BODY-GUARD-WRAPPER T)
4> (DO-BODY-GUARD-WRAPPER T NIL)
<4 (DO-BODY-GUARD-WRAPPER T)
4> (DO$ ((X C D)))
5> (DO-BODY-GUARD-WRAPPER T NIL)
<5 (DO-BODY-GUARD-WRAPPER T)
5> (DO-BODY-GUARD-WRAPPER T NIL)
<5 (DO-BODY-GUARD-WRAPPER T)
5> (DO-BODY-GUARD-WRAPPER T NIL)
<5 (DO-BODY-GUARD-WRAPPER T)
5> (DO$ ((X D)))
6> (DO-BODY-GUARD-WRAPPER T NIL)
<6 (DO-BODY-GUARD-WRAPPER T)
6> (DO-BODY-GUARD-WRAPPER NIL NIL)
<6 (DO-BODY-GUARD-WRAPPER NIL)
ACL2 Error [Evaluation] in TOP-LEVEL: The guard for a DO$ form,
(AND (ALISTP ALIST) (CONSP (CDR (ASSOC-EQ-SAFE 'X ALIST)))),
has been violated by the following alist:
((X)).
See :DOC do-loop$.
ACL2 !>
To understand the trace output above, we first take a look at the
translation of the loop$ expression above. This time we show the
corresponding do$ form with declare forms included, but as
before some parts of this form are simplified, untranslated, or elided. (You
can see the exact translation by applying :trans to the do$
call.) Note that do-body-guard-wrapper is just an identity function (on
its first argument) used by the implementation, but it is handy here for the
explanation that follows.
(DO$
;; measure:
'(LAMBDA (ALIST)
(DECLARE
(XARGS :GUARD
(DO-BODY-GUARD-WRAPPER
(AND (ALISTP ALIST)
(CONSP (CDR (ASSOC-EQ-SAFE 'X ALIST))))
NIL)))
((LAMBDA (X) (ACL2-COUNT X))
(CDR (ASSOC-EQ-SAFE 'X ALIST))))
;; alist:
(LIST (CONS 'X LST))
;; body:
'(LAMBDA (ALIST)
(DECLARE
(XARGS :GUARD
(DO-BODY-GUARD-WRAPPER
(AND (ALISTP ALIST)
(CONSP (CDR (ASSOC-EQ-SAFE 'X ALIST))))
NIL)))
((LAMBDA (X)
(IF (CONSP X)
(LIST NIL NIL
(LET ((X (CDR X))) (LIST (CONS 'X X))))
(LIST :RETURN X (LIST (CONS 'X X)))))
(CDR (ASSOC-EQ-SAFE 'X ALIST))))
.....)
Recall that do$ works by repeatedly applying the given lambda to its
alist argument, which initially binds 'X to LST as shown above.
Do$ recurs when that application returns a triple (mv nil nil
new-alist), where new-alist is the alist returned by the body of the
loop$ expression. But when do$ applies the given lambda
object, it first checks the :guard of that lambda. We also see that
before do$ recurs, it applies its measure-fn argument to the input
alist and to new-alist.
So let's focus on the following from the end of the trace output above.
5> (DO$ ((X D)))
6> (DO-BODY-GUARD-WRAPPER T NIL)
<6 (DO-BODY-GUARD-WRAPPER T)
6> (DO-BODY-GUARD-WRAPPER NIL NIL)
<6 (DO-BODY-GUARD-WRAPPER NIL)
The first DO-BODY-GUARD-WRAPPER call comes from the guard of the
lambda that represents the body of the do$ loop, from the expression
(apply$ do-fn (list alist)) in the definition of do$ (above). Here
alist is ((X D)), so the conjunct (CONSP (CDR (ASSOC-EQ-SAFE 'X
ALIST))) from that lambda's guard is true. The second call of
DO-BODY-GUARD-WRAPPER comes from the expression (apply$
measure-fn (list new-alist)) in the definition of do$. But
new-alist is nil, so the conjunct (CONSP (CDR (ASSOC-EQ-SAFE 'X
ALIST))) from the measure lambda's guard is false, so the guard evaluates to
nil.
Subtopics
- Do$
- Definition of do$
