		Search-engine friendly clone of the ACL2 documentation.

Ld-keyword-aliases

Abbreviation of some keyword commands

Examples:
(set-ld-keyword-aliases '((:q 0 q-fn)
                          (:e 0 exit-acl2-macro))
                        state)
(ld-keyword-aliases state) ; current value of the ld-keyword-aliases table

Ld-keyword-aliases is the name of a ACL2 table (see table) and also the name of a function of state that returns the value of this table. That value must be an alist, each element of which is of the form (:keyword n fn), where :keyword is a keyword, n is a nonnegative integer, and fn is a function symbol of arity n, a macro symbol, or a lambda expression of arity n. When keyword is typed as an ld command, n more forms are read, x1, ..., xn, and the form (fn 'x1 ... 'xn) is then evaluated. The initial value of the ld-keyword-aliases table is nil.

ACL2 provides functions to modify the ld-keyword-aliases table, as follows.

(Set-ld-keyword-aliases val state): sets the table to val, which must be a legal alist as described above. This is an event that may go into a book (see events), but its effect will be local to that book.

Set-ld-keyword-aliases! is the same as set-ld-keyword-aliases, except that its effect is not local. Indeed, the form (set-ld-keyword-aliases val state) is equivalent to the form (local (set-ld-keyword-aliases! val state).

(Add-ld-keyword-alias key val state): modifies the table by binding the keyword key to val, which must be a legal value as described above. This is an event that may go into a book (see events), but its effect will be local to that book.

Add-ld-keyword-alias! is the same as add-ld-keyword-alias, except that its effect is not local. Indeed, the form (add-ld-keyword-alias key val state) is equivalent to the form (local (add-ld-keyword-alias! key val state).

Consider the first example above:

(set-ld-keyword-aliases '((:q 0 q-fn)
                          (:e 0 exit-acl2-macro))
                        state)

With this event, :q is redefined to have the effect of executing (q-fn), so for example if you have defined q-fn with

(defmacro q-fn ()
  '(er soft 'q "You un-bound :q and now we have a soft error."))

then :q will cause an error, and if you have defined

(defmacro exit-acl2-macro () '(exit-ld state))

then :e will cause the effect (it so happens) that :q normally has. If you prefer :e to :q for exiting the ACL2 loop, you might even want to put such definitions of q-fn and exit-acl2-macro together with the set-ld-keyword-aliases form above into your "acl2-customization.lsp" file; see ACL2-customization.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. Note that the ACL2 top-level loop (see lp) results from an invocation of ld.

However, there are various flags that control ld's behavior and ld-keyword-aliases is one of them. Ld-keyword-aliases affects how keyword commands are parsed. Generally speaking, ld's command interpreter reads ``:fn x1 ... xn'' as ``(fn 'x1 ... 'xn)'' when :fn is a keyword and fn is the name of an n-ary function; see keyword-commands. But this parse is overridden, as described above, for the keywords bound in the ld-keyword-aliases table.