		Search-engine friendly clone of the ACL2 documentation.

Binop

Binop-kind

Get the kind (tag) of a binop structure.

Signature
(binop-kind x) → kind
Arguments: x — Guard (binopp x).

Definitions and Theorems

Function: binop-kind$inline

(defun binop-kind$inline (x)
  (declare (xargs :guard (binopp x)))
  (let ((__function__ 'binop-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :mul)) :mul)
                      ((eq (car x) :div) :div)
                      ((eq (car x) :rem) :rem)
                      ((eq (car x) :add) :add)
                      ((eq (car x) :sub) :sub)
                      ((eq (car x) :shl) :shl)
                      ((eq (car x) :shr) :shr)
                      ((eq (car x) :lt) :lt)
                      ((eq (car x) :gt) :gt)
                      ((eq (car x) :le) :le)
                      ((eq (car x) :ge) :ge)
                      ((eq (car x) :eq) :eq)
                      ((eq (car x) :ne) :ne)
                      ((eq (car x) :bitand) :bitand)
                      ((eq (car x) :bitxor) :bitxor)
                      ((eq (car x) :bitior) :bitior)
                      ((eq (car x) :logand) :logand)
                      ((eq (car x) :logor) :logor)
                      ((eq (car x) :asg) :asg)
                      ((eq (car x) :asg-mul) :asg-mul)
                      ((eq (car x) :asg-div) :asg-div)
                      ((eq (car x) :asg-rem) :asg-rem)
                      ((eq (car x) :asg-add) :asg-add)
                      ((eq (car x) :asg-sub) :asg-sub)
                      ((eq (car x) :asg-shl) :asg-shl)
                      ((eq (car x) :asg-shr) :asg-shr)
                      ((eq (car x) :asg-and) :asg-and)
                      ((eq (car x) :asg-xor) :asg-xor)
                      (t :asg-ior))
         :exec (car x))))

Theorem: binop-kind-possibilities

(defthm binop-kind-possibilities
  (or (equal (binop-kind x) :mul)
      (equal (binop-kind x) :div)
      (equal (binop-kind x) :rem)
      (equal (binop-kind x) :add)
      (equal (binop-kind x) :sub)
      (equal (binop-kind x) :shl)
      (equal (binop-kind x) :shr)
      (equal (binop-kind x) :lt)
      (equal (binop-kind x) :gt)
      (equal (binop-kind x) :le)
      (equal (binop-kind x) :ge)
      (equal (binop-kind x) :eq)
      (equal (binop-kind x) :ne)
      (equal (binop-kind x) :bitand)
      (equal (binop-kind x) :bitxor)
      (equal (binop-kind x) :bitior)
      (equal (binop-kind x) :logand)
      (equal (binop-kind x) :logor)
      (equal (binop-kind x) :asg)
      (equal (binop-kind x) :asg-mul)
      (equal (binop-kind x) :asg-div)
      (equal (binop-kind x) :asg-rem)
      (equal (binop-kind x) :asg-add)
      (equal (binop-kind x) :asg-sub)
      (equal (binop-kind x) :asg-shl)
      (equal (binop-kind x) :asg-shr)
      (equal (binop-kind x) :asg-and)
      (equal (binop-kind x) :asg-xor)
      (equal (binop-kind x) :asg-ior))
  :rule-classes
  ((:forward-chaining :trigger-terms ((binop-kind x)))))