		Search-engine friendly clone of the ACL2 documentation.

File-types

Path-exists-p

Does a path exist? After following symlinks, does it refer to any "file" at all (a regular file, a directory, a device, ...)?

Signature
(path-exists-p path &key (state 'state)) → (mv err ans new-state)
Arguments: path — Guard (stringp path).
Returns: err — NIL on success, or an error msg on failure.; ans — Meaningful only when there is no error.
Type (booleanp ans).; new-state — Type (state-p1 new-state), given (force (state-p1 state)).

Note that we return nil in the case of a broken symbolic link. This behavior matches shell tools such as test -e and seems pretty reasonable.

Definitions and Theorems

Function: path-exists-p-fn

(defun path-exists-p-fn (path state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (stringp path)))
  (let ((__function__ 'path-exists-p))
    (declare (ignorable __function__))
    (b* (((mv err ans state) (file-kind path))
         ((when err) (mv err nil state))
         (exists-p (and (not (null ans))
                        (not (eq ans :broken-symbolic-link)))))
      (mv err exists-p state))))

Theorem: booleanp-of-path-exists-p.ans

(defthm booleanp-of-path-exists-p.ans
  (b* (((mv ?err ?ans ?new-state)
        (path-exists-p-fn path state)))
    (booleanp ans))
  :rule-classes :type-prescription)

Theorem: state-p1-of-path-exists-p.new-state

(defthm state-p1-of-path-exists-p.new-state
  (implies (force (state-p1 state))
           (b* (((mv ?err ?ans ?new-state)
                 (path-exists-p-fn path state)))
             (state-p1 new-state)))
  :rule-classes :rewrite)

Theorem: w-state-of-path-exists-p

(defthm w-state-of-path-exists-p
  (b* (((mv ?err ?ans ?new-state)
        (path-exists-p-fn path state)))
    (equal (w new-state) (w state))))