		Search-engine friendly clone of the ACL2 documentation.

Atj-code-generation

Atj-gen-output-subdir

Generate the output subdirectory where the Java files go, if needed.

Signature
(atj-gen-output-subdir output-subdir java-package$ ctx state) → (mv erp _ state)
Arguments: output-subdir — Guard (stringp output-subdir).; java-package$ — Guard (maybe-stringp java-package$).; ctx — Guard (ctxp ctx).
Returns: _ — Type (null _).

If the subdirectory is the same as :output-dir, which happens when there is no named Java package, no subdirectories need to be generated.

Definitions and Theorems

Function: atj-gen-output-subdir

(defun atj-gen-output-subdir (output-subdir java-package$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (stringp output-subdir)
                             (maybe-stringp java-package$)
                             (ctxp ctx))))
 (let ((__function__ 'atj-gen-output-subdir))
  (declare (ignorable __function__))
  (b*
   (((when (not java-package$)) (value nil))
    ((mv successp state)
     (oslib::mkdir output-subdir))
    ((unless successp)
     (er-soft+ ctx t nil
               "The creation of the output subdirectory ~x0 failed."
               output-subdir)))
   (value nil))))

Theorem: null-of-atj-gen-output-subdir._

(defthm null-of-atj-gen-output-subdir._
  (b*
   (((mv ?erp ?_ acl2::?state)
     (atj-gen-output-subdir output-subdir java-package$ ctx state)))
   (null _))
  :rule-classes :rewrite)