• 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
      • 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

• Oslib

Basename

Remove the leading directory part from a path.

Signature

(basename path &optional (state 'state)) 
  → 
(mv err basename state)

Arguments

path — Path to process.
    Guard (stringp path).

Returns

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

basename — Sensible only if there is no error.
    Type (stringp basename).

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 part of path excluding its parent directory in some OS specific way. See also dirname.

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 command:

(basename "/")                       -->  "/"

Definitions and Theorems

Function: basename-fn

(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))))

Theorem: stringp-of-basename.basename

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

Theorem: state-p1-of-basename.state

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