Iteration with an analogue of the Common Lisp

The Introduction below is followed by a discussion of types and guards.
For a discussion of how to state effective lemmas about

But before we get started we emphasize a few key points.

- As noted, The Loop$ Primer (see loop$-primer) may be a good place
to start if you're using ACL2
loop$ s for the first time. - The Table of Contents of the Loop$ Primer (see lp-section-0) lists
some sensible entry points to primer. You'll see sections devoted to
examples, sample proofs, exercises, etc. Keep the primer in mind as an
additional resource. For example, you might visit
Loop$ Primer Section 6 (lp-section-6) for some exercises on writingloop$ s and, when you get to the end, ignore the “Now go to lp-section-7,” and use your browser's Back key to return to the general hypertext user's manual. **Many examples**of`loop$`expressions may be found in community-bookprojects/apply/loop-tests.lisp .- The semantics of
loop$ involveapply$ . Therefore, before usingloop$ , it is**strongly recommended**that you include the same book as is typically included when using`apply$`, as follows.(include-book "projects/apply/top" :dir :system)

- ACL2
loop$ statements are executed as Common Lisploop statements after the relevant guard conjectures are proved. Common Lisploop statements generally execute much faster than equivalent (tail-recursive) functions. **Warning:**Loop$ implements only a modest part of the functionality of Common Lisp'sloop . Aside from the simple fact thatloop$ allows only a limited subset of the syntax ofloop , the main restriction is that the subexpressions of theloop$ expression that are evaluated repeatedly must be tame! These expressions include not only the loop body but, if present, theUNTIL test, theWHEN test, and theFINALLY clause (all discussed below). Thus, all the function symbols used in these expressions must be badged (see`defbadge`and`defwarrant`). Further restrictions are enforced for`defun`'d functions in which recursive calls appear inloop$ bodies, but we say little about that in this documentation topic; see loop$-recursion. We recommend that users unfamiliar withloop$ acquaint themselves with the material below and in for-loop$ before wading intoloop$-recursion !

As noted above, there are two classes of

Below we introduce these two classes of `state`
or stobjs, and they always return a single value.

ACL2's `guard` expressions (discussed below) in
certain places and these are ignored by Common Lisp.

Next we present some

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

Our first

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

But notice the `defwarrant` events below! They are required because
the functions `defstobj` event below. This is in
contrast to the

The semantics of

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 `apply$`: in each iteration
through the loop, a lambda object based on the body of the

The documentation for `apply$` illustrates a simple

In this section we document basic aspects of the `loop$` expressions. See for-loop$ and
do-loop$ for detailed documentation on guards for

The first example below is an acceptable `defun`
that was to be guard verified. The problem is that

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

The examples just above are of

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

As suggested above, when a

- 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$