		Search-engine friendly clone of the ACL2 documentation.

Expr

Expr-kind

Get the kind (tag) of a expr structure.

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

Definitions and Theorems

Function: expr-kind$inline

(defun expr-kind$inline (x)
  (declare (xargs :guard (exprp x)))
  (mbe :logic (cond ((or (atom x) (eq (car x) :ident))
                     :ident)
                    ((eq (car x) :const) :const)
                    ((eq (car x) :string) :string)
                    ((eq (car x) :paren) :paren)
                    ((eq (car x) :gensel) :gensel)
                    ((eq (car x) :arrsub) :arrsub)
                    ((eq (car x) :funcall) :funcall)
                    ((eq (car x) :member) :member)
                    ((eq (car x) :memberp) :memberp)
                    ((eq (car x) :complit) :complit)
                    ((eq (car x) :unary) :unary)
                    ((eq (car x) :label-addr) :label-addr)
                    ((eq (car x) :sizeof) :sizeof)
                    ((eq (car x) :sizeof-ambig)
                     :sizeof-ambig)
                    ((eq (car x) :alignof) :alignof)
                    ((eq (car x) :alignof-ambig)
                     :alignof-ambig)
                    ((eq (car x) :cast) :cast)
                    ((eq (car x) :binary) :binary)
                    ((eq (car x) :cond) :cond)
                    ((eq (car x) :comma) :comma)
                    ((eq (car x) :cast/call-ambig)
                     :cast/call-ambig)
                    ((eq (car x) :cast/mul-ambig)
                     :cast/mul-ambig)
                    ((eq (car x) :cast/add-ambig)
                     :cast/add-ambig)
                    ((eq (car x) :cast/sub-ambig)
                     :cast/sub-ambig)
                    ((eq (car x) :cast/and-ambig)
                     :cast/and-ambig)
                    ((eq (car x) :cast/logand-ambig)
                     :cast/logand-ambig)
                    ((eq (car x) :stmt) :stmt)
                    ((eq (car x) :tycompat) :tycompat)
                    ((eq (car x) :offsetof) :offsetof)
                    ((eq (car x) :va-arg) :va-arg)
                    (t :extension))
       :exec (car x)))

Theorem: expr-kind-possibilities

(defthm expr-kind-possibilities
 (or (equal (expr-kind x) :ident)
     (equal (expr-kind x) :const)
     (equal (expr-kind x) :string)
     (equal (expr-kind x) :paren)
     (equal (expr-kind x) :gensel)
     (equal (expr-kind x) :arrsub)
     (equal (expr-kind x) :funcall)
     (equal (expr-kind x) :member)
     (equal (expr-kind x) :memberp)
     (equal (expr-kind x) :complit)
     (equal (expr-kind x) :unary)
     (equal (expr-kind x) :label-addr)
     (equal (expr-kind x) :sizeof)
     (equal (expr-kind x) :sizeof-ambig)
     (equal (expr-kind x) :alignof)
     (equal (expr-kind x) :alignof-ambig)
     (equal (expr-kind x) :cast)
     (equal (expr-kind x) :binary)
     (equal (expr-kind x) :cond)
     (equal (expr-kind x) :comma)
     (equal (expr-kind x) :cast/call-ambig)
     (equal (expr-kind x) :cast/mul-ambig)
     (equal (expr-kind x) :cast/add-ambig)
     (equal (expr-kind x) :cast/sub-ambig)
     (equal (expr-kind x) :cast/and-ambig)
     (equal (expr-kind x) :cast/logand-ambig)
     (equal (expr-kind x) :stmt)
     (equal (expr-kind x) :tycompat)
     (equal (expr-kind x) :offsetof)
     (equal (expr-kind x) :va-arg)
     (equal (expr-kind x) :extension))
 :rule-classes ((:forward-chaining :trigger-terms ((expr-kind x)))))