		Search-engine friendly clone of the ACL2 documentation.

Prohibition-of-loop$-and-lambda$

Certain events do not allow loop$s or lambda$s

Certain events, including defconst, defmacro, and defpkg, prohibit the use of loop$ and lambda$. The prohibition of loop$s is due to their use of lambda$s, so we focus on why lambda$s are prohibited here.

Lambda$ is prohibited in these events because of the way books are loaded. To speed up the execution of include-book the compiled file for a book is loaded before the events in the book are processed. But the evaluation of lambda$ expressions in raw Lisp depends on the lambda$s having been translated and recorded in the logical world and in the lambda cache (see print-cl-cache). So the execution of these events can't depend on lambda$.

If you have submitted an event that provoked an error citing this topic you must restate the event to avoid those prohibited constructions. Unfortunately, you must also consider ancestral occurrences of the prohibited constructions! We first give two examples of the problem to drive home the message and then we discuss various ways the problem can be dealt with.

Examples of Prohibited Forms

ACL2 !>(defconst *2^10* (apply$ (lambda$ (x) (expt 2 x)) '(10)))

ACL2 Error in ( DEFCONST *2^10* ...):  We prohibit certain events,
including DEFCONST, DEFPKG, and DEFMACRO, from being ancestrally dependent
on loop$ and lambda$ expressions.  But at least one of these prohibited
expressions occurs in this event.  See :DOC prohibition-of-loop$-and-
lambda$.

We will discuss how to avoid such errors in the next section.

Here is an example of an ancestral use of lambda$ in a macro. Suppose we wish to define the macro rat so that (rat "123.4567") expands to the rational 1234567/10000. Our idea is to use loop$ in the definition of the function string-to-rat and then to call string-to-rat in our macro. (We don't recommend this particular use of loop$s to parse a string into a rational but we use it here to make a point later.)

(defun string-to-rat (str)
  (let* ((lst (coerce str 'list))
         (right-of-pt (length (cdr (loop$ for d in lst
                                          as tail on lst
                                          thereis
                                          (if (eql #. d) tail nil))))))
    (loop$ for tail on lst
           when (not (eql (car tail) #.))
           sum
           (* (- (char-code (car tail)) 48)
              (expt 10
                    (- (loop$ for d in tail sum (if (eql d #.) 0 1))
                       (+ 1 right-of-pt)))))))

(defmacro rat (str) (string-to-rat str))

The attempt to define the macro will provoke the error shown above for (defconst *2^10* ...).

Avoiding These Errors

The only way to avoid these errors is to not use lambda$ or loop$ in these events! We can fix the particular defconst example above simply with

(defconst *2^10* (apply$ 'expt '(2 10)))

or, better yet, by

(defconst *2^10* (expt 2 10))

since there is reason apply$ is involved at all.

When it is hard to avoid the prohibited constructs you might be able to use make-event to do the necessary computation during the creation of the event, though this technique seems mainly applicable to defconst and much less useful to the defmacro case.

(make-event
  `(defconst *2^10*
    ',(apply$ (lambda$ (x) (expt 2 x)) '(10))))

However, in general, removing all uses of loop$ and lambda$ can require a lot of re-coding. For example, fixing the rat macro requires several old-fashioned recursive definitions to carry out the iterations done with loop$.

(defun old-fashioned-string-to-rat1 (lst power)
  (cond
   ((endp lst) 0)
   ((eql (car lst) #.)
    (old-fashioned-string-to-rat1 (cdr lst) power))
   (t (+ (* (- (char-code (car lst)) 48)
            (expt 10 power))
         (old-fashioned-string-to-rat1 (cdr lst) (- power 1))))))

(defun left-of-pt (lst)
  (cond ((endp lst) 0)
        ((eql (car lst) #.) 0)
        (t (+ 1 (left-of-pt (cdr lst))))))

(defun old-fashioned-string-to-rat (str)
  (let ((lst (coerce str 'list)))
    (old-fashioned-string-to-rat1 lst (- (left-of-pt lst) 1))))

(defmacro rat (str) (old-fashioned-string-to-rat str))

Another way to eliminate loop$ and lambda$ is to replace the offending expressions with their translations. There is no prohibition of fully-translated quoted lambda objects, just of lambda$ expressions.

(defun string-to-rat (str)
  ((LAMBDA
    (LST)
    ((LAMBDA
      (RIGHT-OF-PT LST)
      (SUM$+
       '(LAMBDA
         (LOOP$-GVARS LOOP$-IVARS)
         (DECLARE (IGNORABLE LOOP$-GVARS LOOP$-IVARS))
         ((LAMBDA
           (RIGHT-OF-PT TAIL)
           (BINARY-*
            (BINARY-+ '-48 (CHAR-CODE (CAR TAIL)))
            (EXPT
             '10
             (BINARY-+
              (SUM$
               '(LAMBDA (LOOP$-IVAR)
                        (DECLARE (IGNORABLE LOOP$-IVAR))
                        ((LAMBDA (D) (IF (EQL D '#.) '0 '1))
                         LOOP$-IVAR))
               TAIL)
              (UNARY-- (BINARY-+ '1 RIGHT-OF-PT))))))
          (CAR LOOP$-GVARS)
          (CAR LOOP$-IVARS)))
       (CONS RIGHT-OF-PT 'NIL)
       (WHEN$+
        '(LAMBDA
          (LOOP$-GVARS LOOP$-IVARS)
          (DECLARE (IGNORABLE LOOP$-GVARS LOOP$-IVARS))
          ((LAMBDA (TAIL)
                   (NOT (EQL (CAR TAIL) '#.)))
           (CAR LOOP$-IVARS)))
        'NIL
        (LOOP$-AS (CONS (TAILS LST) 'NIL)))))
     (LENGTH
      (CDR
       (THEREIS$+
        '(LAMBDA
          (LOOP$-GVARS LOOP$-IVARS)
          (DECLARE (IGNORABLE LOOP$-GVARS LOOP$-IVARS))
          ((LAMBDA (D TAIL)
                   (IF (EQL '#. D) TAIL 'NIL))
           (CAR LOOP$-IVARS)
           (CAR (CDR LOOP$-IVARS))))
        'NIL
        (LOOP$-AS (CONS LST (CONS (TAILS LST) 'NIL))))))
     LST))
   (COERCE STR 'LIST)))

If we define string-to-rat as above then we can define the rat macro as originally desired and the defmacro is accepted.

But there are several arguments against this approach in general:

Defconst, defmacro and defpkg not only prohibit loop$ and lambda$ but also prohibit all uses of apply$ and scions if user-defined functions are involved in the function objects. This is because to compute logically with them one must have warrant hypotheses and there is no provision for supplying warrants with these events. See ignored-attachment. It turns out that the hideous example above does not mention any user-defined functions in the function objects, so this restriction doesn't stop us here.
Eliminating loop$ in favor of scions sacrifices execution speed if the loop$s are guard verified. A guard-verified loop$ executes in raw Lisp as a Common Lisp loop, whereas its translation into nested calls of loop$ scions, even if guard verified, involves far more function calls.
It is much harder to ``maintain'' code derived this way!

There may be cases where no user-defined functions are involved, efficiency doesn't matter, and the loop$ scion translation of a loop$ is as perspicuous as the loop$ itself. So don't dismiss this approach out of hand.