;; typeset.lisp -- Typeset proposition tables
;; Copyright (C) 2024  Alexander Rosenberg
;;
;; This program is free software: you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation, either version 3 of the License, or
;; (at your option) any later version.
;;
;; This program is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;; GNU General Public License for more details.
;;
;; You should have received a copy of the GNU General Public License
;; along with this program.  If not, see <https://www.gnu.org/licenses/>.
(in-package :truth-table/base)

(define-condition table-format-error (error)
  ((format :initarg :format
           :accessor table-format-error-format))
  (:report
   (lambda (con stream)
     (format stream "unknown table format: ~a"
             (table-format-error-format con)))))

(defparameter *operator-ascii-lookup-alist*
  '((and . "&")
    (nand . "nand")
    (or . "|")
    (nor . "nor")
    (xor . "^")
    (not . "~")
    (implies . "->")
    (converse . "<-")
    (iff . "<->")
    (open-paren . "(")
    (close-paren . ")")
    (true . "T")
    (false . "F")
    (latin-true . "T")
    (latin-false . "F"))
  "Lookup table mapping operators to their ASCII representation.")

(defparameter *operator-unicode-lookup-alist*
  '((and . "∧")
    (nand . "⊼")
    (or . "∨")
    (nor . "⊽")
    (xor . "⊕")
    (not . "¬")
    (implies . "→")
    (converse . "←")
    (iff . "↔")
    (open-paren . "(")
    (close-paren . ")")
    (true . "⊤")
    (false . "⊥")
    (latin-true . "T")
    (latin-false . "F"))
  "Lookup table mapping operators to their Unicode representation.")

(defparameter *operator-latex-lookup-alist*
  '((and . "\\land")
    (nand . "\\uparrow")
    (or . "\\lor")
    (nor . "\\downarrow")
    (xor . "\\oplus")
    (not . "\\lnot ")
    (implies . "\\to")
    (converse . "\\gets")
    (iff . "\\leftrightarrow")
    (open-paren . "\\left(")
    (close-paren . "\\right)")
    (true . "\\top")
    (false . "\\bot")
    (latin-true . "\\textrm{T}")
    (latin-false . "\\textrm{F}"))
  "Lookup table mapping operators to their LaTeX representation.")

(defparameter *operator-html-lookup-alist*
  '((and . "&and;")
    (nand . "&uarr;")
    (or . "&or;")
    (nor . "&darr;")
    (xor . "&oplus;")
    (not . "&not;")
    (implies . "&rarr;")
    (converse . "&larr;")
    (iff . "&harr;")
    (open-paren . "(")
    (close-paren . ")")
    (true . "&top;")
    (false . "&perp;")
    (latin-true . "T")
    (latin-false . "F"))
  "Lookup table mapping operators to their HTML representation.")

