		Search-engine friendly clone of the ACL2 documentation.

Vl-read-file

Vl-read-file-loop

Logically nice loop for vl-read-file.

Signature
(vl-read-file-loop channel filename line col &key (state 'state)) → (mv data len state)
Arguments: channel — Channel we're reading from.
Guard (symbolp channel).; filename — Current file name.
Guard (stringp filename).; line — Current line number.
Guard (posp line).; col — Current column number.
Guard (natp col).
Returns: data — Characters from the file.
Type (vl-echarlist-p data).; len — Number of characters read.
Type (equal len (len data)).; state — Type (and (state-p1 state) (open-input-channel-p1 channel :byte state)), given (and (force (state-p1 state)) (force (symbolp channel)) (force (open-input-channel-p1 channel :byte state))) .

Definitions and Theorems

Function: vl-read-file-loop-fn

(defun vl-read-file-loop-fn (channel filename line col state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp channel)
                             (stringp filename)
                             (posp line)
                             (natp col))))
 (declare (xargs :guard (open-input-channel-p channel
                                              :byte state)))
 (let ((__function__ 'vl-read-file-loop))
  (declare (ignorable __function__))
  (mbe
     :logic
     (b* (((unless (state-p state))
           (mv nil 0 state))
          ((mv byte state)
           (read-byte$ channel state))
          ((unless byte) (mv nil 0 state))
          (char (code-char (the (unsigned-byte 8) byte)))
          (echar (make-vl-echar-fast :char char
                                     :filename filename
                                     :line line
                                     :col col))
          (newlinep (eql char #\Newline))
          (next-line (if newlinep (+ 1 line) line))
          (next-col (if newlinep 0 (+ 1 col)))
          ((mv rest len state)
           (vl-read-file-loop channel filename next-line next-col)))
       (mv (cons echar rest) (+ 1 len) state))
     :exec
     (b* (((local-stobjs nrev)
           (mv echars len nrev state))
          ((mv nrev len state)
           (vl-read-file-loop-aux channel filename line col 0 nrev))
          ((mv echars nrev) (nrev-finish nrev)))
       (mv echars len nrev state)))))

Theorem: vl-echarlist-p-of-vl-read-file-loop.data

(defthm vl-echarlist-p-of-vl-read-file-loop.data
  (b* (((mv ?data acl2::?len acl2::?state)
        (vl-read-file-loop-fn channel filename line col state)))
    (vl-echarlist-p data))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-read-file-loop.len

(defthm return-type-of-vl-read-file-loop.len
  (b* (((mv ?data acl2::?len acl2::?state)
        (vl-read-file-loop-fn channel filename line col state)))
    (equal len (len data)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-read-file-loop.state

(defthm return-type-of-vl-read-file-loop.state
 (implies
      (and (force (state-p1 state))
           (force (symbolp channel))
           (force (open-input-channel-p1 channel
                                         :byte state)))
      (b* (((mv ?data acl2::?len acl2::?state)
            (vl-read-file-loop-fn channel filename line col state)))
        (and (state-p1 state)
             (open-input-channel-p1 channel
                                    :byte state))))
 :rule-classes :rewrite)

Theorem: true-listp-of-vl-read-file-loop

(defthm true-listp-of-vl-read-file-loop
 (true-listp (mv-nth 0
                     (vl-read-file-loop channel filename line col)))
 :rule-classes :type-prescription)

Theorem: vl-read-file-loop-aux-redef

(defthm vl-read-file-loop-aux-redef
  (equal (vl-read-file-loop-aux channel filename line col len acc)
         (b* (((mv data & state)
               (vl-read-file-loop channel filename line col)))
           (mv (append acc data)
               (+ (lnfix len) (len data))
               state))))