		Search-engine friendly clone of the ACL2 documentation.

Atc-input-processing

Atc-process-output-dir

Process the :output-dir input.

Signature
(atc-process-output-dir options state) → (mv erp output-dir state)
Arguments: options — Guard (symbol-alistp options).
Returns: output-dir — Type (stringp output-dir).

If successful, return the input itself, with a guaranteed stringp type.

Definitions and Theorems

Function: atc-process-output-dir

(defun atc-process-output-dir (options state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (symbol-alistp options)))
 (let ((__function__ 'atc-process-output-dir))
  (declare (ignorable __function__))
  (b*
   (((reterr) "" state)
    (output-dir-option (assoc-eq :output-dir options))
    (output-dir (if output-dir-option (cdr output-dir-option)
                  "."))
    ((unless (stringp output-dir))
     (reterr
      (msg
       "The :OUTPUT-DIR input must be a string, ~
                      but ~x0 is not a string."
       output-dir)))
    ((mv msg? kind state)
     (oslib::file-kind output-dir))
    ((when msg?)
     (reterr
      (msg
       "The kind of ~
                                  the output directory path ~x0 ~
                                  cannot be tested.  ~
                                  ~@1"
       output-dir msg?)))
    ((unless (eq kind :directory))
     (reterr
      (msg
       "The output directory path ~x0 ~
                      is not a directory; it has kind ~x1 instead."
       output-dir kind))))
   (retok output-dir state))))

Theorem: stringp-of-atc-process-output-dir.output-dir

(defthm stringp-of-atc-process-output-dir.output-dir
  (b* (((mv acl2::?erp ?output-dir acl2::?state)
        (atc-process-output-dir options state)))
    (stringp output-dir))
  :rule-classes :rewrite)