Generate a C expression from an ACL2 term that represents a ternary conditional expression.
(atc-gen-expr-cond term test-term then-term else-term test-expr then-expr else-expr test-type then-type else-type test-thm then-thm else-thm test-events then-events else-events gin state) → (mv erp gout)
Function:
(defun atc-gen-expr-cond (term test-term then-term else-term test-expr then-expr else-expr test-type then-type else-type test-thm then-thm else-thm test-events then-events else-events gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-termp term) (pseudo-termp test-term) (pseudo-termp then-term) (pseudo-termp else-term) (exprp test-expr) (exprp then-expr) (exprp else-expr) (typep test-type) (typep then-type) (typep else-type) (symbolp test-thm) (symbolp then-thm) (symbolp else-thm) (pseudo-event-form-listp test-events) (pseudo-event-form-listp then-events) (pseudo-event-form-listp else-events) (expr-ginp gin)))) (let ((__function__ 'atc-gen-expr-cond)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) (wrld (w state)) ((expr-gin gin) gin) ((unless (equal then-type else-type)) (reterr (msg "When generating C code for the function ~x0, ~ two branches ~x1 and ~x2 of a conditional term ~ have different types ~x3 and ~x4; ~ use conversion operations, if needed, ~ to make the branches of the same type." gin.fn then-term else-term then-type else-type))) (type then-type) ((when (member-equal type (list (type-uchar) (type-schar) (type-ushort) (type-sshort)))) (reterr (msg "When generating C code for the function ~x0, ~ two branches of the conditional term ~x1 ~ have type ~x2, which is disallowed; ~ use conversion operations, if needed, ~ to turn the branches into an integer type of higher rank." gin.fn term type))) (expr (make-expr-cond :test test-expr :then then-expr :else else-expr)) ((when (not gin.proofs)) (retok (make-expr-gout :expr expr :type type :term term :events (append test-events then-events else-events) :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid))) (test-type-pred (atc-type-to-recognizer test-type gin.prec-tags)) (valuep-when-test-type-pred (pack 'valuep-when- test-type-pred)) (type-pred (atc-type-to-recognizer type gin.prec-tags)) (valuep-when-type-pred (pack 'valuep-when- type-pred)) (value-kind-when-type-pred (pack 'value-kind-when- type-pred)) (value-kind-when-test-type-pred (pack 'value-kind-when- test-type-pred)) (term* (cons 'condexpr (cons (cons 'if* (cons test-term (cons then-term (cons else-term 'nil)))) 'nil))) (hints-then (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-cond-and-true (cons '(:e expr-kind) (cons '(:e expr-cond->test) (cons test-thm (cons '(:e expr-cond->then) (cons then-thm (cons '(:e expr-cond->else) (cons else-thm (cons 'booleanp-compound-recognizer (cons valuep-when-test-type-pred (cons 'expr-valuep-of-expr-value (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons valuep-when-type-pred (cons 'apconvert-expr-value-when-not-value-array (cons value-kind-when-type-pred (cons value-kind-when-test-type-pred 'nil))))))))))))))))) 'nil)) 'nil))) 'nil)) (hints-else (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-cond-and-false (cons '(:e expr-kind) (cons '(:e expr-cond->test) (cons test-thm (cons '(:e expr-cond->then) (cons then-thm (cons '(:e expr-cond->else) (cons else-thm (cons 'booleanp-compound-recognizer (cons valuep-when-test-type-pred (cons 'expr-valuep-of-expr-value (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons valuep-when-type-pred (cons 'apconvert-expr-value-when-not-value-array (cons value-kind-when-type-pred (cons value-kind-when-test-type-pred 'nil))))))))))))))))) 'nil)) 'nil))) 'nil)) (instructions (cons (cons 'casesplit (cons (atc-contextualize test-term gin.context nil nil nil nil nil nil wrld) 'nil)) (cons (cons 'claim (cons (atc-contextualize (cons 'test* (cons test-term 'nil)) gin.context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(test*)))))) (cons '(drop 1) (cons (cons 'claim (cons (atc-contextualize (cons 'equal (cons (cons 'condexpr (cons (cons 'if* (cons test-term (cons then-term (cons else-term 'nil)))) 'nil)) (cons then-term 'nil))) gin.context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(acl2::if*-when-true condexpr test*)))))) (cons (cons 'prove (cons ':hints (cons hints-then 'nil))) (cons (cons 'claim (cons (atc-contextualize (cons 'test* (cons (cons 'not (cons test-term 'nil)) 'nil)) gin.context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(test*)))))) (cons '(drop 1) (cons (cons 'claim (cons (atc-contextualize (cons 'equal (cons (cons 'condexpr (cons (cons 'if* (cons test-term (cons then-term (cons else-term 'nil)))) 'nil)) (cons else-term 'nil))) gin.context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(acl2::if*-when-false condexpr test*)))))) (cons (cons 'prove (cons ':hints (cons hints-else 'nil))) 'nil)))))))))) ((mv thm-event thm-name thm-index names-to-avoid) (atc-gen-expr-pure-correct-thm gin.fn gin.fn-guard gin.context expr type term* term* acl2::*nil* gin.compst-var nil instructions gin.prec-tags gin.thm-index gin.names-to-avoid state))) (retok (make-expr-gout :expr expr :type type :term term* :events (append test-events then-events else-events (list thm-event)) :thm-name thm-name :thm-index thm-index :names-to-avoid names-to-avoid)))))
Theorem:
(defthm expr-goutp-of-atc-gen-expr-cond.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-cond term test-term then-term else-term test-expr then-expr else-expr test-type then-type else-type test-thm then-thm else-thm test-events then-events else-events gin state))) (expr-goutp gout)) :rule-classes :rewrite)