A Data Definition Framework for ACL2

The Data Definition Framework supports ground ACL2
*types* and any custom *types* introduced by
a user. It also helps the user conveniently construct
enumerated, union, record and list *types*.
The framework is integrated with our random testing
framework. It also provides ways to specify subtype
and disjoint relations among the supported *types*.

The ACL2 value universe is broadly divided into 5 kinds of data
objects. They are Numbers, Characters, Strings, Symbols and Conses
(Ordered Pairs). These disjoint sets serve as types for our purposes;
we shall call them ground data types. Although ACL2 is an *untyped*
logic, it uses type information internally to deduce types.
ACL2 users provide the prover with type information by specifying
type hypotheses on variables in a conjecture.
Note again that ACL2 is syntactically *untyped*, but that
doesn't prevent us from having and using a notion of a type.
One **cannot create** new *types* in ACL2, in the sense
that one cannot create a new non-empty set of values that
provably extends the ACL2 value universe. Rather, one
typically partitions the existing universe in potentially
new ways to form 'new' sets. These sets (``types'') are
presently characterized by just a type predicate.

The task of specifying user-defined data definitions (``types'') and supporting
random testing is elegantly solved by characterizing 'type' using both a
type predicate and a type enumerator.

What is a *type* in our data definition framwork?
We say that foo is a 'type' if there exists a predicate
function foop and either a constant list of values
*foo-values* (if it's finite) or an enumerator function
nth-foo (if it's infinite) that maps natural numbers to data
objects that satisfy foop. If *foo* is **supported**
by our framework, i.e. the forementioned conditions are met, then
the name *foo* can be used in defining other types using
defdata.

The framework supports all the ground data types and the common
data types present in the initial(ground) ACL2 world.
The framework also treats each data object in the ACL2 universe as a
singleton 'type', i.e. a set with just one element, the data object
itself. The type which represents all of the ACL2 universe is
called all; every 'type' is thus a subset of all.

Sophisticated users may want to define custom
types manually, for example to define a type which represents
positive multiples of 3. In ACL2 we can define such a type by the
following predicate:

(defun pos-multiple-of-threep (v) (if (posp v) (equal 0 (mod v 3)) nil))In order to

(defun nth-pos-multiple-of-three (n) (if (natp n) (* 3 (1+ n)) 3))The framework provides a macro defdata to specify combinations of supported 'types', thus relieving the user of the trouble of defining predicates and enumerators by hand. 'Types' allow users to refer to them by name in these data definitions. One can also use register-data-constructor to introduce custom notions of product data. defdata-subtype and defdata-disjoint are used to specify relations among supported 'types'. We illustrate some uses of the framework:

(register-data-constructor (consp cons) ((allp car) (allp cdr)) :proper t) (register-custom-type nat (t nth-nat . natp)) (defdata loi (oneof 'nil (cons integer loi))) (defdata-subtype nat rational) (defdata-disjoint symbol string)For more details on data-definitions framework refer ___.

- Defdata
- Specify a data definition ('type')
- Defdata-disjoint
- Specify a disjoint relation between two types
- Defdata-subtype
- Specify a subtype relation between two types
- Defdata-testing
- Specify a custom testing enumerator for a type
- Defdata::get-ACL2s-defdata-use-guards
- Get the setting for use of guards in functions generated by defdata
- Defdata::set-ACL2s-defdata-use-guards
- Use(and verify) guards in functions generated by defdata
- Disjoint-p
- Query wether two types are disjoint
- Get-ACL2s-defdata-verbose
- Get the current verbosity for output printed by defdata
- Register-data-constructor
- Register a data constructor to be used in data definitions(FOR ADVANCED USERS)
- Set-ACL2s-defdata-verbose
- Control amount of output printed by defdata
- Subtype-p
- Query wether two types are disjoint