Iteration with `loop$` using local variables and stobjs

This topic assumes that you have read the introduction to

More examples of `loop$` expressions, including

The most basic

(loop$ WITH v1 = a1 ... WITH vn = an DO body)

**A Basic Example**

The example

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

- Initially, variables are initialized according to the
WITH clauses: for each bindingWITH Vi = Ei , we say thatVi is a, andWITH -bound variableVi is initially bound to the value ofEi .- In this example,
x is initially bound to the list(a b c) andy is initially bound tonil .

- In this example,
- Then, the
*loop body*— i.e., the term after theDO keyword — is repeatedly evaluated. An update toWITH -bound variableVj occurs whenever an expression(setq Vj Ej) is encountered while evaluating the loop body, bindingVj to the value ofEj (which may reference the current values ofWITH -bound variables). - Ultimately an expression
(RETURN E) should be encountered, in which case the value ofE is returned — where as before,E may reference the current values ofWITH -bound variables.- In this example, when
x is not a cons (and hence is, in fact,nil ), the current value ofy is returned as the value of theloop$ expression. By this point each element of the initial value ofx has been pushed ontoy , so the value(c b a) is returned.

- In this example, when

Note that

Also note that the

ACL2 !>(loop$ with x = (* 3 4) with y = (* 10 x) do (return (list y))) (120) ACL2 !>

See lp-section-14 of the

**Parallel Assignment Using Mv-setq**

ACL2 also supports parallel assignment to two or more variables, using

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

**The FINALLY Clause**

We have seen the

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

The value returned by a

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

**The :VALUES Keyword**

The

Below we introduce a stobj and add a warrant for its accessor
and updater. Warrants are necessary for functions called in

(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

Notice that the examples above apply

**The OF-TYPE Keyword**

So far our examples have all involved

Consider the following example, which searches for an even number in a
given list of integers, returning

(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

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

The value of the variable `assoc`
whose guard makes no requirements on the alist. The first checkpoint
above (Subgoal 1.2) thus says that if the value of `endp` is that its argument is a cons or
`evenp`
requires its argument to be an integer.

When we add the restriction provided by the `integer-listp`, the checkpoints each get the added
hypothesis

**The :GUARD Keyword**

Consider the following definition, which is identical to the one for

(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

(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 `program`-mode function. The
reason is that in these cases, the `set-guard-checking` and invariant-risk.) However, in other cases the

(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

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

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

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

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. Before execution of the do body the alist was ((X 100 200 300) (STATE . ACL2_INVISIBLE::|The Live State Itself|)). After the execution of the do body the alist was ((X 100 200 300) (STATE . ACL2_INVISIBLE::|The Live State Itself|)). 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

Guard verification requires a proof that the measure does indeed go
down in the sense of

(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

(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 `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 !>

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: ```defun`s. If

All ACL2 function symbols in the measure `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 **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* , orMV-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 eachtermi is a DO-body term; also(PROG2 term1 term2) in that case(RETURN term) , whereterm is an ordinary term(LOOP-FINISH) , but only in a DO body, not in aFINALLY clause(SETQ var term) , where the variablevar is declared in aWITH declaration or is a stobj name, andterm is an ordinary term that returns a single value, that value being a stobj of typevar ifvar is a stobj(MV-SETQ (var0 ... varn) term) for two or more distinct variablesvari , where eachvari is declared in aWITH declaration or is a stobj name, andterm is an ordinary term that returns n+1 values, where ifvari 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

We conclude this section by discussing some syntactic restrictions.

The following restriction applies to

As noted above, assignments with

(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

It is illegal for a `flet` or `macrolet` expression.

As noted above, the measure, body, and

In a function call, it is illegal for a LOOP$ expression to occur in a slot
whose ilk is not

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

Of course,

(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 *untranslated term*; see
term). See also the subsection of `lambda$` entitled ``About

The definition of `apply$`
on the ``Body Function'' above, producing a 3-element list

To see `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

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 `apply$`. Up until the last call,

Now consider this variant of the above example, which was given above when
introducing

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$ ; 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) ... ; Other arguments are omitted here. )

Above, we also took the opportunity to show the fifth argument of

Here is the definition of `do$`.

**Function: **

(defun do$ (measure-fn alist do-fn finally-fn values untrans-measure untrans-do-loop$) (declare (xargs :guard (and (apply$-guard measure-fn '(nil)) (apply$-guard do-fn '(nil)) (apply$-guard finally-fn '(nil))))) (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 untrans-measure untrans-do-loop$)) (t (prog2$ (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. 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) (eviscerate-do$-alist new-alist) (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) <3 (DO-BODY-GUARD-WRAPPER T) 3> (DO-BODY-GUARD-WRAPPER T) <3 (DO-BODY-GUARD-WRAPPER T) 3> (DO-BODY-GUARD-WRAPPER T) <3 (DO-BODY-GUARD-WRAPPER T) 3> (DO$ ((X B C D))) 4> (DO-BODY-GUARD-WRAPPER T) <4 (DO-BODY-GUARD-WRAPPER T) 4> (DO-BODY-GUARD-WRAPPER T) <4 (DO-BODY-GUARD-WRAPPER T) 4> (DO-BODY-GUARD-WRAPPER T) <4 (DO-BODY-GUARD-WRAPPER T) 4> (DO$ ((X C D))) 5> (DO-BODY-GUARD-WRAPPER T) <5 (DO-BODY-GUARD-WRAPPER T) 5> (DO-BODY-GUARD-WRAPPER T) <5 (DO-BODY-GUARD-WRAPPER T) 5> (DO-BODY-GUARD-WRAPPER T) <5 (DO-BODY-GUARD-WRAPPER T) 5> (DO$ ((X D))) 6> (DO-BODY-GUARD-WRAPPER T) <6 (DO-BODY-GUARD-WRAPPER T) 6> (DO-BODY-GUARD-WRAPPER 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 `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$ ;; measure: '(LAMBDA (ALIST) (DECLARE (XARGS :GUARD (DO-BODY-GUARD-WRAPPER (AND (ALISTP ALIST) (CONSP (CDR (ASSOC-EQ-SAFE 'X ALIST))))))) ((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))))))) ((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

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) <6 (DO-BODY-GUARD-WRAPPER T) 6> (DO-BODY-GUARD-WRAPPER NIL) <6 (DO-BODY-GUARD-WRAPPER NIL)

The first

- Do$
- Definition of
do$