		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)