• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
      • Term
      • Ld
      • Hints
      • Type-set
      • Ordinals
      • Clause
      • ACL2-customization
      • With-prover-step-limit
      • Set-prover-step-limit
      • With-prover-time-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Defsum
      • Gcl
      • Oracle-timelimit
      • Thm
      • Defopener
      • Case-split-limitations
      • Set-gc-strategy
      • Default-defun-mode
      • Top-level
      • Reader
      • Ttags-seen
      • Adviser
      • Ttree
      • Abort-soft
      • Defsums
      • Gc$
      • With-timeout
      • Coi-debug::fail
      • Expander
      • Gc-strategy
      • Coi-debug::assert
      • Sin-cos
      • Def::doc
      • Syntax
      • Subversive-inductions
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Miscellaneous

Top-level

Evaluate a top-level form as a function body

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.)

Since the defined function top-level takes only state as a parameter, the given form should not include any user-defined stobjs that occur free in the form.

Finally, note that since top-level runs a function that is defined in :program mode, it is possible for a raw lisp error to occur. Here is an example.

ACL2 !>(top-level (car 3))

***********************************************
************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
Error:  The value 3 is not of the expected type LIST.
While executing: CAR
***********************************************