Defflexsum
Define a (possibly recursive) sum of products type.
Caveat
Defflexsum is not very user-friendly or automatic; it is easy to create
instances that fail in incomprehensible ways. It is used as a backend to
define the deftagsum and defprod type generators, which are easier to
use.
Example
This is essentially the same as the example in deftagsum. Logically,
the way these types work are very similar; only the representation is
different.
(defflexsum arithterm
(:num :cond (atom x)
:fields ((val :type integerp :acc-body x))
:ctor-body val)
(:plus
:cond (eq (car x) '+)
:shape (and (true-listp x) (eql (len x) 3))
:fields ((left :type arithterm :acc-body (cadr x))
(right :type arithterm :acc-body (caddr x)))
:ctor-body (list '+ left right))
(:minus
:shape (and (eq (car x) '-)
(true-listp x)
(eql (len x) 2))
:fields ((arg :type arithterm :acc-body (cadr x)))
:ctor-body (list '- arg)))
(define arithterm-eval ((x arithterm-p))
:returns (xval integerp :rule-classes :type-prescription)
:measure (arithterm-count x)
(case (arithterm-kind x)
(:num (arithterm-num->val x))
(:plus (+ (arithterm-eval (arithterm-plus->left x))
(arithterm-eval (arithterm-plus->right x))))
(t (- (arithterm-eval (arithterm-minus->arg x)))))
///
(deffixequiv arithterm-eval))
(define arithterm-double ((x arithterm-p))
:verify-guards nil ;; requires return type theorem first
:returns (xx arithterm-p)
:measure (arithterm-count x)
(arithterm-case x
:num (arithterm-num (* 2 x.val))
:plus (arithterm-plus (arithterm-double x.left)
(arithterm-double x.right))
:minus (arithterm-minus (arithterm-double x.arg)))
///
(verify-guards arithterm-double)
(deffixequiv arithterm-double)
(local (include-book "arithmetic/top-with-meta" :dir :system))
(defthm arithterm-double-correct
(equal (arithterm-eval (arithterm-double x))
(* 2 (arithterm-eval x)))
:hints(("Goal" :in-theory (enable arithterm-eval)))))
Note: when the constructors are actually defined, mbe is used to allow
the function to logically apply fixing functions to its arguments without a
performance penalty when running with guards checked.
More on the above Caveat
defflexsum is less automatic than most other type-defining utilities.
It requires certain information to be provided by the user that must then be
proved to be self-consistent. For example, the :ctor-body argument in a
product spec determines how that product is constructed, and the :acc-body
argument to a product field spec determines how that field is accessed. These
could easily be inconsistent, or the :ctor-body could produce an object
that is not recognized as that product. If either of these is the case, some
proof within the defflexsum event will fail and it will be up to the user
to figure out what that proof was and why it failed.
Syntax and Options
Defflexsum top-level arguments
Defflexsum takes the following keyword arguments, in addition to a list
of products, which are described further below.
- :pred, :fix, :equiv, :kind, :case, and :count
override the default names for the various generated functions (and case
macro). If any of these is not provided, a default name is used instead. If
:kind nil is provided, then no -kind function is generated and
instead the products are distinguished by their bare :cond fields. If
:count nil is provided, then no count function is defined for this
type.
- :xvar sets the variable name used to represent the SUM object. By
default, we look for a symbol whose name is "X" that occurs in the product
declarations.
- :measure provides the measure for the predicate, fixing function, and
count function. It defaults to (acl2-count x), which is usually
appropriate for stand-alone products, but sometimes a special measure must be
used, especially when defflexsum is used inside a mutually-recursive
deftypes form.
- :prepwork is a list of events to be submitted at the beginning of the
process; usually these are local lemmas needed for the various proofs.
- :parents, :short, and :long provide xdoc for the type
- :inline: sets default for inlining of products and determines whether
the kind and fixing functions are inlined. This may be :all or a subset
of (:kind :fix :acc :xtor), defaulting to (:kind :fix :acc).
Products
Each product starts with a keyword naming its kind; this is the symbol that
the SUM kind function returns on an object of that product type. The rest of
the form is a list of keyword arguments:
- :cond describes how to tell whether an object is of this product type.
To determine the kind of a SUM object, the SUM kind function checks each of
the product conditions in turn, returning the name of the first matching
condition. So the condition for a given product assumes the negations of the
conditions of the previous listed products. The :cond field defaults to
t, so typically it can be left off the last product type.
- :shape adds well-formedness requirements for a product. One purpose
these may serve is to make well-formed objects canonical: it must be a theorem
that the fixing function applied to a well-formed object is the same object.
So if a product is (e.g.) a tuple represented as a list, and the constructor
creates it as a true-list, then there should be a requirement that the object
be a true-list of the appropriate length; otherwise, an object that had a
non-nil final cdr would be recognized as well-formed, but fix to a different
value.
- :fields list the fields of the product; these are described further
below.
- :ctor-body describes how to make a product object from the fields.
This must be consistent with the field accessor bodies (described below) and
with the :cond and :shape fields of this product and the previous
ones (i.e., it can't produce something that could be mistaken for one of the
previous products listed). The actual constructor function will have fixing
functions added; these should not be present in the :ctor-body
argument.
- :type-name overrides the type-name, which by default is
[SUMNAME]-[KIND], e.g. arithterm-plus from the example above. This
is used as a base for generating the field accessor names.
- :ctor-name overrides the name of the product constructor function,
which by default is the type-name.
- :inline, determining whether the constructor and accessors are inlined
or not. This may be :all or a subset of (:xtor :acc). Defaults to
(:acc) if not overridden.
- :require adds a dependent type requirement; see the section on this
feature in defprod.
Product Fields
Each product field is a name followed by a keyword list, in which the
following keywords are allowed:
- :acc-body must be present: a term showing how to fetch the field from
the object.
- :acc-name overrides the accessor name
- :type, the type (fixtype name or predicate) of the field; may be empty
for an untyped field
- :default, the default value of the field in the constructor macro
- :doc will eventually generate xdoc, but is currently ignored
- :rule-classes, the rule classes for the return type of the accessor
function. This is :rewrite by default; you may wish to change it to
:type-prescription when the type is something basic like
integerp.
