		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-jprim-binop-fn-to-jbinop

Map an ACL2 function that models a Java primitive binary operation to the corresponding binary operator in the Java abstract syntax.

Signature
(atj-jprim-binop-fn-to-jbinop fn) → binop
Arguments: fn — Guard (atj-jprim-binop-fn-p fn).
Returns: binop — Type (jbinopp binop).

Definitions and Theorems

Function: atj-jprim-binop-fn-to-jbinop

(defun atj-jprim-binop-fn-to-jbinop (fn)
  (declare (xargs :guard (atj-jprim-binop-fn-p fn)))
  (let ((__function__ 'atj-jprim-binop-fn-to-jbinop))
    (declare (ignorable __function__))
    (case fn
      (boolean-and (jbinop-and))
      (boolean-xor (jbinop-xor))
      (boolean-ior (jbinop-ior))
      (boolean-eq (jbinop-eq))
      (boolean-neq (jbinop-ne))
      (int-add (jbinop-add))
      (long-add (jbinop-add))
      (int-sub (jbinop-sub))
      (long-sub (jbinop-sub))
      (int-mul (jbinop-mul))
      (long-mul (jbinop-mul))
      (int-div (jbinop-div))
      (long-div (jbinop-div))
      (int-rem (jbinop-rem))
      (long-rem (jbinop-rem))
      (int-and (jbinop-and))
      (long-and (jbinop-and))
      (int-xor (jbinop-xor))
      (long-xor (jbinop-xor))
      (int-ior (jbinop-ior))
      (long-ior (jbinop-ior))
      (int-eq (jbinop-eq))
      (long-eq (jbinop-eq))
      (int-neq (jbinop-ne))
      (long-neq (jbinop-ne))
      (int-less (jbinop-lt))
      (long-less (jbinop-lt))
      (int-lesseq (jbinop-le))
      (long-lesseq (jbinop-le))
      (int-great (jbinop-gt))
      (long-great (jbinop-gt))
      (int-greateq (jbinop-ge))
      (long-greateq (jbinop-ge))
      (int-int-shiftl (jbinop-shl))
      (long-long-shiftl (jbinop-shl))
      (long-int-shiftl (jbinop-shl))
      (int-long-shiftl (jbinop-shl))
      (int-int-shiftr (jbinop-sshr))
      (long-long-shiftr (jbinop-sshr))
      (long-int-shiftr (jbinop-sshr))
      (int-long-shiftr (jbinop-sshr))
      (int-int-ushiftr (jbinop-ushr))
      (long-long-ushiftr (jbinop-ushr))
      (long-int-ushiftr (jbinop-ushr))
      (int-long-ushiftr (jbinop-ushr))
      (float-add (jbinop-add))
      (double-add (jbinop-add))
      (float-sub (jbinop-sub))
      (double-sub (jbinop-sub))
      (float-mul (jbinop-mul))
      (double-mul (jbinop-mul))
      (float-div (jbinop-div))
      (double-div (jbinop-div))
      (float-rem (jbinop-rem))
      (double-rem (jbinop-rem))
      (float-eq (jbinop-eq))
      (double-eq (jbinop-eq))
      (float-neq (jbinop-ne))
      (double-neq (jbinop-ne))
      (float-less (jbinop-lt))
      (double-less (jbinop-lt))
      (float-lesseq (jbinop-le))
      (double-lesseq (jbinop-le))
      (float-great (jbinop-gt))
      (double-great (jbinop-gt))
      (float-greateq (jbinop-ge))
      (double-greateq (jbinop-ge))
      (t (prog2$ (impossible)
                 (ec-call (jbinop-fix :irrelevant)))))))

Theorem: jbinopp-of-atj-jprim-binop-fn-to-jbinop

(defthm jbinopp-of-atj-jprim-binop-fn-to-jbinop
  (b* ((binop (atj-jprim-binop-fn-to-jbinop fn)))
    (jbinopp binop))
  :rule-classes :rewrite)