Generate a C expression from an ACL2 term that represents a conversion to ACL2 boolean.
(atc-gen-expr-bool-from-type fn arg-term arg-expr arg-type arg-events arg-thm in-type gin state) → (mv erp gout)
The expression is the same as the one for the argument term: the conversion to ACL2 boolean only serves a purpose in the ACL2 representation but it has no counterpart in the C code.
The argument term is the
The hints include
the compound recognizer
Function:
(defun atc-gen-expr-bool-from-type (fn arg-term arg-expr arg-type arg-events arg-thm in-type gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (pseudo-termp arg-term) (exprp arg-expr) (typep arg-type) (pseudo-event-form-listp arg-events) (symbolp arg-thm) (typep in-type) (expr-ginp gin)))) (let ((__function__ 'atc-gen-expr-bool-from-type)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) ((expr-gin gin) gin) ((unless (equal arg-type in-type)) (reterr (msg "The conversion from ~x0 to boolean is applied to ~ an expression term ~x1 returning ~x2, ~ but a ~x0 operand is expected. ~ This is indicative of provably dead code, ~ given that the code is guard-verified." in-type arg-term arg-type))) (expr arg-expr) (aterm (cons fn (cons arg-term 'nil))) (type arg-type) ((when (not gin.proofs)) (retok (make-expr-gout :expr expr :type arg-type :term aterm :events arg-events :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid))) (cterm arg-term) ((unless (type-nonchar-integerp type)) (reterr (raise "Internal error: non-integer type ~x0." type))) (type-pred (atc-type-to-recognizer type gin.prec-tags)) (test-value-when-type-pred (pack 'test-value-when- type-pred)) (booleanp-of-fn (pack 'booleanp-of- fn)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons arg-thm (cons test-value-when-type-pred (cons booleanp-of-fn '(booleanp-compound-recognizer)))) 'nil)) 'nil))) 'nil)) (objdes (if (expr-case expr :ident) (cons 'objdesign-of-var (cons (cons 'ident (cons (cons 'quote (cons (ident->name (expr-ident->get expr)) 'nil)) 'nil)) (cons gin.compst-var 'nil))) acl2::*nil*)) ((mv thm-event thm-name thm-index names-to-avoid) (atc-gen-expr-bool-correct-thm gin.fn gin.fn-guard gin.context expr type aterm cterm objdes 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 aterm :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-bool-from-type.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-bool-from-type fn arg-term arg-expr arg-type arg-events arg-thm in-type gin state))) (expr-goutp gout)) :rule-classes :rewrite)