		Search-engine friendly clone of the ACL2 documentation.

Atc-term-recognizers

Atc-pure-c-valued-termp

Recognize pure expression terms returning C values terms.

Signature
(atc-pure-c-valued-termp term) → yes/no
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp 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.

Definitions and Theorems

Function: atc-pure-c-valued-termp

(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: booleanp-of-atc-pure-c-valued-termp

(defthm booleanp-of-atc-pure-c-valued-termp
  (b* ((yes/no (atc-pure-c-valued-termp term)))
    (booleanp yes/no))
  :rule-classes :rewrite)