Event to generate the model of arrays of an integer type.
(atc-def-integer-arrays type) → event
We generate the fixtype and the operatiosn that take indices of any C integer types. Note that indices are 0-based. We also generate the function that returns the length of an array, as an ACL2 integer.
We also generate theorems
Function:
(defun atc-def-integer-arrays (type) (declare (xargs :guard (typep type))) (declare (xargs :guard (type-nonchar-integerp type))) (let ((__function__ 'atc-def-integer-arrays)) (declare (ignorable __function__)) (b* ((type-string (integer-type-xdoc-string type)) (<type> (integer-type-to-fixtype type)) (<type>p (pack <type> 'p)) (<type>-fix (pack <type> '-fix)) (<type>-from-integer (pack <type> '-from-integer)) (<type>-list (pack <type> '-list)) (<type>-listp (pack <type> '-listp)) (<type>-array (pack <type> '-array)) (<type>-arrayp (pack <type>-array 'p)) (<type>-arrayp-alt-def (pack <type>-arrayp '-alt-def)) (<type>-array-of (pack <type>-array '-of)) (<type>-array-of-alt-def (pack <type>-array-of '-alt-def)) (<type>-array-fix (pack <type>-array '-fix)) (<type>-array->elemtype (pack <type>-array '->elemtype)) (<type>-array->elements (pack <type>-array '->elements)) (<type>-array->elements-alt-def (pack <type>-array->elements '-alt-def)) (<type>-array-length (pack <type>-array '-length)) (<type>-array-length-alt-def (pack <type>-array-length '-alt-def)) (<type>-array-integer-index-okp (pack <type> '-array-integer-index-okp)) (<type>-array-integer-read (pack <type>-array '-integer-read)) (<type>-array-integer-read-alt-def (pack <type>-array-integer-read '-alt-def)) (<type>-array-integer-write (pack <type>-array '-integer-write)) (<type>-array-integer-write-alt-def (pack <type>-array-integer-write '-alt-def)) (<type>-array-index-okp (pack <type> '-array-index-okp)) (<type>-array-read (pack <type>-array '-read)) (<type>-array-read-alt-def (pack <type>-array '-read-alt-def)) (<type>-array-write (pack <type>-array '-write)) (<type>-array-write-alt-def (pack <type>-array '-write-alt-def)) (<type>-array-of-of-<type>-array->elements (pack <type>-array-of '-of- <type>-array->elements)) (len-of-<type>-array->elements-of-<type>-array-integer-write (pack 'len-of- <type>-array->elements '-of- <type>-array-integer-write)) (len-of-<type>-array->elements-of-<type>-array-write (pack 'len-of- <type>-array->elements '-of- <type>-array-write)) (<type>-array-length-of-<type>-array-integer-write (pack <type> '-array-length-of- <type>-array-integer-write)) (<type>-array-length-of-<type>-array-write (pack <type> '-array-length-of- <type>-array-write)) (type-of-value-when-<type>p (pack 'type-of-value-when- <type>p)) (<type>-array-write-to-integer-write (pack <type>-array-write '-to-integer-write)) (value-listp-when-<type>-listp (pack 'value-listp-when- <type>-listp)) (valuep-when-<type>p (pack 'valuep-when- <type>p))) (cons 'progn (append (and (type-case type :char) (raise "Type ~x0 not supported." type)) (cons (cons 'fty::defprod (cons <type>-array (cons ':short (cons (str::cat "Fixtype of (ATC's model of) arrays of " type-string ".") (cons (cons (cons 'elemtype (cons 'type (cons ':reqfix (cons (cons 'if (cons (cons 'type-case (cons 'elemtype (cons (type-kind type) 'nil))) (cons 'elemtype (cons (type-to-maker type) 'nil)))) 'nil)))) (cons (cons 'elements (cons <type>-list (cons ':reqfix (cons (cons 'if (cons '(consp elements) (cons 'elements (cons (cons 'list (cons (cons <type>-from-integer '(0)) 'nil)) 'nil)))) 'nil)))) 'nil)) (cons ':require (cons (cons 'and (cons (cons 'type-case (cons 'elemtype (cons (type-kind type) 'nil))) '((consp elements)))) (cons ':layout (cons ':list (cons ':tag (cons ':array (cons ':pred (cons <type>-arrayp 'nil))))))))))))) (cons (cons 'defsection (cons (pack <type>-array '-ext) (cons ':extension (cons <type>-array (cons (cons 'defruled (cons <type>-arrayp-alt-def (cons (cons 'equal (cons (cons <type>-arrayp '(x)) (cons (cons 'and (cons '(valuep x) (cons '(value-case x :array) (cons (cons 'equal (cons '(value-array->elemtype x) (cons (type-to-maker type) 'nil))) (cons (cons <type>-listp '((value-array->elements x))) 'nil))))) 'nil))) (cons ':enable (cons (cons <type>-arrayp '(valuep value-kind value-array->elemtype value-array->elements)) 'nil))))) (cons (cons 'defruled (cons <type>-array->elements-alt-def (cons (cons 'implies (cons (cons <type>-arrayp '(array)) (cons (cons 'equal (cons (cons <type>-array->elements '(array)) '((value-array->elements array)))) 'nil))) (cons ':enable (cons (cons <type>-array->elements (cons 'value-array->elements (cons <type>-arrayp (cons 'valuep (cons 'value-kind (cons value-listp-when-<type>-listp 'nil)))))) 'nil))))) 'nil)))))) (cons (cons 'define (cons <type>-array-of (cons (cons (cons 'elements (cons <type>-listp 'nil)) 'nil) (cons ':guard (cons '(consp elements) (cons ':returns (cons (cons 'array (cons <type>-arrayp 'nil)) (cons ':short (cons (str::cat "Build an array of " type-string "from a list of its elements.") (cons (cons <type>-array (cons (type-to-maker type) '(elements))) (cons ':hooks (cons '(:fix) (cons '/// (cons (cons 'defrule (cons <type>-array-of-of-<type>-array->elements (cons (cons 'equal (cons (cons <type>-array-of (cons (cons <type>-array->elements '(array)) 'nil)) (cons (cons <type>-array-fix '(array)) 'nil))) (cons ':enable (cons <type>-array->elemtype 'nil))))) (cons (cons 'defruled (cons <type>-array-of-alt-def (cons (cons 'implies (cons (cons 'and (cons (cons <type>-listp '(elems)) '((consp elems)))) (cons (cons 'equal (cons (cons <type>-array-of '(elems)) (cons (cons 'make-value-array (cons ':elemtype (cons (type-to-maker type) '(:elements elems)))) 'nil))) 'nil))) (cons ':enable (cons (cons <type>-array-of (cons <type>-array '(value-array->elemtype value-array->elements valuep value-kind))) 'nil))))) 'nil))))))))))))))) (cons (cons 'define (cons <type>-array-length (cons (cons (cons 'array (cons <type>-arrayp 'nil)) 'nil) (cons ':returns (cons '(length posp :rule-classes (:rewrite :type-prescription) :hints (("Goal" :in-theory (enable posp)))) (cons ':short (cons (str::cat "Length of an array of " type-string ".") (cons (cons 'len (cons (cons <type>-array->elements '(array)) 'nil)) (cons ':hooks (cons '(:fix) (cons '/// (cons '(more-returns (length natp)) (cons (cons 'defruled (cons <type>-array-length-alt-def (cons (cons 'implies (cons (cons <type>-arrayp '(array)) (cons (cons 'equal (cons (cons <type>-array-length '(array)) '((value-array->length array)))) 'nil))) (cons ':enable (cons (cons <type>-array-length (cons 'value-array->length (cons <type>-array->elements-alt-def 'nil))) 'nil))))) 'nil))))))))))))) (cons (cons 'define (cons <type>-array-integer-index-okp (cons (cons (cons 'array (cons <type>-arrayp 'nil)) '((index integerp))) (cons ':returns (cons '(yes/no booleanp) (cons ':short (cons (str::cat "Check if an ACL2 integer is a valid index (i.e. in range) for an array of " type-string ".") (cons (cons 'integer-range-p (cons '0 (cons (cons <type>-array-length '(array)) '((ifix index))))) '(:hooks (:fix)))))))))) (cons (cons 'define (cons <type>-array-index-okp (cons (cons (cons 'array (cons <type>-arrayp 'nil)) '((index cintegerp))) (cons ':returns (cons '(yes/no booleanp) (cons ':short (cons (str::cat "Check if a C integer is a valid index (i.e. in range) for an array of " type-string ".") (cons (cons 'integer-range-p (cons '0 (cons (cons <type>-array-length '(array)) '((integer-from-cinteger index))))) '(:hooks (:fix)))))))))) (cons (cons 'define (cons <type>-array-integer-read (cons (cons (cons 'array (cons <type>-arrayp 'nil)) '((index integerp))) (cons ':guard (cons (cons <type>-array-integer-index-okp '(array index)) (cons ':returns (cons (cons 'element (cons <type>p 'nil)) (cons ':short (cons (str::cat "Read an element from an array of " type-string ", using an ACL2 integer index.") (cons (cons <type>-fix (cons (cons 'nth (cons 'index (cons (cons <type>-array->elements '(array)) 'nil))) 'nil)) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons <type>-array-integer-index-okp (cons <type>-array-length '(nfix ifix integer-range-p)))) 'nil))) 'nil) (cons '/// (cons (cons 'fty::deffixequiv (cons <type>-array-integer-read '(:hints (("Goal" :in-theory (enable ifix nth)))))) (cons (cons 'defruled (cons <type>-array-integer-read-alt-def (cons (cons 'implies (cons (cons 'and (cons (cons <type>-arrayp '(array)) (cons '(integerp index) (cons (cons <type>-array-integer-index-okp '(array index)) 'nil)))) (cons (cons 'equal (cons (cons <type>-array-integer-read '(array index)) '((value-array-read index array)))) 'nil))) (cons ':enable (cons (cons <type>-array-integer-read (cons 'value-array-read (cons <type>-array->elements-alt-def (cons <type>-array-integer-index-okp (cons <type>-array-length-alt-def (cons 'value-array->length (cons <type>-arrayp-alt-def '(nfix ifix integer-range-p)))))))) 'nil))))) 'nil))))))))))))))) (cons (cons 'define (cons <type>-array-read (cons (cons (cons 'array (cons <type>-arrayp 'nil)) '((index cintegerp))) (cons ':guard (cons (cons <type>-array-index-okp '(array index)) (cons ':returns (cons (cons 'element (cons <type>p 'nil)) (cons ':short (cons (str::cat "Read an element from an array of " type-string ", using a C integer index.") (cons (cons <type>-fix (cons (cons 'nth (cons '(integer-from-cinteger index) (cons (cons <type>-array->elements '(array)) 'nil))) 'nil)) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons <type>-array-index-okp (cons <type>-array-length '(integer-range-p)))) 'nil))) 'nil) (cons ':hooks (cons '(:fix) (cons '/// (cons (cons 'defruled (cons <type>-array-read-alt-def (cons (cons 'implies (cons (cons 'and (cons (cons <type>-arrayp '(array)) (cons '(cintegerp index) (cons (cons <type>-array-index-okp '(array index)) 'nil)))) (cons (cons 'equal (cons (cons <type>-array-read '(array index)) '((value-array-read (integer-from-cinteger index) array)))) 'nil))) (cons ':enable (cons (cons <type>-array-read (cons 'value-array-read (cons <type>-array->elements-alt-def (cons <type>-array-index-okp (cons <type>-array-length-alt-def (cons 'value-array->length (cons <type>-arrayp-alt-def '(integer-range-p)))))))) 'nil))))) 'nil)))))))))))))))) (cons (cons 'define (cons <type>-array-integer-write (cons (cons (cons 'array (cons <type>-arrayp 'nil)) (cons '(index integerp) (cons (cons 'element (cons <type>p 'nil)) 'nil))) (cons ':guard (cons (cons <type>-array-integer-index-okp '(array index)) (cons ':returns (cons (cons 'new-array (cons <type>-arrayp 'nil)) (cons ':short (cons (str::cat "Write an element to an array of " type-string ", using an ACL2 integer index.") (cons (cons 'b* (cons (cons (cons 'array (cons (cons <type>-array-fix '(array)) 'nil)) (cons '(index (ifix index)) (cons (cons 'element (cons (cons <type>-fix '(element)) 'nil)) 'nil))) (cons (cons 'if (cons (cons 'mbt (cons (cons <type>-array-integer-index-okp '(array index)) 'nil)) (cons (cons <type>-array-of (cons (cons 'update-nth (cons 'index (cons 'element (cons (cons <type>-array->elements '(array)) 'nil)))) 'nil)) '(array)))) 'nil))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons <type>-array-integer-index-okp (cons <type>-array-length '(nfix integer-range-p)))) 'nil))) 'nil) (cons ':hooks (cons '(:fix) (cons '/// (cons (cons 'defrule (cons len-of-<type>-array->elements-of-<type>-array-integer-write (cons (cons 'equal (cons (cons 'len (cons (cons <type>-array->elements (cons (cons <type>-array-integer-write '(array index element)) 'nil)) 'nil)) (cons (cons 'len (cons (cons <type>-array->elements '(array)) 'nil)) 'nil))) (cons ':enable (cons (cons <type>-array-integer-index-okp (cons <type>-array-length (cons <type>-array-of '(nfix ifix integer-range-p max)))) 'nil))))) (cons (cons 'defrule (cons <type>-array-length-of-<type>-array-integer-write (cons (cons 'equal (cons (cons <type>-array-length (cons (cons <type>-array-integer-write '(array index element)) 'nil)) (cons (cons <type>-array-length '(array)) 'nil))) (cons ':enable (cons (cons <type>-array-integer-index-okp (cons <type>-array-length (cons <type>-array-of '(nfix ifix integer-range-p max)))) 'nil))))) (cons (cons 'defruled (cons <type>-array-integer-write-alt-def (cons (cons 'implies (cons (cons 'and (cons (cons <type>-arrayp '(array)) (cons '(integerp index) (cons (cons <type>p '(elem)) (cons (cons <type>-array-integer-index-okp '(array index)) 'nil))))) (cons (cons 'equal (cons (cons <type>-array-integer-write '(array index elem)) '((value-array-write index elem array)))) 'nil))) (cons ':enable (cons (cons <type>-array-integer-write (cons 'value-array-write (cons <type>-arrayp-alt-def (cons <type>-array-of-alt-def (cons <type>-array-length-alt-def (cons <type>-array->elements-alt-def (cons <type>-array-integer-index-okp (cons 'value-array->length (cons type-of-value-when-<type>p (cons 'remove-flexible-array-member (cons 'flexible-array-member-p (cons 'nfix (cons 'ifix (cons 'integer-range-p (cons valuep-when-<type>p 'nil))))))))))))))) 'nil))))) 'nil)))))))))))))))))) (cons (cons 'define (cons <type>-array-write (cons (cons (cons 'array (cons <type>-arrayp 'nil)) (cons '(index cintegerp) (cons (cons 'element (cons <type>p 'nil)) 'nil))) (cons ':guard (cons (cons <type>-array-index-okp '(array index)) (cons ':returns (cons (cons 'new-array (cons <type>-arrayp 'nil)) (cons ':short (cons (str::cat "Write an element to an array of " type-string ", using a c integer index.") (cons (cons 'if (cons (cons 'mbt (cons (cons <type>-array-index-okp '(array index)) 'nil)) (cons (cons <type>-array-of (cons (cons 'update-nth (cons '(integer-from-cinteger index) (cons (cons <type>-fix '(element)) (cons (cons <type>-array->elements '(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-index-okp (cons <type>-array-length '(integer-range-p)))) 'nil))) 'nil) (cons ':hooks (cons '(:fix) (cons '/// (cons (cons 'defrule (cons len-of-<type>-array->elements-of-<type>-array-write (cons (cons 'equal (cons (cons 'len (cons (cons <type>-array->elements (cons (cons <type>-array-write '(array index element)) 'nil)) 'nil)) (cons (cons 'len (cons (cons <type>-array->elements '(array)) 'nil)) 'nil))) (cons ':enable (cons (cons <type>-array-index-okp (cons <type>-array-length (cons <type>-array-of '(integer-range-p max)))) 'nil))))) (cons (cons 'defrule (cons <type>-array-length-of-<type>-array-write (cons (cons 'equal (cons (cons <type>-array-length (cons (cons <type>-array-write '(array index element)) 'nil)) (cons (cons <type>-array-length '(array)) 'nil))) (cons ':enable (cons (cons <type>-array-index-okp (cons <type>-array-length (cons <type>-array-of '(integer-range-p max)))) 'nil))))) (cons (cons 'defruled (cons <type>-array-write-to-integer-write (cons (cons 'equal (cons (cons <type>-array-write '(array index val)) (cons (cons <type>-array-integer-write '(array (integer-from-cinteger index) val)) 'nil))) (cons ':enable (cons (cons <type>-array-integer-write (cons <type>-array-index-okp (cons <type>-array-integer-index-okp '(ifix)))) 'nil))))) (cons (cons 'defruled (cons <type>-array-write-alt-def (cons (cons 'implies (cons (cons 'and (cons (cons <type>-arrayp '(array)) (cons '(cintegerp index) (cons (cons <type>p '(elem)) (cons (cons <type>-array-index-okp '(array index)) 'nil))))) (cons (cons 'equal (cons (cons <type>-array-write '(array index elem)) '((value-array-write (integer-from-cinteger index) elem array)))) 'nil))) (cons ':enable (cons (cons <type>-array-write (cons 'value-array-write (cons <type>-arrayp-alt-def (cons <type>-array-of-alt-def (cons <type>-array-length-alt-def (cons <type>-array->elements-alt-def (cons <type>-array-index-okp (cons 'value-array->length (cons type-of-value-when-<type>p (cons 'remove-flexible-array-member (cons 'flexible-array-member-p (cons 'integer-range-p (cons value-listp-when-<type>-listp (cons valuep-when-<type>p 'nil)))))))))))))) 'nil))))) 'nil))))))))))))))))))) 'nil)))))))))))))))
Theorem:
(defthm pseudo-event-formp-of-atc-def-integer-arrays (b* ((event (atc-def-integer-arrays type))) (pseudo-event-formp event)) :rule-classes :rewrite)