Defmapappend
Append transformations of list elements.
Defmapappend allows you to quickly introduce a function like
(loop for elem in x append (f elem))
and produces some basic theorems about this new function.
General form:
(defmapappend name formals
transform
&key guard ; t by default
verify-guards ; t by default
transform-exec ; nil by default
transform-true-list-p ; nil by default
mode ; default defun-mode by default
parents ; nil by default
short ; nil by default
long ; nil by default
rest ; nil by default
already-definedp ; nil by default
)
For instance,
(defmapappend append-square-lists (x)
(square-lists x)
:guard (integer-list-listp x))
would introduce a new function, append-square-lists, that applies
square-lists to every element of its argument and appends together all of
the results.
Note that x is treated in a special way: it refers to the whole list
in the formals and guards, but refers to the individual elements of the list in
the element portion. This is similar to how other macros like deflist, defalist, and defprojection 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 list that will be transformed. Otherwise, the
only restriction on formals is that you may not use the names pkg::a,
pkg::y, and pkg::acc, because we use these variables in the theorems
we generate.
The transform should indicate an element transforming function that
produces a list of some kind as its output. Adopting an ML-like syntax,
transform should have a signature such as the following:
transform : elem -> A list
We produce a new function of the given name, which has the
signature:
name : elem list -> A list
Our new function applies transform to every element in its input list,
and appends together all of the results. That is, the logical definition of
the new function we introduce is as follows:
(defun name (x)
(if (atom x)
nil
(append (transform (car x))
(name (cdr x)))))
The new function will be more efficient than the above. In particular, we
write a mappappend-exec function that builds the answer in reverse using
revappend and reverses it at the end. An even more efficient version is
possible when the :transform-exec option is provided; see below for
details.
The optional :guard and :verify-guards are given to the
defund event that we introduce. Often deflist is convenient for
introducing the necessary guard.
The optional :mode keyword can be set to :logic or :program
to introduce the recognizer in logic or program mode. The default is whatever
the current default defun-mode is for ACL2, i.e., if you are already in program
mode, it will default to program mode, etc.
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
defmapappend theorems without generating a defund event, and is
useful when you are dealing with mutually recursive transformations.
The optional :transform-true-list-p argument can be set to t
whenever the transformation is known to unconditionally produce a true list,
and allows us to slightly optimize our function.
The :transform-exec argument
When provided, the optional :transform-exec argument should be the name
of a function that satisfies the following property:
(equal (transform-exec x acc)
(revappend (transform x)))
Note that such functions are automatically introduced by defprojection. For instance,
(defprojection square-list (x)
(square x))
generates a suitable function named square-list-exec. Amusingly,
suitable functions are also generated by defmapappend, itself.
When such a function is provided, we can use it to generate a more efficient
implementation, which uses the tail-recursive function to build the answer in
reverse, and then reverses it at the very end, avoiding even the intermediate
computation of the lists emitted by transform.
The optional :parents, :short, and :long options are as in
xdoc, and are analogous to those of deflist or defprojection.
The optional :rest option is as in deflist, and allows you to
add theorems into the same section.
