Major Section: ACL2-BUILT-INS
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 simlar, 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.
