		Search-engine friendly clone of the ACL2 documentation.

Do$

Definition of do$

Do$ is the logical function that interprets do loop$s. See do-loop$ for a discussion of do$.

The function takes seven arguments but only the first five are relevant to its logical value.

measure-fn — a lambda object that computes the measure that supposedly decreases (under l<) on each iteration of the do-fn and is checked after each iteration,
alist — an alist the binds the variable symbols used in the body and finally clause (if any) to their values,
do-fn — a lambda object that computes the results of one iteration, where the results are represented by a triple consisting of an exit token that indicates where control goes next, the value (if a return was executed), and a new alist,
finally-fn— a lambda object that computes the value of the finally clause, and
default — the value to be returned if the measure fails to decrease.

Function: do$

(defun do$ (measure-fn alist do-fn finally-fn default
                       untrans-measure untrans-do-loop$)
 (declare (xargs :guard (and (apply$-guard measure-fn '(nil))
                             (apply$-guard do-fn '(nil))
                             (apply$-guard finally-fn '(nil)))))
 (let* ((triple (true-list-fix (apply$ do-fn (list alist))))
        (exit-token (car triple))
        (val (cadr triple))
        (new-alist (caddr triple)))
  (cond
   ((eq exit-token :return) val)
   ((eq exit-token :loop-finish)
    (let*
     ((triple (true-list-fix (apply$ finally-fn (list new-alist))))
      (exit-token (car triple))
      (val (cadr triple)))
     (if (eq exit-token :return) val nil)))
   ((l< (lex-fix (apply$ measure-fn (list new-alist)))
        (lex-fix (apply$ measure-fn (list alist))))
    (do$ measure-fn
         new-alist do-fn finally-fn default
         untrans-measure untrans-do-loop$))
   (t
    (prog2$
     (er
      hard? 'do$
      "The measure, ~x0, used in the do loop$ statement~%~Y12~%failed to ~
            decrease!  In particular, when the incoming alist (an alist of ~
            dotted pairs specifying the values of all the variables) ~
            was~%~Y32the alist produced by the do body was~%~Y42and the ~
            measure went from~%~x5~%to~%~x6.~%Logically, do$ returns ~x7 ~
            in this situation."
      untrans-measure
      untrans-do-loop$ nil alist new-alist
      (apply$ measure-fn (list alist))
      (apply$ measure-fn (list new-alist))
      default)
     default)))))