2.5 "io-utilities"

(include-book "io-utilities" :dir :teachpacks)

Documentation under construction.

;;===== Module: io-utilities ===================================================

;;

;; Defining

;;   string-list->file        write file

;;   file->string             read file

;;   rat->str                 convert rational number to string

;;   str->rat                 convert string to rational number

;;   loc                      report LoC for specified file

;;

;; (string-list->file file-path list-of-strings state)

;;    Produces effect of writing strings to specified file, in sequence

;;    with newline-characters added at the end of each string

;;    Note: Directory separator in file-path string must be "/", not "\"

;;    Note: "Example functions" section shows how to use this function

;;          See: (wfoo state), (rwfoobar state)

;;    Note: Returns multiple value containing error status and state

;;

;; (file->string file-path state)

;;    delivers (mv string state) where string contains all characters in file

;;    Note: Directory separator in file-path string must be "/", not "\"

;;    Note: "Example functions" section shows how to use this function

;;          See: (rfoo state), (rwfoobar state)

;;    Note: Returns multiple value containing characters from file as

;;          string, error status, and state

;;    Warning! Virtual memory might be exhausted by reading really big files

;;

;; (rat->str r d)

;;     delivers string containing decimal representation of a rational

;;     number, r, with d decimal places digits following the decimal point

;;

;; (str->rat str)

;;    delivers rational number represented by str, a string of decimal digits,

;;    possibly containing a decimal point, and possibly with a leading +/- sign

;;

;; (loc file-path state)

;;    Reports number of lines of code in file specified by file-path (a string)

;;    Also reports state, which is annoying

;;==============================================================================

;;===== Function: (dgt->chr dgt) ===============================================

;;

;;  Converts integer in 0-9 range to digit-character

;;

