		Search-engine friendly clone of the ACL2 documentation.

Oslib

Dirnames

Strip non-directory suffixes from a list of file names.

Signature
(dirnames paths &key (state 'state)) → (mv err dirnames state)
Arguments: paths — Guard (string-listp paths).
Returns: err — NIL on success or an error msg on failure.; dirnames — Sensible only if there is no error.
Type (string-listp dirnames).; state — Type (state-p1 state), given (force (state-p1 state)).

This just calls dirname on every path in a list.

Definitions and Theorems

Function: dirnames-fn

(defun dirnames-fn (paths state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (string-listp paths)))
  (let ((__function__ 'dirnames))
    (declare (ignorable __function__))
    (b* (((when (atom paths)) (mv nil nil state))
         ((mv err name1 state)
          (dirname (car paths)))
         ((when err) (mv err nil state))
         ((mv err names2 state)
          (dirnames (cdr paths)))
         ((when err) (mv err nil state)))
      (mv nil (cons name1 names2) state))))

Theorem: string-listp-of-dirnames.dirnames

(defthm string-listp-of-dirnames.dirnames
  (b* (((mv ?err ?dirnames acl2::?state)
        (dirnames-fn paths state)))
    (string-listp dirnames))
  :rule-classes :rewrite)

Theorem: state-p1-of-dirnames.state

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