Major Section: PROGRAMMING
Example: (mv-let (channel state) (open-input-channel "foo.lisp" :object state) (mv-let (eofp obj state) (read-object channel state) (. . (let ((state (close-input-channel channel state))) (mv final-ans state))..)))Also see file-reading-example.
stream. In ACL2, input and output are to or from objects called ``channels,'' which are actually symbols. Although a channel is a symbol, one may think of it intuitively as corresponding to a Common Lisp stream. Channels are in one of two ACL2 packages,
"ACL2-OUTPUT-CHANNEL". When one ``opens'' a file one gets back a channel whose
symbol-nameis the file name passed to ``open,'' postfixed with
nis a counter that is incremented every time an open or close occurs.
There are three channels which are open from the beginning and which cannot be closed:
acl2-input-channel::standard-character-input-0 acl2-input-channel::standard-object-input-0 acl2-input-channel::standard-character-output-0All three of these are really Common Lisp's
For convenience, three global variables are bound to these rather tedious channel names:
*standard-ci* *standard-oi* *standard-co*Common Lisp permits one to open a stream for several different kinds of
io, e.g. character or byte. ACL2 permits an additional type called ``object''. In ACL2 an ``io-type'' is a keyword, either
:object. When one opens a file, one specifies a type, which determines the kind of io operations that can be done on the channel returned. The types
:byteare familiar. Type
:objectis an abstraction not found in Common Lisp. An
:objectfile is a file of Lisp objects. One uses
read-objectto read from
print-object$to print to
:objectfiles. (The reading and printing are really done with the Common Lisp
File-names are strings. ACL2 does not support the Common Lisp type
Here are the names, formals and output descriptions of the ACL2 io functions.
Input Functions: (open-input-channel (file-name io-type state) (mv channel state)) (open-input-channel-p (channel io-type state) boolean) (close-input-channel (channel state) state) (read-char$ (channel state) (mv char/nil state)) (peek-char$ (channel state) boolean) (read-byte$ (channel state) (mv byte/nil state)) (read-object (channel state) (mv eof-read-flg obj-read state))The ``formatting'' functions are particularly useful; see fmt and see cw. In particular,
Output Functions: (open-output-channel (file-name io-type state) (mv channel state)) (open-output-channel-p (channel io-type state) boolean) (close-output-channel (channel state) state) (princ$ (obj channel state) state) (write-byte$ (byte channel state) state) (print-object$ (obj channel state) state) (fms (string alist channel state evisc-tuple) state) (fms! (string alist channel state evisc-tuple) state) (fmt (string alist channel state evisc-tuple) (mv col state)) (fmt! (string alist channel state evisc-tuple) (mv col state)) (fmt1 (string alist col channel state evisc-tuple) (mv col state)) (fmt1! (string alist col channel state evisc-tuple) (mv col state)) (cw (string arg0 arg1 ... argn) nil)
cwprints to a ``comment window'' and does not involve the ACL2
state, so many may find it easier to use than
fmtand its variants. The functions
fmt1!are the same as their respective functions without the ``
!,'' except that the ``
!'' functions are guaranteed to print forms that can be read back in (at a slight readability cost).
When one enters ACL2 with
(lp), input and output are taken from
*standard-co*. Because these are synonyms for
*standard-output*, one can drive ACL2 io off of
arbitrary Common Lisp streams, bound to
*standard-output* before entry to ACL2.
By default, symbols are printed in upper case when vertical bars are not required, as specified by Common Lisp. See set-acl2-print-case for how to get ACL2 to print symbols in lower case.
By default, numbers are printed in radix 10 (base 10).See set-acl2-print-base
for how to get ACL2 to print numbers in radix 2, 8, or 16.