		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-jlong-array

Generate Java code to build a Java long array.

Signature
(atj-gen-jlong-array long-array) → expr
Arguments: long-array — Guard (long-arrayp long-array).
Returns: expr — Type (jexprp expr).

Definitions and Theorems

Function: atj-gen-jlong-array-aux

(defun atj-gen-jlong-array-aux (longs)
  (declare (xargs :guard (long-value-listp longs)))
  (let ((__function__ 'atj-gen-jlong-array-aux))
    (declare (ignorable __function__))
    (cond ((endp longs) nil)
          (t (cons (atj-gen-jlong (long-value->int (car longs)))
                   (atj-gen-jlong-array-aux (cdr longs)))))))

Theorem: jexpr-listp-of-atj-gen-jlong-array-aux

(defthm jexpr-listp-of-atj-gen-jlong-array-aux
  (b* ((exprs (atj-gen-jlong-array-aux longs)))
    (jexpr-listp exprs))
  :rule-classes :rewrite)

Function: atj-gen-jlong-array

(defun atj-gen-jlong-array (long-array)
 (declare (xargs :guard (long-arrayp long-array)))
 (let ((__function__ 'atj-gen-jlong-array))
  (declare (ignorable __function__))
  (jexpr-newarray-init
    (jtype-long)
    (atj-gen-jlong-array-aux (long-array->components long-array)))))

Theorem: jexprp-of-atj-gen-jlong-array

(defthm jexprp-of-atj-gen-jlong-array
  (b* ((expr (atj-gen-jlong-array long-array)))
    (jexprp expr))
  :rule-classes :rewrite)