		Search-engine friendly clone of the ACL2 documentation.

Jexpr-rank

Jexpr-rank-kind

Get the kind (tag) of a jexpr-rank structure.

Signature
(jexpr-rank-kind x) → kind
Arguments: x — Guard (jexpr-rankp x).

Definitions and Theorems

Function: jexpr-rank-kind$inline

(defun jexpr-rank-kind$inline (x)
  (declare (xargs :guard (jexpr-rankp x)))
  (let ((__function__ 'jexpr-rank-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :expression))
                       :expression)
                      ((eq (car x) :assignment) :assignment)
                      ((eq (car x) :conditional) :conditional)
                      ((eq (car x) :conditional-or)
                       :conditional-or)
                      ((eq (car x) :conditional-and)
                       :conditional-and)
                      ((eq (car x) :inclusive-or)
                       :inclusive-or)
                      ((eq (car x) :exclusive-or)
                       :exclusive-or)
                      ((eq (car x) :and) :and)
                      ((eq (car x) :equality) :equality)
                      ((eq (car x) :relational) :relational)
                      ((eq (car x) :shift) :shift)
                      ((eq (car x) :additive) :additive)
                      ((eq (car x) :multiplicative)
                       :multiplicative)
                      ((eq (car x) :unary) :unary)
                      ((eq (car x) :postfix) :postfix)
                      (t :primary))
         :exec (car x))))

Theorem: jexpr-rank-kind-possibilities

(defthm jexpr-rank-kind-possibilities
  (or (equal (jexpr-rank-kind x) :expression)
      (equal (jexpr-rank-kind x) :assignment)
      (equal (jexpr-rank-kind x) :conditional)
      (equal (jexpr-rank-kind x)
             :conditional-or)
      (equal (jexpr-rank-kind x)
             :conditional-and)
      (equal (jexpr-rank-kind x)
             :inclusive-or)
      (equal (jexpr-rank-kind x)
             :exclusive-or)
      (equal (jexpr-rank-kind x) :and)
      (equal (jexpr-rank-kind x) :equality)
      (equal (jexpr-rank-kind x) :relational)
      (equal (jexpr-rank-kind x) :shift)
      (equal (jexpr-rank-kind x) :additive)
      (equal (jexpr-rank-kind x)
             :multiplicative)
      (equal (jexpr-rank-kind x) :unary)
      (equal (jexpr-rank-kind x) :postfix)
      (equal (jexpr-rank-kind x) :primary))
  :rule-classes
  ((:forward-chaining :trigger-terms ((jexpr-rank-kind x)))))