|
|
|---|
|
|
|
|---|
Generate the operations for an integer member of the structures defined by the defstruct.
(defstruct-gen-integer-member-ops
struct-tag struct-tag-p struct-tag-fix
value-kind-when-struct-tag-p
valuep-when-struct-tag-p name type)
→
(mv event reader writer reader-return-thm writer-return-thm)This are one reader and one writer. The reader is a wrapper of value-struct-read, and the writer is a wrapper of value-struct-write, but they have more specialized input and output types; in particular, they never return errors. To prove the output type of the reader, we just need to open some definitions. To prove the output type of the writer, we use an intermediate lemma.
Also return the information about the member for the defstruct table.
Function:
(defun defstruct-gen-integer-member-ops (struct-tag struct-tag-p struct-tag-fix value-kind-when-struct-tag-p valuep-when-struct-tag-p name type) (declare (xargs :guard (and (symbolp struct-tag) (symbolp struct-tag-p) (symbolp struct-tag-fix) (symbolp value-kind-when-struct-tag-p) (symbolp valuep-when-struct-tag-p) (identp name) (typep type)))) (declare (xargs :guard (type-nonchar-integerp type))) (let ((__function__ 'defstruct-gen-integer-member-ops)) (declare (ignorable __function__)) (b* ((fixtype (integer-type-to-fixtype type)) (typep (pack fixtype 'p)) (type-fix (pack fixtype '-fix)) (typep-of-type-fix (pack typep '-of- type-fix)) (type-fix-when-typep (pack type-fix '-when- typep)) (valuep-when-typep (pack 'valuep-when- typep)) (struct-tag-read-name (packn-pos (list struct-tag '-read- (ident->name name)) struct-tag)) (struct-tag-write-name (packn-pos (list struct-tag '-write- (ident->name name)) struct-tag)) (reader-return-thm (packn-pos (list typep '-of- struct-tag-read-name) struct-tag-read-name)) (writer-return-thm (packn-pos (list struct-tag-p '-of- struct-tag-write-name) struct-tag-write-name)) (struct-tag-fix-when-struct-tag-p (packn-pos (list struct-tag-fix '-when- struct-tag-p) struct-tag-p)) (struct-tag-p-of-struct-tag-fix (packn-pos (list struct-tag-p '-of- struct-tag-fix) struct-tag-p)) (lemma-theory (cons '(:e acl2::bool-fix) (cons '(:e ident) (cons '(:e ident-equiv) (cons '(:e ident-fix) (cons (cons ':t (cons struct-tag-p 'nil)) (cons '(:t value-struct) (cons '(:t value-struct-write-aux) (cons struct-tag-p (cons 'value-struct-write (cons 'member-value-list->name-list-of-struct-write-aux (cons 'member-value-list-fix-when-member-value-listp (cons 'member-value-listp-of-value-struct-write-aux (cons 'not-errorp-when-member-value-listp (cons 'remove-flexible-array-member-when-absent (cons 'return-type-of-value-struct (cons 'value-fix-when-valuep (cons 'value-optionp-when-valuep (cons 'value-struct->flexiblep-of-value-struct (cons 'value-struct->members-of-value-struct (cons 'value-struct->tag-of-value-struct (cons 'value-struct-read-aux-of-value-struct-write-aux (cons 'valuep-when-value-optionp (cons (pack 'not-flexible-array-member-p-when- typep) (cons (pack 'type-of-value-when- typep) (cons (pack 'valuep-when- typep) 'nil)))))))))))))))))))))))))) (struct-tag-read-theory (cons '(:e cons) (cons '(:e ident) (cons '(:e member-value) (cons '(:e value-struct) (cons '(:e value-struct->members$inline) (cons '(:e value-struct-read-aux) (cons '(:e repeat) (cons '(:e value-array) (cons '(:e type-uchar) (cons '(:e type-ushort) (cons '(:e type-uint) (cons '(:e type-ulong) (cons '(:e type-ullong) (cons '(:e type-schar) (cons '(:e type-sshort) (cons '(:e type-sint) (cons '(:e type-slong) (cons '(:e type-sllong) (cons '(:e schar-from-integer) (cons '(:e sshort-from-integer) (cons '(:e sint-from-integer) (cons '(:e slong-from-integer) (cons '(:e sllong-from-integer) (cons '(:e uchar-from-integer) (cons '(:e ushort-from-integer) (cons '(:e uint-from-integer) (cons '(:e ulong-from-integer) (cons '(:e ullong-from-integer) (cons (cons ':e (cons typep 'nil)) (cons (cons ':e (cons (pack fixtype '-from-integer) 'nil)) (cons (cons ':t (cons typep 'nil)) (cons (pack 'consp-when- typep) (cons struct-tag-fix (cons struct-tag-p (cons struct-tag-read-name '(value-struct-read))))))))))))))))))))))))))))))))))))) (event (cons 'encapsulate (cons 'nil (cons (cons 'defrulel (cons 'lemma (cons (cons 'implies (cons (cons 'and (cons (cons struct-tag-p '(struct)) (cons (cons typep '(val)) 'nil))) (cons (cons struct-tag-p (cons (cons 'value-struct-write (cons (cons 'quote (cons name 'nil)) '(val struct))) 'nil)) 'nil))) (cons ':in-theory (cons (cons 'quote (cons lemma-theory 'nil)) 'nil))))) (cons (cons 'define (cons struct-tag-read-name (cons (cons (cons 'struct (cons struct-tag-p 'nil)) 'nil) (cons ':returns (cons (cons 'val (cons typep (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons struct-tag-read-theory 'nil)) 'nil))) 'nil) 'nil)))) (cons (cons 'value-struct-read (cons (cons 'ident (cons (ident->name name) 'nil)) (cons (cons struct-tag-fix '(struct)) 'nil))) (cons ':guard-simplify (cons ':limited (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'identp-of-ident (cons value-kind-when-struct-tag-p (cons valuep-when-struct-tag-p (cons struct-tag-fix-when-struct-tag-p 'nil)))) 'nil)) 'nil))) 'nil) (cons '/// (cons (cons 'fty::deffixequiv (cons struct-tag-read-name (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons struct-tag-read-name (cons struct-tag-p-of-struct-tag-fix (cons struct-tag-fix-when-struct-tag-p 'nil))) 'nil)) 'nil))) 'nil) 'nil)))) 'nil)))))))))))) (cons (cons 'define (cons struct-tag-write-name (cons (cons (cons 'val (cons typep 'nil)) (cons (cons 'struct (cons struct-tag-p 'nil)) 'nil)) (cons ':returns (cons (cons 'new-struct (cons struct-tag-p (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons struct-tag-write-name (cons 'lemma (cons typep-of-type-fix (cons struct-tag-p-of-struct-tag-fix '((:e ident)))))) 'nil)) 'nil))) 'nil) 'nil)))) (cons (cons 'value-struct-write (cons (cons 'ident (cons (ident->name name) 'nil)) (cons (cons type-fix '(val)) (cons (cons struct-tag-fix '(struct)) 'nil)))) (cons ':guard-simplify (cons ':limited (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'identp-of-ident (cons struct-tag-fix-when-struct-tag-p (cons valuep-when-struct-tag-p (cons value-kind-when-struct-tag-p (cons type-fix-when-typep (cons valuep-when-typep 'nil)))))) 'nil)) 'nil))) 'nil) (cons '/// (cons (cons 'fty::deffixequiv (cons struct-tag-write-name (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons struct-tag-write-name (cons type-fix-when-typep (cons typep-of-type-fix (cons struct-tag-fix-when-struct-tag-p (cons struct-tag-p-of-struct-tag-fix 'nil))))) 'nil)) 'nil))) 'nil) 'nil)))) 'nil)))))))))))) 'nil))))))) (mv event struct-tag-read-name struct-tag-write-name reader-return-thm writer-return-thm))))
Theorem:
(defthm pseudo-event-formp-of-defstruct-gen-integer-member-ops.event (b* (((mv acl2::?event ?reader ?writer ?reader-return-thm ?writer-return-thm) (defstruct-gen-integer-member-ops struct-tag struct-tag-p struct-tag-fix value-kind-when-struct-tag-p valuep-when-struct-tag-p name type))) (pseudo-event-formp event)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-defstruct-gen-integer-member-ops.reader (b* (((mv acl2::?event ?reader ?writer ?reader-return-thm ?writer-return-thm) (defstruct-gen-integer-member-ops struct-tag struct-tag-p struct-tag-fix value-kind-when-struct-tag-p valuep-when-struct-tag-p name type))) (symbolp reader)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-defstruct-gen-integer-member-ops.writer (b* (((mv acl2::?event ?reader ?writer ?reader-return-thm ?writer-return-thm) (defstruct-gen-integer-member-ops struct-tag struct-tag-p struct-tag-fix value-kind-when-struct-tag-p valuep-when-struct-tag-p name type))) (symbolp writer)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-defstruct-gen-integer-member-ops.reader-return-thm (b* (((mv acl2::?event ?reader ?writer ?reader-return-thm ?writer-return-thm) (defstruct-gen-integer-member-ops struct-tag struct-tag-p struct-tag-fix value-kind-when-struct-tag-p valuep-when-struct-tag-p name type))) (symbolp reader-return-thm)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-defstruct-gen-integer-member-ops.writer-return-thm (b* (((mv acl2::?event ?reader ?writer ?reader-return-thm ?writer-return-thm) (defstruct-gen-integer-member-ops struct-tag struct-tag-p struct-tag-fix value-kind-when-struct-tag-p valuep-when-struct-tag-p name type))) (symbolp writer-return-thm)) :rule-classes :rewrite)