Generate the theorems to rewrite the execution of certain assignment expressions to structure writes, for a member of a structure type.
(atc-gen-tag-member-write-thms tag recognizer fixer-recognizer-thm valuep-thm value-kind-thm meminfo names-to-avoid wrld) → (mv local-events member-write-thms updated-names-to-avoid)
This class of theorems are the structure counterpart of
the ones that rewrite exec-expr-asg
that have
For a scalar member (which must have integer type),
we generate two theorems that
rewrite calls of exec-expr-asg,
where the assignee is a
For an array member (which must have integer element type), we generate 10 theorems, one for each integer index type. The theorem rewrites certain calls of exec-expr-asg to calls of the writers. The generation of these theorems relies on the fact that the order of the writers and the checkers matches the order of the types in *nonchar-integer-types*. Note that the defstruct-member-info contains 11 writers and 11 checkers, where the first writer and checker operate on ACL2 integers, while the other 10 writers and 10 checkers operate on C integers. We iterate through the 10 writers and checkers on C integers, while using the writer and checker on ACL2 integers at each iteration.
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-write-thms (tag recognizer fixer-recognizer-thm valuep-thm value-kind-thm meminfo names-to-avoid wrld) (declare (xargs :guard (and (identp tag) (symbolp recognizer) (symbolp fixer-recognizer-thm) (symbolp valuep-thm) (symbolp value-kind-thm) (defstruct-member-infop meminfo) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-gen-tag-member-write-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)) (writer (defstruct-member-info->writer meminfo)) (writer-element (defstruct-member-info->writer-element meminfo)) (checker (defstruct-member-info->checker meminfo)) (reader-return-thm (defstruct-member-info->reader-return-thm meminfo)) (writer-return-thm (defstruct-member-info->writer-return-thm meminfo)) ((when (type-nonchar-integerp type)) (b* ((thm-member-name (pack 'exec-member-write-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-write-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)) (fixtype (pack (type-kind type))) (typep (pack fixtype 'p)) ((unless typep) (raise "Internal error: unsupported member type ~x0." type) (mv nil nil nil)) (formula-member (cons 'implies (cons (cons 'and (cons '(syntaxp (quotep e)) (cons '(equal (expr-kind e) :binary) (cons '(equal (binop-kind (expr-binary->op e)) :asg) (cons '(equal left (expr-binary->arg1 e)) (cons '(equal right (expr-binary->arg2 e)) (cons '(equal (expr-kind left) :member) (cons '(equal target (expr-member->target left)) (cons '(equal member (expr-member->name left)) (cons '(equal (expr-kind target) :ident) (cons (cons 'equal (cons 'member (cons (cons 'ident (cons (ident->name memname) 'nil)) 'nil))) (cons '(not (zp limit)) (cons '(equal var (expr-ident->get target)) (cons '(equal struct (read-var var compst)) (cons (cons recognizer '(struct)) (cons '(equal eval (exec-expr-pure right compst)) (cons '(expr-valuep eval) (cons '(equal val (expr-value->value eval)) (cons (cons typep '(val)) 'nil))))))))))))))))))) (cons (cons 'equal (cons '(exec-expr-asg e compst fenv limit) (cons (cons 'write-var (cons 'var (cons (cons writer '(val struct)) '(compst)))) 'nil))) 'nil)))) (formula-memberp (cons 'implies (cons (cons 'and (cons '(syntaxp (quotep e)) (cons '(equal (expr-kind e) :binary) (cons '(equal (binop-kind (expr-binary->op e)) :asg) (cons '(equal left (expr-binary->arg1 e)) (cons '(equal right (expr-binary->arg2 e)) (cons '(equal (expr-kind left) :memberp) (cons '(equal target (expr-memberp->target left)) (cons '(equal member (expr-memberp->name left)) (cons '(equal (expr-kind target) :ident) (cons (cons 'equal (cons 'member (cons (cons 'ident (cons (ident->name memname) 'nil)) 'nil))) (cons '(not (zp limit)) (cons '(equal ptr (read-var (expr-ident->get target) compst)) (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 '(equal eval (exec-expr-pure right compst)) (cons '(expr-valuep eval) (cons '(equal val (expr-value->value eval)) (cons (cons typep '(val)) 'nil))))))))))))))))))))))) (cons (cons 'equal (cons '(exec-expr-asg e compst fenv limit) (cons (cons 'write-object (cons '(value-pointer->designator ptr) (cons (cons writer '(val struct)) '(compst)))) 'nil))) 'nil)))) (valuep-when-typep (pack 'valuep-when- typep)) (value-kind-when-typep (pack 'value-kind-when- typep)) (consp-when-typep (pack 'consp-when- typep)) (type-fix-when-typep (pack fixtype '-fix-when- typep)) (hints-member (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-asg (cons 'exec-expr-pure-when-member-no-syntaxp (cons 'exec-expr-pure-when-ident-no-syntaxp (cons 'exec-ident-open-via-object (cons 'exec-member (cons 'not-errorp-when-expr-valuep (cons 'expr-value-fix-when-expr-valuep (cons 'expr-valuep-of-expr-value (cons 'expr-value->value-of-expr-value (cons 'expr-value->object-of-expr-value (cons 'apconvert-expr-value-when-not-value-array-alt (cons 'not-errorp-when-valuep (cons 'value-fix-when-valuep (cons 'mv-nth-of-cons (cons '(:e zp) (cons 'objdesign-of-var-when-valuep-of-read-var (cons 'read-object-of-objdesign-of-var-to-read-var (cons 'write-object-of-objdesign-of-var-to-write-var (cons 'write-object (cons 'objdesign-option-fix (cons 'objdesign-fix-when-objdesignp (cons 'return-type-of-objdesign-member (cons 'objdesignp-of-objdesign-of-var-when-valuep-of-read-var (cons 'objdesign-member->super-of-objdesign-member (cons 'objdesign-member->name-of-objdesign-member (cons '(:t objdesign-member) (cons 'ident-fix-when-identp (cons 'identp-of-ident (cons valuep-when-typep (cons consp-when-typep (cons value-kind-when-typep (cons type-fix-when-typep (cons fixer-recognizer-thm (cons valuep-thm (cons value-kind-thm (cons reader (cons writer 'nil))))))))))))))))))))))))))))))))))))) 'nil)) (cons ':use (cons (cons (cons ':instance (cons reader-return-thm '((struct (read-var (expr-ident->get (expr-member->target (expr-binary->arg1 e))) compst))))) (cons (cons ':instance (cons writer-return-thm '((val (expr-value->value (exec-expr-pure (expr-binary->arg2 e) compst))) (struct (read-var (expr-ident->get (expr-member->target (expr-binary->arg1 e))) compst))))) 'nil)) 'nil))))) 'nil)) (hints-memberp (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-asg (cons 'exec-expr-pure-when-memberp-no-syntaxp (cons 'exec-expr-pure-when-ident-no-syntaxp (cons 'exec-ident-open-via-object (cons 'exec-memberp (cons 'not-errorp-when-expr-valuep (cons 'expr-value-fix-when-expr-valuep (cons 'expr-valuep-of-expr-value (cons 'expr-value->value-of-expr-value (cons 'expr-value->object-of-expr-value (cons 'apconvert-expr-value-when-not-value-array-alt (cons 'not-errorp-when-valuep (cons 'value-fix-when-valuep (cons 'mv-nth-of-cons (cons '(:e zp) (cons 'objdesign-of-var-when-valuep-of-read-var (cons 'read-object-of-objdesign-of-var-to-read-var (cons 'write-object (cons 'objdesign-option-fix (cons 'objdesign-fix-when-objdesignp (cons 'return-type-of-objdesign-member (cons 'objdesignp-of-value-pointer->designator (cons 'objdesign-member->super-of-objdesign-member (cons 'objdesign-member->name-of-objdesign-member (cons '(:t objdesign-member) (cons 'ident-fix-when-identp (cons 'identp-of-ident (cons valuep-when-typep (cons consp-when-typep (cons value-kind-when-typep (cons type-fix-when-typep (cons fixer-recognizer-thm (cons reader (cons writer (cons recognizer 'nil))))))))))))))))))))))))))))))))))) 'nil)) (cons ':use (cons (cons (cons ':instance (cons reader-return-thm '((struct (read-object (value-pointer->designator (read-var (expr-ident->get (expr-memberp->target (expr-binary->arg1 e))) compst)) compst))))) (cons (cons ':instance (cons writer-return-thm '((val (expr-value->value (exec-expr-pure (expr-binary->arg2 e) compst))) (struct (read-object (value-pointer->designator (read-var (expr-ident->get (expr-memberp->target (expr-binary->arg1 e))) compst)) compst))))) 'nil)) 'nil))))) 'nil)) ((mv event-member &) (evmac-generate-defthm thm-member-name :formula formula-member :hints hints-member :enable nil)) ((mv event-memberp &) (evmac-generate-defthm thm-memberp-name :formula formula-memberp :hints hints-memberp :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-write-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-write-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)) (elemfixtype (integer-type-to-fixtype elemtype)) (elemfixtypep (pack elemfixtype 'p)) (valuep-when-elemtype-arrayp (pack 'valuep-when- elemfixtype '-arrayp)) (value-kind-when-elemfixtype-arrayp (pack 'value-kind-when- elemfixtype '-arrayp)) (value-kind-when-elemfixtypep (pack 'value-kind-when- elemfixtype 'p)) (value-array-write-when-elemfixtype-arrayp (pack 'value-array-write-when- elemfixtype '-arrayp)) (elemfixtype-array-index-okp (pack elemfixtype '-array-index-okp)) (elemfixtype-arrayp-of-elemfixtype-array-write (pack elemfixtype '-arrayp-of- elemfixtype '-array-write)) (elemfixtype-array-fix-when-elemfixtype-arrayp (pack elemfixtype '-array-fix-when- elemfixtype '-arrayp)) (elemfixtype-array-length-of-elemfixtype-array-write (pack elemfixtype '-array-length-of- elemfixtype '-array-write)) (valuep-when-elemfixtypep (pack 'valuep-when- elemfixtype 'p)) (consp-when-elemfixtypep (pack 'consp-when- elemfixtype 'p)) (apconvert-expr-value-when-elemfixtype-arrayp (pack 'apconvert-expr-value-when- elemfixtype '-arrayp)) (value-array->elemtype-when-elemtype-arrayp (pack 'value-array->elemtype-when- elemfixtype '-arrayp)) (elemfixtypep-of-elemfixtype-array-read (pack elemfixtype 'p-of- elemfixtype '-array-read)) (value-array-read-when-elemfixtype-arrayp (pack 'value-array-read-when- elemfixtype '-arrayp)) (return-type-of-type-elemfixtype (pack 'return-type-of-type- elemfixtype)) (formula-member (cons 'implies (cons (cons 'and (cons '(equal (expr-kind e) :binary) (cons '(equal (binop-kind (expr-binary->op e)) :asg) (cons '(equal left (expr-binary->arg1 e)) (cons '(equal right (expr-binary->arg2 e)) (cons '(equal (expr-kind left) :arrsub) (cons '(equal array (expr-arrsub->arr left)) (cons '(equal index (expr-arrsub->sub left)) (cons '(equal (expr-kind array) :member) (cons '(equal target (expr-member->target array)) (cons '(equal member (expr-member->name array)) (cons '(equal (expr-kind target) :ident) (cons (cons 'equal (cons 'member (cons (cons 'ident (cons (ident->name memname) 'nil)) 'nil))) (cons '(not (zp limit)) (cons '(equal var (expr-ident->get target)) (cons '(equal struct (read-var var compst)) (cons (cons recognizer '(struct)) (cons '(equal eidx (exec-expr-pure index compst)) (cons '(expr-valuep eidx) (cons '(equal eidx1 (apconvert-expr-value eidx)) (cons '(expr-valuep eidx1) (cons '(equal idx (expr-value->value eidx1)) (cons '(cintegerp idx) (cons (cons checker (cons 'idx (and length (list 'struct)))) (cons '(equal eval (exec-expr-pure right compst)) (cons '(expr-valuep eval) (cons '(equal val (expr-value->value eval)) (cons (cons elemfixtypep '(val)) 'nil)))))))))))))))))))))))))))) (cons (cons 'equal (cons '(exec-expr-asg e compst fenv limit) (cons (cons 'write-var (cons 'var (cons (cons writer-element '(idx val struct)) '(compst)))) 'nil))) 'nil)))) (formula-memberp (cons 'implies (cons (cons 'and (cons '(equal (expr-kind e) :binary) (cons '(equal (binop-kind (expr-binary->op e)) :asg) (cons '(equal left (expr-binary->arg1 e)) (cons '(equal right (expr-binary->arg2 e)) (cons '(equal (expr-kind left) :arrsub) (cons '(equal array (expr-arrsub->arr left)) (cons '(equal index (expr-arrsub->sub left)) (cons '(equal (expr-kind array) :memberp) (cons '(equal target (expr-memberp->target array)) (cons '(equal member (expr-memberp->name array)) (cons '(equal (expr-kind target) :ident) (cons (cons 'equal (cons 'member (cons (cons 'ident (cons (ident->name memname) 'nil)) 'nil))) (cons '(not (zp limit)) (cons '(equal ptr (read-var (expr-ident->get target) compst)) (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 '(equal eidx (exec-expr-pure index compst)) (cons '(expr-valuep eidx) (cons '(equal eidx1 (apconvert-expr-value eidx)) (cons '(expr-valuep eidx1) (cons '(equal idx (expr-value->value eidx1)) (cons '(cintegerp idx) (cons (cons checker (cons 'idx (and length (list 'struct)))) (cons '(equal eval (exec-expr-pure right compst)) (cons '(expr-valuep eval) (cons '(equal eval1 (apconvert-expr-value eval)) (cons '(expr-valuep eval1) (cons '(equal val (expr-value->value eval1)) (cons (cons elemfixtypep '(val)) 'nil)))))))))))))))))))))))))))))))))) (cons (cons 'equal (cons '(exec-expr-asg e compst fenv limit) (cons (cons 'write-object (cons '(value-pointer->designator ptr) (cons (cons writer-element '(idx val struct)) '(compst)))) 'nil))) 'nil)))) (theory-member (cons 'exec-expr-asg (cons 'exec-expr-pure-when-arrsub-of-member-no-syntaxp (cons 'exec-expr-pure-when-ident-no-syntaxp (cons 'exec-ident-open-via-object (cons 'exec-arrsub-of-member (cons 'not-errorp-when-expr-valuep (cons 'expr-value-fix-when-expr-valuep (cons 'expr-valuep-of-expr-value (cons 'expr-valuep-of-expr-value (cons 'expr-value->value-of-expr-value (cons 'expr-value->object-of-expr-value (cons 'apconvert-expr-value-when-not-value-array-alt (cons 'value-fix-when-valuep (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 'value-pointer->reftype-of-value-pointer (cons 'pointer-valid->get-of-pointer-valid (cons 'read-object-of-objdesign-member (cons 'value-integerp-when-cintegerp (cons 'value-integer->get-when-cintegerp (cons 'integer-range-p (cons 'mv-nth-of-cons (cons '(:e zp) (cons 'not-errorp-when-valuep (cons 'objdesign-of-var-when-valuep-of-read-var (cons 'read-object-of-objdesign-of-var-to-read-var (cons 'write-object-of-objdesign-of-var-to-write-var (cons 'write-object (cons 'objdesign-option-fix (cons 'objdesign-fix-when-objdesignp (cons 'objdesignp-when-objdesign-optionp (cons 'objdesign-optionp-of-objdesign-of-var (cons 'objdesign-element->super-of-objdesign-element (cons 'objdesign-element->index-of-objdesign-element (cons 'objdesign-member->super-of-objdesign-member (cons 'objdesign-member->name-of-objdesign-member (cons 'return-type-of-objdesign-member (cons 'return-type-of-objdesign-element (cons 'value-struct-read (cons 'value-struct-write (cons '(:e ident) (cons '(:e ident-fix) (cons '(:t objdesign-element) (cons 'write-object (cons 'nfix (cons 'cintegerp-when-cintegerp-of-apconvert-expr-value (cons 'value-kind-not-array-when-cintegerp (cons 'atc-tag-generation-if-when-true (cons 'type-fix-when-typep (cons apconvert-expr-value-when-elemfixtype-arrayp (cons valuep-when-elemfixtypep (cons consp-when-elemfixtypep (cons value-kind-when-elemfixtypep (cons return-type-of-type-elemfixtype (cons valuep-when-elemtype-arrayp (cons value-kind-when-elemfixtype-arrayp (cons value-array->elemtype-when-elemtype-arrayp (cons value-array-read-when-elemfixtype-arrayp (cons value-array-write-when-elemfixtype-arrayp (cons elemfixtype-array-index-okp (cons elemfixtype-array-fix-when-elemfixtype-arrayp (cons elemfixtypep-of-elemfixtype-array-read (cons elemfixtype-arrayp-of-elemfixtype-array-write (cons elemfixtype-array-length-of-elemfixtype-array-write (cons fixer-recognizer-thm (cons reader (cons writer (cons writer-element (cons recognizer (cons checker (and length (list length))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (hints-member (cons (cons '"Goal" (cons ':use (cons (cons (cons ':instance (cons reader-return-thm '((struct (read-var (expr-ident->get (expr-member->target (expr-arrsub->arr (expr-binary->arg1 e)))) compst))))) (cons (cons ':instance (cons writer-return-thm (cons (cons 'val (cons (cons 'value-array-write (cons '(integer-from-cinteger (expr-value->value (exec-expr-pure (expr-arrsub->sub (expr-binary->arg1 e)) compst))) (cons '(expr-value->value (exec-expr-pure (expr-binary->arg2 e) compst)) (cons (cons 'value-struct-read (cons (cons 'ident (cons (ident->name memname) 'nil)) '((read-var (expr-ident->get (expr-member->target (expr-arrsub->arr (expr-binary->arg1 e)))) compst)))) 'nil)))) 'nil)) '((struct (read-var (expr-ident->get (expr-member->target (expr-arrsub->arr (expr-binary->arg1 e)))) compst)))))) 'nil)) (cons ':in-theory (cons (cons 'quote (cons theory-member 'nil)) 'nil))))) 'nil)) (theory-memberp (cons 'exec-expr-asg (cons 'not-errorp-when-expr-valuep (cons 'expr-valuep-of-expr-value (cons 'mv-nth-of-cons (cons '(:e zp) (cons 'not-errorp-when-valuep (cons valuep-when-elemfixtypep (cons consp-when-elemfixtypep (cons 'exec-expr-pure-when-arrsub-of-memberp-no-syntaxp (cons 'exec-expr-pure-when-ident-no-syntaxp (cons 'exec-ident-open-via-object (cons 'objdesign-of-var-when-valuep-of-read-var (cons 'exec-arrsub-of-memberp (cons 'read-object-of-objdesign-of-var-to-read-var (cons 'apconvert-expr-value-when-not-value-array-alt (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons 'expr-value-fix-when-expr-valuep (cons recognizer (cons reader (cons fixer-recognizer-thm (cons valuep-when-elemtype-arrayp (cons apconvert-expr-value-when-elemfixtype-arrayp (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 'objdesign-fix-when-objdesignp (cons 'read-object-of-objdesign-member (cons value-kind-when-elemfixtype-arrayp (cons 'value-pointer->reftype-of-value-pointer (cons 'type-fix-when-typep (cons return-type-of-type-elemfixtype (cons value-array->elemtype-when-elemtype-arrayp (cons 'cintegerp-when-cintegerp-of-apconvert-expr-value (cons 'value-kind-not-array-when-cintegerp (cons 'value-integerp-when-cintegerp (cons checker (cons 'integer-range-p (cons 'value-integer->get-when-cintegerp (cons value-array-read-when-elemfixtype-arrayp (cons elemfixtype-array-index-okp (cons elemfixtypep-of-elemfixtype-array-read (cons 'expr-value->object-of-expr-value (cons 'objdesign-option-fix (cons '(:t objdesign-element) (cons 'return-type-of-objdesign-element (cons 'write-object (cons 'objdesign-element->super-of-objdesign-element (cons 'objdesign-element->index-of-objdesign-element (cons 'nfix (cons writer (cons value-array-write-when-elemfixtype-arrayp (cons elemfixtype-arrayp-of-elemfixtype-array-write (cons elemfixtype-array-length-of-elemfixtype-array-write (cons 'objdesign-member->super-of-objdesign-member (cons 'objdesignp-of-value-pointer->designator (cons 'objdesign-member->name-of-objdesign-member (cons elemfixtype-array-fix-when-elemfixtype-arrayp (cons writer-element (cons 'value-struct-read (cons 'value-struct-write (cons '(:e ident) (cons '(:e ident-fix) (and length (list length))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (hints-memberp (cons (cons '"Goal" (cons ':use (cons (cons (cons ':instance (cons reader-return-thm '((struct (read-object (value-pointer->designator (read-var (expr-ident->get (expr-memberp->target (expr-arrsub->arr (expr-binary->arg1 e)))) compst)) compst))))) (cons (cons ':instance (cons writer-return-thm (cons (cons 'val (cons (cons 'value-array-write (cons '(integer-from-cinteger (expr-value->value (exec-expr-pure (expr-arrsub->sub (expr-binary->arg1 e)) compst))) (cons '(expr-value->value (apconvert-expr-value (exec-expr-pure (expr-binary->arg2 e) compst))) (cons (cons 'value-struct-read (cons (cons 'ident (cons (ident->name memname) 'nil)) '((read-object (value-pointer->designator (read-var (expr-ident->get (expr-memberp->target (expr-arrsub->arr (expr-binary->arg1 e)))) compst)) compst)))) 'nil)))) 'nil)) '((struct (read-object (value-pointer->designator (read-var (expr-ident->get (expr-memberp->target (expr-arrsub->arr (expr-binary->arg1 e)))) compst)) compst)))))) 'nil)) (cons ':in-theory (cons (cons 'quote (cons theory-memberp 'nil)) 'nil))))) 'nil)) ((mv event-member &) (evmac-generate-defthm thm-member-name :formula formula-member :hints hints-member :enable nil)) ((mv event-memberp &) (evmac-generate-defthm thm-memberp-name :formula formula-memberp :hints hints-memberp :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-write-thms.local-events (b* (((mv ?local-events ?member-write-thms ?updated-names-to-avoid) (atc-gen-tag-member-write-thms tag recognizer fixer-recognizer-thm valuep-thm value-kind-thm meminfo names-to-avoid wrld))) (pseudo-event-form-listp local-events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-tag-member-write-thms.member-write-thms (b* (((mv ?local-events ?member-write-thms ?updated-names-to-avoid) (atc-gen-tag-member-write-thms tag recognizer fixer-recognizer-thm valuep-thm value-kind-thm meminfo names-to-avoid wrld))) (symbol-listp member-write-thms)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-tag-member-write-thms.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?local-events ?member-write-thms ?updated-names-to-avoid) (atc-gen-tag-member-write-thms tag recognizer fixer-recognizer-thm valuep-thm value-kind-thm meminfo names-to-avoid wrld))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)