		Search-engine friendly clone of the ACL2 documentation.

Atj-implementation

Atj-fn

Process the inputs and generate the Java file(s).

Signature
(atj-fn args ctx state) → (mv erp result state)
Arguments: args — Guard (true-listp args).; ctx — Guard (ctxp ctx).
Returns: result — Always (value-triple :invisible).

Since the result of this function is passed to make-event, this function must return an event form. By returning (value-triple :invisible), no return value is printed on the screen. A message of successful completion is printed, regardless of :verbose.

Definitions and Theorems

Function: atj-fn

(defun atj-fn (args ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (true-listp args) (ctxp ctx))))
  (let ((__function__ 'atj-fn))
    (declare (ignorable __function__))
    (b* (((er (list fns-to-translate call-graph
                    pkgs deep$ guards$ no-aij-types$
                    java-package$ java-class$ output-subdir
                    output-file$ output-file-env$
                    output-file-test$ tests$ verbose$))
          (atj-process-inputs args ctx state))
         ((er &)
          (atj-gen-everything deep$
                              guards$ no-aij-types$ java-package$
                              java-class$ output-subdir output-file$
                              output-file-env$ output-file-test$
                              tests$ pkgs fns-to-translate
                              call-graph verbose$ ctx state))
         (- (if output-file-test$
                (cw "~%Generated Java files:~% ~s0~% ~s1~% ~s2~%"
                    output-file$
                    output-file-env$ output-file-test$)
              (cw "~%Generated Java files:~% ~s0~% ~s1~%"
                  output-file$ output-file-env$))))
      (value '(value-triple :invisible)))))