465 lines
18 KiB
Common Lisp
465 lines
18 KiB
Common Lisp
;; 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 . "∧")
|
||
(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 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 "<"
|
||
else if (eq char #\>)
|
||
collect ">"
|
||
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~]"
|
||
"~:[⊥~;⊤~]")
|
||
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))))
|