TOP-LEVEL

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.