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>) |
|