		Search-engine friendly clone of the ACL2 documentation.

Jbinop

Jbinop-kind

Get the kind (tag) of a jbinop structure.

Signature
(jbinop-kind x) → kind
Arguments: x — Guard (jbinopp x).

Definitions and Theorems

Function: jbinop-kind$inline

(defun jbinop-kind$inline (x)
  (declare (xargs :guard (jbinopp x)))
  (let ((__function__ 'jbinop-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) :sshr) :sshr)
                      ((eq (car x) :ushr) :ushr)
                      ((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) :and) :and)
                      ((eq (car x) :xor) :xor)
                      ((eq (car x) :ior) :ior)
                      ((eq (car x) :condand) :condand)
                      ((eq (car x) :condor) :condor)
                      ((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-sshr) :asg-sshr)
                      ((eq (car x) :asg-ushr) :asg-ushr)
                      ((eq (car x) :asg-and) :asg-and)
                      ((eq (car x) :asg-xor) :asg-xor)
                      (t :asg-ior))
         :exec (car x))))

Theorem: jbinop-kind-possibilities

(defthm jbinop-kind-possibilities
  (or (equal (jbinop-kind x) :mul)
      (equal (jbinop-kind x) :div)
      (equal (jbinop-kind x) :rem)
      (equal (jbinop-kind x) :add)
      (equal (jbinop-kind x) :sub)
      (equal (jbinop-kind x) :shl)
      (equal (jbinop-kind x) :sshr)
      (equal (jbinop-kind x) :ushr)
      (equal (jbinop-kind x) :lt)
      (equal (jbinop-kind x) :gt)
      (equal (jbinop-kind x) :le)
      (equal (jbinop-kind x) :ge)
      (equal (jbinop-kind x) :eq)
      (equal (jbinop-kind x) :ne)
      (equal (jbinop-kind x) :and)
      (equal (jbinop-kind x) :xor)
      (equal (jbinop-kind x) :ior)
      (equal (jbinop-kind x) :condand)
      (equal (jbinop-kind x) :condor)
      (equal (jbinop-kind x) :asg)
      (equal (jbinop-kind x) :asg-mul)
      (equal (jbinop-kind x) :asg-div)
      (equal (jbinop-kind x) :asg-rem)
      (equal (jbinop-kind x) :asg-add)
      (equal (jbinop-kind x) :asg-sub)
      (equal (jbinop-kind x) :asg-shl)
      (equal (jbinop-kind x) :asg-sshr)
      (equal (jbinop-kind x) :asg-ushr)
      (equal (jbinop-kind x) :asg-and)
      (equal (jbinop-kind x) :asg-xor)
      (equal (jbinop-kind x) :asg-ior))
  :rule-classes
  ((:forward-chaining :trigger-terms ((jbinop-kind x)))))