ACL2-pc::lisp
(meta)
evaluate the given form in Lisp
Example:
(lisp (assign xxx 3))
General Form:
(lisp form)
Evaluate form. The lisp command is mainly of interest for side
effects. Also see ACL2-pc::print, ACL2-pc::skip, and ACL2-pc::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.
