Canonical-pathname
The true absolute filename, with soft links resolved
For the name fname of a file, the form (canonical-pathname
fname nil state) evaluates to a Unix-style absolute filename representing
the same file as fname, but generally without any use of soft links in
the name. (Below, we explain the qualifier ``generally''.) If however the
file indicated by fname does not exist, (canonical-pathname fname nil
state) is nil. Thus, canonical-pathname can be used as one would
use the raw Lisp function probe-file.
The specification of (canonical-pathname fname dir-p state) when
dir-p is not nil is similar, except that if the specified file
exists but is not a directory, then the result is nil.
The function canonical-pathname has a guard of t, though the
second argument must be the ACL2 state. This function is introduced
with the following properties.
(defthm canonical-pathname-is-idempotent
(equal (canonical-pathname (canonical-pathname x dir-p state) dir-p state)
(canonical-pathname x dir-p state)))
(defthm canonical-pathname-type
(or (equal (canonical-pathname x dir-p state) nil)
(stringp (canonical-pathname x dir-p state)))
:rule-classes :type-prescription)
We use the qualifier ``generally'', above, because there is no guarantee
that the filename will be canonical without soft links, though we expect this
to be true in practice. ACL2 attempts to compute the desired result and then
checks that the input and result have the same Common Lisp ``truename''.
This check is expected to succeed, but if it fails then the input string is
returned unchanged, and to be conservative, the value returned is nil in
this case if dir-p is true.
