scan

(defun find-char
  (s c i)
  (declare (xargs :guard (and (stringp s)
        (characterp c)
        (natp i))
      :measure (nfix (- (length s) (nfix i)))))
  (let ((i (nfix i)))
    (cond ((>= i (length s)) nil)
      ((eql (char s i) c) i)
      (t (find-char s c (+ 1 i))))))

(defun extract-quoted-string
  (s i)
  (declare (xargs :guard (and (stringp s) (natp i))))
  (let* ((len (length s)) (i (nfix i)))
    (cond ((>= i len) (mv nil i))
      ((not (eql (char s i) #\")) (mv nil i))
      (t (let* ((start (+ 1 i)) (end (find-char s #\" start)))
          (if end
            (mv (subseq s start end)
              (+ 1 end))
            (mv nil i)))))))

(defun parse-include-book
  (line)
  (declare (xargs :guard (stringp line)))
  (let* ((trimmed (trim line)) (trimmed-len (length trimmed))
      (localp (and (>= trimmed-len 7)
          (strprefixp "(local" trimmed)))
      (work (if localp
          (trim (subseq trimmed 6 trimmed-len))
          trimmed)))
    (if (not (strprefixp "(include-book" work))
      nil
      (let ((quote-pos (find-char work #\" 0)))
        (if (not quote-pos)
          nil
          (mv-let (name end-pos)
            (extract-quoted-string work
              quote-pos)
            (declare (ignore end-pos))
            (if name
              (make-book-dep :path name
                :localp localp)
              nil)))))))

(defun scan-lines-for-deps
  (lines)
  (declare (xargs :guard (string-listp lines)))
  (if (atom lines)
    nil
    (let ((dep (parse-include-book (car lines))) (rest (scan-lines-for-deps (cdr lines))))
      (if dep
        (cons dep rest)
        rest))))