		Search-engine friendly clone of the ACL2 documentation.

Output-files-implementation

Output-files-process-path

Process the :path input.

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

Definitions and Theorems

Function: output-files-process-path

(defun output-files-process-path (options)
 (declare (xargs :guard (symbol-alistp options)))
 (let ((__function__ 'output-files-process-path))
  (declare (ignorable __function__))
  (b*
   (((reterr) "")
    (path-option (assoc-eq :path options))
    (path (if path-option (cdr path-option) "."))
    ((unless (stringp path))
     (reterr
      (msg
       "The :PATH input must be a string, ~
                      but it is ~x0 instead."
       path)))
    (path-chars (acl2::explode path))
    ((unless (consp path-chars))
     (reterr
      (msg
       "The :PATH input must be not empty, ~
                      but it is the empty string instead.")))
    (path-chars (if (and (consp (cdr path-chars))
                         (eql (car (last path-chars)) #\/))
                    (butlast path-chars 1)
                  path-chars))
    (path (acl2::implode path-chars)))
   (retok path))))

Theorem: stringp-of-output-files-process-path.path

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