		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-condexpr

Check if a term may represent a C conditional expression.

Signature
(atc-check-condexpr term) → (mv erp yes/no test then else)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; test — Type (pseudo-termp test).; then — Type (pseudo-termp then).; else — Type (pseudo-termp else).

Definitions and Theorems

Function: atc-check-condexpr

(defun atc-check-condexpr (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'atc-check-condexpr))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil nil nil nil)
    ((acl2::fun (no))
     (retok nil nil nil nil))
    ((mv okp fn args)
     (fty-check-fn-call term))
    ((unless (and okp (eq fn 'condexpr)))
     (no))
    ((unless (list-lenp 1 args))
     (reterr (raise "Internal error: ~x0 not applied to 1 argument."
                    fn)))
    (arg (first args))
    ((mv okp test then else)
     (fty-check-if-call arg))
    ((when (not okp))
     (reterr
      (msg
       "The function CONDEXPR is not applied to an IF, ~
                      but instead to the term ~x0."
       arg))))
   (retok t test then else))))

Theorem: booleanp-of-atc-check-condexpr.yes/no

(defthm booleanp-of-atc-check-condexpr.yes/no
  (b* (((mv acl2::?erp ?yes/no ?test ?then ?else)
        (atc-check-condexpr term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-condexpr.test

(defthm pseudo-termp-of-atc-check-condexpr.test
  (b* (((mv acl2::?erp ?yes/no ?test ?then ?else)
        (atc-check-condexpr term)))
    (pseudo-termp test))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-condexpr.then

(defthm pseudo-termp-of-atc-check-condexpr.then
  (b* (((mv acl2::?erp ?yes/no ?test ?then ?else)
        (atc-check-condexpr term)))
    (pseudo-termp then))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-condexpr.else

(defthm pseudo-termp-of-atc-check-condexpr.else
  (b* (((mv acl2::?erp ?yes/no ?test ?then ?else)
        (atc-check-condexpr term)))
    (pseudo-termp else))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-atc-check-condexpr.test

(defthm pseudo-term-count-of-atc-check-condexpr.test
  (b* (((mv acl2::?erp ?yes/no ?test ?then ?else)
        (atc-check-condexpr term)))
    (implies yes/no
             (< (pseudo-term-count test)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-atc-check-condexpr.then

(defthm pseudo-term-count-of-atc-check-condexpr.then
  (b* (((mv acl2::?erp ?yes/no ?test ?then ?else)
        (atc-check-condexpr term)))
    (implies yes/no
             (< (pseudo-term-count then)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-atc-check-condexpr.else

(defthm pseudo-term-count-of-atc-check-condexpr.else
  (b* (((mv acl2::?erp ?yes/no ?test ?then ?else)
        (atc-check-condexpr term)))
    (implies yes/no
             (< (pseudo-term-count else)
                (pseudo-term-count term))))
  :rule-classes :linear)