		Search-engine friendly clone of the ACL2 documentation.

Statement

Statement-kind

Get the kind (tag) of a statement structure.

Signature
(statement-kind x) → kind
Arguments: x — Guard (statementp x).

Definitions and Theorems

Function: statement-kind$inline

(defun statement-kind$inline (x)
  (declare (xargs :guard (statementp x)))
  (let ((__function__ 'statement-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((eq (car x) :block) :block)
                      ((or (atom x)
                           (eq (car x) :variable-single))
                       :variable-single)
                      ((eq (car x) :variable-multi)
                       :variable-multi)
                      ((eq (car x) :assign-single)
                       :assign-single)
                      ((eq (car x) :assign-multi)
                       :assign-multi)
                      ((eq (car x) :funcall) :funcall)
                      ((eq (car x) :if) :if)
                      ((eq (car x) :for) :for)
                      ((eq (car x) :switch) :switch)
                      ((eq (car x) :leave) :leave)
                      ((eq (car x) :break) :break)
                      ((eq (car x) :continue) :continue)
                      (t :fundef))
         :exec (car x))))

Theorem: statement-kind-possibilities

(defthm statement-kind-possibilities
  (or (equal (statement-kind x) :block)
      (equal (statement-kind x)
             :variable-single)
      (equal (statement-kind x)
             :variable-multi)
      (equal (statement-kind x)
             :assign-single)
      (equal (statement-kind x) :assign-multi)
      (equal (statement-kind x) :funcall)
      (equal (statement-kind x) :if)
      (equal (statement-kind x) :for)
      (equal (statement-kind x) :switch)
      (equal (statement-kind x) :leave)
      (equal (statement-kind x) :break)
      (equal (statement-kind x) :continue)
      (equal (statement-kind x) :fundef))
  :rule-classes
  ((:forward-chaining :trigger-terms ((statement-kind x)))))