Generate a C block item statement that consists of a variable declaration.
(atc-gen-block-item-var-decl var var-info? val-term gin state) → (mv erp item val-term* limit events thm-name new-inscope new-context thm-index names-to-avoid)
The information about the variable,
retrieved in atc-gen-stmt and passed here,
must be absent (i.e.
Function:
(defun atc-gen-block-item-var-decl (var var-info? val-term gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp var) (atc-var-info-optionp var-info?) (pseudo-termp val-term) (stmt-ginp gin)))) (let ((__function__ 'atc-gen-block-item-var-decl)) (declare (ignorable __function__)) (b* (((reterr) (irr-block-item) nil nil nil nil nil (irr-atc-context) 1 nil) ((stmt-gin gin) gin) ((when var-info?) (reterr (msg "The variable ~x0 in the function ~x1 ~ is already in scope and cannot be re-declared." var gin.fn))) ((unless (paident-stringp (symbol-name var))) (reterr (msg "The symbol name ~s0 of ~ the LET variable ~x1 of the function ~x2 ~ must be a portable ASCII C identifier, ~ but it is not." (symbol-name var) var gin.fn))) ((erp init.expr init.type init.term & & init.limit init.events init.thm-name & & init.thm-index init.names-to-avoid) (atc-gen-expr val-term (change-stmt-gin gin :affect nil) state)) ((when (or (type-case init.type :pointer) (type-case init.type :array))) (reterr (msg "When generating C code for the function ~x0, ~ the term ~x1 of type ~x2 ~ is being assigned to a new variable ~x3. ~ This is currently disallowed, ~ because it would create an alias." gin.fn val-term init.type var))) ((mv item item-limit item-events item-thm inscope-body context-body thm-index names-to-avoid) (atc-gen-block-item-declon var init.type init.expr init.term init.limit init.events init.thm-name (change-stmt-gin gin :thm-index init.thm-index :names-to-avoid init.names-to-avoid :proofs (and init.thm-name t)) state))) (retok item init.term item-limit item-events item-thm inscope-body context-body thm-index names-to-avoid))))
Theorem:
(defthm block-itemp-of-atc-gen-block-item-var-decl.item (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-var-decl var var-info? val-term gin state))) (block-itemp item)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-gen-block-item-var-decl.val-term* (implies (pseudo-termp val-term) (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-var-decl var var-info? val-term gin state))) (pseudo-termp val-term*))) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-gen-block-item-var-decl.limit (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-var-decl var var-info? val-term gin state))) (pseudo-termp limit)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-block-item-var-decl.events (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-var-decl var var-info? val-term gin state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-block-item-var-decl.thm-name (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-var-decl var var-info? val-term gin state))) (symbolp thm-name)) :rule-classes :rewrite)
Theorem:
(defthm atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-var-decl.new-inscope (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-var-decl var var-info? val-term gin state))) (atc-symbol-varinfo-alist-listp new-inscope)) :rule-classes :rewrite)
Theorem:
(defthm atc-contextp-of-atc-gen-block-item-var-decl.new-context (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-var-decl var var-info? val-term gin state))) (atc-contextp new-context)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atc-gen-block-item-var-decl.thm-index (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-var-decl var var-info? val-term gin state))) (posp thm-index)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-block-item-var-decl.names-to-avoid (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-var-decl var var-info? val-term gin state))) (symbol-listp names-to-avoid)) :rule-classes :rewrite)