		Search-engine friendly clone of the ACL2 documentation.

Vl-find-file

Vl-find-file-aux

Look for a file in a list of search directories.

Definitions and Theorems

Function: vl-find-file-aux

(defun vl-find-file-aux (filename searchpath state)
  (declare (xargs :guard (and (stringp filename)
                              (string-listp searchpath)
                              (state-p state))))
  (b* (((when (atom searchpath))
        (mv nil state))
       (attempt (vl-extend-pathname (car searchpath)
                                    filename))
       ((mv channel state)
        (open-input-channel attempt
                            :character state))
       ((unless channel)
        (vl-find-file-aux filename (cdr searchpath)
                          state))
       (state (close-input-channel channel state)))
    (mv attempt state)))

Theorem: state-p1-of-vl-find-file-aux

(defthm state-p1-of-vl-find-file-aux
 (implies
  (force (state-p1 state))
  (state-p1 (mv-nth 1
                    (vl-find-file-aux filename searchpath state)))))

Theorem: stringp-of-vl-find-file-aux

(defthm stringp-of-vl-find-file-aux
 (equal
     (stringp (mv-nth 0
                      (vl-find-file-aux filename searchpath state)))
     (if (mv-nth 0
                 (vl-find-file-aux filename searchpath state))
         t
       nil)))