		Search-engine friendly clone of the ACL2 documentation.

Vl-stmt

Vl-stmt-kind

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

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

Definitions and Theorems

Function: vl-stmt-kind$inline

(defun vl-stmt-kind$inline (x)
  (declare (xargs :guard (vl-stmt-p x)))
  (let ((__function__ 'vl-stmt-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :vl-nullstmt))
                       :vl-nullstmt)
                      ((eq (car x) :vl-assignstmt)
                       :vl-assignstmt)
                      ((eq (car x) :vl-deassignstmt)
                       :vl-deassignstmt)
                      ((eq (car x) :vl-callstmt) :vl-callstmt)
                      ((eq (car x) :vl-disablestmt)
                       :vl-disablestmt)
                      ((eq (car x) :vl-eventtriggerstmt)
                       :vl-eventtriggerstmt)
                      ((eq (car x) :vl-casestmt) :vl-casestmt)
                      ((eq (car x) :vl-ifstmt) :vl-ifstmt)
                      ((eq (car x) :vl-foreverstmt)
                       :vl-foreverstmt)
                      ((eq (car x) :vl-waitstmt) :vl-waitstmt)
                      ((eq (car x) :vl-repeatstmt)
                       :vl-repeatstmt)
                      ((eq (car x) :vl-whilestmt)
                       :vl-whilestmt)
                      ((eq (car x) :vl-dostmt) :vl-dostmt)
                      ((eq (car x) :vl-forstmt) :vl-forstmt)
                      ((eq (car x) :vl-foreachstmt)
                       :vl-foreachstmt)
                      ((eq (car x) :vl-breakstmt)
                       :vl-breakstmt)
                      ((eq (car x) :vl-continuestmt)
                       :vl-continuestmt)
                      ((eq (car x) :vl-blockstmt)
                       :vl-blockstmt)
                      ((eq (car x) :vl-timingstmt)
                       :vl-timingstmt)
                      ((eq (car x) :vl-returnstmt)
                       :vl-returnstmt)
                      ((eq (car x) :vl-assertstmt)
                       :vl-assertstmt)
                      (t :vl-cassertstmt))
         :exec (car x))))

Theorem: vl-stmt-kind-possibilities

(defthm vl-stmt-kind-possibilities
  (or (equal (vl-stmt-kind x) :vl-nullstmt)
      (equal (vl-stmt-kind x) :vl-assignstmt)
      (equal (vl-stmt-kind x)
             :vl-deassignstmt)
      (equal (vl-stmt-kind x) :vl-callstmt)
      (equal (vl-stmt-kind x) :vl-disablestmt)
      (equal (vl-stmt-kind x)
             :vl-eventtriggerstmt)
      (equal (vl-stmt-kind x) :vl-casestmt)
      (equal (vl-stmt-kind x) :vl-ifstmt)
      (equal (vl-stmt-kind x) :vl-foreverstmt)
      (equal (vl-stmt-kind x) :vl-waitstmt)
      (equal (vl-stmt-kind x) :vl-repeatstmt)
      (equal (vl-stmt-kind x) :vl-whilestmt)
      (equal (vl-stmt-kind x) :vl-dostmt)
      (equal (vl-stmt-kind x) :vl-forstmt)
      (equal (vl-stmt-kind x) :vl-foreachstmt)
      (equal (vl-stmt-kind x) :vl-breakstmt)
      (equal (vl-stmt-kind x)
             :vl-continuestmt)
      (equal (vl-stmt-kind x) :vl-blockstmt)
      (equal (vl-stmt-kind x) :vl-timingstmt)
      (equal (vl-stmt-kind x) :vl-returnstmt)
      (equal (vl-stmt-kind x) :vl-assertstmt)
      (equal (vl-stmt-kind x)
             :vl-cassertstmt))
  :rule-classes
  ((:forward-chaining :trigger-terms ((vl-stmt-kind x)))))