ACL2-PC::LISP

(meta) evaluate the given form in Lisp
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(lisp (assign xxx 3))

General Form: (lisp form)

Evaluate form. The lisp command is mainly of interest for side effects. See also print, skip, and fail.

The rest of the documentation for lisp is of interest only to those who use it in macro commands. If the Lisp evaluation (by trans-eval) of form returns an ``error triple'' of the form (mv erp ((NIL NIL STATE) . (erp-1 val-1 &)) state), then the lisp command returns the appropriate error triple

(mv (or erp erp-1)
    val-1
    state) .
Otherwise, the trans-eval of form must return an ``error triple'' of the form (mv erp (cons stobjs-out val) &), and the lisp command returns the appropriate error triple
(mv erp
    val
    state).

Note that the output signature of the form has been lost. The user must know the signature in order to use the output of the lisp command. Trans-eval, which is undocumented except by comments in the ACL2 source code, has replaced, in val, any occurrence of the current state or the current values of stobjs by simple symbols such as REPLACED-STATE. The actual values of these objects may be recovered, in principle, from the state returned and the user-stobj-alist within that state. However, in practice, the stobjs cannot be recovered because the user is denied access to user-stobj-alist. The moral is: do not try to write macro commands that manipulate stobjs. Should the returned val contain REPLACED-STATE the value may simply be ignored and state used, since that is what REPLACED-STATE denotes.