Process the subdirectories specified by
the
(atj-process-output-subdir current-subdir current-exists next-subdirs ctx state) → (mv erp final-dir state)
This is part of the processing of
Here we ensure that the subdirectories in the sequence either exists and are directories, or do not exist. It is allowed for no subdirectory to exist, or for some initial prefix to exist, or for all of them to exist; any non-existing subdirectories will be created just before generating the Java files.
This ACL2 function recursively checks the subdirectories.
The
Function:
(defun atj-process-output-subdir (current-subdir current-exists next-subdirs ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (stringp current-subdir) (booleanp current-exists) (string-listp next-subdirs) (ctxp ctx)))) (let ((__function__ 'atj-process-output-subdir)) (declare (ignorable __function__)) (b* (((when (endp next-subdirs)) (value (mbe :logic (str-fix current-subdir) :exec current-subdir))) (current-subdir (oslib::catpath current-subdir (car next-subdirs))) ((when current-exists) (atj-process-output-subdir current-subdir current-exists (cdr next-subdirs) ctx state)) ((mv err-msg exists state) (oslib::path-exists-p current-subdir)) ((when err-msg) (er-soft+ ctx t "" "The existence of the output subdirectory path ~x0 ~ cannot be tested. ~@1" current-subdir err-msg)) ((when (not exists)) (atj-process-output-subdir current-subdir t (cdr next-subdirs) ctx state)) ((mv err-msg kind state) (oslib::file-kind current-subdir)) ((when err-msg) (er-soft+ ctx t "" "The kind of the output subdirectory path ~x0 ~ cannot be tested. ~@1." current-subdir err-msg)) ((unless (eq kind :directory)) (er-soft+ ctx t "" "The output subdirectory path ~x0 ~ exists but is not a directory." current-subdir))) (atj-process-output-subdir current-subdir nil (cdr next-subdirs) ctx state))))
Theorem:
(defthm stringp-of-atj-process-output-subdir.final-dir (b* (((mv ?erp ?final-dir acl2::?state) (atj-process-output-subdir current-subdir current-exists next-subdirs ctx state))) (stringp final-dir)) :rule-classes :rewrite)