• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
      • Open-channel-lemmas
      • Std/io/read-char$
      • Std/io/read-object
      • Std/io/open-output-channel
      • Unsound-read
      • Read-string
      • Read-bytes$
      • File-measure
      • Read-bytes$-n
      • Std/io/read-byte$
      • Std/io/open-input-channel
      • Print-compressed
      • Read-file-lines-no-newlines
      • Nthcdr-bytes
      • Read-file-lines
      • Std/io/close-output-channel
      • Read-file-characters
      • Read-file-bytes
      • Print-legibly
      • Std/io/close-input-channel
      • Read-file-objects
      • Logical-story-of-io
      • Take-bytes
      • Std/io/peek-char$
      • Read-file-characters-rev
      • Read-file-as-string
      • Std/io/write-byte$
      • Std/io/set-serialize-character
      • Std/io/print-object$
      • Std/io/princ$
      • Std/io/read-file-into-string
      • *file-types*
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/io
• Open-input-channel

Std/io/open-input-channel

Open an file for reading.

Signature: (open-input-channel file-name typ state-state) returns (mv channel state)

• file-name is a string that names the file to open.
• typ is the type of input to be used and must be one of the valid *file-types*.
• state is the ACL2 state.

This is a logic-mode function, but its logical definition is tricky; see logical-story-of-io. The main logical consequence is that (on success) channel will become an open input channel of the indicated type, and hence can be read from or closed.

Under the hood, we use Lisp's file operations to try to open the file. On success, channel is a symbol in the ACL2-INPUT-CHANNEL package. Under the hood, this symbol will be associated with a raw Lisp file stream. Note that to avoid resource leaks, you should eventually use close-input-channel to free this stream.

On failure, channel is nil. There are various reasons that open-input-channel can fail. For example, this can happen if you try to open a file that does not exist or for which you do not have permission.

Definitions and Theorems

Theorem: state-p1-of-open-input-channel

(defthm
    state-p1-of-open-input-channel
    (implies
         (and (state-p1 state)
              (stringp fname)
              (member type *file-types*))
         (state-p1 (mv-nth 1
                           (open-input-channel fname type state)))))

Theorem: symbolp-of-open-input-channel

(defthm symbolp-of-open-input-channel
        (symbolp (mv-nth 0
                         (open-input-channel fname type state)))
        :rule-classes (:rewrite :type-prescription))

Theorem: open-input-channel-p1-of-open-input-channel

(defthm
    open-input-channel-p1-of-open-input-channel
    (implies
         (and (state-p1 state)
              (stringp fname)
              (member type *file-types*)
              (equal channel
                     (mv-nth 0
                             (open-input-channel fname type state)))
              channel)
         (open-input-channel-p1
              channel type
              (mv-nth 1
                      (open-input-channel fname type state)))))