Remove the leading directory part from a path.
(basename path &optional (state 'state)) → (mv err basename state)
In the logic this function reads from the ACL2 oracle. In the
execution we use Common Lisp functions to determine the part of
Examples (assuming a Unix style operating system):
(basename "/home/jared/hello.txt") --> "hello.txt" (basename "/home/jared/") --> "jared" (basename "/home/jared") --> "jared"
A special case is the basename of the root directory. In this case we mimic
the (arguably nonsensical) behavior of the unix
(basename "/") --> "/"
(defun basename-fn (path state) (declare (xargs :stobjs (state))) (declare (xargs :guard (stringp path))) (declare (ignorable path)) (let ((__function__ 'basename)) (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 basename" "" state))) (mv nil val2 state))))
(defthm stringp-of-basename.basename (b* (((mv ?err ?basename acl2::?state) (basename-fn path state))) (stringp basename)) :rule-classes :type-prescription)