Generate a list of block items by consing a block item to a list of block items.
(atc-gen-block-item-list-cons term item item-limit item-events item-thm items items-limit items-events items-thm items-type new-context new-inscope gin state) → gout
We need a limit that suffices for both
The context in
The
Currently this function is only called on a
Function:
(defun atc-gen-block-item-list-cons (term item item-limit item-events item-thm items items-limit items-events items-thm items-type new-context new-inscope gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-termp term) (block-itemp item) (pseudo-termp item-limit) (pseudo-event-form-listp item-events) (symbolp item-thm) (block-item-listp items) (pseudo-termp items-limit) (pseudo-event-form-listp items-events) (symbolp items-thm) (typep items-type) (atc-contextp new-context) (atc-symbol-varinfo-alist-listp new-inscope) (stmt-ginp gin)))) (let ((__function__ 'atc-gen-block-item-list-cons)) (declare (ignorable __function__)) (b* ((wrld (w state)) ((stmt-gin gin) gin) (all-items (cons item items)) (all-items-limit (cons 'binary-+ (cons ''1 (cons (cons 'binary-+ (cons item-limit (cons items-limit 'nil))) 'nil)))) ((when (not gin.proofs)) (make-stmt-gout :items all-items :type items-type :term term :context gin.context :inscope gin.inscope :limit all-items-limit :events (append item-events items-events) :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid)) (new-compst (atc-contextualize-compustate gin.compst-var gin.context new-context)) ((mv result type-formula &) (atc-gen-uterm-result-and-type-formula (untranslate$ term nil state) items-type gin.affect gin.inscope gin.prec-tags)) (exec-formula (cons 'equal (cons (cons 'exec-block-item-list (cons (cons 'quote (cons all-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 all-items-limit t wrld)) (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 item-thm (cons 'mv-nth-of-cons (cons '(:e zp) (cons '(:e value-optionp) (cons 'not-zp-of-limit-minus-const (cons '(:e valuep) (cons items-thm '(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)) (thm-name (pack gin.fn '-correct- gin.thm-index)) (thm-index (1+ gin.thm-index)) ((mv thm-name names-to-avoid) (fresh-logical-name-with-$s-suffix thm-name nil gin.names-to-avoid wrld)) ((mv event &) (evmac-generate-defthm thm-name :formula formula :hints hints :enable nil))) (make-stmt-gout :items all-items :type items-type :term term :context new-context :inscope new-inscope :limit all-items-limit :events (append item-events items-events (list event)) :thm-name thm-name :thm-index thm-index :names-to-avoid names-to-avoid))))
Theorem:
(defthm stmt-goutp-of-atc-gen-block-item-list-cons (b* ((gout (atc-gen-block-item-list-cons term item item-limit item-events item-thm items items-limit items-events items-thm items-type new-context new-inscope gin state))) (stmt-goutp gout)) :rule-classes :rewrite)