		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-number

Generate Java code to build an ACL2 number.

Signature
(atj-gen-number number) → expr
Arguments: number — Guard (acl2-numberp number).
Returns: expr — Type (jexprp expr).

Definitions and Theorems

Function: atj-gen-number

(defun atj-gen-number (number)
  (declare (xargs :guard (acl2-numberp number)))
  (let ((__function__ 'atj-gen-number))
    (declare (ignorable __function__))
    (b* ((realpart (realpart number))
         (imagpart (imagpart number))
         ((mv realpart-arg imagpart-arg)
          (cond ((and (sbyte32p realpart)
                      (sbyte32p imagpart))
                 (mv (atj-gen-jint realpart)
                     (atj-gen-jint imagpart)))
                ((and (sbyte64p realpart)
                      (sbyte64p imagpart))
                 (mv (atj-gen-jlong realpart)
                     (atj-gen-jlong imagpart)))
                ((and (integerp realpart)
                      (integerp imagpart))
                 (mv (atj-gen-jbigint realpart)
                     (atj-gen-jbigint imagpart)))
                (t (mv (atj-gen-rational realpart)
                       (atj-gen-rational imagpart))))))
      (jexpr-smethod *aij-type-number* "make"
                     (list realpart-arg imagpart-arg)))))

Theorem: jexprp-of-atj-gen-number

(defthm jexprp-of-atj-gen-number
  (b* ((expr (atj-gen-number number)))
    (jexprp expr))
  :rule-classes :rewrite)