• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
      • Io
      • Defttag
      • Sys-call
      • Save-exec
      • Quicklisp
      • Oslib
        • File-types
          • File-kind
          • Regular-files
          • Existing-paths
          • Missing-paths
          • Directories
          • Path-exists-p
            • Regular-file-p
            • Directory-p
            • Regular-files-p
            • Paths-all-missing-p
            • Paths-all-exist-p
            • Directories-p
            • Regular-files-exec
            • File-kind-p
            • Existing-paths-exec
            • Missing-paths-exec
            • Directories-exec
          • Argv
          • Copy
          • Catpath
          • Universal-time
          • Ls
          • Basename
          • Tempfile
          • Dirname
          • Copy!
          • Mkdir
          • Ls-files
          • Lisp-version
          • Rmtree
          • Ls-subdirs
          • Lisp-type
          • Date
          • Getpid
          • Basenames
          • Dirnames
          • Ls-subdirs!
          • Ls-files!
          • Dirname!
          • Basename!
          • Catpaths
          • Mkdir!
          • Ls!
          • Rmtree!
          • Remove-nonstrings
        • Std/io
        • Bridge
        • Clex
        • Tshell
        • Unsound-eval
        • Hacker
        • Startup-banner
        • Command-line
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • 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))))