Major Section: OTHER
Some forms, such as calls of with-local-stobj, are illegal when
supplied directly to the ACL2 top-level loop. The macro top-level
provides a workaround in such cases, by defining a temporary
:program-mode function named top-level-fn whose only argument
is state and whose body is the form to be evaluated. When the call of
top-level returns there is no change to the existing ACL2 logical
world. The following edited log illustrates all of the above points.
ACL2 !>:pbt 0
0 (EXIT-BOOT-STRAP-MODE)
ACL2 !>(defstobj st fld)
Summary
Form: ( DEFSTOBJ ST ...)
Rules: NIL
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ST
ACL2 !>(top-level
(with-local-stobj
st
(mv-let (result st)
(let ((st (update-fld 17 st)))
(mv (fld st) st))
result)))
17
ACL2 !>(top-level
(with-local-stobj
st
(mv-let (result st)
(let ((st (update-fld 17 st)))
(mv (fld st) st))
(mv nil result state))))
17
ACL2 !>(top-level
(with-local-stobj
st
(mv-let (result st)
(let ((st (update-fld 17 st)))
(mv (fld st) st))
(mv result state))))
(17 <state>)
ACL2 !>:pbt 0
0 (EXIT-BOOT-STRAP-MODE)
d 1:x(DEFSTOBJ ST FLD)
ACL2 !>
Each argument of top-level after the first should be a declare form
or documentation string, as the list of these extra arguments will be
placed before the first argument when forming the definition of
top-level-fn.
Top-level generates a call of ld, so that the value returned is
printed in the normal way. The call of top-level itself actually
evaluates to (mv erp :invisible state), where erp is t if and
only evaluation of the call of top-level-fn caused an error, which
normally results in no additional output. (For details about ``caused an
error'', see the definition of top-level in the ACL2 source code, and
see ld-error-action.)
