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 support this type within our framework, all one needs to do is to define its enumerator, which is a bijection from the set of natural numbers to the set of positive multiples of 3:
(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 ___.