• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
      • File-types
        • File-kind
        • Regular-files
        • Existing-paths
        • Missing-paths
        • Directories
        • Path-exists-p
        • Regular-file-p
        • Directory-p
        • Regular-files-p
        • Paths-all-missing-p
        • Paths-all-exist-p
        • Directories-p
        • Regular-files-exec
        • File-kind-p
        • Existing-paths-exec
        • Missing-paths-exec
        • Directories-exec
      • Argv
      • Copy
      • Catpath
      • Universal-time
      • Ls
      • Basename
      • Tempfile
      • Dirname
      • Copy!
      • Mkdir
      • Ls-files
      • Lisp-version
      • Rmtree
      • Ls-subdirs
      • Lisp-type
      • Date
      • Getpid
      • Basenames
      • Dirnames
      • Ls-subdirs!
      • Ls-files!
      • Dirname!
      • Basename!
      • Catpaths
      • Mkdir!
      • Ls!
      • Rmtree!
      • Remove-nonstrings
    • Std/io
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• File-types

Existing-paths

Collect paths that exist.

Signature

(existing-paths paths &key (state 'state)) 
  → 
(mv err ans new-state)

Arguments

paths — Guard (string-listp paths).

Returns

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

ans — Meaningful only when there is no error.
    Type (string-listp ans), given (string-listp paths).

new-state — Type (state-p1 new-state), given (force (state-p1 state)).

Definitions and Theorems

Function: existing-paths-exec-fn

(defun existing-paths-exec-fn (paths acc state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard (string-listp paths)))
       "Tail recursive version for execution."
       (let ((__function__ 'existing-paths-exec))
            (declare (ignorable __function__))
            (b* (((when (atom paths)) (mv nil acc state))
                 ((mv err exists-p state)
                  (path-exists-p (car paths)))
                 ((when err) (mv err acc state))
                 (acc (if exists-p (cons (car paths) acc)
                          acc)))
                (existing-paths-exec (cdr paths) acc))))

Function: existing-paths-fn

(defun
     existing-paths-fn (paths state)
     (declare (xargs :stobjs (state)))
     (declare (xargs :guard (string-listp paths)))
     (let ((__function__ 'existing-paths))
          (declare (ignorable __function__))
          (mbe :logic (b* (((when (atom paths)) (mv nil nil state))
                           ((mv err exists-p state)
                            (path-exists-p (car paths)))
                           ((when err) (mv err nil state))
                           ((mv err rest state)
                            (existing-paths (cdr paths)))
                           (ans (if exists-p (cons (car paths) rest)
                                    rest)))
                          (mv err ans state))
               :exec (b* (((mv err acc state)
                           (existing-paths-exec paths nil)))
                         (mv err (reverse acc) state)))))

Theorem: string-listp-of-existing-paths.ans

(defthm string-listp-of-existing-paths.ans
        (implies (string-listp paths)
                 (b* (((mv ?err ?ans ?new-state)
                       (existing-paths-fn paths state)))
                     (string-listp ans)))
        :rule-classes :rewrite)

Theorem: state-p1-of-existing-paths.new-state

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

Theorem: existing-paths-exec-removal

(defthm existing-paths-exec-removal
        (equal (existing-paths-exec paths acc)
               (b* (((mv err ans state)
                     (existing-paths paths)))
                   (mv err (revappend ans acc) state))))

Theorem: true-listp-of-existing-paths

(defthm true-listp-of-existing-paths
        (true-listp (mv-nth 1 (existing-paths paths)))
        :rule-classes :type-prescription)

Theorem: w-state-of-existing-paths

(defthm w-state-of-existing-paths
        (b* (((mv ?err ?ans ?new-state)
              (existing-paths-fn paths state)))
            (equal (w new-state) (w state))))