		Search-engine friendly clone of the ACL2 documentation.

Expr-grade

Expr-grade-kind

Get the kind (tag) of a expr-grade structure.

Signature
(expr-grade-kind x) → kind
Arguments: x — Guard (expr-gradep x).

Definitions and Theorems

Function: expr-grade-kind$inline

(defun expr-grade-kind$inline (x)
  (declare (xargs :guard (expr-gradep x)))
  (let ((__function__ 'expr-grade-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :top)) :top)
                      ((eq (car x) :conditional) :conditional)
                      ((eq (car x) :disjunctive) :disjunctive)
                      ((eq (car x) :conjunctive) :conjunctive)
                      ((eq (car x) :equality) :equality)
                      ((eq (car x) :ordering) :ordering)
                      ((eq (car x) :bitwise-xor) :bitwise-xor)
                      ((eq (car x) :bitwise-ior) :bitwise-ior)
                      ((eq (car x) :bitwise-and) :bitwise-and)
                      ((eq (car x) :shift) :shift)
                      ((eq (car x) :additive) :additive)
                      ((eq (car x) :multiplicative)
                       :multiplicative)
                      ((eq (car x) :exponential) :exponential)
                      ((eq (car x) :unary) :unary)
                      ((eq (car x) :postfix) :postfix)
                      (t :primary))
         :exec (car x))))

Theorem: expr-grade-kind-possibilities

(defthm expr-grade-kind-possibilities
  (or (equal (expr-grade-kind x) :top)
      (equal (expr-grade-kind x) :conditional)
      (equal (expr-grade-kind x) :disjunctive)
      (equal (expr-grade-kind x) :conjunctive)
      (equal (expr-grade-kind x) :equality)
      (equal (expr-grade-kind x) :ordering)
      (equal (expr-grade-kind x) :bitwise-xor)
      (equal (expr-grade-kind x) :bitwise-ior)
      (equal (expr-grade-kind x) :bitwise-and)
      (equal (expr-grade-kind x) :shift)
      (equal (expr-grade-kind x) :additive)
      (equal (expr-grade-kind x)
             :multiplicative)
      (equal (expr-grade-kind x) :exponential)
      (equal (expr-grade-kind x) :unary)
      (equal (expr-grade-kind x) :postfix)
      (equal (expr-grade-kind x) :primary))
  :rule-classes
  ((:forward-chaining :trigger-terms ((expr-grade-kind x)))))