Mark code as non-executable

The following example, although rather contrived, illustrates the use of

(defun double (x) (case x (1 2) (2 4) (3 6) (otherwise (non-exec (* 2 x)))))

We can prove that

(verify-guards double) (thm (equal (double x) (* 2 x)))

We can evaluate double on the specified arguments. But a call of

ACL2 !>(double 3) 6 ACL2 !>(double 10) ACL2 Error in TOP-LEVEL: ACL2 has been instructed to cause an error because of an attempt to evaluate the following form (see :DOC non- exec): (* 2 X). To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>

During proofs, the error is silent; it is ``caught'' by the proof mechanism
and generally results in the introduction of a call of `hide` during a
proof.

Also see defun-nx for a utility that makes every call of a function
non-executable, rather than a specified form. The following examples contrast
`defun-nx`, in particular illustrating the role of
`non-exec` in avoiding guard proof obligations.

; Guard verification fails: (defun-nx f1 (x) (declare (xargs :guard t)) (car x)) ; Guard verification succeeds after changing the guard above: (defun-nx f1 (x) (declare (xargs :guard (consp x))) (car x)) ; Guard verification succeeds: (defun f2 (x) (declare (xargs :guard t)) (non-exec (car x))) ; Evaluating (g1) prints "Hello" before signaling an error. (defun g1 () (f1 (cw "Hello"))) ; Evaluating (g2) does not print before signaling an error. (defun g2 () (non-exec (cw "Hello"))) ; Evaluating (h1) gives a guard violation for taking reciprocal of 0. (defun h1 () (f1 (/ 1 0))) ; Evaluating (h2) does not take a reciprocal, hence there is no guard ; violation for that; we just get the error expected from using non-exec. (defun h2 () (non-exec (/ 0)))