Description of classifications for commands in ACL2s
Each input form submitted to ACL2 from the plugin is placed into one of the following categories based on its purpose and potential effect. Basically, if you use RAW or ACTION input, we cannot guarantee that the plugin will behave in a consistent way with respect to UNDOing, etc., but the rest should behave as expected. We present them in decreasing order of commonness or importance to the user:
|EVENT||These correspond to ACL2 embedded event forms, which are those forms that can appear in ACL2 books. Calls to defun, defmacro, and defthm are examples of embedded event forms and EVENTs.|
Such forms are simple computations which return a value when (and if)
No VALUE form can alter ACL2's state and, therefore, never
affects undoing or redoing.
A precise definition is that if ACL2 permits (cons <form> nil), then <form> is a VALUE.
Advanced Note: some VALUE forms have transient side effects, but they have no logical consequence (e.g. CW and WORMHOLE).
These are calls to some built-in ACL2 functions that report information about
the current state but are known not to modify state. Examples include
(internal initiation only)
|Various UI actions which have to do with "undoing" or "moving the line up" can initiate the execution of an UNDO in the session. An ordinary user need not concern him/herself with how this works (See How undo and redo are implemented in the ACL2s implementation notes), but should keep in mind that UNDOing an ACTION or RAW form may not have the desired effect.|
(internal initiation only)
This is the counterpart of UNDO. It is used when resubmitting
something with the same abstract syntax and in the same environment as
something that was previously undone.
REDO enables one to (for example) edit comments above the line, by retreating the line far enough to edit what one wants to change, and then moving the "todo" line back to where it was. If only comments were changed, the session will accept the forms as REDOs, which happen almost instantaneously.
If the input is a parseable ACL2 object but is an ill-formed expression
according to the current history, we call it "BAD" input. Examples of
violations that would cause input to be statically ill-formed are:
|COMMAND||There are many forms that are illegal in books but we are able to undo the effect of. If we recognize a form as such, we call it a COMMAND-- except for special case IN-PACKAGE. The best example of a command is ":set-guard-checking :none".|
|ACTION||This is the "catch-all" categorization for forms that may have effects that we don't know how to properly undo or might even break or hang the ACL2 session. Users who use STOBJs or other STATE beyond the logical WORLD will need to use ACTIONs heavily, but these are advanced uses of ACL2.|
|EVENT/VALUE||These are a special type of embedded event form (value-triples) that have no logical consequence--except that they could halt progress by generating a hard lisp error.|
|RAW||Most users of ACL2 are familiar with breaking into "raw lisp" by typing ":q" at the top-level prompt. This is not supported in our plugin, but "raw mode" is supported. Most forms submitted under this mode are classified as RAW because they have no well-defined meaning from the ACL2 view of things. With raw mode, the user can easily break many things, and it's only supported for the benefit of experts.|