Ld-query-control-alist
How to default answers to queries
Ld-query-control-alist is an ld special (see ld). The accessor is (ld-query-control-alist state) and the updater is
(set-ld-query-control-alist val state). Roughly speaking,
ld-query-control-alist is either nil (meaning all queries should be
interactive), t (meaning all should default to the first accepted
response), or an alist that pairs query ids to keyword responses. The alist
may end in either t or nil, indicating the default value for all ids
not listed explicitly. Formally, the ld-query-control-alist must satisfy
ld-query-control-alistp. The initial ld-query-control-alist is
nil, which means all queries are handled interactively.
When an ACL2 query is raised, a unique identifying symbol is printed in
parentheses after the word ``Query''. This symbol, called the ``query id,''
can be used in conjunction with ld-query-control-alist to prevent the
query from being handled interactively. By ``handled interactively'' we mean
that the query is printed to *standard-co* and a response is read from
*standard-oi*. The alist can be used to obtain a ``default value''
for each query id. If this value is nil, then the query is handled
interactively. In all other cases, the system handles the query without
interaction (although text may be printed to standard-co to make it
appear that an interaction has occurred; see below). If the default value is
t, the system acts as though the user responded to the query by typing
the first response listed among the acceptable responses. If the default
value is neither nil nor t, then it must be a keyword and one of the
acceptable responses. In that case, the system acts as though the user
responded with the given keyword.
Next, we discuss how the ld-query-control-alist assigns a default
value to each query id. It assigns each id the first value paired with the id
in the alist, or, if no such pair appears in the alist, it assigns the final
cdr of the alist as the value. Thus, nil assigns all ids
nil. T assigns all ids t. '((:filter . nil) (:sysdef . :n)
. t) assigns nil to the :filter query, :n to the :sysdef
query, and t to all others.
It remains only to discuss how the system prints text when the default
value is not nil, i.e., when the query is handled without interaction.
In fact, it is allowed to pair a query id with a singleton list containing a
keyword, rather than a keyword, and this indicates that no printing is to be
done. Thus for the example above, :sysdef queries would be handled
noninteractively, with printing done to simulate the interaction. But if we
change the example so that :sysdef is paired with (:n), i.e., if
ld-query-control-alist is '((:filter . nil) (:sysdef :n) . t), then
no such printing would take place for sysdef queries. Instead, the
default value of :n would be assigned ``quietly''.
