define a non-executable function symbol
Major Section:  EVENTS


(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))
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, the symbol printed will include the suffix {local-stobj}, for example, |<st>{local-stobj}|.

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.