Catpath
Basic concatenation operation for paths.
- Signature
(catpath basedir filename) → path
- Arguments
- basedir — Directory whose name should be extended, which may
or may not end with a slash. Idioms like ~,
~jared, and .. will be preserved. The
empty string means the current directory.
Guard (stringp basedir).
- filename — File or subdirectory name to append to basedir.
Guard (stringp filename).
- Returns
- path — A new string like basedir/filename. We only insert a
slash if basedir does not end with a slash. We don't
normalize the path by collapsing ...
Type (stringp path).
ACL2 includes a built-in function named extend-pathname that
is similar to catpath. In some ways ACL2's version is nicer than
catpath. It sometimes cleans up the path and gets rid of ..
characters. But it also sometimes expands away symlinks, which you may not
want to do. At the time of this writing, extend-pathname is not easy to
effectively bring into logic mode, but that may change in the future.
Our catpath function is comparatively primitive. It doesn't try to
simplify the path in any way.
We assume Unix style paths, i.e., / is the path separator. It's not
clear what we should do to support other systems like Windows.
Definitions and Theorems
Function: catpath
(defun catpath (basedir filename)
(declare (xargs :guard (and (stringp basedir)
(stringp filename))))
(let ((__function__ 'catpath))
(declare (ignorable __function__))
(b* ((len (length basedir))
((when (or (int= len 0)
(eql (char basedir (- len 1)) #\/)))
(cat basedir filename)))
(cat basedir "/" filename))))
Theorem: stringp-of-catpath
(defthm stringp-of-catpath
(b* ((path (catpath basedir filename)))
(stringp path))
:rule-classes :rewrite)
