		Search-engine friendly clone of the ACL2 documentation.

Loader

Vl-read-file-report

Signature
(vl-read-file-report state) → state
Returns: state — Type (state-p1 state), given (state-p1 state).

Definitions and Theorems

Function: vl-read-file-report

(defun vl-read-file-report (state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-read-file-report))
   (declare (ignorable __function__))
   (b* ((file-alist (and (boundp-global 'vl-read-file-alist
                                        state)
                         (f-get-global 'vl-read-file-alist
                                       state)))
        (file-alist (fast-alist-free (fast-alist-clean file-alist)))
        (state (f-put-global 'vl-read-file-alist
                             nil state))
        ((mv lines total-reads total-bytes)
         (vl-read-file-report-gather file-alist nil 0 0)))
     (cw "Input file statistics:~%")
     (cw "  - Unique files: ~x0~%"
         (len file-alist))
     (cw "  - Number of files read: ~x0~%"
         total-reads)
     (cw "  - Total bytes read: ~x0~%"
         total-bytes)
     (cw "Details:~%")
     (cw "   ~x0~%" (rev (mergesort lines)))
     state)))

Theorem: state-p1-of-vl-read-file-report

(defthm state-p1-of-vl-read-file-report
  (implies (state-p1 state)
           (b* ((state (vl-read-file-report state)))
             (state-p1 state)))
  :rule-classes :rewrite)