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

• File-types

File-kind

See what kind of file a path refers to.

Signature

(file-kind path &key (follow-symlinks 't) (state 'state)) 
  → 
(mv err ans new-state)

Arguments

path — The path to test.
    Guard (stringp path).

follow-symlinks — Guard (booleanp follow-symlinks).

Returns

err — NIL on success, or an error msg on failure.

ans — On success: the kind of file.
    Type (file-kind-p ans).

new-state — Type (state-p1 new-state), given (force (state-p1 state)).

We check whether path exists. If so, we determine what kind of file it is.

This is complicated by symbolic links. You can control how symlinks are handled using :follow-symlinks.

By default, :follow-symlinks is t. In this case, the idea is to tell you what kind of file is ultimately pointed to after resolving all the symlinks. Since we are following all links, we will never return :symbolic-link in this case. However, we may return :broken-symbolic-link if there is a problem following the symlinks.

For finer-grained handling of symlinks, you can set :follow-symlinks to nil. In this case, we return :symbolic-link for all symbolic links, no matter whether they are valid or broken. Unless you're doing something very fancy with symlinks, this is almost surely not what you want.

Definitions and Theorems

Function: file-kind-fn

(defun file-kind-fn (path follow-symlinks state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (stringp path)
                              (booleanp follow-symlinks))))
  (let ((__function__ 'file-kind))
    (declare (ignorable __function__))
    (b* ((- (raise "Raw Lisp definition not installed?"))
         ((mv & err state)
          (read-acl2-oracle state))
         ((mv & ans state)
          (read-acl2-oracle state)))
      (mv err (if (file-kind-p ans) ans nil)
          state))))

Theorem: file-kind-p-of-file-kind.ans

(defthm file-kind-p-of-file-kind.ans
  (b* (((mv ?err ?ans ?new-state)
        (file-kind-fn path follow-symlinks state)))
    (file-kind-p ans))
  :rule-classes :rewrite)

Theorem: state-p1-of-file-kind.new-state

(defthm state-p1-of-file-kind.new-state
  (implies (force (state-p1 state))
           (b* (((mv ?err ?ans ?new-state)
                 (file-kind-fn path follow-symlinks state)))
             (state-p1 new-state)))
  :rule-classes :rewrite)

Theorem: type-of-file-kind.ans

(defthm type-of-file-kind.ans
  (let ((ans (mv-nth 1 (file-kind path))))
    (and (symbolp ans) (not (equal ans t))))
  :rule-classes :type-prescription)

Theorem: w-state-of-file-kind

(defthm w-state-of-file-kind
  (b* (((mv ?err ?ans ?new-state)
        (file-kind-fn path follow-symlinks state)))
    (equal (w new-state) (w state))))