		Search-engine friendly clone of the ACL2 documentation.

Atj-code-generation

Atj-gen-main-file

Generate the main Java file.

Signature
(atj-gen-main-file deep$ guards$ no-aij-types$ java-package$ java-class$ output-file$ pkgs fns-to-translate call-graph verbose$ state) → (mv pkg-class-names fn-method-names state)
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$).; output-file$ — Guard (stringp output-file$).; 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$).
Returns: pkg-class-names — A string-string-alistp.; fn-method-names — A symbol-string-alistp.

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. These are nil in the deep embedding approach; they are only used in the shallow embedding approach.

Definitions and Theorems

Function: atj-gen-main-file

(defun atj-gen-main-file
       (deep$ guards$
              no-aij-types$ java-package$ java-class$
              output-file$ pkgs fns-to-translate
              call-graph verbose$ state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp deep$)
                             (booleanp guards$)
                             (booleanp no-aij-types$)
                             (maybe-stringp java-package$)
                             (stringp java-class$)
                             (stringp output-file$)
                             (string-listp pkgs)
                             (symbol-listp fns-to-translate)
                             (symbol-symbollist-alistp call-graph)
                             (booleanp verbose$))))
 (let ((__function__ 'atj-gen-main-file))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((mv cunit pkg-class-names fn-method-names)
     (if deep$
      (mv
        (atj-gen-deep-main-cunit java-package$ java-class$ verbose$)
        nil nil)
      (atj-gen-shallow-main-cunit
           guards$ no-aij-types$ java-package$
           java-class$ pkgs fns-to-translate
           call-graph verbose$ wrld)))
    ((unless (jcunitp cunit))
     (raise
          "Internal error: generated an invalid compilation unit.")
     (mv nil nil state))
    ((run-when verbose$)
     (cw "~%Generate the main Java file.~%"))
    (state (print-to-jfile (print-jcunit cunit)
                           output-file$ state)))
   (mv pkg-class-names
       fn-method-names state))))