Generate a C structure type declaration, with accompanying theorems.
(atc-gen-tag-declon tag info prec-tags proofs names-to-avoid wrld) → (mv declon local-events updated-prec-tags updated-names-to-avoid)
Function:
(defun atc-gen-tag-declon (tag info prec-tags proofs names-to-avoid wrld) (declare (xargs :guard (and (stringp tag) (defstruct-infop info) (atc-string-taginfo-alistp prec-tags) (booleanp proofs) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-gen-tag-declon)) (declare (ignorable __function__)) (b* ((meminfos (defstruct-info->members info)) (memtypes (defstruct-member-info-list->memtype-list meminfos)) (tag-ident (defstruct-info->tag info)) (recognizer (defstruct-info->recognizer info)) (fixer (defstruct-info->fixer info)) (fixer-recognizer-thm (defstruct-info->fixer-recognizer-thm info)) (not-error-thm (defstruct-info->not-error-thm info)) (valuep-thm (defstruct-info->valuep-thm info)) (value-kind-thm (defstruct-info->value-kind-thm info)) (struct-declons (atc-gen-struct-declon-list memtypes)) ((mv read-thm-events read-thm-names names-to-avoid) (if proofs (atc-gen-tag-member-read-all-thms tag-ident recognizer fixer fixer-recognizer-thm not-error-thm meminfos names-to-avoid wrld) (mv nil nil names-to-avoid))) ((mv write-thm-events write-thm-names names-to-avoid) (if proofs (atc-gen-tag-member-write-all-thms tag-ident recognizer fixer-recognizer-thm valuep-thm value-kind-thm meminfos names-to-avoid wrld) (mv nil nil names-to-avoid))) (thm-events (append read-thm-events write-thm-events)) (info (make-atc-tag-info :defstruct info :member-read-thms read-thm-names :member-write-thms write-thm-names)) (prec-tags (acons tag info prec-tags))) (mv (make-tag-declon-struct :tag tag-ident :members struct-declons) thm-events prec-tags names-to-avoid))))
Theorem:
(defthm tag-declonp-of-atc-gen-tag-declon.declon (b* (((mv ?declon ?local-events ?updated-prec-tags ?updated-names-to-avoid) (atc-gen-tag-declon tag info prec-tags proofs names-to-avoid wrld))) (tag-declonp declon)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-tag-declon.local-events (b* (((mv ?declon ?local-events ?updated-prec-tags ?updated-names-to-avoid) (atc-gen-tag-declon tag info prec-tags proofs names-to-avoid wrld))) (pseudo-event-form-listp local-events)) :rule-classes :rewrite)
Theorem:
(defthm atc-string-taginfo-alistp-of-atc-gen-tag-declon.updated-prec-tags (implies (and (stringp tag) (atc-string-taginfo-alistp prec-tags)) (b* (((mv ?declon ?local-events ?updated-prec-tags ?updated-names-to-avoid) (atc-gen-tag-declon tag info prec-tags proofs names-to-avoid wrld))) (atc-string-taginfo-alistp updated-prec-tags))) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-tag-declon.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?declon ?local-events ?updated-prec-tags ?updated-names-to-avoid) (atc-gen-tag-declon tag info prec-tags proofs names-to-avoid wrld))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)