		Search-engine friendly clone of the ACL2 documentation.

Defdata

A Data Definition Framework

Introduction

The defdata framework enables the convenient specification of data types in ACL2s, the ACL2 Sedan. The framework concisely supports common data definition patterns, e.g., list types, map types, enumerated types, record types, and mutually-recursive types. It also provides support for polymorphic functions and tight integration with Tau.

The data definition framework is a key component of counterexample generation support in ACL2s, but can be independently used in ACL2, and is available as a community book.

The defdata framework maintains both a predicative characterization, via a predicate recognizing elements of the datatype, and an enumerative characterization, via a function that can be used to enumerate all the elements of the datatype. ACL2s picks out the recognizers in a conjecture and can use the datatype enumerators to generate random elements of the datatype. This is a key part of counterexample generation in ACL2s.

The defdata framework also allows us to increase the amount of automation ACL2s provides for reasoning about data definitions. For example, our framework generates useful theorems, with appropriate rule-classes, for list types; it generates accessor and constructor functions for records with a suitable theory for reasoning about compositions of these functions; it generates theorems that characterize the type relations such as inclusion and exclusion; and it generates events that support polymorphic type reasoning.

The defdata framework is described in our ACL2 2014 paper (a link to the paper appears later). Below, we provide some examples of its use.

Note: If you are trying these examples in a package other than ACL2S, then you might have to prefix the basic typenames i.e. acl2s::pos.

Examples

Union and Product types

(defdata inode nat)

(defdata file (cons inode string))
(defdata er-file (oneof file nil))

(defdata UPNest 
  (oneof (oneof (cons (oneof 11 7) pos-list) 'ok symbol-alist) 
         (cons symbol (complex integer -1))
         (oneof (oneof 42 (cons pos file) er-file) t 7/6)
         "nice"))

(defdata loi (oneof nil (cons integer loi)))

Range types

(defdata cache-miss-ratio (range rational (0 < _ < 1)))

(defdata big-unsigned-num (range integer ((expt 2 64) < _)))

Macros are allowed and the meaning of the defdata body is the given by its macroexpansion.

(defdata 3d-point (list rational rational rational))

Enum types

(defdata op-code (enum '(lw sw addi subi beqz jr)))

(defun generate-instruction-opcodes (x)
  (if (eq x 'mips-risc-model)
      '(lw sw addi subi beqz jr)
    '()))

(defdata op-code1 (enum (generate-instruction-opcodes 'mips-risc-model)))

List and Alist types

(defdata files (listof file))

(defdata symb-alist (alistof symbol all))

Mutually-recursive types

(defdata 
  (dir (listof (cons string dir-entry)))
  (dir-entry (oneof file dir)))

(defdata
  (sexpr (oneof symbol
                (cons symbol sexpr-list)))
  (sexpr-list (oneof nil
                     (cons sexpr sexpr-list))))

Record (Struct) types

(defdata reg-num (range integer (0 <= _ < 64)))
(defdata immediate-range (range integer (0 <= _ < (expt 2 16))))

(defdata inst (record (op  . op-code)
                      (rd  . reg-num)
                      (rs1 . reg-num)
                      (imm . immediate-range)))

Map (unique and sorted entries) types

(defdata p-addr (range integer (0 <= _ < (expt 2 64))))
(defdata imem (map p-addr inst))

Using record and map types

(b* (;; pick a random imemory
       (I (nth-imem 4511))
       ;; fix a program counter value
       (pc 1)
       ;; get the instruction pointed to by pc
       (instr (mget pc I)) 
       ;; get immediate value field of instr
       (im (inst-imm instr))
       ;; set immediate value field and the pc entry 
       (I1 (mset pc (set-inst-imm (1+ im) instr) I))
       ;; alternative way of getting immediate value field
       (im2 (mget :imm (mget pc I1)))
       ((inst op rd rs1 ?imm) instr)
       )
  (equal (inst op rd rs1 (1- im2)) instr))

Custom types

(defun make-descending-addresses (n)
  (if (zp n)
    nil
    (cons (1- n) (make-descending-addresses (- n 1)))))

(defun imem-custom-enum (n)
  (declare (xargs :mode :program))
  (let* ((m (nth-imem-builtin n))
         (vals (strip-cdrs m))
         (keys (make-descending-addresses (len m))))
    (pairlis$ keys vals)))

(defun imem-customp (x)
  (or (null x)
      (and (consp x)
           (consp (car x))
           (imem-customp (cdr x))
           (instp (cdar x))
           (p-addrp (caar x))
           (or (and (null (cdr x))
                    (equal 0 (caar x)))
               (> (caar x) (caadr x))))))

(register-type imem-custom
               :predicate imem-customp
               :enumerator imem-custom-enum)


(defdata-attach imem :test-enumerator imem-custom-enum)

Recursive record types (similar to ML datatype facility)

(defdata tree (oneof 'Leaf 
                     (node (val   . string)
                           (left  . tree)
                           (right . tree))))

Polymorphic Type Signatures

(sig binary-append ((listof :a) (listof :a)) => (listof :a))
(sig nthcdr (nat (listof :a)) => (listof :a))
(sig nth (nat (listof :a)) => :a 
     :satisfies (< x1 (len x2)))
;; xi corresponds to the ith type appearing in the sig form. For example,
;; x1 corresponds to nat and x2 to (listof :a)

Registering a data constructor

(defun acons-caar (x)  (caar x))
(defun acons-cdar (x)  (cdar x))
(defun acons-cdr (x)  (cdr x))

(defthm acons-acl2-count-lemma
  (equal (acl2-count (acons x1 x2 x3))
         (+ 2 (acl2-count x1) (acl2-count x2) (acl2-count x3))))

(register-data-constructor (aconsp acons)
                           ((allp acons-caar) (allp acons-cdar) (allp acons-cdr))
                           :rule-classes (:rewrite)
                           :verbose t)

Registering a type

(defun nth-even-builtin (n) 
  (declare (xargs :guard (natp n)))
  (* 2 (nth-integer n)))

(register-type even 
               :predicate evenp 
               :enumerator nth-even-builtin)

Registering user-defined combinators

(register-user-combinator alistof 
 :arity 2 :verbose t
 :aliases (acl2::alistof)
 :expansion (lambda (_name _args) `(OR nil (acons ,(car _args) ,(cadr _args) ,_name)))
 :syntax-restriction-fn proper-symbol-listp
 :polymorphic-type-form (alistof :a :b)
 :post-pred-hook-fns (user-alistof-theory-events))

Debugging

To debug a failed defdata form, you can proceed in multiple ways:

At the session editor (or emacs prompt), submit/evaluate :trans1 (defdata ...) And from the output, evaluate the form that says (defdata-events ...).
Use keyword options :verbose t and examine the ACL2 output.

More details

Although most constructs of the defdata language are package-agnostic, some of the API functions/macros of the Defdata framework (like sig) reside in the ACL2S package. Use list (*acl2s-exports*) to import these symbols into your own package.

For a comprehensive user guide and more details please refer to the following paper

Subtopics

Match: Pattern matching supporting predicates, including recognizers automatically generated by defdata, disjunctive patterns and patterns containing arbitrary code. Can be thought of as ACL2s version of case-match.
Sig: Specify type signatures for polymorphic functions
Register-data-constructor: Register a data constructor (to extend the defdata language)
Register-type: Register a name as a defdata type
Defdata-attach: Attach/modify metadata for a defdata type
Register-user-combinator: Register a user-defined combinator (to add sugar to defdata language)