;;  Pre : (member-equal dgt '(0 1 2 3 4 5 6 7 8 9))

;;  Post: (member-equal (dgt->chr dgt)

;;                      '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)

;;  Note: defaults to #\0 if dgt is not a one-digit, nonnegative integer

;;==============================================================================

;;====== Function: (dgts->chrs dgts) ===========================================

;;

;;  Converts every digit in a list to the corresponding character

;;

;;  Pre : (and (integer-listp dgts)

;;             (implies (and (integerp d) (member d dgts))

;;                      (member d '(0 1 2 3 4 5 6 7 8 9)))

;;  Post: (implies (and (characterp c) (member c (dgts->char dgts)))

;;                 (member c (#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)))

;;==============================================================================

;;===== Function: (chr->dgt dgt-chr) ===========================================

;;

;;  Converts a digit-character to the corresponding one-digit integer

;;

;;  Pre : (member-equal dgt-chr '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9))

;;  Post: (member (char->dgt dgt-chr) '(0 1 2 3 4 5 6 7 8 9))

;;  Note: defaults to 0 if dgt-chr is not a digit character

;;==============================================================================

;;====== Function: (chrs->dgts chrs) ===========================================

;;

;;  Converts every digit in a list to the corresponding character

;;

;;  Pre : (and (character-listp chrs)

;;             (implies (and (characterp c) (member c chrs))

;;                      (member c '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9))

;;  Post: (implies (and (integerp d) (member d (chrs->dgts chrs)))

;;                 (member d '(0 1 2 3 4 5 6 7 8 9)))

;;==============================================================================

;;===== Function: (horner s x coefficients) ====================================

;;

;;  Computes s*(x^n) + polynomial in x with given coefficients

;;    where n = (length coefficients)

;;  Note: Coefficient list ordering is high-order to low-order

;;        That is, (nth k coefficients) is coefficient of x^(n - k - 1)

;;        where n = (length coefficients) - 1, k = 0, 1, ... n-1

;;

;;  Pre : (and (numberp s) (numberp x) (number-listp coefficients))

;;  Post: (integerp (horner s x coefficients))

;;==============================================================================

;;===== Function: (dgts->int dgts) =============================================

;;

;;  Delivers integer whose decimal digits comprise dgts (high-order to low-order)

;;

;;  Pre : (implies (member-equal d dgts)

;;                 (member-equal d '(0 1 2 3 4 5 6 7 8 9)))

;;  Post: (and (integerp (dgts->int dgts))

;;             (>= (dgts->int dgts) 0))

;;==============================================================================

;;===== Function: (int->append-dgts n dgts) ====================================

;;

;;  Append dgts to digits of decimal representation of n

;;

;;  Pre:  (and (integerp n) (>= n 0)

;;             (implies (member-equal d dgts)

;;                      (member-equal d '(0 1 2 3 4 5 6 7 8 9))))

;;  Post: (equal (dgts->int (int->append-dgts n nil))

;;               n)

;;==============================================================================

;;===== Function: (int->dgts n) ================================================

;;

;;  Deliver digits of decimal representation of n

;;

;;  Pre:  (and (integerp n) (>= n 0))

;;  Post: (equal (dgts->int (int->dgts n))

;;               n)

;;==============================================================================

;;===== Function: (str->int str) ===============================================

;;

;;  Returns integer represented by string

;;

;;  Pre:  (implies (member-equal chr (str->chrs str))

;;                 (member-equal chr '(#\0 #\1 #\2 ... #\9)))

;;  Post: (str->int str) is the integer specifed, in decimal notation, in str

;;==============================================================================

;;===== Function: (int->str n) =================================================

;;

;;  Returns string containing decimal representation of n

;;

;;  Pre:  (and (integerp n)

;;             (>= n 0))

;;  Post: (equal (str->int (int->str n))

;;               n)

;;==============================================================================

;;===== Function: (str->rat str) ===============================================

;;

;;  Returns number whose decimal representation is str

;;

;;  Pre:  (and (implies (member chr (str->chrs str))

;;                      (or (member chr '(#\0 #\1 #\2 ... #\9))

;;                          (equal chr #\+)

;;                          (equal chr #\-)

;;                          (equal chr #\.))

;;             (not (member #\+ (drop-past #\+ (str->chrs str))))

;;             (not (member #\- (drop-past #\+ (str->chrs str))))

;;             (not (member #\- (drop-past #\- (str->chrs str))))

;;             (not (member #\+ (drop-past #\- (str->chrs str)))))

;;  Post: (and (rationalp (str->rat str))

;;             (= (str->rat str)

;;                (str->rat (rat->str (str->rat str) (length str)))))

;;  Note: (equal (str->rat nil) 0)

;;  Note: Defaults to zero if str does not meet expectations

;;==============================================================================

;;===== Function: (rat->str r d) ===========================================

;;

;;  Returns string containing decimal representation of r, to d decimal places

;;

;;  Pre:  (and (rationalp r)

;;             (integerp d)

;;             (>= d 0))

;;  Post: (<= (abs(- (str->rat (rat->str r d))

;;                    r))

;;            (/ 5 (expt 10 (+ d 1))))

;;  Note: Defaults to "0" if parameters fail to meet expectations

;;==============================================================================

;;===== (read-n-chars n li channel state) ======================================

;;

;;  Inserts up to n characters from channel into li, leaving the new characters

;;  at the beginning of li in the reverse of the order in they were received in

;;

;;  Pre : (and (integerp n)

;;             (>= n 0)

;;             (character-listp li)

;;             (character-input-channelp channel))

;;  Post: Up to n characters have been received from channel

;;        Returns multiple value containing list of chars, channel, and state

;;==============================================================================

;;===== (write-all-strings strli channel state) ================================

;;

;;  Writes characters from each string in strli to channel

;;  (inserting a newline after the characters comprising each element of strli)

;;

;;  Pre : (and (string-listp strli)

;;             (character-input-channelp channel))

;;  Post: channel has received chars from strings in strli, plus newlines

;;        Returns multiple value containing channel and new state

;;==============================================================================

;;===== (file->string file-path state) =========================================

;;

;;  Makes character sequence comprising file accessible as string

;;

;;  Pre : (character-listp file-path)

;;  Post: Characters in file become accessible as string portion

;;          of returned multiple value

;;        Returns multiple value:

;;          (1) string comprising first million characters from file

;;          (2) status (nil indicates success)

;;          (3) state

;;  Warning! System may run out of virtual memory when reading large files

;;  Warning! This function will not read files exceeding about 4GB

;;==============================================================================

;;===== (string-list->file list-of-strings file-path state) ====================

;;

;;  Writes strings to specified file, in sequence, and with

;;  newline characters added at the end of each string

;;

;;  Pre:  (and (string-listp list-of-strings)

;;             (character-listp file-path))

;;  Post: Designated file contains characters from list-of-strings

;;          with newline characters inserted

;;        Returns multiple value:

;;          (1) status (nil indicates success)

;;          (2) state

;;==============================================================================

;;===== (loc file-path state) ==================================================

;;

;;  Reports number of lines of code in file specified by file-path (a string)

;;  Also reports state, which is annoying

;;

;; Note: Lines consisting entirely of commentary or whitespace

;;       are not counted as lines of code

;; Warning! Unix-style path names required ("dir/nam", not "dir\nam")

;; WARNING! The input file must use Unix-style line-terminators.

;;          If you created the file using Notepad or Wordpad,

;;          you must convert it to Unix style, which you can do like this:

;;             dos2unix "some-program.lisp"

;;          Of course, you'll need to convet the file back to Windows style

;;          (unix2dos) when you want to edit it

;; Sample usage:

;; First:

;;   Copy file to be LoC-counted to a convenient place and convert to

;;   Unix-style line terminators, eg by using the following DOS commands

;;   copy "c:\Program Files\ACL2-2.8\Sources\Books\SE\io-utilities.lisp" c:\

;;   dos2unix c:\io-utilities.lisp

;; Then, in an ACL2 session:

;;   (include-book "C:/Program Files/ACL2-2.8/sources/books/SE/io-utilities")

;;   (set-state-ok t)

;;   :comp read-n-chars ; Warning! This cmd is for sessions only, not books

;;   (loc "c:/io-utilities.lisp" state)

;; Response in ACL2 session:

;;   (177 <state>)