		Search-engine friendly clone of the ACL2 documentation.

Prog2$

Execute two forms and return the value of the second one

See hard-error, see illegal, and see cw for examples of functions to call in the first argument of prog2$. Also see progn$ for an extension of prog2$ that handles than two arguments.

Semantically, (Prog2$ x y) equals y; the value of x is ignored. However, x is first evaluated for side effect. Since the ACL2 programming language is applicative, there can be no logical impact of evaluating x. However, x may involve a call of a function such as hard-error or illegal, which can cause so-called ``hard errors'', or a call of cw to perform output.

Here is a simple, contrived example using hard-error. The intention is to check at run-time that the input is appropriate before calling function bar.

(defun foo-a (x)
  (declare (xargs :guard (consp x)))
  (prog2$
   (or (good-car-p (car x))
       (hard-error 'foo-a
                   "Bad value for x: ~x0"
                   (list (cons #\0 x))))
   (bar x)))

The following similar function uses illegal instead of hard-error. Since illegal has a guard of nil, guard verification would guarantee that the call of illegal below will never be made (at least when guard checking is on; see set-guard-checking).

(defun foo-b (x)
  (declare (xargs :guard (and (consp x) (good-car-p (car x)))))
  (prog2$
   (or (good-car-p (car x))
       (illegal 'foo-b
                "Bad value for x: ~x0"
                (list (cons #\0 x))))
   (bar x)))

We conclude with a simple example using cw from the ACL2 sources.

(defun print-terms (terms iff-flg wrld evisc-tuple)

; Print untranslations of the given terms with respect to iff-flg, following
; each with a newline.

; We use cw instead of the fmt functions because we want to be able to use this
; function in print-type-alist-segments (used in brkpt1), which does not return
; state.

  (if (endp terms)
      terms
    (prog2$
     (cw "~Y01"
         (untranslate (car terms) iff-flg wrld)
         evisc-tuple)
     (print-terms (cdr terms) iff-flg wrld evisc-tuple))))