Major Section: PROGRAMMING
See hard-error and see illegal for examples of functions
to call in the first argument of
(Prog2$ x y) equals
y; the value of
x is ignored.
x is first evaluated for side effect. Since the ACL2
programming language is applicative, there can be no logical impact
x may involve a call of a function such
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
(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
illegalhas a guard of
guardverification would guarantee that the call of
illegalbelow 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)))