Defsum
Define a recursive data type similar to a Haskell type definition.
Example:
(include-book "tools/defsum" :dir :system)
(set-ignore-ok :warn)
(defsum my-list
(my-empty)
(my-cons car (my-list-p cdr)))
This declaration says that an object is of the type my-list if it
is either of the type my-empty or my-cons, where my-empty
is an empty structure and my-cons is a structure with two fields:
the car, an arbitrary object; and the cdr which is of type
my-list. In this case, recognizers my-list-p, my-empty-p,
and my-cons-p are defined along with constructors my-empty and
my-cons and destructors my-cons-car and my-cons-cdr. The
necessary macros are also defined to enable pattern-matching using the
constructors (see pattern-match). For mutually-recursive data types
see defsums. It may also be informative to look at the translated
version of a defsum form using :trans1.
Note that a defsum form produces several logic-mode events inside an
encapsulate. Despite the author's best intentions, not every such
automatically-generated event will complete successfully. If you
encounter a defsum form that fails, please email it to
sswords@cs.utexas.edu (with or without fixing the bug yourself.)
Several theorems about the new type are defined so as to enable
reasoning based on their abstract model rather than their underlying
list representation. For most reasoning these theorems should be
sufficient without enabling the function definitions or
executable-counterparts. In case these do need to be enabled,
theories named (for the above example) my-list-functions and
my-list-executable-counterparts are defined.
In addition to the recognizer, constructor, and destructor functions,
a measure function is also defined which counts the number of nested
objects of the sum type. In the example above, the measure function
is my-list-measure and the measure of an object is 1 if it is not a
my-cons, and 1 plus the measure of its my-cons-cdr if it is.
Defsum accepts some keyword arguments. Be aware that not all
combinations of these arguments have been tested extensively. Again,
please send bug reports to sswords@cs.utexas.edu if you find a defsum
form that does not succeed.
:arithmetic - By default, each defsum event expands to an
encapsulate which locally includes the book arithmetic/top-with-meta.
If an incompatible arithmetic book has already been included, this may
cause the defsum to fail. But the other arithmetic book may also have
theorems that allow the defsum event to succeed if we don't attempt to
include the arithmetic book. This can be done by setting
:arithmetic nil.
:guard - may be set to t, nil, or :fast. By default
it is set to t, in which case minimal guards are set for all
functions. If set to nil, guards will not be verified for any
functions; this is useful in case some field type recognizers don't
have their guards verified. If set to :fast, an additional
recognizer for each product is defined named ``foo-p-fast'' if the
product is named foo. This has a guard such that its argument must be
a valid sum object. It is then logically equivalent to the other
recognizer, but in execution only checks that the symbol in the car of
the object matches the name of the product. The pattern matcher for
each product then uses the fast recognizers. Thus fast guards result
in a small (?) gain in performance in exchange for a (hopefully
trivial) degradation in logical complexity.
:short-accessors - t by default; may be set to nil. If
t, each field accessor first checks whether the object is of the
correct product type and returns nil if not. This allows for an
additional theorem saying that if x is not of the correct product
type, then the accessor returns nil. If nil, the nth accessor
returns (nth n x) regardless of x's type. When guards are turned
on, this is implemented with an mbe so there should be no
performance difference between the two options. When guards are off,
performance will be somewhat better if this feature is turned off.
:compact - By default, a defsum constructor makes a product
object by putting its components into a cons tree using n-1 conses,
but a prettier list representation is also supported which uses n
conses to store the elements in a flattened list which is easier to
read when printed. Set :compact nil if you prefer this
representation.
:hons - If HONS mode is in use, the flag :hons t causes all
defsum forms to be built with HONSes rather than regular conses. See
hons-and-memoization.
It may be necessary to include some function definition in a mutual
recursion with the sum recognizer function. In this case simply put
the defun form inside the defsum form, i.e.
(defsum lisp-term
(lisp-atom val)
(func-app (symbolp function) (lisp-term-listp args))
(defun lisp-term-listp (args)
(declare (xargs :guard t))
(if (atom args)
(null args)
(and (lisp-term-p (car args))
(lisp-term-listp (cdr args))))))
If such a function is included, however, no measure function will be
defined for the sum.
Usually it is not necessary to specify a measure for such a function;
because there is currently no way of directly specifying the measure
for the sum's recognizer, specifying an exotic measure on such a
function is likely to fail. If you come up against this limitation,
please send an example to sswords@cs.utexas.edu.
