LD-QUERY-CONTROL-ALIST

Major Section:  MISCELLANEOUS

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''.