• 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
        • File-kind
        • Regular-files
        • Missing-paths
        • Existing-paths
        • Directories
        • Path-exists-p
        • Regular-file-p
        • Paths-all-missing-p
        • Directory-p
        • Regular-files-p
        • Paths-all-exist-p
        • Directories-p
        • File-kind-p
        • Regular-files-exec
        • Missing-paths-exec
        • Existing-paths-exec
        • Directories-exec
      • 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

• File-types

Missing-paths

Collect paths that do not exist.

Signature

(missing-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: missing-paths-exec-fn

(defun missing-paths-exec-fn (paths acc state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (string-listp paths)))
  "Tail recursive version for execution."
  (let ((__function__ 'missing-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 acc
                (cons (car paths) acc))))
      (missing-paths-exec (cdr paths) acc))))

Function: missing-paths-fn

(defun missing-paths-fn (paths state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (string-listp paths)))
  (let ((__function__ 'missing-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)
               (missing-paths (cdr paths)))
              (ans (if exists-p rest
                     (cons (car paths) rest))))
           (mv err ans state))
         :exec
         (b* (((mv err acc state)
               (missing-paths-exec paths nil)))
           (mv err (reverse acc) state)))))

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

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

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

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

Theorem: missing-paths-exec-removal

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

Theorem: true-listp-of-missing-paths

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

Theorem: w-state-of-missing-paths

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