Register-data-constructor
Register a data constructor (to extend the defdata language)
Introduction
You must be familiar with compound data types specified by defdata
using cons. Although cons has a unique status in ACL2, it
is not natively available in the defdata language unlike
built-in combinators such as oneof and range. In fact,
advanced users can introduce custom notions of product data by
using the register-data-constructor macro, whose usage we show below.
Example
Consider the symbol-alist type defined as (oneof nil (cons (cons symbol
all) symbol-alist)). We could have registered acons as a data
constructor, and alternatively defined symbol-alist using acons
instead of cons.
(defun aconsp (x)
(and (consp x) (consp (car x))))
(defun acons-caar (x) (caar x))
(defun acons-cdar (x) (cdar x))
(defun acons-cdr (x) (cdr x))
(register-data-constructor (aconsp acons)
((allp acons-caar) (allp acons-cdar) (allp acons-cdr)))
(defdata symbol-alist (oneof nil (acons symbol all symbol-alist)))
In fact, this is how we setup the base environment in
"defdata/base.lisp": we use register-data-constructor to
preregister all the primitive data constructors in ACL2. In
particular, the following (primitive) constructors are available to
build product types: cons, intern$, / and complex.
General Form:
(register-data-constructor (recognizer constructor)
((destructor-pred1 destructor1) ...)
[:proper bool]
[:hints hints]
[:rule-classes rule-classes])
