evaluate a top-level form as a function body
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.