		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-process-path

Process the :path input.

Signature
(input-files-process-path path) → (mv erp new-path)
Returns: new-path — Type (stringp new-path).

If the string is not / but ends with /, we remove the ending /. This is for uniformity when concatenating this with the files specified in the :files input.

Definitions and Theorems

Function: input-files-process-path

(defun input-files-process-path (path)
 (declare (xargs :guard t))
 (let ((__function__ 'input-files-process-path))
  (declare (ignorable __function__))
  (b*
   (((reterr) "")
    ((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-input-files-process-path.new-path

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