Data-definitions

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

Subtopics

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