Defprojection
Project a transformation across a list.
Defprojection allows you to quickly introduce a function like
map f. That is, given an element-transforming function, f, it can
define a new function that applies f to every element in a list. It also
sets up a basic theory with rules about len, append, etc., and
generates basic, automatic xdoc documentation.
General form:
(defprojection name extended-formals
element
[keyword options]
[/// other events]
)
Options Defaults
:nil-preservingp nil
:guard t
:verify-guards t
:result-type nil
:returns nil
:mode current defun-mode
:already-definedp nil
:parallelize nil
:verbosep nil
:share-suffix nil
:parents nil
:short nil
:long nil
Basic Examples
(defprojection my-strip-cars (x)
(car x)
:guard (alistp x))
defines a new function, my-strip-cars, that is like the built-in ACL2
function strip-cars.
Note: x is treated in a special
way. It refers to the whole list in the formals and guards, but refers to
individual elements of the list in the element portion. This is similar
to how other macros like deflist, defalist, and defmapappend handle x.
A define-like syntax is also available:
(defprojection my-square-list ((x integer-listp))
:result (squared-x integer-listp)
(* x x))
Usage and Optional 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::n, pkg::y, and pkg::acc, because we use these variables in
the theorems we generate.
The optional :nil-preservingp argument can be set to t when the
element transformation satisfies (element nil ...) = nil. This allows
defprojection to produce slightly better theorems.
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 :result-type keyword defaults to nil, and in this
case no additional "type theorem" will be inferred. But, if you instead give
the name of a unary predicate like nat-listp, then a defthm will be
generated that looks like (implies (force guard) (nat-listp (name ...)))
while name is still enabled. This is not a very general mechanism, but it
is often good enough to save a lot of typing.
The optional :returns keyword is similar to that of define, and
is a more general mechanism than :result-type.
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
defprojection theorems without generating a defund event, and is
useful when you are dealing with mutually recursive transformations.
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 :parallelize keyword can be set to t if you want to
try to speed up the execution of new function using parallelism. This is
experimental and only works with ACL2(p). Note: we don't do anything smart to
split the work up into large chunks, and you lose tail-recursion when you use
this.
The optional :share-suffix keyword can be set to t if you want to
try to reuse a suffix of the original list in cases where the transformation
sometimes does nothing (returns the identical element), in order to reduce
memory footprint. This only works if the optimized nrev implementation is
used, which carries a trust tag -- to use this, do (include-book
"centaur/nrev/fast" :dir :system).
The optional :verbosep flag can be set to t if you want
defprojection to print everything it's doing. This may be useful if you run
into any failures, or if you are simply curious about what is being
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.
Support for Other Events
Defprojection implements the same /// syntax as other macros like define. This allows you to put related events near the definition and have
them included in the automatic documentation. As with define, the new
projection function is enabled during the /// section. Here is an
example:
(defprojection square-each (x)
(square x)
:guard (integer-listp x)
///
(defthm pos-listp-of-square-each
(pos-listp (square-each x))))
It is valid to use an /// section with a :result-type theorem. We
arbitrarily say the :result-type theorem comes first.
Deprecated. The optional :rest keyword was a precursor to ///.
It is still implemented, but its use is now discouraged. If both :rest
and /// events are used, we arbitrarily put the :rest events
first.
The optional :optimize keyword was historically used to optionally
optimize the projection using nreverse. We now use ACL2::nrev
instead, and since this doesn't require a ttag, the :optimize flag
now does nothing.
