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.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.
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 ld-keyword-aliases.
