Defun-nx
Define a non-executable function symbol
Example:
(defun-nx foo (x state)
(declare (xargs :guard t))
(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)
(declare (xargs :stobjs state))
(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)
generates the following definition.
(defun name (x1 ... xk)
(declare (xargs :non-executable t :mode :logic))
...
(prog2$ (throw-nonexec-error 'name (list x1 ... xk))
body))
But defun-nx does two other things. Before executing the defun
form displayed above, ACL2 arranges that state is allowed as a formal
parameter, by first introducing (set-state-ok t) in a way that is local to the generated event. After executing the defun, the executable-counterpart rune for name is disabled. You can
evaluate :trans1 (defun-nx ...) for your defun-nx form to see its
single-step macroexpansion.
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 is essentially identical
to defun-nx except that as with defund, defund-nx leaves the
definition rune disabled for the new function symbol.
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.
