		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-env-cunit

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

Signature
(atj-gen-shallow-env-cunit java-package$ java-class$ pkgs verbose$) → cunit
Arguments: java-package$ — Guard (stringp java-package$).; java-class$ — Guard (stringp java-class$).; pkgs — Guard (string-listp pkgs).; verbose$ — Guard (booleanp verbose$).
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 List and ArrayList, used to build the packages' import lists.

Definitions and Theorems

Function: atj-gen-shallow-env-cunit

(defun atj-gen-shallow-env-cunit
       (java-package$ java-class$ pkgs verbose$)
 (declare (xargs :guard (and (stringp java-package$)
                             (stringp java-class$)
                             (string-listp pkgs)
                             (booleanp verbose$))))
 (declare (xargs :guard (no-duplicatesp-equal pkgs)))
 (let ((__function__ 'atj-gen-shallow-env-cunit))
  (declare (ignorable __function__))
  (b*
   ((class (atj-gen-shallow-env-class pkgs java-class$ verbose$))
    ((run-when verbose$)
     (cw
      "~%Generate the Java compilation unit ~
             to build the ACL2 environment.~%")))
   (make-jcunit
        :package? java-package$
        :imports
        (list (make-jimport :static? nil
                            :target (str::cat *aij-package* ".*"))
              (make-jimport :static? nil
                            :target "java.util.ArrayList")
              (make-jimport :static? nil
                            :target "java.util.List"))
        :types (list class)))))

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

(defthm jcunitp-of-atj-gen-shallow-env-cunit
 (b* ((cunit (atj-gen-shallow-env-cunit java-package$
                                        java-class$ pkgs verbose$)))
   (jcunitp cunit))
 :rule-classes :rewrite)