		Search-engine friendly clone of the ACL2 documentation.

Oslib

Dirname

Strip the non-directory suffix from a path.

Signature
(dirname path &optional (state 'state)) → (mv err dirname state)
Arguments: path — Path to process.
Guard (stringp path).
Returns: err — NIL on success or an error msg on failure.; dirname — Sensible only if there is no error.
Type (stringp dirname).; state — Type (state-p1 state), given (force (state-p1 state)).

In the logic this function reads from the ACL2 oracle. In the execution we use Common Lisp functions to determine the parent directory of path in some OS specific way. See also basename.

Examples (assuming a Unix style operating system):

(dirname "/home/jared/hello.txt")   -->  "/home/jared/"
(dirname "/home/jared/")            -->  "/home/"
(dirname "/home/jared")             -->  "/home/"

A special case is the dirname of the root directory. In this case we mimic the (arguably nonsensical) behavior of the unix dirname command:

(dirname "/")                       -->  "/"

Definitions and Theorems

Function: dirname-fn

(defun dirname-fn (path state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (stringp path)))
  (declare (ignorable path))
  (let ((__function__ 'dirname))
    (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 "" state))
         ((unless (stringp val2))
          (mv "Error with dirname" "" state)))
      (mv nil val2 state))))

Theorem: stringp-of-dirname.dirname

(defthm stringp-of-dirname.dirname
  (b* (((mv ?err ?dirname acl2::?state)
        (dirname-fn path state)))
    (stringp dirname))
  :rule-classes :type-prescription)

Theorem: state-p1-of-dirname.state

(defthm state-p1-of-dirname.state
  (implies (force (state-p1 state))
           (b* (((mv ?err ?dirname acl2::?state)
                 (dirname-fn path state)))
             (state-p1 state)))
  :rule-classes :rewrite)