		Search-engine friendly clone of the ACL2 documentation.

Simpadd0

Simpadd0-filepath

Transform a file path.

Signature
(simpadd0-filepath path) → new-path
Arguments: path — Guard (filepathp path).
Returns: new-path — Type (filepathp new-path).

We only support file paths that consist of strings. We transform the path by interposing .simpadd0 just before the rightmost dot of the file extension, if any; if there is no file extension, we just add .simpadd0 at the end. So for instance a path path/to/file.c becomes path/to/file.simpadd0.c.

Note that this kind of file path transformations supports chaining of transformations, e.g. path/to/file.xform1.xform2.xform3.c.

Definitions and Theorems

Function: simpadd0-filepath

(defun simpadd0-filepath (path)
 (declare (xargs :guard (filepathp path)))
 (let ((__function__ 'simpadd0-filepath))
  (declare (ignorable __function__))
  (b*
   ((string (filepath->unwrap path))
    ((unless (stringp string))
     (raise "Misusage error: file path ~x0 is not a string."
            string)
     (filepath "irrelevant"))
    (chars (acl2::explode string))
    (dot-pos-in-rev (index-of #\. (rev chars)))
    ((when (not dot-pos-in-rev))
     (filepath
        (acl2::implode (append chars (acl2::explode ".simpadd0")))))
    (last-dot-pos (- (len chars) dot-pos-in-rev))
    (new-chars (append (take last-dot-pos chars)
                       (acl2::explode "simpadd0.")
                       (nthcdr last-dot-pos chars)))
    (new-string (acl2::implode new-chars)))
   (filepath new-string))))

Theorem: filepathp-of-simpadd0-filepath

(defthm filepathp-of-simpadd0-filepath
  (b* ((new-path (simpadd0-filepath path)))
    (filepathp new-path))
  :rule-classes :rewrite)

Theorem: simpadd0-filepath-of-filepath-fix-path

(defthm simpadd0-filepath-of-filepath-fix-path
  (equal (simpadd0-filepath (c$::filepath-fix path))
         (simpadd0-filepath path)))

Theorem: simpadd0-filepath-filepath-equiv-congruence-on-path

(defthm simpadd0-filepath-filepath-equiv-congruence-on-path
  (implies (c$::filepath-equiv path path-equiv)
           (equal (simpadd0-filepath path)
                  (simpadd0-filepath path-equiv)))
  :rule-classes :congruence)