		Search-engine friendly clone of the ACL2 documentation.

Utilities

Defloop

Macro for defining simple iteration schemes as functions.

Syntax:

DEFLOOP name arglist [documentation] {declaration}* loop-form

loop-form ::= (FOR ({!for-clause}+) main-clause)

for-clause ::= for-in-clause | for-on-clause

for-in-clause ::= (var IN arg [ BY fn ])

for-on-clause ::= (var ON arg [ BY fn ])

main-clause ::= !list-accumulation | (!conditional form !value-clause) |
                (!termination-test form)

value-clause ::= !list-accumulation | (RETURN form)

list-accumulation ::= ({COLLECT | APPEND} form)

value-clause ::= ({COLLECT | APPEND | RETURN} form)

conditional ::= IF | WHEN | UNLESS

termination-test ::= ALWAYS | THEREIS | NEVER

Arguments and Values:

arg -- a symbol appearing in the arglist.

arglist -- an argument list satisfying ACL2::ARGLISTP.

declaration -- any valid declaration.

documentation -- a string; not evaluated.

form -- a form.

fn -- a symbol; must be the function symbol of a unary function
      well-defined on true lists.

var -- a symbol.

name -- a symbol.

Special Note: The symbols FOR, IN, ON, BY, RETURN, COLLECT, APPEND, IF, WHEN, UNLESS, ALWAYS, THEREIS, and NEVER appearing above may be in any package; DEFLOOP checks the print name of the symbol, not the symbol itself.

Description

DEFLOOP is a macro that creates iterative functions. The description of the iteration is specified with an abstract syntax based on a small but useful subset of the Common Lisp LOOP construct (as defined by ANSI X3J13). Using DEFLOOP one can easily define functions analogous to MAPCAR and MAPCAN, list type recognizers, and MEMBER- and ASSOC-like functions.

The syntax of DEFLOOP is similar to DEFUN: The function name is followed by the arglist, optional documentation and declarations, and the function body. Note that any guards on any of the arguments are the responsibility of the user.

The function body is in a special format, i.e., the loop-form as defined in the Syntax description.

Each for-clause defines an iteration on one of the args in arglist. The for-in-clause

(var IN arg [ BY fn ])

specifies that in each iteration, var will be bound to successive CARs of arg, and arg will be reduced by fn on each iteration. The default value of fn is CDR. The for-on-clause

(var ON arg [ BY fn ])

specifies that var will first be bound to arg, and then reduced by fn on each iteration. Again, the default value of fn is CDR.

Using a list-accumulation one can specify MAPCAR- and MAPCAN-like functions. Here is an example of how the Acl2 function STRIP-CARS could be defined with DEFLOOP:

(DEFLOOP STRIP-CARS (L)
  (DECLARE (XARGS :GUARD (ALISTP L)))
  (FOR ((X IN L))
       (COLLECT (CAR X))))

Iteration on multiple lists may be specified; iteration will terminate as soon as any of the lists are ATOMic, e.g.,

(DEFLOOP PAIRLIS$ (KEYS VALS)
  (DECLARE (XARGS :GUARD (AND (TRUE-LISTP KEYS)
                              (TRUE-LISTP VALS))))
  (FOR ((KEY IN KEYS) (VAL IN VALS))
       (COLLECT (CONS KEY VAL))))

This example shows reduction by a function other than CDR:

(DEFLOOP EVENS (L) (FOR ((X IN L BY CDDR)) (COLLECT X)))

List-accumulations can be coupled with a test, e.g., this function that selects all of the numbers <= n from l, and the ODDS function:

(DEFLOOP <=-LIST (N L)
  (DECLARE (XARGS :GUARD (AND (INTEGERP N)
                              (INTEGERP-LISTP L))))
  (FOR ((X IN L))
       (WHEN (<= X N)
         (COLLECT X))))

(DEFLOOP ODDS (L)
  (DECLARE (XARGS :GUARD (TRUE-LISTP L)))
  (FOR ((TAIL ON L BY CDDR))
       (UNLESS (NULL (CDR TAIL))
         (COLLECT (CADR TAIL)))))

The definition of <=-LIST shows that any functional arguments may appear free in the various DEFLOOP forms. Non-iterated arguments are simply passed unchanged during recursive calls. Also note that IF and WHEN are synonymous as DEFLOOP tests.

A RETURN can also be coupled with a test. If the test is never satisfied then the resulting function will return NIL. Here are examples of how ASSOC-EQUAL and MEMBER-EQUAL could have been defined with DEFLOOP:

(DEFLOOP ASSOC-EQUAL (KEY ALIST)
  (DECLARE (XARGS :GUARD (ALISTP ALIST)))
  (FOR ((PAIR IN ALIST))
       (WHEN (EQUAL KEY (CAR PAIR))
         (RETURN PAIR))))

(DEFLOOP MEMBER-EQUAL (X L)
  (DECLARE (XARGS :GUARD (TRUE-LISTP L)))
  (FOR ((TAIL ON L))
       (WHEN (EQUAL X (CAR TAIL))
         (RETURN TAIL))))

The termination-tests can be used to create various recognizers and `un'-recognizers. Note that a DEFLOOP with a termination test of ALWAYS or NEVER will only return T if iteration terminates on NIL, i.e, they only recognize true lists. The termination test (THEREIS form) will return the first non-NIL value returned by form, or NIL if there is none. Here for example are functions that recognize true lists of integers, true lists of un-integers, and lists containing an integer:

(DEFLOOP INTEGERP-LISTP (L) (FOR ((X IN L)) (ALWAYS (INTEGERP X))))

(DEFLOOP NO-INTEGERP-LISTP (L) (FOR ((X IN L)) (NEVER (INTEGERP X))))

(DEFLOOP HAS-INTEGERP-LISTP (L) (FOR ((X IN L)) (THEREIS (INTEGERP X))))

Note that in accordance with the semantics of the LOOP construct, the THEREIS form above simply returns the first non-NIL result computed. If you want a function that returns the first integer in a list then you can use a conditional return:

(DEFLOOP FIRST-INTEGER (L)
  (FOR ((X IN L)) (IF (INTEGERP X) (RETURN X))))

Final note: If in doubt, simply TRANS1 the DEFLOOP form and have a look at the generated function.