		Search-engine friendly clone of the ACL2 documentation.

Loader

Vl-read-file-report-gather

Signature
(vl-read-file-report-gather alist lines total-reads total-bytes) → (mv lines total-reads total-bytes)
Arguments: total-reads — Guard (natp total-reads).; total-bytes — Guard (natp total-bytes).
Returns: total-reads — Type (natp total-reads).; total-bytes — Type (natp total-bytes).

Definitions and Theorems

Function: vl-read-file-report-gather

(defun
    vl-read-file-report-gather
    (alist lines total-reads total-bytes)
    (declare (xargs :guard (and (natp total-reads)
                                (natp total-bytes))))
    (let ((__function__ 'vl-read-file-report-gather))
         (declare (ignorable __function__))
         (b* (((when (atom alist))
               (mv lines (lnfix total-reads)
                   (lnfix total-bytes)))
              ((unless (and (consp (car alist))
                            (stringp (caar alist))
                            (consp (cdar alist))
                            (natp (car (cdar alist)))
                            (natp (cdr (cdar alist)))))
               (raise "Unexpected vl-read-file-alist entry: ~x0"
                      (car alist))
               (mv lines (lnfix total-reads)
                   (lnfix total-bytes)))
              ((cons filename (cons num-reads len))
               (car alist))
              (bytes-for-this-file (* num-reads len))
              (total-reads (+ num-reads (lnfix total-reads)))
              (total-bytes (+ bytes-for-this-file
                              (lnfix total-bytes)))
              (line (list :fromdisk bytes-for-this-file
                          :reads num-reads
                          :size len
                          :file filename)))
             (vl-read-file-report-gather (cdr alist)
                                         (cons line lines)
                                         total-reads total-bytes))))

Theorem: natp-of-vl-read-file-report-gather.total-reads

(defthm natp-of-vl-read-file-report-gather.total-reads
        (b* (((mv ?lines ?total-reads ?total-bytes)
              (vl-read-file-report-gather
                   alist lines total-reads total-bytes)))
            (natp total-reads))
        :rule-classes :type-prescription)

Theorem: natp-of-vl-read-file-report-gather.total-bytes

(defthm natp-of-vl-read-file-report-gather.total-bytes
        (b* (((mv ?lines ?total-reads ?total-bytes)
              (vl-read-file-report-gather
                   alist lines total-reads total-bytes)))
            (natp total-bytes))
        :rule-classes :type-prescription)