		Search-engine friendly clone of the ACL2 documentation.

Jexpr

Jexpr-kind

Get the kind (tag) of a jexpr structure.

Signature
(jexpr-kind x) → kind
Arguments: x — Guard (jexprp x).

Definitions and Theorems

Function: jexpr-kind$inline

(defun jexpr-kind$inline (x)
  (declare (xargs :guard (jexprp x)))
  (let ((__function__ 'jexpr-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :literal))
                       :literal)
                      ((eq (car x) :name) :name)
                      ((eq (car x) :newarray) :newarray)
                      ((eq (car x) :newarray-init)
                       :newarray-init)
                      ((eq (car x) :array) :array)
                      ((eq (car x) :newclass) :newclass)
                      ((eq (car x) :field) :field)
                      ((eq (car x) :method) :method)
                      ((eq (car x) :smethod) :smethod)
                      ((eq (car x) :imethod) :imethod)
                      ((eq (car x) :postinc) :postinc)
                      ((eq (car x) :postdec) :postdec)
                      ((eq (car x) :cast) :cast)
                      ((eq (car x) :unary) :unary)
                      ((eq (car x) :binary) :binary)
                      ((eq (car x) :instanceof) :instanceof)
                      ((eq (car x) :cond) :cond)
                      (t :paren))
         :exec (car x))))

Theorem: jexpr-kind-possibilities

(defthm jexpr-kind-possibilities
  (or (equal (jexpr-kind x) :literal)
      (equal (jexpr-kind x) :name)
      (equal (jexpr-kind x) :newarray)
      (equal (jexpr-kind x) :newarray-init)
      (equal (jexpr-kind x) :array)
      (equal (jexpr-kind x) :newclass)
      (equal (jexpr-kind x) :field)
      (equal (jexpr-kind x) :method)
      (equal (jexpr-kind x) :smethod)
      (equal (jexpr-kind x) :imethod)
      (equal (jexpr-kind x) :postinc)
      (equal (jexpr-kind x) :postdec)
      (equal (jexpr-kind x) :cast)
      (equal (jexpr-kind x) :unary)
      (equal (jexpr-kind x) :binary)
      (equal (jexpr-kind x) :instanceof)
      (equal (jexpr-kind x) :cond)
      (equal (jexpr-kind x) :paren))
  :rule-classes
  ((:forward-chaining :trigger-terms ((jexpr-kind x)))))