@

get the value of a global variable in state


Parent topic:  OTHER
Home

Examples:
(+ (@ y) 1)
(assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))

General Form:
(@ symbol)

where symbol is any symbol to which you have assigned a global value. This macro expands into (f-get-global 'symbol state), which retrieves the stored value of the symbol.

The macro assign makes it convenient to set the value of a symbol. The :ubt operation has no effect on the global-table of state. Thus, you may use these globals to hang onto useful data structures even though you may undo back past where you computed and saved them.

ACL2-DEFAULTS-TABLE

a table specifying certain defaults, e.g., the default defun-mode


Parent topic:  OTHER
Home

Example Forms:
(table acl2-defaults-table :defun-mode) ; current default defun-mode
(table acl2-defaults-table :defun-mode :program)
           ; set default defun-mode to :program

See table for a discussion of tables in general. The legal keys for this table are shown below. They may be accessed and changed via the general mechanisms provided by tables. However, there are often more convenient ways to access and/or change the defaults. (See also the note below.)

:defun-mode

the default defun-mode, which must be :program or :logic. See defun-mode for a general discussion of defun-modes. The :defun-mode key may be conveniently set by keyword commands naming the new defun-mode, :program and :logic. See program and see logic.

:verify-guards-eagerness

an integer between 0 and 2 indicating how eager the system is to verify the guards of a defun event. See set-verify-guards-eagerness.

:compile-fns

When this key's value is t, functions are compiled when they are defun'd; otherwise, the value is nil. To set the flag, see set-compile-fns.

:measure-function

the default measure function used by defun when no :measure is supplied in xargs. The default measure function must be a function symbol of one argument. Let mfn be the default measure function and suppose no :measure is supplied with some recursive function definition. Then defun finds the first formal, var, that is tested along every branch and changed in each recursive call. The system then ``guesses'' that (mfn var) is the :measure for that defun.

:well-founded-relation

the default well-founded relation used by defun when no :well-founded-relation is supplied in xargs. The default well-founded relation must be a function symbol, rel, of two arguments about which a :well-founded-relation rule has been proved. See well-founded-relation.

:invisible-fns-alist

an alist used in the control of permutative rewriting. Each entry in this alist must be of the form (fn ufn1 ufn2 ... ufnk), where fn and each ufni is a function symbol and the ufni are all unary functions. Such an entry makes each of the ufni ``invisible'' when ordering the arguments of fn via commutative rules. See set-invisible-fns-alist.

:irrelevant-formals-ok

When this key's value is t, the check for irrelevant formals is bypassed; otherwise, the value is the keyword nil (the default). See irrelevant-formals and see set-irrelevant-formals-ok.

:ignore-ok

When this key's value is t, the check for ignored variables is bypassed; otherwise, the value is the keyword nil (the default). See set-ignore-ok.

:inhibit-warnings

ACL2 prints warnings that may, from time to time, seem excessive to experienced users. Each warning is ``labeled'' with a string identifying the type of warning. Consider for example

ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE ....

Here, the label is "Use". The value of the key :inhibit-warnings is a list of such labels, where case is ignored. Any warning whose label is a member of this list (where again, case is ignored) is suppressed. See set-inhibit-warnings and also see set-inhibit-output-lst.

:bdd-constructors

This key's value is a list of function symbols used to define the notion of ``BDD normal form.'' See bdd-algorithm and see hints.

Note: Unlike all other tables, acl2-defaults-table can affect the soundness of the system. The table mechanism therefore enforces on it a restriction not imposed on other tables: when table is used to update the acl2-defaults-table, the key and value must be variable-free forms. Thus, while

(table acl2-defaults-table :defun-mode :program),

(table acl2-defaults-table :defun-mode ':program), and


(table acl2-defaults-table :defun-mode (compute-mode *my-data*))

are all examples of legal events (assuming compute-mode is a function of one non-state argument that produces a defun-mode as its single value),

(table acl2-defaults-table :defun-mode (compute-mode (w state)))

is not legal because the value form is state-sensitive.

Consider for example the following three events which one might make into the text of a book.

(in-package "ACL2")

(table acl2-defaults-table
  :defun-mode
  (if (ld-skip-proofsp state) :logic :program))


(defun crash-and-burn (x) (car x))

The second event is illegal because its value form is state-sensitive. If it were not illegal, then it would set the :defun-mode to :program when the book was being certified but would set the defun-mode to :logic when the book was being loaded by include-book. That is because during certification, ld-skip-proofsp is nil (proof obligations are generated and proved), but during book inclusion ld-skip-proofsp is non-nil (those obligations are assumed to have been satisfied.) Thus, the above book, when loaded, would create a function in :logic mode that does not actually meet the conditions for such status.

For similar reasons, table events affecting acl2-defaults-table are illegal within the scope of local forms. That is, the text

(in-package "ACL2")

(local (table acl2-defaults-table :defun-mode :program))


(defun crash-and-burn (x) (car x))

is illegal because acl2-defaults-table is changed locally. If this text were acceptable as a book, then when the book was certified, crash-and-burn would be processed in :program mode, but when the certified book was included later, crash-and-burn would have :logic mode because the local event would be skipped.

The text

(in-package "ACL2")

(program) ;which is (table acl2-defaults-table :defun-mode :program)


(defun crash-and-burn (x) (car x))

is acceptable and defines crash-and-burn in :program mode, both during certification and subsequent inclusion.

We conclude with an important observation about the relation between acl2-defaults-table and include-book, certify-book, and encapsulate. Including or certifying a book never has an effect on the acl2-defaults-table, nor does executing an encapsulate event; we always restore the value of this table as a final act. (Also see include-book, see encapsulate, and see certify-book.) That is, no matter how a book fiddles with the acl2-defaults-table, its value immediately after including that book is the same as immediately before including that book. If you want to set the acl2-defaults-table in a way that persists, you need to do so using commands that are not inside books. It may be useful to set your favorite defaults in your acl2-customization file; see acl2-customization.

ASSIGN

assign to a global variable in state


Parent topic:  OTHER
Home

Examples:
(assign x (expt 2 10))
(assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))

General Form:
(assign symbol term)

where symbol is any symbol (with certain enforced exclusions to avoid overwriting ACL2 system ``globals'') and term is any ACL2 term that could be evaluated at the top-level. Assign evaluates the term, stores the result as the value of the given symbol in the global-table of state, and returns the result. (Note: the actual implementation of the storage of this value is much more efficient than this discussion of the logic might suggest.) Assign is a macro that effectively expands to the more complicated but understandable:

(pprogn (f-put-global 'symbol term state)
        (mv nil (f-get-global 'symbol term state) state)).

The macro @ gives convenient access to the value of such globals. The :ubt operation has no effect on the global-table of state. Thus, you may use these globals to hang onto useful data structures even though you may undo back past where you computed and saved them.

CERTIFY-BOOK!

a variant of certify-book


Parent topic:  OTHER
Home

Examples:
(certify-book! "my-arith" 3)     ;Certify in a world with 3
                                   ; commands, starting in a world
                                   ; with at least 3 commands.
(certify-book! "my-arith")       ;Certify in the initial world.
(certify-book! "my-arith" 0 nil) ;As above, but do not compile.

General Form:
(certify-book! book-name k compile-flg)

where book-name is a book name (see book-name), k is a nonnegative integer used to indicate the ``certification world,'' and compile-flg indicates whether you wish to compile the (functions in the) book.

This command is identical to certify-book, except that the second argument k may not be t in certify-book! and if k exceeds the current command number, then an appropriate ubt! will be executed first. See certify-book and see ubt!.

COMP

compile some ACL2 functions


Parent topic:  OTHER
Home

Examples:
:comp t          ; compile all uncompiled ACL2 functions
:comp foo        ; compile the defined function foo
:comp (foo bar)  ; compile the defined functions foo and bar

General Form:
:comp specifier
where specifier is one of the following:


  t                     compile all defined ACL2 functions that are currently
                          uncompiled
  (name-1 ... name-k)   a non-empty list of names of functions defined by
                          DEFUN in ACL2
  name                  same as (name)

Note: Unless a single function is specified (either as a symbol or as a one-element list containing its name), ACL2 will write out files "TMP.lisp" and "TMP1.lisp" (the latter is for the executable counterparts; see executable-counterpart) that are subsequently compiled. Also see set-compile-fns for a way to get each function to be compiled as you go along.

GOOD-BYE

quit entirely out of Lisp


Parent topic:  OTHER
Home

Example:
ACL2 !>:good-bye

Note: Your entire session will disappear forever when you type :good-bye.

The command :good-bye quits not only out of the ACL2 command loop, but in fact quits entirely out of the underlying Lisp. Thus, there is no going back! You will not be able to re-enter the command loop after typing :good-bye! All your work will be lost!!!

This command may not work in some underlying Common Lisp implementations. But we don't expect there to be any harm in trying. It does work in AKCL and GCL, at least as of this writing.

If you merely want to exit the ACL2 command loop, use :q instead (see q).

LD

the ACL2 read-eval-print loop, file loader, and command processor


Parent topic:  OTHER
Home

Example:
(LD standard-oi              ; open obj in channel, stringp file name
                             ; to open and close, or list of forms

                             ; Optional keyword arguments:
    :standard-co        ...  ; open char out or file to open and close
    :proofs-co          ...  ; open char out or file to open and close
    :current-package    ...  ; known package name
    :ld-skip-proofsp    ...  ; nil, 'include-book, t, or 
                             ;   see ld-skip-proofsp
    :ld-redefinition-action  ; nil or '(:a . :b)
    :ld-prompt          ...  ; nil, t, or some prompt printer fn
    :ld-keyword-aliases ...  ; an alist pairing keywords to parse info
    :ld-pre-eval-filter ...  ; :all, :query, or some new name
    :ld-pre-eval-print  ...  ; nil, t, or :never
    :ld-post-eval-print ...  ; nil, t, or :command-conventions
    :ld-evisc-tuple     ...  ; nil or '(alist nil nil level length)
    :ld-error-triples   ...  ; nil or t
    :ld-error-action    ...  ; :return (default), :continue or :error
    :ld-query-control-alist  ; alist supplying default responses
    :ld-verbose         ...) ; nil or t

Ld is the top-level ACL2 read-eval-print loop. (When you call lp, a little initialization is done in raw Common Lisp and then ld is called.) ld is also a general-purpose ACL2 file loader and a command interpreter. Ld is actually a macro that expands to a function call involving state. Ld returns an ``error/value/state'' triple as explained below.

The arguments to ld all happen to be global variables in state. For example, 'current-package and 'ld-verbose are global variables, which may be accessed via (@ current-package) and (@ ld-verbose). When ld is called, it ``binds'' these variables. By ``binds'' we actually mean the variables are globally set but restored to their old values on exit. Because ld provides the illusion of state global variables being bound, they are called ``ld specials'' (after the Lisp convention of calling a variable ``special'' if it is referenced freely after having been bound).

Note that all arguments but the first are passed via keyword. Any variable not explicitly given a value in a call retains its pre-call value, with the exception of :ld-error-action, which defaults to :return if not explicitly specified.

Just as an example to drive the point home: If current-package is "ACL2" and you typed

(ld *standard-oi* :current-package "MY-PKG")

you would find yourself in (an inner) read-eval-print loop in which the current-package was "MY-PKG". You could operate there as long as you wished, changing the current package at will. But when you typed :q you would return to the outer read-eval-print loop where the current package would still be "ACL2".

Roughly speaking, ld repeatedly reads a form from standard-oi, evaluates it, and prints its result to standard-co. It does this until the form evaluates to an error triple whose value component is :q or until the input channel or list is emptied. However, ld has many bells and whistles controlled by the ld specials. Each such special is documented individually. For example, see the documentation for standard-oi, current-package, ld-pre-eval-print, etc.

A more precise description of ld is as follows. In the description below we use the ld specials as variables, e.g., we say ``a form is read from standard-oi.'' By this usage we refer to the current value of the named state global variable, e.g., we mean ``a form is read from the current value of 'standard-oi.'' This technicality has an important implication: If while interacting with ld you change the value of one of the ld specials, e.g., 'standard-oi, you will change the behavior of ld, e.g., subsequent input will be taken from the new value.

Three ld specials are treated as channels: standard-oi is treated as an object input channel and is the source of forms evaluated by ld; standard-co and proofs-co are treated as character output channels and various flavors of output are printed to them. However, the supplied values of these specials need not actually be channels; several special cases are recognized. If the supplied value of one of these is in fact an open channel of the appropriate type, that channel is used and is not closed by ld. If the supplied value of one of these specials is a string, the string is treated as a file name and a channel of the appropriate type is opened to/from that file. (Note that ld does not support structured pathnames, as described in the documentation for pathname.) Any channel opened by ld during the binding of the ld specials is automatically closed by ld upon termination. If standard-co and proofs-co are equal strings, only one channel to that file is opened and is used for both.

Several other alternatives are allowed for standard-oi. If standard-oi is a true list then it is taken as the list of forms to be processed. If standard-oi is a list ending in an open channel, then ld processes the forms in the list and then reads and processes the forms from the channel. Analogously, if standard-oi is a list ending a string, an object channel from the named file is opened and ld processes the forms in the list followed by the forms in the file. That channel is closed upon termination of ld.

The remaining ld specials are handled more simply and generally have to be bound to one of a finite number of tokens described in the :doc entries for each ld special. Should any ld special be supplied an inappropriate value, an error message is printed.

Next, if ld-verbose is t, ld prints the message ``ACL2 loading name'' where name names the file or channel from which forms are being read. At the conclusion of ld, it will print ``Finished loading name'' if ld-verbose is t.

Finally, ld repeatedly executes the ACL2 read-eval-print step, which may be described as follows. A prompt is printed to standard-co if ld-prompt is non-nil. The format of the prompt is determined by ld-prompt. If it is t, the default ACL2 prompt is used. If it is any other non-nil value then it is treated as an ACL2 function that will print the desired prompt. See ld-prompt. In the exceptional case where ld's input is coming from the terminal (*standard-oi*) but its output is going to a different sink (i.e., standard-co is not *standard-co*), we also print the prompt to the terminal.

Ld then reads a form from standard-oi. If the object read is a keyword, ld constructs a ``keyword command form'' by possibly reading several more objects. See keyword-commands. This construction process is sensitive to the value of ld-keyword-aliases. See ld-keyword-aliases. Otherwise, the object read is treated as the command form.

Ld next decides whether to evaluate or skip this form, depending on ld-pre-eval-filter. Initially, the filter must be either :all, :query, or a new name. If it is :all, it means all forms are evaluated. If it is :query, it means each form that is read is displayed and the user is queried. Otherwise, the filter is a name and each form that is read is evaluated as long as the name remains new, but if the name is ever introduced then no more forms are read and ld terminates. See ld-pre-eval-filter.

If the form is to be evaluated, first prints the form to standard-co, if ld-pre-eval-print is t. With this feature, ld can process an input file or form list and construct a script of the session that appears as though each form was typed in. See ld-pre-eval-print.

Ld then evaluates the form, with state bound to the current state. The result is some list of multiple values. If a state is among the values, then ld uses that state as the subsequent current state.

Depending on ld-error-triples, ld may interpret the result as an ``error.'' See ld-error-triples. We first discuss ld's behavior if no error signal is detected (either because none was sent or because ld is ignoring them as per ld-error-triples).

In the case of a non-erroneous result, ld does two things: First, if the logical world in the now current state is different than the world before execution of the form, ld adds to the world a ``command landmark'' containing the form evaluated. See command-descriptor. Second, ld prints the result to standard-co, according to ld-post-eval-print. If ld-post-eval-print is nil, no result is printed. If it is t, all of the results are printed as a list of multiple values. Otherwise, it is :command-conventions and only the non-erroneous ``value'' component of the result is printed. See ld-post-eval-print.

Whenever ld prints anything (whether the input form, a query, or some results) it ``eviscerates'' it if ld-evisc-tuple is non-nil. Essentially, evisceration is a generalization of Common Lisp's use of *print-level* and *print-length* to hide large substructures. See ld-evisc-tuple.

We now return to the case of a form whose evaluation signals an error. In this case, ld first restores the ACL2 logical world to what it was just before the erroneous form was evaluated. Thus, a form that partially changes the world (i.e., begins to store properties) and then signals an error, has no effect on the world. You may see this happen on commands that execute several events (e.g., an encapsulate or a progn of several defuns): even though the output makes it appear that the initial events were executed, if an error is signalled by a later event the entire block of events is discarded.

After rolling back, ld takes an action determined by ld-error-action. If the action is :continue, ld merely iterates the read-eval-print step. Note that nothing suggestive of the value of the ``erroneous'' form is printed. If the action is :return, ld terminates normally. If the action is :error, ld terminates signalling an error to its caller. If its caller is in fact another instance of ld and that instance is watching out for error signals, the entire world created by the erroneous inner ld will be discarded by the outer ld.

Ld returns an error triple, (mv erp val state). Erp is t or nil indicating whether an error is being signalled. If no error is signalled, val is the ``reason'' ld terminated and is one of :exit (meaning :q was read), :eof (meaning the input source was exhausted), :error (meaning an error occurred but has been supressed) or :filter (meaning the ld-pre-eval-filter terminated ld).

PROPS

print the ACL2 properties on a symbol


Parent topic:  OTHER
Home

Example:
:props assoc-eq

Props takes one argument, a symbol, and prints all of the properties that are on that symbol in the ACL2 world.

Q

quit ACL2 (type :q) -- reenter with (lp)


Parent topic:  OTHER
Home

Example:
ACL2 !>:Q

The keyword command :q typed at the top-level of the ACL2 loop will terminate the loop and return control to the Common Lisp top-level (or, more precisely, to whatever program invoked lp). To reenter the ACL2 loop, execute (acl2::lp) in Common Lisp. You will be in the same state as you were when you exited with :q, unless during your stay in Common Lisp you messed the data structures representating the ACL2 state.

Unlike all other keyword commands, typing :q is not equivalent to invoking the function q. There is no function q.

REBUILD

a convenient way to reconstruct your old state


Parent topic:  OTHER
Home

Examples:
ACL2 !>(rebuild "project.lisp")
ACL2 !>(rebuild "project.lisp" t)
ACL2 !>(rebuild "project.lisp" :all)
ACL2 !>(rebuild "project.lisp" :query)
ACL2 !>(rebuild "project.lisp" 'lemma-22)

Rebuild allows you to assume all the commands in a given file or list, supplied in the first argument. Because rebuild processes an arbitrary sequence of commands with ld-skip-proofsp t, it is unsound! However, if each of these commands is in fact admissible, then processing them with rebuild will construct the same logical state that you would be in if you typed each command and waited through the proofs again. Thus, rebuild is a way to reconstruct a state previously obtained by proving your way through the commands.

The second, optional argument to rebuild is a ``filter'' (see ld-pre-eval-filter) that lets you specify which commands to process. You may specify t, :all, :query, or a new logical name. t and :all both mean that you expect the entire file or list to be processed. :query means that you will be asked about each command in turn. A new name means that all commands will be processed as long as the name is new, i.e., rebuild will stop processing commands immediately after executing a command that introduces name. Rebuild will also stop if any command causes an error. You may therefore wish to plant an erroneous form in the file, e.g., (mv t nil state), (see ld-error-triples), to cause rebuild to stop there. The form (i-am-here) is such a pre-defined form. If you do not specify a filter, rebuild will query you for one.

Inspection of the definition of rebuild, e.g., via :pc rebuild-fn, will reveal that it is just a glorified call to the function ld. See ld if you find yourself wishing that rebuild had additional functionality.

RESET-LD-SPECIALS

restores initial settings of the ld specials


Parent topic:  OTHER
Home

Examples:
(reset-ld-specials t)
(reset-ld-specials nil)

Roughly speaking, the ld specials are certain state global variables, such as current-package, ld-prompt, and ld-pre-eval-filter, which are managed by ld as though they were local variables. These variables determine the channels on which ld reads and prints and control many options of ld. See ld for the details on what the ld specials are.

This function, reset-ld-specials, takes one Boolean argument, flg. The function resets all of the ld specials to their initial, top-level values, except for the three channel variables, standard-oi, standard-co, and proofs-co, which are reset to their initial values only if flg is non-nil. Of course, if you are in a recursive call of ld, then when you exit that call, the ld specials will be restored to the values they had at the time ld was called recursively. To see what the initial values are, inspect the value of the constant *initial-ld-special-bindings*.

SET-GUARD-CHECKING

control checking guards during execution of top-level forms


Parent topic:  OTHER
Home

The top-level ACL2 loop has a variable which controls which sense of execution is provided. To turn ``guard checking on,'' by which we mean that guards are checked at runtime, execute the top-level form :set-guard-checking t. To turn it off, do :set-guard-checking nil. The status of this variable is reflected in the prompt.

ACL2 !>

means guard checking is on and

ACL2 >

means guard checking is off. The exclamation mark can be thought of as ``barring'' certain computations. The absence of the mark suggests the absence of error messages or unbarred access to the logical axioms. Thus, for example

ACL2 !>(car 'abc)

will signal an error, while

ACL2 >(car 'abc)

will return nil.

Whether guards are checked during evaluation is independent of the default-defun-mode. We note this simply because it is easy to confuse ``:program mode'' with ``evaluation in Common Lisp'' and thus with ``guard checking on;'' and it is easy to confuse ``:logic mode'' with ``evaluation in the logic'' and with ``guard checking off.'' But the default-defun-mode determines whether newly submitted definitions introduce programs or add logical axioms. That mode is independent of whether evaluation checks guards or not. You can operate in :logic mode with runtime guard checking on or off. Analogously, you can operate in :program mode with runtime guard checking on or off.

However, one caveat is appropriate: functions introduced only as programs have no logical definitions and hence when they are evaluated their Common Lisp definitions must be used and thus their guards (if any) checked. That is, if you are defining functions in :program mode and evaluating expressions containing only such functions, guard checking may as well be on because guards are checked regardless. This same caveat applies to a few ACL2 system functions that take state as an argument. This list of functions includes all the keys of the alist *super-defun-wart-alist* and all function whose names are members of the list *initial-untouchables*.

See guard for a general discussion of guards.