Generate a list of C block items that consists of a given item.
(atc-gen-block-item-list-one term type item item-limit item-events item-thm result new-compst new-context new-inscope gin state) → gout
This is used to lift generated block items to generated block item lists.
Besides the (singleton) block item list,
we also generate a theorem saying that
exec-block-item-list applied to the quoted block item list
yields an mv pair consisting of
a result term (or
The limit for the block item list is 1 more than the limit for the block item, because we need 1 to go from exec-block-item-list to exec-block-item.
When this function is called on a block item
that is an
The
Function:
(defun atc-gen-block-item-list-one (term type item item-limit item-events item-thm result new-compst new-context new-inscope gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-termp term) (typep type) (block-itemp item) (pseudo-termp item-limit) (pseudo-event-form-listp item-events) (symbolp item-thm) (atc-contextp new-context) (atc-symbol-varinfo-alist-listp new-inscope) (stmt-ginp gin)))) (let ((__function__ 'atc-gen-block-item-list-one)) (declare (ignorable __function__)) (b* (((stmt-gin gin) gin) (wrld (w state)) (items (list item)) (items-limit (pseudo-term-fncall 'binary-+ (list (pseudo-term-quote 1) item-limit))) ((when (not gin.proofs)) (make-stmt-gout :items items :type type :term term :context new-context :inscope new-inscope :limit items-limit :events item-events :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid)) (name (pack gin.fn '-correct- gin.thm-index)) (thm-index (1+ gin.thm-index)) ((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix name nil gin.names-to-avoid wrld)) (voidp (type-case type :void)) (exec-formula (cons 'equal (cons (cons 'exec-block-item-list (cons (cons 'quote (cons items 'nil)) (cons gin.compst-var (cons gin.fenv-var (cons gin.limit-var 'nil))))) (cons (cons 'mv (cons result (cons new-compst 'nil))) 'nil)))) (exec-formula (atc-contextualize exec-formula gin.context gin.fn gin.fn-guard gin.compst-var gin.limit-var items-limit t wrld)) (uterm (untranslate$ term nil state)) ((mv type-formula &) (atc-gen-term-type-formula uterm type gin.affect gin.inscope gin.prec-tags)) (type-formula (atc-contextualize type-formula gin.context gin.fn gin.fn-guard nil nil nil nil wrld)) (formula (cons 'and (cons exec-formula (cons type-formula 'nil)))) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-block-item-list-when-consp (cons 'not-zp-of-limit-variable (cons 'mv-nth-of-cons (cons '(:e zp) (cons 'value-optionp-when-valuep (cons '(:e value-optionp) (cons '(:e valuep) (append (and (not voidp) (list (atc-type-to-valuep-thm type gin.prec-tags))) (cons item-thm '(exec-block-item-list-of-nil not-zp-of-limit-minus-const compustatep-of-exit-scope compustatep-of-update-object compustatep-of-update-static-var compustatep-of-if*-when-both-compustatep uchar-array-length-of-uchar-array-write schar-array-length-of-schar-array-write ushort-array-length-of-ushort-array-write sshort-array-length-of-sshort-array-write uint-array-length-of-uint-array-write sint-array-length-of-sint-array-write ulong-array-length-of-ulong-array-write slong-array-length-of-slong-array-write ullong-array-length-of-ullong-array-write sllong-array-length-of-sllong-array-write)))))))))) 'nil)) 'nil))) 'nil)) ((mv event &) (evmac-generate-defthm name :formula formula :hints hints :enable nil))) (make-stmt-gout :items items :type type :term term :context new-context :inscope new-inscope :limit items-limit :events (append item-events (list event)) :thm-name name :thm-index thm-index :names-to-avoid names-to-avoid))))
Theorem:
(defthm stmt-goutp-of-atc-gen-block-item-list-one (b* ((gout (atc-gen-block-item-list-one term type item item-limit item-events item-thm result new-compst new-context new-inscope gin state))) (stmt-goutp gout)) :rule-classes :rewrite)