Defalist
Introduce a recognizer for a typed association list (alist).
Defalist allows you to quickly introduce a recognizer for a typed
association list (e.g., string-nat-alistp) and proves basic theorems about
it.
Unlike many ACL2 alist recognizers, the recognizers introduced by defalist
do not, by default, imply (alistp x), but they do imply something
like (cons-listp x). That is,
- We require that each element is a cons, but
- We do not require the alists to be nil-terminated.
Not requiring nil termination has some advantages. It plays well with
ACL2::equivalence relations like list-equiv and alist-equiv. It also allows you to use features of ACL2::fast-alists such as "size hints" and "alist names" (see hons-acons for details).
But there is also a disadvantage. Namely, it may be difficult to operate on
a defalist using traditional alist functions, whose guards require alistp. Fortunately, there are generally good alternatives to these
traditional functions with no such requirement, e.g.,:
General form:
(defalist name formals
&key key ; required
val ; required
guard ; t by default
verify-guards ; t by default
keyp-of-nil ; :unknown by default
valp-of-nil ; :unknown by default
true-listp ; nil by default
mode ; current defun-mode by default
already-definedp ; nil by default
parents ; nil by default
short ; nil by default
long ; nil by default
)
For example,
(defalist string-nat-alistp (x)
:key (stringp x)
:val (natp x))
introduces a new function, string-nat-alistp, that recognizes alists
whose keys are strings and whose values are natural numbers. It also proves
many theorems about this new function.
Note that x is treated in a special way: it refers to the whole alist
in the formals and guards, but refers to individual keys or values in the
:key and :val positions. This is similar to how deflist,
defprojection, and defmapappend handle x.
Usage and Arguments
Let pkg be the package of name. All functions, theorems, and
variables are created in this package. One of the formals must be pkg::x,
and this argument represents the alist to check. Otherwise, the only
restriction on the formals is that you may not use the names pkg::a,
pkg::n, or pkg::y, because we use these variables in the theorems we
generate.
The :key and :val arguments are required and should be simple
function calls involving some subset of the formals. The basic idea is that
you write x for the particular key or value that is being inspected.
The optional :guard and :verify-guards are given to the
defund event that we introduce. In other words, these are the guards that
will be used for the list recognizer, not the element recognizer.
The optional :true-listp argument can be used to make the new
recognizer "strict" and only accept alists that are nil-terminated; by
default the recognizer will be "loose" and will not pay attention to the
final cdr. See strict-list-recognizers for further
discussion.
The optional :keyp-of-nil (similarly :valp-of-nil) keywords can be
used when (key-recognizer nil ...) (similarly (val-recognzier nil
...)) is always known to be t or nil. When it is provided,
defalist can generate slightly better theorems.
The optional :already-definedp keyword can be set if you have already
defined the function. This can be used to generate all of the ordinary
defalist theorems without generating a defund event, and is useful
when you are dealing with mutually recursive recognizers.
The optional :mode keyword can be set to :program to introduce the
recognizer in program mode. In this case, no theorems are introduced.
The optional :parents, :short, and :long keywords are as in
defxdoc. Typically you only need to specify :parents, perhaps
implicitly with ACL2::set-default-parents, and suitable documentation
will be automatically generated for :short and :long. If you don't
like this documentation, you can supply your own :short and/or :long
to override it.
