Major Section: TUTORIAL5-MISCELLANEOUS-EXAMPLES
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
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
(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-file1referred 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)))))