		Search-engine friendly clone of the ACL2 documentation.

Std/io/close-input-channel

Close an input channel.

Signature: (close-input-channel channel state-state) returns state.

channel is a symbol that must refer to a currently open input channel; see open-input-channel.
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 channel will no longer be an open input channel, and hence can no longer be read from or closed.

Under the hood, we close the raw Lisp stream associated with channel. It is generally necessary to close the input channels when you are done with them to avoid resource leaks.

Definitions and Theorems

Theorem: state-p1-of-close-input-channel-free

(defthm state-p1-of-close-input-channel-free
        (implies (and (open-input-channel-p1 channel type state)
                      (state-p1 state))
                 (state-p1 (close-input-channel channel state))))

Theorem: state-p1-of-close-input-channel-types

(defthm state-p1-of-close-input-channel-types
        (implies (and (or (open-input-channel-p1 channel
                                                 :byte state)
                          (open-input-channel-p1 channel
                                                 :object state)
                          (open-input-channel-p1 channel
                                                 :character state))
                      (state-p1 state))
                 (state-p1 (close-input-channel channel state))))

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

(defthm
 state-p1-of-close-input-channel-of-open
 (implies
      (and (open-input-channel-p1
                (mv-nth 0
                        (open-input-channel fname type state1))
                type state)
           (state-p1 state))
      (state-p1 (close-input-channel
                     (mv-nth 0
                             (open-input-channel fname type state1))
                     state))))