Macro to define the models of Java primitive arrays.
The models vary slightly across the eight Java primitive array types, but they have a lot of common structure, which is captured via this macro. We define this macro and then we call it eight times.
This macro introduces, for each Java primitive (array) type:
Macro:
(defmacro atj-def-java-primitive-array-model (type) (declare (xargs :guard (member-eq type '(boolean char byte short int long float double)))) (b* ((type-name (symbol-name type)) (type-doc (str::cat "@('" (str::downcase-string type-name) "')")) (jwit (pkg-witness "JAVA")) (type-value (packn-pos (list type '-value) jwit)) (type-valuep (packn-pos (list type '-valuep) jwit)) (type-value-fix (packn-pos (list type '-value-fix) jwit)) (type-value->get (case type (boolean 'boolean-value->bool) (char 'char-value->nat) (byte 'byte-value->int) (short 'short-value->int) (int 'int-value->int) (long 'long-value->int) (t nil))) (type-value-list (packn-pos (list type '-value-list) jwit)) (type-value-listp (packn-pos (list type '-value-listp) jwit)) (type-array (packn-pos (list type '-array) jwit)) (type-arrayp (packn-pos (list type-array 'p) jwit)) (type-array-fix (packn-pos (list type-array '-fix) jwit)) (type-array->components (packn-pos (list type-array '->components) jwit)) (type-array-index-in-range-p (packn-pos (list type '-array-index-in-range-p) jwit)) (type-array-read (packn-pos (list type '-array-read) jwit)) (type-array-length (packn-pos (list type '-array-length) jwit)) (type-array-write (packn-pos (list type '-array-write) jwit)) (type-array-new-len (packn-pos (list type '-array-new-len) jwit)) (type-array-new-init (packn-pos (list type '-array-new-init) jwit)) (acl2type (case type (boolean 'boolean) (char 'ubyte16) (byte 'sbyte8) (short 'sbyte16) (int 'sbyte32) (long 'sbyte64) (t nil))) (acl2type-listp (case type (boolean 'boolean-listp) (char 'ubyte16-listp) (byte 'sbyte8-listp) (short 'sbyte16-listp) (int 'sbyte32-listp) (long 'sbyte64-listp) (t nil))) (acl2type-doc (case type (boolean "booleans") (char "unsigned 16-bit integers") (byte "signed 8-bit integers") (short "signed 16-bit integers") (int "signed 32-bit integers") (long "signed 64-bit integers") (t ""))) (type-array-to-list (packn-pos (list type-array '-to- acl2type '-list) jwit)) (type-array-to-list-aux (packn-pos (list type-array-to-list '-aux) jwit)) (type-array-from-list (packn-pos (list type-array '-from- acl2type '-list) jwit)) (type-array-from-list-aux (packn-pos (list type-array-from-list '-aux) jwit))) (cons 'progn (cons (cons 'fty::defprod (cons type-array (cons ':short (cons (str::cat "Fixtype of (our model of) Java " type-doc " arrays.") (cons (cons (cons 'components (cons type-value-list '(:reqfix (if (< (len components) (expt 2 31)) components nil)))) 'nil) (cons ':require (cons '(< (len components) (expt 2 31)) (cons ':layout (cons ':list (cons ':tag (cons (intern (symbol-name type-array) "KEYWORD") (cons ':pred (cons type-arrayp (cons '/// (cons (cons 'defrule (cons (packn-pos (list 'len-of- type-array->components '-upper-bound) jwit) (cons (cons '< (cons (cons 'len (cons (cons type-array->components '(array)) 'nil)) '((expt 2 31)))) (cons ':rule-classes (cons ':linear (cons ':enable (cons type-array->components 'nil))))))) 'nil))))))))))))))) (cons (cons 'define (cons type-array-index-in-range-p (cons (cons (cons 'array (cons type-arrayp 'nil)) '((index int-valuep))) (cons ':returns (cons '(yes/no booleanp) (cons ':short (cons (str::cat "Check if a Java @('int') is a valid index (i.e. in range) for a " type-doc " array.") (cons (cons 'integer-range-p (cons '0 (cons (cons 'len (cons (cons type-array->components '(array)) 'nil)) '((int-value->int index))))) 'nil)))))))) (cons (cons 'define (cons type-array-read (cons (cons (cons 'array (cons type-arrayp 'nil)) '((index int-valuep))) (cons ':guard (cons (cons type-array-index-in-range-p '(array index)) (cons ':returns (cons (cons 'component (cons type-valuep 'nil)) (cons ':short (cons (str::cat "Read a component from a Java " type-doc " array.") (cons (cons type-value-fix (cons (cons 'nth (cons '(int-value->int index) (cons (cons type-array->components '(array)) 'nil))) 'nil)) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons type-array-index-in-range-p 'nil)) 'nil))) 'nil) (cons ':prepwork (cons (cons '(local (include-book "std/lists/nth" :dir :system)) (cons (cons 'local (cons (cons 'fty::deflist (cons type-value-list (cons ':elt-type (cons type-value (cons ':true-listp (cons 't (cons ':elementp-of-nil (cons 'nil (cons ':pred (cons type-value-listp 'nil)))))))))) 'nil)) 'nil)) 'nil)))))))))))))) (cons (cons 'define (cons type-array-length (cons (cons (cons 'array (cons type-arrayp 'nil)) 'nil) (cons ':returns (cons '(length int-valuep) (cons ':short (cons (str::cat "Obtain the length of a Java " type-doc " array.") (cons (cons 'int-value (cons (cons 'len (cons (cons type-array->components '(array)) 'nil)) 'nil)) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons type-array->components '(sbyte32p))) 'nil))) 'nil) 'nil)))))))))) (cons (cons 'define (cons type-array-write (cons (cons (cons 'array (cons type-arrayp 'nil)) (cons '(index int-valuep) (cons (cons 'component (cons type-valuep 'nil)) 'nil))) (cons ':guard (cons (cons type-array-index-in-range-p '(array index)) (cons ':returns (cons (cons 'new-array (cons type-arrayp 'nil)) (cons ':short (cons (str::cat "Write a component to a Java " type-doc " array.") (cons (cons 'if (cons (cons 'mbt (cons (cons type-array-index-in-range-p '(array index)) 'nil)) (cons (cons type-array (cons (cons 'update-nth (cons '(int-value->int index) (cons 'component (cons (cons type-array->components '(array)) 'nil)))) 'nil)) (cons (cons type-array-fix '(array)) 'nil)))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons type-array->components (cons type-array-index-in-range-p 'nil))) 'nil))) 'nil) (cons ':prepwork (cons (cons '(local (include-book "std/lists/update-nth" :dir :system)) (cons (cons 'local (cons (cons 'fty::deflist (cons type-value-list (cons ':elt-type (cons type-value (cons ':true-listp (cons 't (cons ':elementp-of-nil (cons 'nil (cons ':pred (cons type-value-listp 'nil)))))))))) 'nil)) 'nil)) (cons '/// (cons (cons 'defret (cons (packn-pos (list 'len-of-components-of- type-array-write) jwit) (cons (cons 'equal (cons (cons 'len (cons (cons type-array->components '(new-array)) 'nil)) (cons (cons 'len (cons (cons type-array->components '(array)) 'nil)) 'nil))) (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons type-array->components (cons type-array-index-in-range-p (cons type-array (cons type-array-fix 'nil))))) 'nil))) 'nil) 'nil))))) (cons (cons 'defret (cons (packn-pos (list type-array-index-in-range-p '-of- type-array-write) jwit) (cons (cons 'equal (cons (cons type-array-index-in-range-p '(new-array index1)) (cons (cons type-array-index-in-range-p '(array index1)) 'nil))) (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons type-array-index-in-range-p 'nil)) 'nil))) 'nil) 'nil))))) 'nil))))))))))))))))) (cons (cons 'define (cons type-array-new-len (cons '((length int-valuep)) (cons ':guard (cons '(>= (int-value->int length) 0) (cons ':returns (cons (cons 'array (cons type-arrayp 'nil)) (cons ':short (cons (str::cat "Construct a Java " type-doc " array with the given length and with default components.") (cons (cons type-array (cons (cons 'repeat (cons '(int-value->int length) (cons (case type (boolean '(boolean-value nil)) (char '(char-value 0)) (byte '(byte-value 0)) (short '(short-value 0)) (int '(int-value 0)) (long '(long-value 0)) (float '(float-value (float-value-abs-pos-zero))) (double '(double-value (double-value-abs-pos-zero))) (t (impossible))) 'nil))) 'nil)) (cons ':prepwork (cons (cons '(local (include-book "std/lists/repeat" :dir :system)) (cons (cons 'local (cons (cons 'fty::deflist (cons type-value-list (cons ':elt-type (cons type-value (cons ':true-listp (cons 't (cons ':elementp-of-nil (cons 'nil (cons ':pred (cons type-value-listp 'nil)))))))))) 'nil)) 'nil)) 'nil)))))))))))) (cons (cons 'define (cons type-array-new-init (cons (cons (cons 'comps (cons type-value-listp 'nil)) 'nil) (cons ':guard (cons '(< (len comps) (expt 2 31)) (cons ':returns (cons (cons 'array (cons type-arrayp 'nil)) (cons ':short (cons (str::cat "Construct a Java " type-doc " array with the given initializer (i.e. components).") (cons (cons type-array '(comps)) 'nil)))))))))) (append (and acl2type (cons (cons 'define (cons type-array-to-list (cons (cons (cons 'array (cons type-arrayp 'nil)) 'nil) (cons ':returns (cons (cons 'list (cons acl2type-listp 'nil)) (cons ':short (cons (str::cat "Convert a Java " type-doc " array to an ACL2 list of " acl2type-doc ".") (cons (cons type-array-to-list-aux (cons (cons type-array->components '(array)) 'nil)) (cons ':prepwork (cons (cons (cons 'define (cons type-array-to-list-aux (cons (cons (cons 'comps (cons type-value-listp 'nil)) 'nil) (cons ':returns (cons (cons 'list (cons acl2type-listp 'nil)) (cons ':parents (cons 'nil (cons (cons 'cond (cons '((endp comps) nil) (cons (cons 't (cons (cons 'cons (cons (cons type-value->get '((car comps))) (cons (cons type-array-to-list-aux '((cdr comps))) 'nil))) 'nil)) 'nil))) (cons '/// (cons (cons 'defret (cons (packn-pos (list 'len-of- type-array-to-list-aux) jwit) '((equal (len list) (len comps))))) 'nil)))))))))) 'nil) (cons '/// (cons (cons 'defret (cons (packn-pos (list 'len-of- type-array-to-list) jwit) (cons (cons 'equal (cons '(len list) (cons (cons 'len (cons (cons type-array->components '(array)) 'nil)) 'nil))) 'nil))) 'nil)))))))))))) 'nil)) (and acl2type (cons (cons 'define (cons type-array-from-list (cons (cons (cons 'list (cons acl2type-listp 'nil)) 'nil) (cons ':guard (cons '(< (len list) (expt 2 31)) (cons ':returns (cons (cons 'array (cons type-arrayp 'nil)) (cons ':short (cons (str::cat "Convert an ACL2 list of " acl2type-doc " to a Java @('boolean') array.") (cons (cons type-array (cons (cons type-array-from-list-aux '(list)) 'nil)) (cons ':prepwork (cons (cons (cons 'define (cons type-array-from-list-aux (cons (cons (cons 'list (cons acl2type-listp 'nil)) 'nil) (cons ':returns (cons (cons 'comps (cons type-value-listp 'nil)) (cons ':parents (cons 'nil (cons (cons 'cond (cons '((endp list) nil) (cons (cons 't (cons (cons 'cons (cons (cons type-value '((car list))) (cons (cons type-array-from-list-aux '((cdr list))) 'nil))) 'nil)) 'nil))) (cons '/// (cons (cons 'defret (cons (packn-pos (list 'len-of- type-array-from-list-aux) jwit) '((equal (len comps) (len list))))) 'nil)))))))))) 'nil) 'nil)))))))))))) 'nil)))))))))))))