Definition of
The function takes seven arguments but only the first five are relevant to its logical value.
Function:
(defun do$ (measure-fn alist do-fn finally-fn values 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 values untrans-measure untrans-do-loop$)) (t (prog2$ (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. 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) (eviscerate-do$-alist new-alist) (apply$ measure-fn (list alist)) (apply$ measure-fn (list new-alist)) values) (loop$-default-values values new-alist))))))