		Search-engine friendly clone of the ACL2 documentation.

Std/io/read-char$

Read one character from an open :character stream.

NOTE: We generally prefer to avoid read-char$. It is easy to use read-byte$ instead, which is generally more efficient and avoids certain character-encoding issues; see below for details.

Signature: (read-char$ channel state-state) returns (mv char/nil state).

channel is a symbol that must refer to an open :character 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 the updating of state.

Under the hood, we read a character from the Lisp input stream that is associated with channel. If we reach the end of the file, nil is returned.

Character versus Byte Input

In some sense, it is redundant for ACL2 to have separate kinds of input channels for characters and bytes. After all, ACL2 has exactly 256 characters corresponding to bytes 0-255, and provides functions like char-code and code-char for converting between these characters and bytes. So, one could easily define read-char$ as a wrapper that calls code-char on read-byte$, or could define read-byte$ as a wrapper for read-char$ that calls char-code.

That being said, we generally prefer to use byte input. Common Lisp implementations have some freedom in how they implement characters. Because of this, and because different Lisps might try to use different encodings when reading files, ACL2's read-char$ has some extra checks to make sure that the characters being read in are legal. At any rate, for a basic timing test on CCL, we measured read-char$ at 12.5% slower than read-byte$ with code-char.

On the other hand, there is no equivalent of peek-char$ for :byte input streams. So, that might be worth considering.

Definitions and Theorems

Theorem: state-p1-of-read-char$

(defthm state-p1-of-read-char$
        (implies (and (state-p1 state)
                      (symbolp channel)
                      (open-input-channel-p1 channel
                                             :character state))
                 (state-p1 (mv-nth 1 (read-char$ channel state)))))

Theorem: open-input-channel-p1-of-read-char$

(defthm
   open-input-channel-p1-of-read-char$
   (implies (and (state-p1 state)
                 (open-input-channel-p1 channel
                                        :character state))
            (open-input-channel-p1
                 channel
                 :character (mv-nth 1 (read-char$ channel state)))))

Theorem: characterp-of-read-char$

(defthm
 characterp-of-read-char$
 (implies (and (mv-nth 0 (read-char$ channel state))
               (state-p1 state)
               (open-input-channel-p1 channel
                                      :character state))
          (characterp (mv-nth 0 (read-char$ channel state))))
 :rule-classes
 (:rewrite
  (:type-prescription
     :corollary
     (implies (and (state-p1 state)
                   (open-input-channel-p1 channel
                                          :character state))
              (or (characterp (mv-nth 0 (read-char$ channel state)))
                  (null (mv-nth 0 (read-char$ channel state))))))))

Theorem: state-preserved-by-read-char$-when-eof

(defthm state-preserved-by-read-char$-when-eof
        (implies (and (not (mv-nth 0 (read-char$ channel state)))
                      (state-p1 state)
                      (open-input-channel-p1 channel
                                             :character state))
                 (equal (mv-nth 1 (read-char$ channel state))
                        state)))