Generate a C block item that consists of an object declaration.
(atc-gen-block-item-declon var type expr expr-term expr-limit expr-events expr-thm gin state) → (mv item item-limit item-events item-thm new-inscope new-context thm-index names-to-avoid)
We get the (ACL2) variable, the type, and the expressions as inputs. We return not only the block item, and also a symbol table updated with the variable.
We generate a theorem about executing the initializer. We will soon generate an additional theorem, about executing the block item.
Function:
(defun atc-gen-block-item-declon (var type expr expr-term expr-limit expr-events expr-thm gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp var) (typep type) (exprp expr) (pseudo-termp expr-term) (pseudo-termp expr-limit) (pseudo-event-form-listp expr-events) (symbolp expr-thm) (stmt-ginp gin)))) (let ((__function__ 'atc-gen-block-item-declon)) (declare (ignorable __function__)) (b* (((stmt-gin gin) gin) (wrld (w state)) ((mv tyspec declor) (ident+type-to-tyspec+declor (make-ident :name (symbol-name var)) type)) (initer (initer-single expr)) (initer-limit (cons 'binary-+ (cons ''1 (cons expr-limit 'nil)))) (declon (make-obj-declon :scspec (scspecseq-none) :tyspec tyspec :declor declor :init? initer)) (item (block-item-declon declon)) (item-limit (cons 'binary-+ (cons ''1 (cons initer-limit 'nil)))) (varinfo (make-atc-var-info :type type :thm nil :externalp nil)) ((when (not gin.proofs)) (mv item item-limit expr-events nil (atc-add-var var varinfo gin.inscope) gin.context gin.thm-index gin.names-to-avoid)) (initer-thm-name (pack gin.fn '-correct- gin.thm-index)) (thm-index (1+ gin.thm-index)) ((mv initer-thm-name names-to-avoid) (fresh-logical-name-with-$s-suffix initer-thm-name nil gin.names-to-avoid wrld)) (initer-formula (cons 'equal (cons (cons 'exec-initer (cons (cons 'quote (cons initer 'nil)) (cons gin.compst-var (cons gin.fenv-var (cons gin.limit-var 'nil))))) (cons (cons 'mv (cons (cons 'init-value-single (cons expr-term 'nil)) (cons gin.compst-var 'nil))) 'nil)))) (initer-formula (atc-contextualize initer-formula gin.context gin.fn gin.fn-guard gin.compst-var gin.limit-var initer-limit t wrld)) (valuep-when-type-pred (atc-type-to-valuep-thm type gin.prec-tags)) (initer-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-initer-when-single (cons '(:e initer-kind) (cons 'not-zp-of-limit-variable (cons '(:e initer-single->get) (cons expr-thm (cons valuep-when-type-pred '(mv-nth-of-cons (:e zp)))))))) 'nil)) 'nil))) 'nil)) ((mv initer-thm-event &) (evmac-generate-defthm initer-thm-name :formula initer-formula :hints initer-hints :enable nil)) (new-compst (cons 'add-var (cons (cons 'ident (cons (cons 'quote (cons (symbol-name var) 'nil)) 'nil)) (cons expr-term (cons gin.compst-var 'nil))))) (item-thm-name (pack gin.fn '-correct- thm-index)) (thm-index (1+ thm-index)) ((mv item-thm-name names-to-avoid) (fresh-logical-name-with-$s-suffix item-thm-name nil names-to-avoid wrld)) (item-formula (cons 'equal (cons (cons 'exec-block-item (cons (cons 'quote (cons item 'nil)) (cons gin.compst-var (cons gin.fenv-var (cons gin.limit-var 'nil))))) (cons (cons 'mv (cons 'nil (cons (untranslate$ new-compst nil state) 'nil))) 'nil)))) (item-formula (atc-contextualize item-formula gin.context gin.fn gin.fn-guard gin.compst-var gin.limit-var item-limit t wrld)) (type-of-value-when-type-pred (atc-type-to-type-of-value-thm type gin.prec-tags)) (e-type (cons ':e (cons (car (type-to-maker type)) 'nil))) (item-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-block-item-when-declon (cons '(:e block-item-kind) (cons 'not-zp-of-limit-variable (cons '(:e block-item-declon->get) (cons '(:e obj-declon-to-ident+scspec+tyname+init) (cons 'mv-nth-of-cons (cons '(:e zp) (cons '(:e scspecseq-kind) (cons '(:e tyname-to-type) (cons '(:e type-kind) (cons initer-thm-name (cons 'return-type-of-init-value-single (cons 'init-value-to-value-when-single (cons expr-thm (cons valuep-when-type-pred (cons type-of-value-when-type-pred (cons e-type '(create-var-of-const-identifier (:e identp) (:e ident->name) create-var-to-add-var create-var-okp-of-add-var create-var-okp-of-enter-scope create-var-okp-of-add-frame create-var-okp-of-update-var create-var-okp-of-update-object ident-fix-when-identp equal-of-ident-and-ident (:e str-fix) identp-of-ident compustate-frames-number-of-add-var-not-zero compustate-frames-number-of-enter-scope-not-zero compustate-frames-number-of-add-frame-not-zero compustate-frames-number-of-update-var compustate-frames-number-of-update-object compustatep-of-add-var)))))))))))))))))) 'nil)) 'nil))) 'nil)) ((mv item-thm-event &) (evmac-generate-defthm item-thm-name :formula item-formula :hints item-hints :enable nil)) ((mv new-inscope new-context new-inscope-events thm-index names-to-avoid) (atc-gen-vardecl-inscope gin.fn gin.fn-guard gin.inscope gin.context var type (untranslate$ expr-term nil state) expr-thm gin.compst-var gin.prec-tags thm-index names-to-avoid wrld))) (mv item item-limit (append expr-events (list initer-thm-event item-thm-event) new-inscope-events) item-thm-name new-inscope new-context thm-index names-to-avoid))))
Theorem:
(defthm block-itemp-of-atc-gen-block-item-declon.item (b* (((mv ?item ?item-limit ?item-events ?item-thm ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-declon var type expr expr-term expr-limit expr-events expr-thm gin state))) (block-itemp item)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-gen-block-item-declon.item-limit (implies (pseudo-termp expr-limit) (b* (((mv ?item ?item-limit ?item-events ?item-thm ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-declon var type expr expr-term expr-limit expr-events expr-thm gin state))) (pseudo-termp item-limit))) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-block-item-declon.item-events (implies (pseudo-event-form-listp expr-events) (b* (((mv ?item ?item-limit ?item-events ?item-thm ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-declon var type expr expr-term expr-limit expr-events expr-thm gin state))) (pseudo-event-form-listp item-events))) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-block-item-declon.item-thm (b* (((mv ?item ?item-limit ?item-events ?item-thm ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-declon var type expr expr-term expr-limit expr-events expr-thm gin state))) (symbolp item-thm)) :rule-classes :rewrite)
Theorem:
(defthm atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-declon.new-inscope (b* (((mv ?item ?item-limit ?item-events ?item-thm ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-declon var type expr expr-term expr-limit expr-events expr-thm gin state))) (atc-symbol-varinfo-alist-listp new-inscope)) :rule-classes :rewrite)
Theorem:
(defthm atc-contextp-of-atc-gen-block-item-declon.new-context (b* (((mv ?item ?item-limit ?item-events ?item-thm ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-declon var type expr expr-term expr-limit expr-events expr-thm gin state))) (atc-contextp new-context)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atc-gen-block-item-declon.thm-index (b* (((mv ?item ?item-limit ?item-events ?item-thm ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-declon var type expr expr-term expr-limit expr-events expr-thm gin state))) (posp thm-index)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-block-item-declon.names-to-avoid (b* (((mv ?item ?item-limit ?item-events ?item-thm ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-declon var type expr expr-term expr-limit expr-events expr-thm gin state))) (symbol-listp names-to-avoid)) :rule-classes :rewrite)