Process the
(atj-process-output-dir output-dir no-aij-types$ java-package$ java-class$ tests$ ctx state) → (mv erp val state)
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
Function:
(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:
(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)