		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) :assignment) :assignment)
                      ((eq (car x) :conditional) :conditional)
                      ((eq (car x) :logical-or) :logical-or)
                      ((eq (car x) :logical-and) :logical-and)
                      ((eq (car x) :ior) :ior)
                      ((eq (car x) :xor) :xor)
                      ((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) :cast) :cast)
                      ((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) :assignment)
      (equal (expr-grade-kind x) :conditional)
      (equal (expr-grade-kind x) :logical-or)
      (equal (expr-grade-kind x) :logical-and)
      (equal (expr-grade-kind x) :ior)
      (equal (expr-grade-kind x) :xor)
      (equal (expr-grade-kind x) :and)
      (equal (expr-grade-kind x) :equality)
      (equal (expr-grade-kind x) :relational)
      (equal (expr-grade-kind x) :shift)
      (equal (expr-grade-kind x) :additive)
      (equal (expr-grade-kind x)
             :multiplicative)
      (equal (expr-grade-kind x) :cast)
      (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)))))