Generate the fixer of the structures defined by the defstruct.
(defstruct-gen-fixer struct-tag-fix struct-tag-p tag memtypes flexiblep) → (mv event fixer-recognizer-thm)
As the fixing value, we pick a structure with the right tag, the right member names, zero integer values of appropriate types for the integer members, and arrays of zeros of appropriate types and appropriate lengths for the integer array mmbers.
We also return the name of the theorem that rewrites the fixer away when the recognizer holds.
Function:
(defun defstruct-gen-fixer-aux (memtypes) (declare (xargs :guard (member-type-listp memtypes))) (let ((__function__ 'defstruct-gen-fixer-aux)) (declare (ignorable __function__)) (b* (((when (endp memtypes)) nil) ((member-type member) (car memtypes)) (val (defstruct-gen-fixing-term member.type)) (term (cons 'make-member-value (cons ':name (cons (cons 'quote (cons member.name 'nil)) (cons ':value (cons val 'nil)))))) (terms (defstruct-gen-fixer-aux (cdr memtypes)))) (cons term terms))))
Theorem:
(defthm true-listp-of-defstruct-gen-fixer-aux (b* ((terms (defstruct-gen-fixer-aux memtypes))) (true-listp terms)) :rule-classes :rewrite)
Function:
(defun defstruct-gen-fixer (struct-tag-fix struct-tag-p tag memtypes flexiblep) (declare (xargs :guard (and (symbolp struct-tag-fix) (symbolp struct-tag-p) (symbolp tag) (member-type-listp memtypes) (booleanp flexiblep)))) (let ((__function__ 'defstruct-gen-fixer)) (declare (ignorable __function__)) (b* ((event-theory (cons '(:e cons) (cons '(:e ident) (cons '(:e repeat) (cons '(:e member-value) (cons '(:e value-array) (cons '(:e value-struct) (cons (cons ':e (cons struct-tag-p 'nil)) (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 uchar-from-integer) (cons '(:e ushort-from-integer) (cons '(:e uint-from-integer) (cons '(:e ulong-from-integer) (cons '(:e ullong-from-integer) (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 '(:t value-struct) (cons (cons ':t (cons struct-tag-p 'nil)) 'nil)))))))))))))))))))))))))))))) (event (cons 'encapsulate (cons 'nil (cons (cons 'local (cons (cons 'in-theory (cons (cons 'quote (cons event-theory 'nil)) 'nil)) 'nil)) (cons (cons 'std::deffixer (cons struct-tag-fix (cons ':pred (cons struct-tag-p (cons ':param (cons 'x (cons ':body-fix (cons (cons 'make-value-struct (cons ':tag (cons (cons 'ident (cons (symbol-name tag) 'nil)) (cons ':members (cons (cons 'list (defstruct-gen-fixer-aux memtypes)) (cons ':flexiblep (cons flexiblep 'nil))))))) 'nil)))))))) 'nil))))) (thm (packn-pos (list struct-tag-fix '-when- struct-tag-p) struct-tag-fix))) (mv event thm))))
Theorem:
(defthm pseudo-event-formp-of-defstruct-gen-fixer.event (b* (((mv acl2::?event ?fixer-recognizer-thm) (defstruct-gen-fixer struct-tag-fix struct-tag-p tag memtypes flexiblep))) (pseudo-event-formp event)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-defstruct-gen-fixer.fixer-recognizer-thm (b* (((mv acl2::?event ?fixer-recognizer-thm) (defstruct-gen-fixer struct-tag-fix struct-tag-p tag memtypes flexiblep))) (symbolp fixer-recognizer-thm)) :rule-classes :rewrite)