		Search-engine friendly clone of the ACL2 documentation.

Oslib

Ls

Get a (full) directory listing.

Signature
(ls path &key (state 'state)) → (mv error val state)
Arguments: path — Directory to list files in.
Guard (stringp path).
Returns: error — NIL on success or an error msg on failure.; val — On success: a list of names of files (and directories) within this directory.
Type (string-listp val).; state — Type (state-p1 state), given (force (state-p1 state)).

In the logic this function reads from the ACL2 oracle. In the execution we query the file system to obtain a listing of the files within the given path. This listing can contain the names of any kind of file, e.g., it may contain ordinary files, directories, and special files such as block devices and symbolic links.

The names returned are not complete paths. For instance, if /home/users/jared contains directories named foo and bar, then the resulting val will have "foo" and "bar", not full paths like "/home/users/jared/foo".

Definitions and Theorems

Function: ls-fn

(defun ls-fn (path state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (stringp path)))
  (let ((__function__ 'ls))
    (declare (ignorable __function__))
    (b* ((- (raise "Raw Lisp definition not installed?"))
         ((mv ?err1 val1 state)
          (read-acl2-oracle state))
         ((mv ?err2 val2 state)
          (read-acl2-oracle state))
         ((when val1) (mv val1 nil state)))
      (mv nil (remove-nonstrings val2)
          state))))

Theorem: string-listp-of-ls.val

(defthm string-listp-of-ls.val
  (b* (((mv common-lisp::?error ?val acl2::?state)
        (ls-fn path state)))
    (string-listp val))
  :rule-classes :rewrite)

Theorem: state-p1-of-ls.state

(defthm state-p1-of-ls.state
  (implies (force (state-p1 state))
           (b* (((mv common-lisp::?error ?val acl2::?state)
                 (ls-fn path state)))
             (state-p1 state)))
  :rule-classes :rewrite)