File-reading-example
Example of reading files in ACL2
This example illustrates the use of ACL2's io primitives to
read the forms in a file. See io.
This example provides a solution to the following problem. Let's say that
you have a file that contains s-expressions. Suppose that you want to build a
list by starting with nil, and updating it ``appropriately'' upon
encountering each successive s-expression in the file. That is, suppose that
you have written a function update-list such that (update-list obj
current-list) returns the list obtained by ``updating'' current-list
with the next object, obj, encountered in the file. The top-level
function for processing such a file, returning the final list, could be
defined as follows. Notice that because it opens a channel to the given file,
this function modifies state and hence must return state. Thus
it actually returns two values: the final list and the new state.
(defun process-file (filename state)
(mv-let
(channel state)
(open-input-channel filename :object state)
(mv-let (result state)
(process-file1 nil channel state) ;see below
(let ((state (close-input-channel channel state)))
(mv result state)))))
The function process-file1 referred to above takes the currently
constructed list (initially, nil), together with a channel to the file
being read and the state, and returns the final updated list. Notice
that this function is tail recursive. This is important because many Lisp
compilers will remove tail recursion, thus avoiding the potential for stack
overflows when the file contains a large number of forms.
(defun process-file1 (current-list channel state)
(mv-let (eofp obj state)
(read-object channel state)
(cond
(eofp (mv current-list state))
(t (process-file1 (update-list obj current-list)
channel state)))))
As an exercise, you might want to add guards to the functions above
and verify the guards (see verify-guards). See args or make a
call of the form (guard 'your-function nil (w state)) to see the guard of
an existing function.
