Major Section: PROGRAMMING
See hard-error and see illegal for examples of functions
to call in the first argument of prog2$.
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.''
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: ~p0"
(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: ~p0"
(list (cons #\0 x))))
(bar x)))