(defun latex-var-name-transform (name)
  "Transform NAME so that it is escaped for use in LaTeX."
  (format nil "{~{~A~}}" (loop for char across name
                               if (eq char #\\)
                                 collect "\\backslash "
                               else if (eq char #\_)
                                      collect "\\_"
                               else if (eq char #\$)
                                      collect "\\$"
                               else
                                 collect char)))

(defun html-var-name-transform (name)
  "Transform NAME so that it is escaped for use in HTML."
  (format nil "~{~A~}" (loop for char across name
                             if (eq char #\<)
                               collect "&lt;"
                             else if (eq char #\>)
                                    collect "&gt;"
                             else
                               collect char)))

(defun flattenable-p (oper)
  "Return t if OPER is able to be flattened. That is, it does not care a bout
argument ordering."
  (multiple-value-bind (min max)
      (operator-argument-count oper)
    (declare (ignorable min))
    ;; currently, all unordered operators take any number of arguments max, and
    ;; all ordered operators have some max number of arguments (as a
    ;; proposition: an operator is unordered if and only if it takes any number
    ;; of arguments)
    (not max)))

(defun flatten-proposition (prop)
  "Flatten PROP, such that adjacent operators with the same precedence and with
no ordering (such as \"and\" or \"or\") are not surrounded by parenthesis when
typeset."
  (if (consp prop)
      (loop with my-oper = (car prop)
            for raw-sub-expr in (cdr prop)
            for sub-expr = (flatten-proposition raw-sub-expr)
            when (and (flattenable-p my-oper)
                      (consp sub-expr)
                      (eq (car sub-expr) my-oper))
              append (cdr sub-expr) into out-args
            else
              collect sub-expr into out-args
            finally (return (cons my-oper out-args)))
      prop))

(defun typeset-proposition (expr &key
                                   (lookup-table *operator-ascii-lookup-alist*)
                                   var-name-transform
                                   (parent-prec most-positive-fixnum)
                                   latin-truths
                                   (flatten-prop t))
  "Typeset the propositional expression EXPR to plain text.  LOOKUP-TABLE should
be a table mapping operators to their textual representation. VAR-NAME-TRANSFORM
(if non-nil) should take a single string argument which is a variable name and
escape it for use in the target typesetting system. PARENT-PERC is for internal
use (it controls when parentheses are applied.)"
  (cond
    ;; expr is empty
    ((null expr)
     "")
    ;; expr is a variable name
    ((stringp expr)
     (if var-name-transform 
         (funcall var-name-transform expr)
         expr))
    ;; expr is true or false
    ((eq expr 'true)
     (if latin-truths
         (cdr (assoc 'latin-true lookup-table))
         (cdr (assoc 'true lookup-table))))
    ((eq expr 'false)
     (if latin-truths
         (cdr (assoc 'latin-false lookup-table))
         (cdr (assoc 'false lookup-table))))
    ;; expr is a compound expression
    (t
     (destructuring-bind (oper first-arg &rest args)
         (if flatten-prop
             (flatten-proposition expr)
             expr)
       (let* ((our-prec (operator-precedence oper))
              (oper-ascii (cdr (assoc oper lookup-table)))
              (prefix-suffix (if (<= parent-prec our-prec)
                                 (cons (cdr (assoc 'open-paren lookup-table))
                                       (cdr (assoc 'close-paren lookup-table)))
                                 '("" . ""))))
         (if (null args)
             ;; we have one argument
             (format nil "~A~A~A~A" (car prefix-suffix) oper-ascii
                     (typeset-proposition first-arg
                                          :lookup-table lookup-table
                                          :var-name-transform var-name-transform
                                          :latin-truths latin-truths
                                          :parent-prec our-prec
                                          :flatten-prop nil)
                     (cdr prefix-suffix))
             ;; we have many arguments
             (loop for arg in args
                   collect oper-ascii into output
                   collect
                   (typeset-proposition arg
                                        :lookup-table lookup-table
                                        :var-name-transform var-name-transform
                                        :latin-truths latin-truths
                                        :parent-prec our-prec
                                        :flatten-prop nil)
                     into output
                   finally
                      (push (typeset-proposition first-arg
                                                 :lookup-table lookup-table
                                                 :var-name-transform var-name-transform
                                                 :latin-truths latin-truths
                                                 :parent-prec our-prec
                                                 :flatten-prop nil)
                            output)
                      (return (format nil "~A~{~A~^ ~}~A" (car prefix-suffix)
                                      output (cdr prefix-suffix))))))))))

(defun convert-truth-table-to-latex (table &key pretty-print latin-truths)
  "Convert TABLE, which should be a truth table as returned by
`create-truth-table' to latex. If PRETTY-PRINT, add newlines to make the
generated code easier to read.
NOTE: though the overall order does not matter, the order must be the same
between each row."
  (let ((typeset-exprs (mapcar (lambda (expr)
                                 (typeset-proposition
                                  expr :lookup-table *operator-latex-lookup-alist*
                                       :var-name-transform 'latex-var-name-transform
                                       :latin-truths latin-truths))
                               (extract-truth-table-expressions table))))
    (with-output-to-string (str)
      (format str "~
\\begin{tabular}{~{~*|c~}|}~@[~%  ~*~]~
  \\hline~:[ ~;~%  ~]~
  ~{$ ~A $~^ & ~} \\\\~:[ ~;~%  ~]~
  \\hline~:[ ~;~%  ~]"
              typeset-exprs
              pretty-print pretty-print
              typeset-exprs
              pretty-print pretty-print)
      (let ((format-str
              (if latin-truths
                  "~{~:[F~;T~]~^ & ~} \\\\~:[ ~;~%  ~]"
                  "~{$ ~:[\\bot~;\\top~] $~^ & ~} \\\\~:[ ~;~%  ~]")))
        (dolist (row (extract-truth-table-values table))
          (format str format-str row pretty-print)))
      (format str "\\hline~@[~%~]\\end{tabular}" pretty-print))))

(defun format-html-properties-alist (props)
  "Format PROPS, a list of conses, as a list of HTML properties."
  (loop for (name . value) in props
        when (eq value t)
          collect (format nil "~A=\"\"" name)
        else when value
               collect (format nil "~A=~S" name (princ-to-string value))))


(defun convert-truth-table-to-html (table &key class id more-props
                                            pretty-print latin-truths)
  "Convert TABLE, which should be a truth table as returned by
`create-truth-table' to HTML. CLASS and ID are their respective HTML
properties. MORE-PROPS is an alist mapping properties to values.
NOTE: though the overall order does not matter, the order must be the same
between each row."
  (with-output-to-string (str)
    (format str "<table~@[ class=~s~]~@[ id=~s~]~{ ~A~}>~@[~%  ~*~]<tr>"
            class id (format-html-properties-alist more-props)
            pretty-print)
    (dolist (expr (extract-truth-table-expressions table))
      (format str "~@[~%    ~*~]<th>~a</th>"
              pretty-print
              (typeset-proposition
               expr :lookup-table *operator-html-lookup-alist*
               :var-name-transform 'html-var-name-transform
               :latin-truths latin-truths)))
    (format str "~@[~%  ~]</tr>" pretty-print)
    (dolist (row (extract-truth-table-values table))
      (format str "~@[~%  ~*~]<tr>~@[~%    ~*~]" pretty-print pretty-print)
      (loop with truth-str = (if latin-truths
                                 "~:[F~;T~]"
                                 "~:[&perp;~;&top;~]")
            for now = row then (cdr now)
            for value = (car now)
            while now do
              (format str "<td>~?</td>" truth-str (list value))
            when (and pretty-print (cdr now)) do
              (format str "~%    "))
      (format str "~@[~%  ~*~]</tr>" pretty-print))
    (format str "~@[~%~]</table>" pretty-print)))

(defparameter *table-border-ascii-alist*
  '((vertical . #\|)
    (horizontal . #\-)
    (right . #\|)
    (left . #\|)
    (up . #\-)
    (down . #\-)
    (cross . #\+)
    (top-left . #\+)
    (top-right . #\+)
    (bottom-left . #\+)
    (bottom-right . #\+))
  "Characters used to draw ASCII table borders.")

(defparameter *table-border-unicode-alist*
  '((vertical . #\│)
    (horizontal . #\─)
    (right . #\├)
    (left . #\┤)
    (up . #\┴)
    (down . #\┬)
    (cross . #\┼)
    (top-left . #\┌)
    (top-right . #\┐)
    (bottom-left . #\└)
    (bottom-right . #\┘))
  "Characters used to draw Unicode table borders.")

(defun typeset-table-break (stream lengths horiz start column end
                            &key (left-pad-len 0) (right-pad-len 0))
  "Typeset the first row, the last row, or a break to STREAM. The proper box
character will be placed at each intersection. LENGTHS is a list of column
lengths. HORIZ, START, COLUMN, and END are the box characters to use when
drawing."
  (format stream "~c" start)
  (loop for (length . rest) = lengths then rest
        while length
        do
           (format stream "~a"
                   (make-string (+ left-pad-len length right-pad-len)
                                :initial-element horiz))
        when rest do
          (format stream "~c" column))
  (format stream "~c" end))

(defun typeset-table-row (stream lengths row vert
                          &key (align :center) (left-pad-str "")
                            (right-pad-str ""))
  "Typeset ROW to STREAM. VERT is the vertical separator. LENGTHS should be the
length of each column."
  (loop with format = (case align
                        (:right
                         "~c~a~v:<~a~>~a")
                        (:left
                         "~c~a~v@<~a~>~a")
                        (t ;; :center
                         "~c~a~v:@<~a~>~a"))
        for col in row
        for length in lengths
        do
           (format stream format
                   vert left-pad-str length col right-pad-str))
  (format stream "~c" vert))

(defmacro with-draw-table ((stream col-widths lookup-table
                            &key (padding 0) (align :center))
                           &body body)
  "Execute BODY with the function \=:seperator and \=:row bound. STREAM is the
stream to write the table to. COL-WIDTHS is a list of column
widths. LOOKUP-TABLE is the table to use to lookup characters for the table
border. PADDING is the number to spaces to both append and prepend to each table
cell. ALIGN is one of \=:right, \=:center, or \=:left."
  (let ((pad-str-var (gensym)))
    `(let ((,pad-str-var (make-string ,padding :initial-element #\space)))
       (truth-table/base::typeset-table-break
        ,stream ,col-widths
        (cdr (assoc 'horizontal ,lookup-table))
        (cdr (assoc 'top-left ,lookup-table))
        (cdr (assoc 'down ,lookup-table))
        (cdr (assoc 'top-right ,lookup-table))
        :right-pad-len ,padding
        :left-pad-len ,padding)
       (format ,stream "~%")
       (flet ((:seperator ()
               (truth-table/base::typeset-table-break
                ,stream ,col-widths
                (cdr (assoc 'horizontal ,lookup-table))
                (cdr (assoc 'right ,lookup-table))
                (cdr (assoc 'cross ,lookup-table))
                (cdr (assoc 'left ,lookup-table))
                :right-pad-len ,padding
                :left-pad-len ,padding)
               (format ,stream "~%"))
              (:row (row)
               (truth-table/base::typeset-table-row
                ,stream ,col-widths row 
                (cdr (assoc 'vertical ,lookup-table))
                :align ,align
                :left-pad-str ,pad-str-var
                :right-pad-str ,pad-str-var)
               (format ,stream "~%")))
         ,@body)
       (truth-table/base::typeset-table-break
        ,stream ,col-widths
        (cdr (assoc 'horizontal ,lookup-table))
        (cdr (assoc 'bottom-left ,lookup-table))
        (cdr (assoc 'up ,lookup-table))
        (cdr (assoc 'bottom-right ,lookup-table))
        :right-pad-len ,padding
        :left-pad-len ,padding))))

(defun typeset-truth-table (table &optional
                                    (expr-lookup-table
                                     *operator-ascii-lookup-alist*)
                                    (box-lookup-table
                                     *table-border-ascii-alist*)
                                    latin-truths)
  "Convert TABLE, which should be a truth table as returned by
`create-truth-table' to text.
NOTE: though the overall order does not matter, the order must be the same
between each row."
  (let* ((typeset-exprs (mapcar (lambda (expr)
                                  (typeset-proposition
                                   expr :lookup-table expr-lookup-table
                                   :latin-truths latin-truths))
                                (extract-truth-table-expressions table)))
         (col-widths (mapcar 'length typeset-exprs)))
    (with-output-to-string (str)
      (with-draw-table (str col-widths box-lookup-table
                        :padding 1)
        (:row typeset-exprs)
        (:seperator)
        (dolist (row (extract-truth-table-values table))
          (:row (mapcar
                 (lambda (entry)
                   (cdr (assoc
                         (if entry
                             (if latin-truths
                                 'latin-true
                                 'true)
                             (if latin-truths
                                 'latin-false
                                 'false))
                         expr-lookup-table)))
                 row)))))))

(defparameter *known-formats*
  '("unicode" "ascii" "latex" "html")
  "The known formats that `typeset-table-to-format' can take.")

(defun typeset-table-to-format (table format
                                &key pretty-print latin-truths)
  "Typeset TABLE into FORMAT, or error if FORMAT is not a know format."
  (cond 
    ((equal format "unicode")
     (typeset-truth-table table *operator-unicode-lookup-alist*
                          *table-border-unicode-alist*
                          latin-truths))
    ((equal format "ascii")
     (typeset-truth-table table *operator-ascii-lookup-alist*
                          *table-border-ascii-alist*
                          latin-truths))
    ((equal format "latex")
     (convert-truth-table-to-latex table
                                   :pretty-print pretty-print
                                   :latin-truths latin-truths))
    ((equal format "html")
     (convert-truth-table-to-html table
                                  :pretty-print pretty-print
                                  :latin-truths latin-truths))
    (t (error 'table-format-error :format format))))