		Search-engine friendly clone of the ACL2 documentation.

Vl-expr

Vl-expr-kind

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

Signature
(vl-expr-kind x) → kind
Arguments: x — Guard (vl-expr-p x).

Definitions and Theorems

Function: vl-expr-kind$inline

(defun vl-expr-kind$inline (x)
  (declare (xargs :guard (vl-expr-p x)))
  (let ((__function__ 'vl-expr-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :vl-literal))
                       :vl-literal)
                      ((eq (car x) :vl-index) :vl-index)
                      ((eq (car x) :vl-unary) :vl-unary)
                      ((eq (car x) :vl-binary) :vl-binary)
                      ((eq (car x) :vl-qmark) :vl-qmark)
                      ((eq (car x) :vl-concat) :vl-concat)
                      ((eq (car x) :vl-multiconcat)
                       :vl-multiconcat)
                      ((eq (car x) :vl-bitselect-expr)
                       :vl-bitselect-expr)
                      ((eq (car x) :vl-partselect-expr)
                       :vl-partselect-expr)
                      ((eq (car x) :vl-mintypmax)
                       :vl-mintypmax)
                      ((eq (car x) :vl-call) :vl-call)
                      ((eq (car x) :vl-stream) :vl-stream)
                      ((eq (car x) :vl-cast) :vl-cast)
                      ((eq (car x) :vl-inside) :vl-inside)
                      ((eq (car x) :vl-tagged) :vl-tagged)
                      ((eq (car x) :vl-pattern) :vl-pattern)
                      ((eq (car x) :vl-special) :vl-special)
                      (t :vl-eventexpr))
         :exec (car x))))

Theorem: vl-expr-kind-possibilities

(defthm vl-expr-kind-possibilities
  (or (equal (vl-expr-kind x) :vl-literal)
      (equal (vl-expr-kind x) :vl-index)
      (equal (vl-expr-kind x) :vl-unary)
      (equal (vl-expr-kind x) :vl-binary)
      (equal (vl-expr-kind x) :vl-qmark)
      (equal (vl-expr-kind x) :vl-concat)
      (equal (vl-expr-kind x) :vl-multiconcat)
      (equal (vl-expr-kind x)
             :vl-bitselect-expr)
      (equal (vl-expr-kind x)
             :vl-partselect-expr)
      (equal (vl-expr-kind x) :vl-mintypmax)
      (equal (vl-expr-kind x) :vl-call)
      (equal (vl-expr-kind x) :vl-stream)
      (equal (vl-expr-kind x) :vl-cast)
      (equal (vl-expr-kind x) :vl-inside)
      (equal (vl-expr-kind x) :vl-tagged)
      (equal (vl-expr-kind x) :vl-pattern)
      (equal (vl-expr-kind x) :vl-special)
      (equal (vl-expr-kind x) :vl-eventexpr))
  :rule-classes
  ((:forward-chaining :trigger-terms ((vl-expr-kind x)))))