		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-process-output-dir

Process the :output-dir input.

Signature
(atj-process-output-dir output-dir no-aij-types$ java-package$ java-class$ tests$ ctx state) → (mv erp val state)
Arguments: no-aij-types$ — Guard (booleanp no-aij-types$).; java-package$ — Guard (maybe-stringp java-package$).; java-class$ — Guard (stringp java-class$).; tests$ — Guard (atj-test-listp tests$).; ctx — Guard (ctxp ctx).
Returns: val — Type (tuple (output-subdir stringp) (output-file$ stringp) (output-file-env$ maybe-stringp) (output-file-test$ maybe-stringp) val) .

If successful, return the paths for the (sub)directory where the generated files must go, and for the generated main, environment, and test Java files, or nil for files not generated.

Definitions and Theorems

Function: atj-process-output-dir

(defun atj-process-output-dir
       (output-dir no-aij-types$ java-package$
                   java-class$ tests$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp no-aij-types$)
                             (maybe-stringp java-package$)
                             (stringp java-class$)
                             (atj-test-listp tests$)
                             (ctxp ctx))))
 (let ((__function__ 'atj-process-output-dir))
  (declare (ignorable __function__))
  (b*
   ((irrelevant (list "" "" nil nil))
    ((mv erp & state)
     (ensure-value-is-string$ output-dir
                              "The :OUTPUT-DIR input" t nil))
    ((when erp) (mv erp irrelevant state))
    ((mv err-msg exists state)
     (oslib::path-exists-p output-dir))
    ((when err-msg)
     (er-soft+
      ctx t irrelevant
      "The existence of the output directory path ~x0 ~
                   cannot be tested.  ~@1"
      output-dir err-msg))
    ((when (not exists))
     (er-soft+ ctx t irrelevant
               "The output directory path ~x0 does not exist."
               output-dir))
    ((mv err-msg kind state)
     (oslib::file-kind output-dir))
    ((when err-msg)
     (er-soft+
      ctx t irrelevant
      "The kind of the output directory path ~x0 ~
                   cannot be tested.  ~@1"
      output-dir err-msg))
    ((unless (eq kind :directory))
     (er-soft+
      ctx t irrelevant
      "The output directory path ~x0 ~
                   exists but is not a directory."
      output-dir))
    ((mv erp output-subdir state)
     (if java-package$ (atj-process-output-subdir
                            output-dir t
                            (str::strtok! java-package$ (list #\.))
                            ctx state)
       (value (mbe :logic (str-fix output-dir)
                   :exec output-dir))))
    ((when erp) (mv erp irrelevant state))
    (file (oslib::catpath output-subdir
                          (concatenate 'string
                                       java-class$ ".java")))
    ((er &)
     (b*
      (((mv err-msg exists state)
        (oslib::path-exists-p file))
       ((when err-msg)
        (er-soft+
         ctx t irrelevant
         "The existence of the output file path ~x0 ~
                                cannot be tested.  ~@1"
         file err-msg))
       ((when (not exists))
        (value :this-is-irrelevant))
       ((mv err-msg kind state)
        (oslib::file-kind file))
       ((when err-msg)
        (er-soft+
         ctx t irrelevant
         "The kind of the output file path ~x0 ~
                                cannot be tested.  ~@1"
         file err-msg))
       ((when (not (eq kind :regular-file)))
        (er-soft+
         ctx t irrelevant
         "The output file path ~x0 ~
                                exists but is not a regular file."
         file)))
      (value :this-is-irrelevant)))
    (file-env (if no-aij-types$ nil
                (oslib::catpath
                     output-subdir
                     (concatenate 'string
                                  java-class$ "Environment.java"))))
    ((er &)
     (b*
      (((when (null file-env))
        (value :this-is-irrelevant))
       ((mv err-msg exists state)
        (oslib::path-exists-p file-env))
       ((when err-msg)
        (er-soft+
         ctx t irrelevant
         "The existence of the output file path ~x0 ~
                                cannot be tested.  ~@1"
         file-env err-msg))
       ((when (not exists))
        (value :this-is-irrelevant))
       ((mv err-msg kind state)
        (oslib::file-kind file-env))
       ((when err-msg)
        (er-soft+
         ctx t irrelevant
         "The kind of the output file path ~x0 ~
                                cannot be tested.  ~@1"
         file-env err-msg))
       ((when (not (eq kind :regular-file)))
        (er-soft+
         ctx t irrelevant
         "The output file path ~x0 ~
                                exists but is not a regular file."
         file-env)))
      (value :this-is-irrelevant)))
    (file-test
         (if tests$
             (oslib::catpath output-subdir
                             (concatenate 'string
                                          java-class$ "Tests.java"))
           nil))
    ((er &)
     (b*
      (((when (null file-test))
        (value :this-is-irrelevant))
       ((mv err-msg exists state)
        (oslib::path-exists-p file-test))
       ((when err-msg)
        (er-soft+
         ctx t irrelevant
         "The existence of the output file path ~x0 ~
                                cannot be tested.  ~@1"
         file-test err-msg))
       ((when (not exists))
        (value :this-is-irrelevant))
       ((mv err-msg kind state)
        (oslib::file-kind file-test))
       ((when err-msg)
        (er-soft+
         ctx t irrelevant
         "The kind of the output file path ~x0 ~
                                cannot be tested.  ~@1"
         file-test err-msg))
       ((when (not (eq kind :regular-file)))
        (er-soft+
         ctx t irrelevant
         "The output file path ~x0 ~
                                exists but is not a regular file."
         file-test)))
      (value :this-is-irrelevant))))
   (value (list output-subdir
                file file-env file-test)))))

Theorem: return-type-of-atj-process-output-dir.val

(defthm return-type-of-atj-process-output-dir.val
  (b*
    (((mv ?erp ?val acl2::?state)
      (atj-process-output-dir output-dir no-aij-types$ java-package$
                              java-class$ tests$ ctx state)))
    (tuple (output-subdir stringp)
           (output-file$ stringp)
           (output-file-env$ maybe-stringp)
           (output-file-test$ maybe-stringp)
           val))
  :rule-classes :rewrite)