#lang racket/base

(require "../lang/dracula.rkt"
         "../lang/check.rkt"
         "list-utilities.rkt")

(provide (all-defined-out))

(begin-below

 (set-state-ok t)

 (defun file->string (fname state)
   (with-handlers ([exn:fail:filesystem? 
                    (lambda (e) 
                      (list '() 
                            (string-append
                             "Error while opening file for input: "
                             fname)
                            state))])
     (with-input-from-file fname
       (lambda ()
         (let ([str (make-string (file-size fname))])
           (begin (read-string! str)
                  (list str '() state)))))))

 (defun string-list->file (fname strlist state)
   (with-handlers ([exn:fail:filesystem?
                    (lambda (e) 
                      (list (string-append
                             "Error while opening file for output: "
                             fname) 
                            state))])
     (let ([port (open-output-file fname)])
       (begin
         (for ([str (in-list strlist)])
           (write-string str port)
           (newline port))
         (flush-output port)
         (close-output-port port)
         (list '() state)))))

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

 ;;===== 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
 ;;==============================================================================
 (defun dgt->chr (dgt)
   (cond ((equal dgt 0) #\0)
         ((equal dgt 1) #\1)
         ((equal dgt 2) #\2)
         ((equal dgt 3) #\3)
         ((equal dgt 4) #\4)
         ((equal dgt 5) #\5)
         ((equal dgt 6) #\6)
         ((equal dgt 7) #\7)
         ((equal dgt 8) #\8)
         ((equal dgt 9) #\9)
         (t             #\0)))

 ;;====== 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)))             
 ;;==============================================================================
 (defun dgts->chrs (dgts)
   (if (not (consp dgts))
       nil
       (cons (dgt->chr (car dgts))
             (dgts->chrs (cdr dgts)))))

 ;;===== 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
 ;;==============================================================================
 (defun chr->dgt (chr)
   (cond ((equal chr #\0) 0)
         ((equal chr #\1) 1)
         ((equal chr #\2) 2)
         ((equal chr #\3) 3)
         ((equal chr #\4) 4)
         ((equal chr #\5) 5)
         ((equal chr #\6) 6)
         ((equal chr #\7) 7)
         ((equal chr #\8) 8)
         ((equal chr #\9) 9)
         (t               0)))

 ;;====== 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)))             
 ;;==============================================================================
 (defun chrs->dgts (chrs)
   (if (not (consp chrs))
       nil
       (cons (chr->dgt (car chrs))
             (chrs->dgts (cdr chrs)))))

 ;;===== 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))
 ;;==============================================================================
 (defun horner (accumulator x coefficients )
   (if (not (consp coefficients))
       accumulator
       (horner (+ (car coefficients) (* x  accumulator))
               x
               (cdr 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))
 ;;==============================================================================
 (defun dgts->int (dgts)
   (horner 0 10 dgts))

 ;;===== 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)
 ;;==============================================================================
 (defun int->append-dgts (n dgts)
   (if (or (not (integerp n))
           (not (> n 0)))
       dgts
       (int->append-dgts (floor n 10) (cons (mod n 10) dgts))))

 ;;===== 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)
 ;;==============================================================================
 (defun int->dgts (n)
   (int->append-dgts n nil))

 ;;===== 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
 ;;==============================================================================
 (defun str->int (str)
   (dgts->int (chrs->dgts (str->chrs 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)
 ;;==============================================================================
 (defun int->str (n)
   (chrs->str (dgts->chrs (int->dgts 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
 ;;==============================================================================
 (defun str->rat (str)
   (if (or (not (stringp str))
           (string-equal str ""))
       0
       (let* ((chrs (str->chrs str))
              (maybe-sign (car chrs))
              (sans-sign (if (member maybe-sign '(#\+ #\-))
                             (cdr chrs)
                             chrs))
              (parts (break-at #\. sans-sign))
              (int-part (car parts))
              (frc-part (cdr (cadr parts)))
              (int-dgts (chrs->dgts int-part))
              (frc-dgts (chrs->dgts frc-part))
              (r-magnitude  (+ (dgts->int int-dgts)
                               (/ (dgts->int frc-dgts)
                                  (expt 10 (length frc-dgts))))))
         (if (char-equal maybe-sign #\-)
             (- r-magnitude)
             r-magnitude))))

 ;;===== 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
 ;;==============================================================================
 (defun rat->str (r d)
   (if (or (not (rationalp r))
           (= r 0)
           (not (integerp d))
           (< d 0))
       "0"
       (let* ((r-shifted (round (* (abs r) (expt 10 d)) 1))
              (r-chrs (dgts->chrs (int->dgts r-shifted)))
              (n (length r-chrs))
              (num-dgts-before-decimal-pt (max 0 (- n d)))
              (minus-sign-if-needed (if (< r 0) '(#\-) nil)) 
              (parts (break-at-nth num-dgts-before-decimal-pt r-chrs))
              (int-part (car parts))
              (decimal-pt-if-needed (if (> d 0) '(#\.) nil))
              (frc-part (cadr parts)))
         (chrs->str (append minus-sign-if-needed
                            int-part
                            decimal-pt-if-needed
                            (pad-left d #\0 frc-part))))))

 ;;===== (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
 ;;==============================================================================
 (defun read-n-chars (n li channel state)
   (if (or (not (integerp n)) (<= n 0))
       (mv li channel state)
       (mv-let (chr state) (read-char$ channel state)
               (if (null chr)
                   (mv li channel state)
                   (read-n-chars (- n 1) (cons chr li) channel 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
 ;;==============================================================================
 (defun write-all-strings (strli channel state)
   (if (endp strli)
       (mv channel state)
       (let ((state (princ$ (string-append (car strli)
                                           (coerce '(#\newline) 'STRING)) 
                            channel 
                            state)))
         (write-all-strings (cdr strli) channel 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
 ;;==============================================================================
 #|(defun file->string (fname state)
 (mv-let (chli error state)
 (mv-let (channel state) (open-input-channel fname :character state)
 (if (null channel)
 (mv nil
 (string-append "Error while opening file for input: "
 fname)
 state)
 (mv-let (chlist chnl state)
 (read-n-chars 4000000000 '() channel state)
 (let ((state (close-input-channel chnl state)))
 (mv chlist nil state)))))
 (mv (reverse (chrs->str chli)) error state)))|#

 ;;===== (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
 ;;==============================================================================
 #|(defun string-list->file (fname strli state)
 (mv-let (channel state)
 (open-output-channel fname :character state)
 (if (null channel)
 (mv (string-append "Error while opening file for output: " fname)
 state)
 (mv-let (channel state)
 (write-all-strings strli channel state)
 (let ((state (close-output-channel channel state)))
 (mv nil 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>)

 (defun num-noncomments (lines count)
   (if (not (consp lines))
       count
       (let* ((whitespace '(#\Space #\Newline #\Tab))
              (leading-white-stripped (drop-set whitespace (car lines))))
         (if (and (consp leading-white-stripped)
                  (not (char-equal #\; (car leading-white-stripped))))
             (num-noncomments (cdr lines) (+ count 1))
             (num-noncomments (cdr lines) count)))))
 (defun loc-from-file-as-string (str)
   (num-noncomments (packets #\Newline (str->chrs str)) 0))
 (defun loc (file-path state)
   (mv-let (str error state) (file->string file-path state)
           (if error
               (mv error state)
               (mv (loc-from-file-as-string str) state))))

 ;;===== Example functions using file i/o =======================================
 ;;
 ;;  Warning!
 ;;    The variable "state"
 ;;      (1) cannot have any other name
 ;;      (2) can be used only in certain contexts
 ;;
 ;;  Note: You must issue the command
 ;;           (set-state-ok t)
 ;;        before invoking any function that refers to the variable state
 ;;
 ;;  Note: Directory separator in file-path string is "/", not "\"

 ;; (wfoo state)   ; This formula writes the file "C:/foo.wpd"
 ;;                  Well...actually...it's "C:\foo.wpd"
 ;;                  but ACL2 uses Unix conventions in path names

 (defun wfoo (state)
   (mv-let (error state)
           (string-list->file "C:/foo.wpd"
                              (list "this is the first line"
                                    "this is the second line")
                              state)
           (if error
               (mv error state)
               (mv "Write C:/foo.wpd succeeded" state))))

 ;; (rfoo state)   ; This formula reads the file "C:/foo.wpd"
 ;;                  Well...actually...it's "C:\foo.wpd"
 ;;                  but ACL2 uses Unix conventions in path names

 (defun formula-for-rfoo-result (str)
   (string-append "input file as string follows: " str))

 (defun rfoo (state)
   (mv-let (str error state) (file->string "C:/foo.wpd" state)
           (if error
               (mv error state)
               (mv (formula-for-rfoo-result str) state))))

 ;; (rwfoobar state)  ; This formula reads the file "C:/foo.wpd"
 ;;                     then writes the file "C:/bar.wpd"
 ;;                     Well...actually...it's "C:\foo.wpd" and "C:\bar.wpd"
 ;;                     but ACL2 uses Unix conventions in path names

 (defun rwfoobar (state)
   (mv-let (input-as-string error-open state) (file->string "C:/foo.wpd" state)
           (if error-open
               (mv error-open state)
               (mv-let (error-close state)
                       (string-list->file "C:/bar.wpd"
                                          (list "c:/foo.wpd follows:"
                                                input-as-string)
                                          state)
                       (if error-close
                           (mv error-close state)
                           (mv "Success: read c:/foo.wpd, wrote c:/bar.wpd"
                               state))))))

 ;; (map-chrs->str list-list-chrs)  ; This formula applies chrs->str to
 ;;                                 ;   each element in a list in which each
 ;;                                 ;   element is a list of characters
 ;;                                 ; Thus, a list of lists of characters
 ;;                                 ;   becomes a list of strings

 (defun map-chrs->str (list-list-chrs)
   (if (consp list-list-chrs)
       (cons (chrs->str (car list-list-chrs))
             (map-chrs->str (cdr list-list-chrs)))
       nil))

 ;; (your-computation str)  ; This formula converts a string to a list strings
 ;;                         ;   each of which is a substring of str filling in
 ;;                         ;   the gap between two newline-characters
 ;;                         ; In a real program, this function would do a
 ;;                         ;   more elaborate computation, to carry out
 ;;                         ;   whatever transformation you intended your
 ;;                         ;   program to do, and then it would represent the
 ;;                         ;   results of th comptutation as a list of strings

 (defun your-computation (str)
   (map-chrs->str (packets #\Newline (str->chrs str))))

 ;; (ipo f-in f-out state)  ; This formula uses the function file->string reads
 ;;                         ;   the file f-in, producing a string containing all
 ;;                         ;   the characters in the file
 ;;                         ; Then it invokes the function "your-computation"
 ;;                         ;   to transform the string to a list of strings
 ;;                         ; Finally, it writes the list of strings delivered
 ;;                         ;   by your-computation to a file named f-out,
 ;;                         ;   one string per line
 ;;                         ; USING THIS INPUT/PROCESS/OUTPUT TEMPLATE
 ;;                             Copy the defun for ipo,
 ;;                         ;   change its name to something appropriate,
 ;;                         ;   define a new function to do the computation
 ;;                         ;   you are working on (note: your the input to
 ;;                         ;   your function will be a string consisting
 ;;                         ;   of all the characters from your input file,
 ;;                         ;   and the output must be a list of strings,
 ;;                         ;   one string for each line you want in your
 ;;                         ;   output file), and, finally,
 ;;                         ;   replace the invocation of "your-computation"
 ;;                         ;   by an invoction of the function you defined
 ;;                         ; Warning! The input file f-in must be a text-file
 ;;                         ;   with Unix-style line separators
 ;;                         ;   (You can convert DOS-style files to Unix-style
 ;;                         ;   with the dos2unix program.)
 ;;                         ; Warning! The strings f-in and f-out must be
 ;;                         ;   Unix-style file-path specs, with forward slashes
 ;;                         ;   not Windows-style back slashes
 ;;                         ;   For example, "C:/yourfolder/yourfile.wpd",
 ;;                         ;            not "C:\yourfolder\yourfile.wpd"
 ;;                         ; Warning! The third parameter of ipo cannot be
 ;;                         ;   any symbol other than the symbol whose name
 ;;                         ;   is "state"
 ;;                         ; Warning! Before invoking this function from an
 ;;                         ;   ACL2 session, you must issue these commands:
 ;;                         ;   (set-state-ok t)
 ;;                         ;   :comp read-n-chars
 ;;                         ;   :comp write-all-strings

 (defun ipo (f-in f-out state)
   (mv-let (input-as-string error-open state) (file->string f-in state)
           (if error-open
               (mv error-open state)
               (mv-let (error-close state)
                       (string-list->file f-out
                                          (your-computation input-as-string)
                                          state)
                       (if error-close
                           (mv error-close state)
                           (mv (string-append
                                "Read "
                                (string-append
                                 f-in
                                 (string-append ", compute, then write " f-out)))
                               state))))))
 ;;===== end of example functions ===============================================

 )