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 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.