Generate the theorems to rewrite the execution of certain pure expressions to structure reads, for a member of a structure type.
(atc-gen-tag-member-read-thms tag recognizer fixer fixer-recognizer-thm not-error-thm meminfo names-to-avoid wrld) → (mv local-events member-read-thms updated-names-to-avoid)
This class of theorems are the structure counterpart of the ones that rewrite exec-arrsub to array readers, generated in atc-exec-arrsub-rules-generation.
For a scalar member (which must have integer type), we generate two theorems that rewrite calls of exec-member and exec-memberp to calls of the reader.
For an array member (which must have integer element type),
we generate 20 theorems,
for each integer index type (10)
and for each of exec-member and exec-memberp.
The theorems rewrite calls of
If the structure type has a flexible array member, we avoid generating theorems for accessing members by structure value, because in ATC-generated code we only allow access by pointer.
Function:
(defun atc-gen-tag-member-read-thms (tag recognizer fixer fixer-recognizer-thm not-error-thm meminfo names-to-avoid wrld) (declare (xargs :guard (and (identp tag) (symbolp recognizer) (symbolp fixer) (symbolp fixer-recognizer-thm) (symbolp not-error-thm) (defstruct-member-infop meminfo) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-gen-tag-member-read-thms)) (declare (ignorable __function__)) (b* ((memtype (defstruct-member-info->memtype meminfo)) (memname (member-type->name memtype)) (type (member-type->type memtype)) (length (defstruct-member-info->length meminfo)) (reader (defstruct-member-info->reader meminfo)) (reader-element (defstruct-member-info->reader-element meminfo)) (checker (defstruct-member-info->checker meminfo)) ((when (type-nonchar-integerp type)) (b* ((thm-member-name (pack 'exec-member-read-when- recognizer '-and- (ident->name memname))) ((mv thm-member-name names-to-avoid) (fresh-logical-name-with-$s-suffix thm-member-name nil names-to-avoid wrld)) (thm-memberp-name (pack 'exec-memberp-read-when- recognizer '-and- (ident->name memname))) ((mv thm-memberp-name names-to-avoid) (fresh-logical-name-with-$s-suffix thm-memberp-name nil names-to-avoid wrld)) (formula-member (cons 'implies (cons (cons 'and (cons (atc-syntaxp-hyp-for-expr-pure 'struct) (cons (cons recognizer '(struct)) 'nil))) (cons (cons 'equal (cons (cons 'exec-member (cons '(expr-value struct objdes) (cons (cons 'ident (cons (ident->name memname) 'nil)) 'nil))) (cons (cons 'expr-value (cons (cons reader '(struct)) (cons (cons 'if (cons '(objdesign-option-fix objdes) (cons (cons 'objdesign-member (cons '(objdesign-option-fix objdes) (cons (cons 'ident (cons (ident->name memname) 'nil)) 'nil))) '(nil)))) 'nil))) 'nil))) 'nil)))) (formula-memberp (cons 'implies (cons (cons 'and (cons (atc-syntaxp-hyp-for-expr-pure 'ptr) (cons '(valuep ptr) (cons '(value-case ptr :pointer) (cons '(value-pointer-validp ptr) (cons (cons 'equal (cons '(value-pointer->reftype ptr) (cons (cons 'type-struct (cons (cons 'ident (cons (ident->name tag) 'nil)) 'nil)) 'nil))) (cons '(equal struct (read-object (value-pointer->designator ptr) compst)) (cons (cons recognizer '(struct)) 'nil)))))))) (cons (cons 'equal (cons (cons 'exec-memberp (cons '(expr-value ptr objdes) (cons (cons 'ident (cons (ident->name memname) 'nil)) '(compst)))) (cons (cons 'expr-value (cons (cons reader '(struct)) (cons (cons 'objdesign-member (cons '(value-pointer->designator ptr) (cons (cons 'ident (cons (ident->name memname) 'nil)) 'nil))) 'nil))) 'nil))) 'nil)))) (value-kind-when-typep (pack 'value-kind-when- (integer-type-to-fixtype type) 'p)) (valuep-when-typep (pack 'valuep-when- (integer-type-to-fixtype type) 'p)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-member (cons 'exec-memberp (cons 'not-errorp-when-valuep (cons 'value-resultp-when-valuep (cons 'value-result-fix-when-value-resultp (cons recognizer (cons reader (cons not-error-thm (cons fixer-recognizer-thm (cons 'value-struct-read (cons value-kind-when-typep (cons '(:e ident) (cons 'expr-value->value-of-expr-value (cons 'expr-value->object-of-expr-value (cons 'value-fix-when-valuep (cons 'not-errorp-when-valuep (cons valuep-when-typep '((:e objdesign-option-fix) apconvert-expr-value-when-not-value-array expr-valuep-of-expr-value not-errorp-when-expr-valuep)))))))))))))))))) 'nil)) 'nil))) 'nil)) ((mv event-member &) (evmac-generate-defthm thm-member-name :formula formula-member :hints hints :enable nil)) ((mv event-memberp &) (evmac-generate-defthm thm-memberp-name :formula formula-memberp :hints hints :enable nil))) (mv (list event-member event-memberp) (list thm-member-name thm-memberp-name) names-to-avoid))) ((unless (type-case type :array)) (prog2$ (raise "Internal error: member type ~x0." type) (mv nil nil nil))) (elemtype (type-array->of type)) ((unless (type-nonchar-integerp elemtype)) (prog2$ (raise "Internal error: array member element type ~x0." elemtype) (mv nil nil nil))) (thm-member-name (pack 'exec-member-read-when- recognizer '-and- (ident->name memname) '-element)) ((mv thm-member-name names-to-avoid) (fresh-logical-name-with-$s-suffix thm-member-name nil names-to-avoid wrld)) (thm-memberp-name (pack 'exec-memberp-read-when- recognizer '-and- (ident->name memname) '-element)) ((mv thm-memberp-name names-to-avoid) (fresh-logical-name-with-$s-suffix thm-memberp-name nil names-to-avoid wrld)) (formula-member (cons 'implies (cons (cons 'and (cons (cons recognizer '(struct)) (cons '(cintegerp index) (cons (cons checker (cons 'index (and length (list 'struct)))) '((objdesignp objdes-struct) (equal (read-object objdes-struct compst) struct)))))) (cons (cons 'equal (cons (cons 'exec-arrsub-of-member (cons '(expr-value struct objdes-struct) (cons (cons 'ident (cons (ident->name memname) 'nil)) '((expr-value index objdes-index) compst)))) (cons (cons 'expr-value (cons (cons reader-element '(index struct)) (cons (cons 'objdesign-element (cons (cons 'objdesign-member (cons 'objdes-struct (cons (cons 'ident (cons (ident->name memname) 'nil)) 'nil))) '((value-integer->get index)))) 'nil))) 'nil))) 'nil)))) (formula-memberp (cons 'implies (cons (cons 'and (cons '(valuep ptr) (cons '(value-case ptr :pointer) (cons '(value-pointer-validp ptr) (cons (cons 'equal (cons '(value-pointer->reftype ptr) (cons (cons 'type-struct (cons (cons 'ident (cons (ident->name tag) 'nil)) 'nil)) 'nil))) (cons '(equal struct (read-object (value-pointer->designator ptr) compst)) (cons (cons recognizer '(struct)) (cons '(cintegerp index) (cons (cons checker (cons 'index (and length (list 'struct)))) 'nil))))))))) (cons (cons 'equal (cons (cons 'exec-arrsub-of-memberp (cons '(expr-value ptr objdes-ptr) (cons (cons 'ident (cons (ident->name memname) 'nil)) '((expr-value index objdes-index) compst)))) (cons (cons 'expr-value (cons (cons reader-element '(index struct)) (cons (cons 'objdesign-element (cons (cons 'objdesign-member (cons '(value-pointer->designator ptr) (cons (cons 'ident (cons (ident->name memname) 'nil)) 'nil))) '((value-integer->get index)))) 'nil))) 'nil))) 'nil)))) (elemfixtype (integer-type-to-fixtype elemtype)) (valuep-when-elemtype-arrayp (pack 'valuep-when- elemfixtype '-arrayp)) (value-kind-when-elemtype-arrayp (pack 'value-kind-when- elemfixtype '-arrayp)) (value-array->elemtype-when-elemtype-arrayp (pack 'value-array->elemtype-when- elemfixtype '-arrayp)) (value-array-read-when-elemtype-arrayp (pack 'value-array-read-when- elemfixtype '-arrayp)) (apconvert-expr-value-when-elemtype-arrayp (pack 'apconvert-expr-value-when- elemfixtype '-arrayp)) (elemfixtype-array-index-okp (pack elemfixtype '-array-index-okp)) (type-elemfixtype (pack 'type- elemfixtype)) (elemfixtypep-of-elemfixtype-array-read (pack elemfixtype 'p-of- elemfixtype '-array-read)) (valuep-when-elemfixtypep (pack 'valuep-when- elemfixtype 'p)) (theory-member (cons 'exec-arrsub-of-member (cons 'apconvert-expr-value-when-not-value-array-alt (cons 'expr-value->value-of-expr-value (cons 'expr-value->object-of-expr-value (cons 'value-fix-when-valuep (cons recognizer (cons 'expr-value-fix-when-expr-valuep (cons 'expr-valuep-of-expr-value (cons 'not-errorp-when-expr-valuep (cons 'value-struct-read (cons '(:e ident) (cons 'not-errorp-when-valuep (cons valuep-when-elemtype-arrayp (cons apconvert-expr-value-when-elemtype-arrayp (cons 'objdesign-option-fix (cons 'not-nil-when-objdesignp (cons 'objdesign-fix-when-objdesignp (cons 'return-type-of-objdesign-member (cons 'return-type-of-value-pointer (cons 'value-pointer-validp-of-value-pointer (cons 'return-type-of-pointer-valid (cons 'value-pointer->designator-of-value-pointer (cons 'pointer-valid->get-of-pointer-valid (cons 'read-object-of-objdesign-member (cons value-kind-when-elemtype-arrayp (cons 'value-pointer->reftype-of-value-pointer (cons value-array->elemtype-when-elemtype-arrayp (cons '(:e type-fix) (cons (cons ':e (cons type-elemfixtype 'nil)) (cons 'value-kind-not-array-when-cintegerp (cons 'valuep-when-cintegerp (cons 'value-integerp-when-cintegerp (cons 'value-integer->get-when-cintegerp (cons checker (cons 'integer-range-p (cons value-array-read-when-elemtype-arrayp (cons elemfixtype-array-index-okp (cons elemfixtypep-of-elemfixtype-array-read (cons valuep-when-elemfixtypep (cons reader-element (cons reader (cons fixer (and length (list length))))))))))))))))))))))))))))))))))))))))))))) (theory-memberp (cons 'exec-arrsub-of-memberp (cons 'apconvert-expr-value-when-not-value-array-alt (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons recognizer (cons 'expr-value-fix-when-expr-valuep (cons 'expr-valuep-of-expr-value (cons 'not-errorp-when-expr-valuep (cons 'value-struct-read (cons '(:e ident) (cons 'not-errorp-when-valuep (cons valuep-when-elemtype-arrayp (cons apconvert-expr-value-when-elemtype-arrayp (cons 'objdesign-fix-when-objdesignp (cons 'return-type-of-objdesign-member (cons 'return-type-of-value-pointer (cons 'value-pointer-validp-of-value-pointer (cons 'return-type-of-pointer-valid (cons 'value-pointer->designator-of-value-pointer (cons 'pointer-valid->get-of-pointer-valid (cons 'read-object-of-objdesign-member (cons value-kind-when-elemtype-arrayp (cons 'value-pointer->reftype-of-value-pointer (cons value-array->elemtype-when-elemtype-arrayp (cons '(:e type-fix) (cons (cons ':e (cons type-elemfixtype 'nil)) (cons 'value-kind-not-array-when-cintegerp (cons 'valuep-when-cintegerp (cons 'value-integerp-when-cintegerp (cons 'value-integer->get-when-cintegerp (cons checker (cons 'integer-range-p (cons value-array-read-when-elemtype-arrayp (cons elemfixtype-array-index-okp (cons elemfixtypep-of-elemfixtype-array-read (cons valuep-when-elemfixtypep (cons reader-element (cons reader (cons fixer (and length (list length)))))))))))))))))))))))))))))))))))))))))) ((mv event-member &) (evmac-generate-defthm thm-member-name :formula formula-member :hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons theory-member 'nil)) 'nil))) 'nil) :enable nil)) ((mv event-memberp &) (evmac-generate-defthm thm-memberp-name :formula formula-memberp :hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons theory-memberp 'nil)) 'nil))) 'nil) :enable nil))) (mv (list event-member event-memberp) (list thm-member-name thm-memberp-name) names-to-avoid))))
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-tag-member-read-thms.local-events (b* (((mv ?local-events ?member-read-thms ?updated-names-to-avoid) (atc-gen-tag-member-read-thms tag recognizer fixer fixer-recognizer-thm not-error-thm meminfo names-to-avoid wrld))) (pseudo-event-form-listp local-events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-tag-member-read-thms.member-read-thms (b* (((mv ?local-events ?member-read-thms ?updated-names-to-avoid) (atc-gen-tag-member-read-thms tag recognizer fixer fixer-recognizer-thm not-error-thm meminfo names-to-avoid wrld))) (symbol-listp member-read-thms)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-tag-member-read-thms.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?local-events ?member-read-thms ?updated-names-to-avoid) (atc-gen-tag-member-read-thms tag recognizer fixer fixer-recognizer-thm not-error-thm meminfo names-to-avoid wrld))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)