		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-process-output-subdir

Process the subdirectories specified by the :output-dir and :java-package inputs.

Signature
(atj-process-output-subdir current-subdir current-exists next-subdirs ctx state) → (mv erp final-dir state)
Arguments: current-subdir — Guard (stringp current-subdir).; current-exists — Guard (booleanp current-exists).; next-subdirs — Guard (string-listp next-subdirs).; ctx — Guard (ctxp ctx).
Returns: final-dir — Type (stringp final-dir).

This is part of the processing of :output-dir. As explained in the user documentation, if :java-package is not nil, the Java files are generated in a subdirectory of the directory specified by :output-dir, corresponding to the identifiers that form the Java package name.

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 current-subdir parameter is the path consisting of the :output-dir directory plus the subdirectories examined so far; its initial value is :output-dir. The current-exists parameter says whether the current-subdir exists or not; its initial value is t. The next-subdirs parameter contains the remaining subdirectories to examine; its initial value is the list of identifiers that form the Java package name. As soon as a subdirectory is encountered that does not exist, the current-exists is set to nil, and it stays that way. In any case eventually the final subdirectory path, starting with :output-dir, is returned.

Definitions and Theorems

Function: atj-process-output-subdir

(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: stringp-of-atj-process-output-subdir.final-dir

(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)