LD-KEYWORD-ALIASES

allows the abbreviation of some keyword commands 
Major Section:  MISCELLANEOUS


Example:
(set-ld-keyword-aliases '((:q 0 q-fn)
                          (:e 0 exit-acl2-macro))
                        state)
Ld-keyword-aliases is an ld special (see ld). The accessor is (ld-keyword-aliases state) and the updater is (set-ld-keyword-aliases val state). Ld-keyword-aliases 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 ld-keyword-aliases is nil.

In the example above, :q has been redefined to have the effect of executing (q-fn), so for example if you define 

(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 define 
(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 in your "acl2-customization.lisp" 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. 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. But this parse is overridden, as described above, for the keywords bound in ld-keyword-aliases.