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.
