		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-rational

Generate Java code to build an ACL2 rational.

Signature
(atj-gen-rational rational) → expr
Arguments: rational — Guard (rationalp rational).
Returns: expr — Type (jexprp expr).

Definitions and Theorems

Function: atj-gen-rational

(defun atj-gen-rational (rational)
  (declare (xargs :guard (rationalp rational)))
  (let ((__function__ 'atj-gen-rational))
    (declare (ignorable __function__))
    (b* ((numerator (numerator rational))
         (denominator (denominator rational))
         ((mv numerator-arg denominator-arg)
          (cond ((and (sbyte32p numerator)
                      (sbyte32p denominator))
                 (mv (atj-gen-jint numerator)
                     (atj-gen-jint denominator)))
                ((and (sbyte64p numerator)
                      (sbyte64p denominator))
                 (mv (atj-gen-jlong numerator)
                     (atj-gen-jlong denominator)))
                (t (mv (atj-gen-jbigint numerator)
                       (atj-gen-jbigint denominator))))))
      (jexpr-smethod *aij-type-rational* "make"
                     (list numerator-arg denominator-arg)))))

Theorem: jexprp-of-atj-gen-rational

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