Std/io/open-output-channel
Open a file for writing.
Signature: (open-output-channel file-name typ state-state) returns (mv
channel state)
- file-name can be either :string (to indicate that you want to
print to a string stream), or a string like "temp.txt" that names the
file to write to.
- 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 output channel of the indicated type,
and hence can be written to or closed.
Under the hood, we either create a new Lisp string stream in memory (when
file-name is :string) or we use Lisp's file operations to open
file-name for writing. Note that if file-name refers to a file that
already exists, it will be overwritten (i.e., not appended to).
On success, channel is a symbol in the ACL2-OUTPUT-CHANNEL
package. Under the hood, this symbol will be associated with the Lisp stream.
Note that to avoid resource leaks, you should eventually use close-output-channel to free this stream.
On failure, channel is nil. There are various reasons that
open-output-channel can fail. For example, this can happen if you try to
write to a file in a directory that does not exist, and it may happen
(depending on your host Lisp) if you try to open a file for which you do not
have permission.
Definitions and Theorems
Theorem: state-p1-of-open-output-channel
(defthm
state-p1-of-open-output-channel
(implies
(and (state-p1 state)
(stringp fname)
(member type *file-types*))
(state-p1 (mv-nth 1
(open-output-channel fname type state)))))
Theorem: symbolp-of-open-output-channel
(defthm symbolp-of-open-output-channel
(symbolp (mv-nth 0
(open-output-channel fname type state)))
:rule-classes (:rewrite :type-prescription))
Theorem: open-output-channel-p1-of-open-output-channel
(defthm
open-output-channel-p1-of-open-output-channel
(implies
(and (state-p1 state)
(stringp fname)
(member type *file-types*)
(equal channel
(mv-nth 0
(open-output-channel fname type state)))
channel)
(open-output-channel-p1
channel type
(mv-nth 1
(open-output-channel fname type state)))))
Theorem: open-output-channel-p1-of-put-global
(defthm
open-output-channel-p1-of-put-global
(equal
(open-output-channel-p1 channel type (put-global key val state))
(open-output-channel-p1 channel type state)))
