#lang scheme/base

(require "../lang/dracula.ss")
(require "list-utilities.ss")

(provide (all-defined-out))

(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 ===============================================