		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 six 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 that 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
values — the output signature of the value to be returned if the measure fails to decrease.

Function: do$

(defun do$ (measure-fn alist do-fn finally-fn values dolia)
 (declare (xargs :guard (and (apply$-guard measure-fn '(nil))
                             (apply$-guard do-fn '(nil))
                             (apply$-guard finally-fn '(nil))
                             (weak-dolia-p dolia))))
 (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 values dolia))
   (t
    (prog2$
     (let
       ((all-stobj-names
             (true-list-fix (access dolia dolia :all-stobj-names)))
        (untrans-measure (access dolia dolia :untrans-measure))
        (untrans-do-loop$ (access dolia dolia :untrans-do-loop$)))
      (er
       hard? 'do$
       "The measure, ~x0, used in the do loop$ ~
                statement~%~Y12~%failed to decrease!  Recall that do$ tracks ~
                the values of do loop$ variables in an alist.  The measure is ~
                computed using the values in the alist from before and after ~
                execution of the body.  We cannot print the values of double ~
                floats and live stobjs, if any are found in the alist, ~
                because they are raw Lisp objects, not ACL2 objects.  We ~
                print any double float as its corresponding rational and ~
                simply print the name of any live stobj (as a ~
                string).~%~%Before execution of the do body the alist ~
                was~%~Y32.~|After the execution of the do body the alist ~
                was~%~Y42.~|Before the execution of the body the measure ~
                was~%~x5.~|After the execution of the body the measure ~
                was~%~x6.~|~%Logically, in this situation the do$ returns the ~
                value of a term whose output signature is ~x7, where the ~
                value of any component of type :df is #d0.0 and the value of ~
                any stobj component is the last latched value of that stobj."
       untrans-measure untrans-do-loop$ nil
       (eviscerate-do$-alist alist all-stobj-names)
       (eviscerate-do$-alist new-alist all-stobj-names)
       (apply$ measure-fn (list alist))
       (apply$ measure-fn (list new-alist))
       values))
     (loop$-default-values values new-alist))))))

The last argument is only relevant in the error message printed if the do$ fails to terminate and that message is not part of the returned value.