		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-integer

Generate Java code to build an ACL2 integer.

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

If the ACL2 integer is representable as a Java integer, we generate a Java integer literal. Otherwise, if it is representable as a Java long integer, we generate a Java long integer literal. Otherwise, we generate a Java big integer built out of the string representation of the ACL2 integer.

These are passed to the Acl2Integer.make. However, if the integer is 0 or 1, we simply generate a reference to the respective Java static final fields in the Acl2Integer class.

Definitions and Theorems

Function: atj-gen-integer

(defun atj-gen-integer (integer)
  (declare (xargs :guard (integerp integer)))
  (let ((__function__ 'atj-gen-integer))
    (declare (ignorable __function__))
    (b* ((arg (cond ((sbyte32p integer)
                     (atj-gen-jint integer))
                    ((sbyte64p integer)
                     (atj-gen-jlong integer))
                    (t (atj-gen-jbigint integer)))))
      (jexpr-smethod *aij-type-int* "make" (list arg)))))

Theorem: jexprp-of-atj-gen-integer

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