		Search-engine friendly clone of the ACL2 documentation.

Atj-deep-code-generation

Atj-gen-deep-main-cunit

Generate the main Java compilation unit, in the deep embedding approach.

Signature
(atj-gen-deep-main-cunit java-package$ java-class$ verbose$) → cunit
Arguments: java-package$ — Guard (maybe-stringp java-package$).; java-class$ — Guard (stringp java-class$).; 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.

Definitions and Theorems

Function: atj-gen-deep-main-cunit

(defun atj-gen-deep-main-cunit (java-package$ java-class$ verbose$)
 (declare (xargs :guard (and (maybe-stringp java-package$)
                             (stringp java-class$)
                             (booleanp verbose$))))
 (let ((__function__ 'atj-gen-deep-main-cunit))
  (declare (ignorable __function__))
  (b* ((class (atj-gen-deep-main-class java-class$ verbose$))
       ((run-when verbose$)
        (cw "~%Generate the main Java compilation unit.~%")))
    (make-jcunit
         :package? java-package$
         :imports (list (jimport nil (str::cat *aij-package* ".*")))
         :types (list class)))))

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

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