Deftagsum
Define a (possibly recursive) tagged union, a.k.a. ``sum of
products'' type.
Deftagsum produces a tagged union type consisting of several
product types, each with a tag to distinguish them. It is similar in spirit to
ML or Haskell's recursive data types, although without the dependent-type
features.
Deftagsum is compatible with deftypes, and can be
mutually-recursive with other deftypes compatible type generators. As
with all deftypes-compatible type generators, the types of the fields of
its products must each either be one produced by a compatible type generator or
else have an associated fixing function given by deffixtype. (Fields
can also be untyped.) See basetypes for some base types with fixing
functions.
Example
Note: It may be helpful to be familiar with defprod.
(deftagsum arithtm
(:num ((val integerp)))
(:plus ((left arithtm-p)
(right arithtm-p)))
(:minus ((arg arithtm-p))))
This defines the following functions and macros:
- Recognizer arithtm-p
- Fixing function arithtm-fix
- Equivalence relation arithtm-equiv
- arithtm-kind, which returns either :num, :plus, or
:minus to distinguish the different kinds of arithtm objects
- Constructors arithtm-num, arithtm-plus, arithtm-minus
- Accessors arithtm-num->val, arithtm-plus->left,
arithtm-plus->right, and arithtm-minus->arg
- Constructor macros make-aritherm-num, make-arithtm-plus,
make-arithtm-minus, similarly to defprod
- Changer macros change-arithtm-num, change-arithtm-plus,
change-arithtm-minus, similarly to defprod
- b* binders arithtm-num, arithtm-plus,
arithtm-minus
- arithtm-case, a macro that combines case splitting and accessor binding.
Note: The individual products in a deftagsum type are not themselves
types: they have no recognizer or fixing function of their own. The guard for
accessors is the sum type and the kind, e.g., for arithtm-plus->right,
(and (arithtm-p x) (equal (arithtm-kind x) :plus))
Using Tagsum Objects
The following example shows how to use an arithtm object. We define an
evaluator function that computes the value of an arithtm and a transformation
that doubles every leaf in an arithtm, and prove that the doubling function
doubles the value according to the evaluator. The doubling function also shows
how the arithtm-case macro is used. Note that the return type theorems and
the theorem about the evaluation of arithtm-double are all hypothesis-free --
a benefit of following a consistent type-fixing convention.
(define arithtm-eval ((x arithtm-p))
:returns (val integerp :rule-classes :type-prescription)
:measure (arithtm-count x)
:verify-guards nil
(case (arithtm-kind x)
(:num (arithtm-num->val x))
(:plus (+ (arithtm-eval (arithtm-plus->left x))
(arithtm-eval (arithtm-plus->right x))))
(:minus (- (arithtm-eval (arithtm-minus->arg x)))))
///
(verify-guards arithtm-eval))
(define arithtm-double ((x arithtm-p))
:returns (xx arithtm-p)
:measure (arithtm-count x)
:verify-guards nil
(arithtm-case x
:num (arithtm-num (* 2 x.val))
:plus (arithtm-plus (arithtm-double x.left)
(arithtm-double x.right))
:minus (arithtm-minus (arithtm-double x.arg)))
///
(verify-guards arithtm-double)
(local (include-book "arithmetic/top-with-meta" :dir :system))
(defthm arithtm-eval-of-double
(equal (arithtm-eval (arithtm-double x))
(* 2 (arithtm-eval x)))
:hints(("Goal" :in-theory (enable arithtm-eval)))))
Deftagsum Usage and Options
A deftagsum form consists of the type name, a list of product
specifiers, and some optional keyword arguments.
Product specifiers
A product specifier consists of a tag (a keyword symbol), a list of fields
given as std::extended-formals, and some optional keyword arguments.
The possible keyword arguments are:
- :layout, one of :tree, :list, or :alist, determining
the arrangement of fields within the product object (as in defprod),
- :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.
- :hons, NIL by default, determining whether objects are constructed
with hons.
- :base-name, overrides the name of the constructor and the base name
used to generate accessors.
- :require adds a dependent type requirement; see the section on this
feature in defprod.
Tagsum Options
The following keyword options are recognized at the top level of a
deftagsum form (as opposed to inside the individual product forms):
- :pred, :fix, :equiv, :kind, :count: override
default function names. :count may also be set to NIL, to turn of
generation of the count function.
- :parents, :short, :long: add xdoc about the type.
- :measure: override the measures used to admit the recognizer, fixing
function, and count function; the default is (acl2-count x).
- :prepwork: events submitted before
- :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).
- :layout: sets default layout for products
- :base-case-override: Override which product is the base case. This
may affect termination of the fixing function; see below.
Dealing with Base Cases
Consider the following type definition:
(deftypes fntree
(deftagsum fntree
(:pair ((left fntree-p) (right fntree-p)))
(:call ((fn symbol) (args fntreelist-p))))
(deflist fntreelist-p :elt-type fntree))
As is, deftypes will fail to admit this event, saying:
We couldn't find a base case for tagsum FNTREE, so we don't know what its
fixing function should return when the input is an atom. To override this, add
keyword arg :base-case-override [product], where [product] is one of your
product keywords, and provide a measure that will allow the fixing function to
terminate.
What is the problem? As the text suggests, the problem lies in what we
should do when given an atom as input to the fixing function. With the default
measure of (acl2-count x), we're not allowed to recur on, say, NIL,
because its acl2-count is already 0. This is fine as long as we can pick a
product type that has no recursive components, but in this case, the :pair
and :call product both do. However, the :call product could have an
empty list as its arguments, and this seems like a reasonable thing to use as
the fix of an atom. To give deftagsum the hint to do this, we need to
tell it which product to fix an atom to, and what measure to use. The
following modification of the above form works:
(deftypes fntree
(deftagsum fntree
(:pair ((left fntree-p) (right fntree-p)))
(:call ((fn symbol) (arg fntreelist-p)))
:base-case-override :call
:measure (two-nats-measure (acl2-count x) 1))
(deflist fntreelist-p :elt-type fntree
:measure (two-nats-measure (acl2-count x) 0)))
