A Data Definition Framework
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.
(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)))
(defdata cache-miss-ratio (range rational (0 < _ < 1))) (defdata big-unsigned-num (range integer ((expt 2 32) < _)))
Macros are allowed and the meaning of the defdata body is the given by its macroexpansion.
(defdata 3d-point (list rational rational rational))
(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)))
(defdata files (listof file)) (defdata symb-alist (alistof symbol all))
(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))))
(defdata reg-num (range integer (0 <= _ < 32))) (defdata immediate-range (range integer (0 <= _ < (expt 2 16)))) (defdata inst (record (op . op-code) (rd . reg-num) (rs1 . reg-num) (imm . immediate-range)))
(defdata p-addr (range integer (0 <= _ < (expt 2 32)))) (defdata imem (map p-addr inst))
(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))
(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)
(defdata tree (oneof 'Leaf (node (val . string) (left . tree) (right . tree))))
(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)
(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)
(defun nth-even-builtin (n) (declare (xargs :guard (natp n))) (* 2 (nth-integer n))) (register-type even :predicate evenp :enumerator nth-even-builtin)
(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))
To debug a failed defdata form, you can proceed in multiple ways:
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