		Search-engine friendly clone of the ACL2 documentation.

Std/io/read-object

Read one object from an open :object stream.

Signature: (read-object channel state-state) returns (mv eofp obj state).

channel is a symbol that must refer to an open :object 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 use the Lisp reader to try to read an object from the Lisp input stream that is associated with channel.

Ideally, the input stream contains well-formed S-expressions that are free of "bad" objects like 0.75, symbols from packages that ACL2 doesn't know about, etc; see About Types. In this case, read-object reads the first S-expression in the file and returns it as obj, setting eofp to nil. If there are no more S-expressions in the file, eofp is t and obj is nil.

But the input stream can also be malformed. For instance, we might encounter malformed S-expressions without enough closing parens, or bad objects like 0.75. These sorts of problems will cause hard errors or raw Lisp errors!

Note that if the input contains plain symbols without explicit package name prefixes, e.g., foo instead of acl2::foo, then these symbols will be treated as coming from the current package. If that isn't what you want, you can explicily call in-package to switch into whatever package you want to be the default. For example, if the file temp contains exactly:

foo

Then the following book:

(in-package "ACL2")
(include-book "std/util/bstar" :dir :system)
(include-book "centaur/vl/portcullis" :dir :system)

(make-event
 (b* (((mv ?err ?val state) (in-package "VL"))
      ((mv channel state)   (open-input-channel "temp" :object state))
      ((mv ?eofp obj state) (read-object channel state))
      (state                (close-input-channel channel state)))
   (value `(defconst *foo* ',obj))))

Defines *foo* as the symbol vl::foo, instead of acl2::foo.

Definitions and Theorems

Theorem: state-p1-of-read-object

(defthm state-p1-of-read-object
        (implies (and (state-p1 state)
                      (symbolp channel)
                      (open-input-channel-p1 channel
                                             :object state))
                 (state-p1 (mv-nth 2 (read-object channel state)))))

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

(defthm
     open-input-channel-p1-of-read-object
     (implies (and (state-p1 state)
                   (open-input-channel-p1 channel
                                          :object state))
              (open-input-channel-p1
                   channel
                   :object (mv-nth 2 (read-object channel state)))))

Theorem: state-preserved-by-read-object-when-eof

(defthm state-preserved-by-read-object-when-eof
        (implies (and (mv-nth 0 (read-object channel state))
                      (state-p1 state)
                      (open-input-channel-p1 channel
                                             :object state))
                 (equal (mv-nth 2 (read-object channel state))
                        state)))