Recognize pure expression terms returning C values terms.
(atc-pure-c-valued-termp term) → yes/no
We just check that the term is either a variable or a call of one of the functions listed in the user documentation for pure expression terms returning C values.
Function:
(defun atc-pure-c-valued-termp (term) (declare (xargs :guard (pseudo-termp term))) (let ((__function__ 'atc-pure-c-valued-termp)) (declare (ignorable __function__)) (b* (((when (variablep term)) t)) (case-match term ((fn . &) (if (or (member-eq fn *atc-type-base-const-fns*) (member-eq fn *atc-op-type-fns*) (member-eq fn *atc-op-type1-type2-fns*) (member-eq fn *atc-type1-from-type2-fns*) (eq fn 'uchar-array-read-sint) (eq fn 'sint-from-boolean) (eq fn 'condexpr)) t nil)) (& nil)))))
Theorem:
(defthm booleanp-of-atc-pure-c-valued-termp (b* ((yes/no (atc-pure-c-valued-termp term))) (booleanp yes/no)) :rule-classes :rewrite)