		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Check-if-call

Check if a term is a call of if.

Signature
(check-if-call term) → (mv yes/no test then else)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; test — Type (pseudo-termp test), given the guard.; then — Type (pseudo-termp then), given the guard.; else — Type (pseudo-termp else), given the guard.

If it is, return its test and branches. If it is not, all results are nil.

Definitions and Theorems

Function: check-if-call

(defun check-if-call (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'check-if-call))
  (declare (ignorable __function__))
  (b*
   (((when (variablep term))
     (mv nil nil nil nil))
    ((when (fquotep term))
     (mv nil nil nil nil))
    (fn (ffn-symb term))
    ((unless (eq fn 'if))
     (mv nil nil nil nil))
    ((unless (= (len (fargs term)) 3))
     (prog2$
      (raise
       "Internal error: ~
                        the IF call ~x0 has arguments ~x1."
       term (fargs term))
      (mv nil nil nil nil))))
   (mv t (fargn term 1)
       (fargn term 2)
       (fargn term 3)))))

Theorem: booleanp-of-check-if-call.yes/no

(defthm booleanp-of-check-if-call.yes/no
  (b* (((mv ?yes/no ?test ?then ?else)
        (check-if-call term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-check-if-call.test

(defthm pseudo-termp-of-check-if-call.test
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?test ?then ?else)
                 (check-if-call term)))
             (pseudo-termp test)))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-check-if-call.then

(defthm pseudo-termp-of-check-if-call.then
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?test ?then ?else)
                 (check-if-call term)))
             (pseudo-termp then)))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-check-if-call.else

(defthm pseudo-termp-of-check-if-call.else
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?test ?then ?else)
                 (check-if-call term)))
             (pseudo-termp else)))
  :rule-classes :rewrite)

Theorem: acl2-count-of-check-if-call.test

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

Theorem: acl2-count-of-check-if-call.then

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

Theorem: acl2-count-of-check-if-call.else

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