		Search-engine friendly clone of the ACL2 documentation.

Loop$-primer

Lp-section-13

Examples of DO Loop$s

LP13: Examples of DO Loop$s

Below is a log of an ACL2 session demonstrating the behavior of a few DO loop$s. As usual with loop$s, one should always work in a session in which the book shown below is included. The examples below do not illustrate guards or proofs about DO loop$s.

We'll describe the syntax and semantics of DO loop$s later. But we expect you can intuit the syntax and semantics of these loop$ statements from these examples. The following may help if you're unfamiliar with the following Common Lisp primitives.

In ACL2, These primitives may only be used within DO loop$s!

(RETURN expr) terminates the loop$ and returns the value of expr as the value.
(SETQ var expr) evaluates expr and assigns the value to the variable var. Parallel assignment with mv-setq is also supported but not illustrated here.
(PROGN stmt_1 … stmt_n) evaluates each stmt_i in turn and returns the value of the last one.
(LOOP-FINISH) terminates the iteration in the loop$ and passes control to the FINALLY clause, if any.

We start the session with the following commands, whose output we do not display here. Note that we use defstobj to introduce a single-threaded object, st, with one field, fld1. We initialize (fld1 st) to 0. In addition, we warrant two of the functions introduced by the defstobj. We warrant those functions because they are user-defined :logic mode functions that we'll use in a DO loop$. Defstobj does not automatically badge or warrant the functions it defines but they are warrantable.

(include-book "projects/apply/top" :dir :system)
(defstobj st fld1)
(update-fld1 0 st)
(defwarrant fld1)
(defwarrant update-fld1)

So having set up our session, we now experiment with DO loop$s.

; Reverse the elements of the initial value of temp.

ACL2 !>(loop$ with temp = '(a b c)
              with  ans = nil
              do
              (cond ((endp temp) (return ans))
                    (t (progn (setq ans (cons (car temp) ans))
                              (setq temp (cdr temp))))))
(C B A)

; Reverse the elements of lst down to the first xxx, or return
; not-found if there is no xxx in lst.

ACL2 !>(defun reverse-to-xxx (lst)
         (loop$ with temp = lst
                with  ans = nil
                do
                (cond ((endp temp) (return 'not-found))
                      (t (progn (cond ((eq (car temp) 'xxx) (loop-finish))
                                      (t (setq ans (cons (car temp) ans))))
                                (setq temp (cdr temp)))))
                finally
                (return ans)))

Since REVERSE-TO-XXX is non-recursive, its admission is trivial.  We
could deduce no constraints on the type of REVERSE-TO-XXX.

Summary
Form:  ( DEFUN REVERSE-TO-XXX ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 REVERSE-TO-XXX

ACL2 !>(reverse-to-xxx '(a b c xxx d e f))
(C B A)

ACL2 !>(reverse-to-xxx '(a b c d e f))
NOT-FOUND

; In the next example we will reverse the elements of the initial value of
; temp, except for the xxx's which we just drop but count.  We use (fld1 st)
; to store the accumulated count.  This loop$ returns the reversed elements
; and the final value of st.  But first we'll show that (fld1 st) is
; initially 0.

ACL2 !>(fld1 st)
0

ACL2 !>(loop$ with temp = '(a b c xxx d e xxx f g)
              with ans = nil
              do
              :values (nil st)
              (cond ((endp temp) (return (mv ans st)))
                    (t (progn
                         (cond ((eq (car temp) 'xxx)
                                (setq st (update-fld1 (+ 1 (fld1 st)) st)))
                               (t (setq ans (cons (car temp) ans))))
                         (setq temp (cdr temp))))))
((G F E D C B A) <st>)

ACL2 !>(fld1 st)
2

We included the last example showing that stobjs can be used inside of DO loop$s just to alert you to that feature. However, in the rest of this primer we do not deal with stobjs in loop$ because there is enough to cover without that!

See the ACL2 documentation topic DO-loop$ for a more thorough discussion of DO loop$s.

Now go to lp-section-14 (or return to the Table of Contents).