Check if a term may represent a conversion from a C integer value to an ACL2 boolean.
(atc-check-boolean-from-type term) → (mv erp yes/no fn arg in-type)
We also return the input C type of the conversion. The output type is known (boolean), and it is in fact an ACL2 type.
Function:
(defun atc-check-boolean-from-type (term) (declare (xargs :guard (pseudo-termp term))) (let ((__function__ 'atc-check-boolean-from-type)) (declare (ignorable __function__)) (b* (((reterr) nil nil nil (irr-type)) ((acl2::fun (no)) (retok nil nil nil (irr-type))) ((mv okp fn args) (fty-check-fn-call term)) ((unless okp) (no)) ((mv okp boolean from type) (atc-check-symbol-3part fn)) (in-type (fixtype-to-integer-type type)) ((unless (and okp (eq boolean 'boolean) (eq from 'from) in-type)) (no)) ((unless (equal (symbol-package-name fn) "C")) (reterr (msg "Invalid function ~x0 encountered: ~ it has the form of a conversion to boolean from integer, ~ but it is not in the \"C\" package." fn))) ((unless (list-lenp 1 args)) (reterr (raise "Internal error: ~x0 not applied to 1 argument." fn)))) (retok t fn (first args) in-type))))
Theorem:
(defthm booleanp-of-atc-check-boolean-from-type.yes/no (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?in-type) (atc-check-boolean-from-type term))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-check-boolean-from-type.fn (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?in-type) (atc-check-boolean-from-type term))) (symbolp fn)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-check-boolean-from-type.arg (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?in-type) (atc-check-boolean-from-type term))) (pseudo-termp arg)) :rule-classes :rewrite)
Theorem:
(defthm typep-of-atc-check-boolean-from-type.in-type (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?in-type) (atc-check-boolean-from-type term))) (typep in-type)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-term-count-of-atc-check-boolean-from-type (b* (((mv acl2::?erp ?yes/no ?fn ?arg ?in-type) (atc-check-boolean-from-type term))) (implies yes/no (< (pseudo-term-count arg) (pseudo-term-count term)))) :rule-classes :linear)