Define a (possibly recursive) tagged union, a.k.a. ``sum of products'' type.

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 , andarithtm-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

(and (arithtm-p x) (equal (arithtm-kind x) :plus))

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)))))

A

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.

The following keyword options are recognized at the top level of a

: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.

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

(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)))