		Search-engine friendly clone of the ACL2 documentation.

Atj-code-generation

Atj-gen-test-cunit

Generate the test Java compilation unit.

Signature
(atj-gen-test-cunit deep$ guards$ no-aij-types$ java-package$ java-class$ tests$ verbose$ pkg-class-names fn-method-names wrld) → cunit
Arguments: deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).; no-aij-types$ — Guard (booleanp no-aij-types$).; java-package$ — Guard (maybe-stringp java-package$).; java-class$ — Guard (stringp java-class$).; tests$ — Guard (atj-test-listp tests$).; verbose$ — Guard (booleanp verbose$).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; fn-method-names — Guard (symbol-string-alistp fn-method-names).; wrld — Guard (plist-worldp wrld).
Returns: cunit — Type (jcunitp cunit).

The compilation unit imports all the AIJ public classes, since it needs to reference (at least some of) them. It also imports BigInteger, used to build certain ACL2 value. It also imports Arrays, whose equals() method is used to compare array results. However, if the :no-aij-types input is t, there are no imports.

Definitions and Theorems

Function: atj-gen-test-cunit

(defun atj-gen-test-cunit
       (deep$ guards$ no-aij-types$ java-package$
              java-class$ tests$ verbose$
              pkg-class-names fn-method-names wrld)
 (declare (xargs :guard (and (booleanp deep$)
                             (booleanp guards$)
                             (booleanp no-aij-types$)
                             (maybe-stringp java-package$)
                             (stringp java-class$)
                             (atj-test-listp tests$)
                             (booleanp verbose$)
                             (string-string-alistp pkg-class-names)
                             (symbol-string-alistp fn-method-names)
                             (plist-worldp wrld))))
 (let ((__function__ 'atj-gen-test-cunit))
   (declare (ignorable __function__))
   (b*
    ((class
          (atj-gen-test-class tests$ deep$ guards$
                              no-aij-types$ java-class$ verbose$
                              pkg-class-names fn-method-names wrld))
     (imports
          (if no-aij-types$ (list (jimport nil "java.util.Arrays"))
            (list (jimport nil (str::cat *aij-package* ".*"))
                  (jimport nil "java.math.BigInteger")
                  (jimport nil "java.util.Arrays"))))
     ((run-when verbose$)
      (cw "~%Generate the test Java compilation unit.~%")))
    (make-jcunit :package? java-package$
                 :imports imports
                 :types (list class)))))

Theorem: jcunitp-of-atj-gen-test-cunit

(defthm jcunitp-of-atj-gen-test-cunit
  (b*
   ((cunit
         (atj-gen-test-cunit deep$
                             guards$ no-aij-types$ java-package$
                             java-class$ tests$ verbose$
                             pkg-class-names fn-method-names wrld)))
   (jcunitp cunit))
  :rule-classes :rewrite)