Type-alist
An ACL2 representation of contextual knowledge
The ACL2 prover maintains many structures that need not be
understood by the user. One of these, the type-alist structure, is
usually in this category. But some utilities refer to the type-alist, so we
summarize it here.
A type-alist is an association list, each element of which is of the form
(u ts . ttree), where u is a term (in internal,
``translated'' form), ts is a type-set, and ttree is a
tag-tree (see ttree). Such an element means that the term u has
the type-set ts, which is a number. While you are welcome to see the
documentation of type-set for details, this is not necessary,
since user-level utilities generally display a type-alist without displaying
numeric type-sets. Instead, they often use a symbol of the form
*TS-typ* to denote the type described by typ, and for
complements they use (TS-COMPLEMENT *TS-typ*). For example, a
context in which the terms (p x y), (no-duplicatesp-equal y),
and (natp x) are assumed to be true (i.e., non-nil) may be
displayed using the following lines.
-----
Terms with type *TS-T*:
(NO-DUPLICATESP-EQUAL Y)
-----
Terms with type (TS-COMPLEMENT *TS-NIL*):
(P X Y)
-----
Terms with type *TS-NON-NEGATIVE-INTEGER*:
X
-----
These lines says that (no-duplicatesp-equal y) is the symbol t,
(p x y) is not the symbol nil, and x is a non-negative
integer (i.e., a natp).
ACL2 computes a type-alist based on contextual information including the
hypotheses of the current goal (technically: the negations of the literals in
the goal that are not currently being rewritten), forward-chaining
from those literals, and the surrounding tests in calls of if. The
type-alist is of course not all that is known, since an entire logical world of facts is also known; and additional known information may be
recorded in the current database of linear rules.
