		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-main-cunit

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

Signature
(atj-gen-shallow-main-cunit guards$ no-aij-types$ java-package$ java-class$ pkgs fns-to-translate call-graph verbose$ wrld) → (mv cunit pkg-class-names fn-method-names)
Arguments: guards$ — Guard (booleanp guards$).; no-aij-types$ — Guard (booleanp no-aij-types$).; java-package$ — Guard (stringp java-package$).; java-class$ — Guard (stringp java-class$).; pkgs — Guard (string-listp pkgs).; fns-to-translate — Guard (symbol-listp fns-to-translate).; call-graph — Guard (symbol-symbollist-alistp call-graph).; verbose$ — Guard (booleanp verbose$).; wrld — Guard (plist-worldp wrld).
Returns: cunit — Type (jcunitp cunit).; pkg-class-names — Type (string-string-alistp pkg-class-names), given (string-listp pkgs).; fn-method-names — Type (symbol-string-alistp fn-method-names), given (symbol-listp fns-to-translate).

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. However, if the :no-aij-types input is t, there are no imports.

We also return the alist from ACL2 package names to Java class names and the alist from ACL2 function symbols to Java method names, which must be eventually passed to the functions that generate the Java test class.

Definitions and Theorems

Function: atj-gen-shallow-main-cunit

(defun atj-gen-shallow-main-cunit
       (guards$ no-aij-types$ java-package$
                java-class$ pkgs fns-to-translate
                call-graph verbose$ wrld)
 (declare (xargs :guard (and (booleanp guards$)
                             (booleanp no-aij-types$)
                             (stringp java-package$)
                             (stringp java-class$)
                             (string-listp pkgs)
                             (symbol-listp fns-to-translate)
                             (symbol-symbollist-alistp call-graph)
                             (booleanp verbose$)
                             (plist-worldp wrld))))
 (declare (xargs :guard (no-duplicatesp-equal pkgs)))
 (let ((__function__ 'atj-gen-shallow-main-cunit))
  (declare (ignorable __function__))
  (b*
   (((mv class pkg-class-names fn-method-names)
     (atj-gen-shallow-main-class pkgs fns-to-translate
                                 call-graph guards$ no-aij-types$
                                 java-class$ verbose$ wrld))
    (imports
        (if no-aij-types$ nil
          (list (make-jimport :static? nil
                              :target (str::cat *aij-package* ".*"))
                (make-jimport :static? nil
                              :target "java.math.BigInteger"))))
    ((run-when verbose$)
     (cw "~%Generate the main Java compilation unit.~%"))
    (cunit (make-jcunit :package? java-package$
                        :imports imports
                        :types (list class))))
   (mv cunit
       pkg-class-names fn-method-names))))

Theorem: jcunitp-of-atj-gen-shallow-main-cunit.cunit

(defthm jcunitp-of-atj-gen-shallow-main-cunit.cunit
  (b*
   (((mv ?cunit
         ?pkg-class-names ?fn-method-names)
     (atj-gen-shallow-main-cunit guards$ no-aij-types$ java-package$
                                 java-class$ pkgs fns-to-translate
                                 call-graph verbose$ wrld)))
   (jcunitp cunit))
  :rule-classes :rewrite)

Theorem: string-string-alistp-of-atj-gen-shallow-main-cunit.pkg-class-names

(defthm
 string-string-alistp-of-atj-gen-shallow-main-cunit.pkg-class-names
 (implies
  (string-listp pkgs)
  (b*
   (((mv ?cunit
         ?pkg-class-names ?fn-method-names)
     (atj-gen-shallow-main-cunit guards$ no-aij-types$ java-package$
                                 java-class$ pkgs fns-to-translate
                                 call-graph verbose$ wrld)))
   (string-string-alistp pkg-class-names)))
 :rule-classes :rewrite)

Theorem: symbol-string-alistp-of-atj-gen-shallow-main-cunit.fn-method-names

(defthm
 symbol-string-alistp-of-atj-gen-shallow-main-cunit.fn-method-names
 (implies
  (symbol-listp fns-to-translate)
  (b*
   (((mv ?cunit
         ?pkg-class-names ?fn-method-names)
     (atj-gen-shallow-main-cunit guards$ no-aij-types$ java-package$
                                 java-class$ pkgs fns-to-translate
                                 call-graph verbose$ wrld)))
   (symbol-string-alistp fn-method-names)))
 :rule-classes :rewrite)