Strip the non-directory suffix from a path.
(dirname path &optional (state 'state)) → (mv err dirname 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
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 "/") --> "/"
(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))))
(defthm stringp-of-dirname.dirname (b* (((mv ?err ?dirname acl2::?state) (dirname-fn path state))) (stringp dirname)) :rule-classes :type-prescription)