|
|
|---|
|
|
|
|---|
Get the kind (tag) of a expression structure.
(expression-kind x) → kind
Function:
(defun expression-kind$inline (x) (declare (xargs :guard (expressionp x))) (let ((__function__ 'expression-kind)) (declare (ignorable __function__)) (mbe :logic (cond ((or (atom x) (eq (car x) :literal)) :literal) ((eq (car x) :var/const) :var/const) ((eq (car x) :assoc-const) :assoc-const) ((eq (car x) :unary) :unary) ((eq (car x) :binary) :binary) ((eq (car x) :cond) :cond) ((eq (car x) :unit) :unit) ((eq (car x) :tuple) :tuple) ((eq (car x) :tuple-component) :tuple-component) ((eq (car x) :struct) :struct) ((eq (car x) :struct-component) :struct-component) ((eq (car x) :internal-call) :internal-call) ((eq (car x) :external-call) :external-call) (t :static-call)) :exec (car x))))
Theorem:
(defthm expression-kind-possibilities (or (equal (expression-kind x) :literal) (equal (expression-kind x) :var/const) (equal (expression-kind x) :assoc-const) (equal (expression-kind x) :unary) (equal (expression-kind x) :binary) (equal (expression-kind x) :cond) (equal (expression-kind x) :unit) (equal (expression-kind x) :tuple) (equal (expression-kind x) :tuple-component) (equal (expression-kind x) :struct) (equal (expression-kind x) :struct-component) (equal (expression-kind x) :internal-call) (equal (expression-kind x) :external-call) (equal (expression-kind x) :static-call)) :rule-classes ((:forward-chaining :trigger-terms ((expression-kind x)))))