Generate a C expression from an ACL2 term that represents a conversion from ACL2 boolean.
(atc-gen-expr-sint-from-bool arg-term arg-expr arg-events arg-thm gin state) → (mv erp gout)
The expression is the same as the argument expression: the conversion from ACL2 boolean only serves a purpose in the ACL2 representation but it has no counterpart in the C code.
To check that the argument term is an and or or, as described in the user documentation, is carried out on transformed terms. So we check that the argument term is a call of if*.
The proof of the correctness theorem is very simple. Since the argument term must be a call of and or or, the correctness theorem already states that sint-from-boolean applied to the argument term is equal to executing the expression and has the appropriate C type.
Function:
(defun atc-gen-expr-sint-from-bool (arg-term arg-expr arg-events arg-thm gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-termp arg-term) (exprp arg-expr) (pseudo-event-form-listp arg-events) (symbolp arg-thm) (expr-ginp gin)))) (let ((__function__ 'atc-gen-expr-sint-from-bool)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) ((expr-gin gin) gin) ((unless (and (consp arg-term) (eq (car arg-term) 'if*))) (reterr (msg "The conversion from boolean to C (signed) int ~ is applied to a boolean expression term ~x0 ~ that is not a (transformed) call of AND or OR." arg-term))) (term (cons 'sint-from-boolean (cons arg-term 'nil))) (expr arg-expr) (type (type-sint)) ((when (not gin.proofs)) (retok (make-expr-gout :expr expr :type type :term term :events arg-events :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid))) (hints (cons (cons '"Goal" (cons ':by (cons arg-thm '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 hints nil gin.prec-tags gin.thm-index gin.names-to-avoid state))) (retok (make-expr-gout :expr expr :type type :term term :events (append arg-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-sint-from-bool.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-sint-from-bool arg-term arg-expr arg-events arg-thm gin state))) (expr-goutp gout)) :rule-classes :rewrite)