Deftypes
Generate mutually recursive types with equivalence relations and
fixing functions.
Deftypes generates mutually-recursive types. We'll begin with
an example.
;; Associate fixing functions and equivalence relations
;; with component types. Note: this is done for most
;; basic types in the book centaur/fty/basetypes.lisp.
(deffixtype integer :pred integerp :fix ifix :equiv int-equiv :define t)
(deffixtype symbol :pred symbolp :fix symbol-fix :equiv sym-equiv :define t)
(deftypes intterm
(defflexsum intterm
(:num :cond (atom x)
:fields ((val :type integerp :acc-body x))
:ctor-body val)
(:call
:fields ((fn :type symbol :acc-body (car x))
(args :type inttermlist :acc-body (cdr x)))
:ctor-body (cons fn args)))
(deflist inttermlist
:elt-type intterm))
This generates recognizers and fixing functions for two new types:
- intterm, which is either a "num" consisting of a single integer or a
"call" consisting of a symbol consed onto an inttermlist,
- inttermlist, which is a list of intterms.
The deftypes form just bundles together two other forms -- a defflexsum and a deflist. These two forms would be admissible by
themselves, except that the types they are defining are mutually recursive, and
therefore so are their recognizer predicates and fixing functions.
The syntax and behavior of individual type generators is documented further
in their own topics. So far, the supported type generators are:
- deflist: a list of elements of a particular type
- defprod: a product (AKA record, aggregate, struct) type
- defalist: an alist mapping keys of some type to values of some type
- defset: an oset of elements of a particular type
- defomap: an omap mapping keys of some type to values of some type
- deftagsum: a sum-of-products (AKA tagged union) type
- defflexsum: a very flexible (and not as automated) sum-of-products
type used to implement defprod and deftagsum.
Deftypes and its component type generators are intended to
implement the type discipline described in the fty topic. In
particular, this means:
- the type predicates generated by any of these events each have an
associated fixing function and equivalence relation, and these associations
are recorded using a deffixtype event
- accessors and constructors of the sum and product types unconditionally
return values of the appropriate type
- accessors and constructors have equality congruences based on the types of
their arguments.
To support these nice properties, all the component types (the fields of
products, elements of lists, keys and values of alists) are required to also
have an associated fixing function and equivalence relation, either produced by
a deftypes compatible type generator or recorded by a deffixtype
event. (They may also be untyped.) The "preparation" forms in the example
above show how this can be done. Also see basetypes for some base types
with fixing functions.
Subtopics
- Deftagsum
- Define a (possibly recursive) tagged union, a.k.a. ``sum of
products'' type.
- Defprod
- Define a new product type, like a struct in C, following the
fty-discipline.
- Defflexsum
- Define a (possibly recursive) sum of products type.
- Deflist
- Define a list type with a fixing function, supported by deftypes.
- Defalist
- Define an alist type with a fixing function, supported by deftypes.
- Defoption
- Define an option type.
- Deftranssum
- Introduce a transparent sum of products. (beta)
- Defmap
- Define an alist type with a fixing function that drops pairs with malformed keys rather than fixing them.
