Major Section: EVENTS
Example:
(set-state-ok t)
(defun-nx foo (x state)
(mv-let (a b c)
(cons x state)
(list a b c b a)))
; Note ``ill-formed'' call of foo just below.
(defun bar (state y)
(foo state y))
The macro defun-nx introduces definitions using the defun macro,
always in :logic mode, such that the calls of the resulting
function cannot be evaluated. Such a definition is admitted without
enforcing syntactic restrictions for executability, in particular for
single-threadedness (see stobj) and multiple-values passing (see mv and
see mv-let). After such a definition is admitted, the usual syntactic rules
for state and user-defined stobjs are relaxed for calls of the
function it defines. Also see non-exec for a way to designate subterms of
function bodies, or subterms of code to be executed at the top level, as
non-executable.
The syntax of defun-nx is identical to that of defun. A form
(defun-nx name (x1 ... xk) ... body)expands to the following form.
(defun name (x1 ... xk)
(declare (xargs :non-executable t :mode :logic))
...
(prog2$ (throw-nonexec-error 'name (list x1 ... xk))
body))
Note that because of the insertion of the above call of
throw-nonexec-error, no formal is ignored when using defun-nx.
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. If an error message is produced by evaluating a call of the function
on a list of arguments that includes state or user-defined stobjs,
these arguments will be shown as symbols such as |<state>| in the error
message. In the case of a user-defined stobj bound by
with-local-stobj or stobj-let, the symbol printed will include
the suffix {instance}, for example, |<st>{instance}|.
It is harmless to include :non-executable t in your own xargs
declare form; defun-nx will still lay down its own such
declaration, but ACL2 can tolerate the duplication.
Note that defund-nx is also available. It has an effect identical to
that of defun-nx except that as with defund, it leaves the function
disabled.
If you use guards (see guard), please be aware that even though syntactic
restrictions are relaxed for defun-nx, guard verification proceeds
exactly as for defun. If you want ACL2 to skip a form for purposes of
generating guard proof obligations, use the macro non-exec, which
generates a call of throw-nonexec-error that differs somewhat from the
one displayed above. See non-exec.
See defun for documentation of defun.
