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 prove inductive theorems about

**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$-recursion
- Defining functions that recur from within
FOR loop$ expressions - For-loop$
- Iteration with
`loop$`over an interval of integers or a list - Do-loop$
- Iteration with
`loop$`using local variables and stobjs - Loop$-recursion-induction
- Advice on inductive theorems about
`loop$`-recursive functions - Loop$-proofs
- Proving inductive theorems about
loop$ s