		Search-engine friendly clone of the ACL2 documentation.

Atj-deep-code-generation

Atj-gen-deep-env-cunit

Generate the Java compilation unit with the environment Java class, in the deep embedding approach.

Signature
(atj-gen-deep-env-cunit guards$ java-package$ java-class$ pkgs fns-to-translate verbose$ wrld) → cunit
Arguments: guards$ — Guard (booleanp guards$).; java-package$ — Guard (maybe-stringp java-package$).; java-class$ — Guard (stringp java-class$).; pkgs — Guard (string-listp pkgs).; fns-to-translate — Guard (symbol-listp fns-to-translate).; verbose$ — Guard (booleanp verbose$).; 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 quoted constants. It also imports List and ArrayList, used to build the packages' import lists.

Definitions and Theorems

Function: atj-gen-deep-env-cunit

(defun atj-gen-deep-env-cunit
       (guards$ java-package$ java-class$
                pkgs fns-to-translate verbose$ wrld)
 (declare (xargs :guard (and (booleanp guards$)
                             (maybe-stringp java-package$)
                             (stringp java-class$)
                             (string-listp pkgs)
                             (symbol-listp fns-to-translate)
                             (booleanp verbose$)
                             (plist-worldp wrld))))
 (let ((__function__ 'atj-gen-deep-env-cunit))
  (declare (ignorable __function__))
  (b*
   ((class
         (atj-gen-deep-env-class pkgs fns-to-translate
                                 guards$ java-class$ verbose$ wrld))
    ((run-when verbose$)
     (cw
      "~%Generate the Java compilation unit ~
             to build the ACL2 environment.~%")))
   (make-jcunit
        :package? java-package$
        :imports (list (jimport nil (str::cat *aij-package* ".*"))
                       (jimport nil "java.math.BigInteger")
                       (jimport nil "java.util.ArrayList")
                       (jimport nil "java.util.List"))
        :types (list class)))))

Theorem: jcunitp-of-atj-gen-deep-env-cunit

(defthm jcunitp-of-atj-gen-deep-env-cunit
 (b*
  ((cunit
      (atj-gen-deep-env-cunit guards$ java-package$ java-class$
                              pkgs fns-to-translate verbose$ wrld)))
  (jcunitp cunit))
 :rule-classes :rewrite)