• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
          • Preprocessor
          • Vl-loadconfig
          • Lexer
          • Vl-loadstate
          • Parser
          • Vl-load-merge-descriptions
          • Scope-of-defines
          • Vl-load-file
          • Vl-flush-out-descriptions
          • Vl-description
          • Vl-loadresult
          • Vl-read-file
            • Vl-read-file-loop
              • Vl-read-file-loop-aux
              • Vl-read-file-rchars
            • Vl-find-basename/extension
            • Vl-find-file
            • Vl-read-files
            • Extended-characters
            • Vl-load
            • Vl-load-main
            • Vl-load-description
            • Vl-descriptions-left-to-load
            • Inject-warnings
            • Vl-load-descriptions
            • Vl-load-files
            • Vl-load-summary
            • Vl-collect-modules-from-descriptions
            • Vl-descriptionlist
          • Transforms
          • Lint
          • Mlib
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • 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 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), given the guard.
    state — Type (state-p1 state), given the guard.

    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 state))
            ((mv byte state)
             (read-byte$ channel state))
            ((unless byte) (mv nil 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 state)
             (vl-read-file-loop channel filename next-line next-col)))
         (mv (cons echar rest) state))
       :exec
       (with-local-stobj
         nrev
         (mv-let
           (echars nrev state)
           (b* (((mv nrev state)
                 (vl-read-file-loop-aux channel filename line col nrev))
                ((mv echars nrev) (nrev-finish nrev)))
             (mv echars nrev state))
           (mv echars state))))))

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

    (defthm vl-echarlist-p-of-vl-read-file-loop.data
     (implies
          (and (force (state-p state))
               (force (symbolp channel))
               (force (stringp filename))
               (force (posp line))
               (force (natp col))
               (force (open-input-channel-p channel ':byte
                                            state)))
          (b* (((mv ?data acl2::?state)
                (vl-read-file-loop-fn channel filename line col state)))
            (vl-echarlist-p data)))
     :rule-classes :rewrite)

    Theorem: state-p1-of-vl-read-file-loop.state

    (defthm state-p1-of-vl-read-file-loop.state
     (implies
          (and (force (state-p state))
               (force (symbolp channel))
               (force (stringp filename))
               (force (posp line))
               (force (natp col))
               (force (open-input-channel-p channel ':byte
                                            state)))
          (b* (((mv ?data acl2::?state)
                (vl-read-file-loop-fn channel filename line col state)))
            (state-p1 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 acc)
             (b* (((mv data state)
                   (vl-read-file-loop channel filename line col)))
               (mv (append acc data) state))))

    Theorem: vl-read-file-loop-preserves-open-input-channel-p1

    (defthm vl-read-file-loop-preserves-open-input-channel-p1
      (implies (and (force (state-p1 state))
                    (force (symbolp channel))
                    (force (open-input-channel-p1 channel
                                                  :byte state)))
               (b* (((mv ?data state)
                     (vl-read-file-loop channel filename line col)))
                 (open-input-channel-p1 channel
                                        :byte state))))