truth-table/truth-table.lisp

;; truth-table.lisp -- Generate truth tables from proposition strings
;; 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/>.
#+slynk (ql:quickload '(:uiop :with-user-abort) :silent t)

(defpackage :truth-table
  (:use :cl)
  (:export :toplevel))

(in-package :truth-table)

(defun whitespace-p (char)
  "Return nil unless CHAR is whitespace."
  (member char '(#\newline #\space) :test 'eq))

(defun paren-p (char)
  "Return nil unless CHAR is a parenthesis."
  (member char '(#\( #\))))

(defun delim-p (char)
  "Return nil unless CHAR is either whitespace or a parenthesis."
  (or (whitespace-p char) (paren-p char)))

(defun symbol-char-p (char)
  "Return nil until CHAR is a valid character for use in proposition variable
names."
  (or (alpha-char-p char) (eq char #\_) (digit-char-p char)))

(defun replace-in-string (str chars new-char)
  "Replace all instances of any of CHARS in STR with NEW-CHAR."
  (coerce (loop with lchars = (if (atom chars)
                                  (list chars)
                                  chars)
                for char across str
                when (member char lchars)
                  collect new-char
                else
                  collect char)
          'string))

(define-condition proposition-parse-error (error)
  ((position :initarg :position
             :accessor parse-error-position
             :initform nil)
   (proposition :initarg :proposition
                :accessor parse-error-proposition
                :initform nil)
   (message :initarg :message
            :accessor parse-error-message
            :initform nil))
  (:report (lambda (con stream)
             (with-slots (position proposition message) con
               (format stream
                       "parse error~@[ at column ~d~]~@[: ~a~]~
                          ~@[:~%  ~a~@[~%  ~a^~]~]"
                       (when position
                         (1+ position))
                       message
                       (when proposition
                         (replace-in-string proposition 
                                            '(#\newline #\return)
                                            #\space))
                       (when position
                         (make-string position
                                      :initial-element #\space))))))
  (:documentation "Condition representing an error during parsing of a
proposition."))

(define-condition proposition-eval-error (error)
  ((message :initarg :message
            :accessor proposition-eval-error-message)
   (proposition :initarg :proposition
                :accessor proposition-eval-error-proposition
                :initform nil))
  (:report (lambda (con stream)
             (with-slots (message proposition)
                 con
               (format stream "~a~@[:~%  ~a~]"
                       message proposition))))
  (:documentation "Condition representing an error that occurred during
evaluation for a proposition."))

(define-condition command-line-error (error)
  ((message :initarg :message
            :accessor command-line-error-message))
  (:report (lambda (con stream)
             (format stream "~a"
                     (command-line-error-message con))))
  (:documentation "The parent condition of all command line errors."))

(define-condition cli-argument-error (command-line-error)
  ((opt :initarg :opt
        :accessor cli-argument-error-opt))
  (:report (lambda (con stream)
             (with-slots (opt message) con
               (format stream
                       "~a: ~:[--~a~;-~c~]" message (characterp opt) opt))))
  (:documentation "Condition representing an error that occurred during
processing of command line arguments."))

(define-condition unknown-option-error (cli-argument-error)
  ((message :initform "unknown option"))
  (:documentation "Condition representing an unknown command line option."))

(define-condition option-no-arg-error (cli-argument-error)
  ((message :initform "option requires an argument"))
  (:documentation "Condition representing an error that occurred because a
command line option did not have its required argument."))

(define-condition no-input-error (command-line-error)
  ((message :initform "no propositions given"))
  (:documentation "Condition representing no propositions given on the command
line."))

(defconstant operator-symbol-table
  '((open-paren "(")
    (close-paren ")")
    (and "/\\" "and" "&&" "&" "∧" ".")
    (nand "nand" "↑" "⊼")
    (or "\\/" "or" "||" "|" "∥" "+" "∨")
    (nor "nor" "↓" "⊽")
    (xor "xor" "⊕" "⊻" "↮" "≢" "^" "!=")
    (not "¬" "~" "!" "not")
    (implies "->" ">" "=>" "⇒" "⟹" "→" "⊃" "implies")
    (converse "<-" "<" "<=" "←" "⇐" "⟸" "⊂" "converse")
    (iff "<->" "<>" "<=>" "⇔" "↔" "≡" "iff" "=" "==" "xnor" "⊙"))
  "Alist table of operator symbols and their possible string representations.")

(defun operator-symbol (oper-str)
  "Return the symbol for OPER-STR, or nil if it is not a know operator."
  (loop for (oper-sym . strs) in operator-symbol-table
        when (member oper-str strs :test 'equalp)
          do (return oper-sym)))

(defun operator-precedence (oper)
  "Return the precedence for OPER."
  (case oper
    (not 1)
    (and 2)
    (nand 2)
    (xor 3)
    (or 4)
    (nor 4)
    (implies 5)
    (converse 5)
    (iff 6)
    (open-paren most-positive-fixnum)
    (t nil)))

(defun operator-argument-count (oper)
  "Return the minimum number of arguments that OPER takes as the first value,
and the maximum number (or nil for infinity) as a second value."
  (case oper
    (and (values 2 nil))
    (or (values 2 nil))
    (xor (values 2 nil))
    (not (values 1 1))
    (implies (values 2 2))
    (converse (values 2 2))
    (iff (values 2 2))
    (nand (values 2 nil))
    (nor (values 2 2))
    (t (error "unknown operator: ~S" oper))))

(defun interpret-operand (oper-str)
  "Return a symbol representing OPER-STR, or the string itself if it represents
a variable."
  (cond
    ((member oper-str '("t" "true" "⊤" "1") :test 'equalp)
     'true)
    ((member oper-str '("f" "false" "⊥" "0") :test 'equalp)
     'false)
    (t
     (loop for char across oper-str
           unless (symbol-char-p char)
             do (return nil)
           finally (return oper-str)))))

(defun string-first-char-safe (str)
  "Return the first character of STR, or nil if it is empty."
  (unless (zerop (length str))
    (elt str 0)))

(defun next-symbol-token (str &key multi-char-names)
  "Return the next token from STR that is not a paren. If MULTI-CHAR-NAMES is
non-nil, allow names to be more than one character long."
  (loop with mode = (if (symbol-char-p (elt str 0))
                        'alpha
                        'sym)
        for char across str
        for chari from 0
        while (or (and (eq mode 'alpha) (symbol-char-p char))
                  (and (eq mode 'sym) (not (symbol-char-p char))
                       (not (delim-p char))))
        collect char into token
        finally
           (let ((str (coerce token 'string)))
             (return
               ;; the multi-char token is an operator. its a variable, so defer
               ;; to multi-char-names
               (if (or multi-char-names
                       (operator-symbol str)
                       (symbolp (interpret-operand str)))
                   str
                   (string (first token)))))))

(defun next-token (str &key multi-char-names)
  "Return a list of the next token in STR and how much whitespace it had."
  (let ((whitespace-chars 0))
    (loop for char across str
          while (whitespace-p char) do
            (setq whitespace-chars (1+ whitespace-chars)))
    (setq str (subseq str whitespace-chars))
    (let ((next-char (string-first-char-safe str)))
      (cond
        ((not next-char)
         (list nil whitespace-chars))
        ((paren-p next-char)
         (list (string next-char) whitespace-chars))
        (t
         (let ((token (next-symbol-token str :multi-char-names multi-char-names)))
           (list token whitespace-chars)))))))

(defmacro dotokens ((var pos-var str &optional (retval nil retvalp))
                    (&key multi-char-names &allow-other-keys)
                    &body body)
  "Execute BODY once with VAR bound to each token in STR. Optionally, return
RETVAL. The position of each token will be stored in POS-VAR. If
MULTI-CHAR-NAMES is enabled, allow multiple characters in variable names."
  (let ((stream-var (gensym))
        (token-start-var (gensym))
        (token-var (gensym))
        (read-chars-var (gensym))
        (whitespace-var (gensym)))
    `(loop for ,stream-var = ,str then (subseq ,str ,read-chars-var)
           for (,token-var ,whitespace-var)
             = (next-token ,stream-var :multi-char-names ,multi-char-names)
           for ,token-start-var = ,whitespace-var
             then (+ ,read-chars-var ,whitespace-var)
           for ,read-chars-var = (+ ,whitespace-var (length ,token-var))
             then (+ ,read-chars-var ,whitespace-var (length ,token-var))
           while ,token-var do
             (let ((,var ,token-var)
                   (,pos-var ,token-start-var))
               (declare (ignorable ,pos-var))
               ,@body)
           finally
              (return ,(when retvalp
                         retval)))))

(defun interpret-token (token)
  "Return a list of the form (type value), where type is one of: `operator' or
`operand', and value is the tokens value, as returned by `operator-symbol' or
`interpret-operand'. If the token is of an unknown type, return a list of (nil
nil)."
  (let ((operator-value (operator-symbol token)))
    (if operator-value
        (list 'operator operator-value)
        (let ((operand-value (interpret-operand token)))
          (if operand-value
              (list 'operand operand-value)
              (list nil nil))))))

(defun apply-one-operator (operator-stack operand-stack
                           &optional proposition position)
  "Apply the next operator from OPERATOR-STACK to its operands from
OPERAND-STACK, return the new state of both stacks as values."
  (let* ((operator (pop operator-stack)))
    (when (not operator)
      (error 'proposition-parse-error :message "no more operators"
             :position position :proposition proposition))
    (let ((oper-args (operator-argument-count operator))
          (cur-operands (list (pop operand-stack))))
      (when (not (car cur-operands))
        (error 'proposition-parse-error
               :position position
               :proposition proposition
               :message (format nil
                                "operator ~A expects ~D arguments, found none"
                                operator oper-args)))
      (when (= oper-args 2)
        (push (pop operand-stack) cur-operands)
        (when (not (car cur-operands))
          (error 'proposition-parse-error
                 :position position
                 :proposition proposition
                 :message (format nil "operator ~A expects ~D arguments, found 1"
                                  operator oper-args))))
      (push (cons operator cur-operands) operand-stack)))
  (values operator-stack operand-stack))

(defun apply-lower-precedent (prec operators operands
                            &optional proposition position)
  "Apply all operators with lower precedent than PREC. Return the values of the
new operators and operands stack, as well as the number of operators removed."
  (loop with pop-count = 0
        while (<= (or (operator-precedence (car operators))
                      most-positive-fixnum)
                  prec)
        do
           (setf (values operators operands)
                 (apply-one-operator operators operands
                                     proposition position)
                 pop-count (1+ pop-count))
        finally (return (values operators operands pop-count))))

(defun parse-proposition-string (str &key (implicit-and t) multi-char-names)
  "Parse STR, which is a proposition string.
The return value is the values set of the parsed string, and the list of all
found variables."
  (let ((found-vars '())
        (operators '())
        (operands '())
        (oper-poses '())
        (last-was-operand nil))
    (dotokens (token token-pos str)
        (:multi-char-names multi-char-names)
      (destructuring-bind (type value) (interpret-token token)
        (cond
          ;; unknown type
          ((not type)
           (error 'proposition-parse-error
                  :position token-pos
                  :proposition str
                  :message "unknown token"))
          ;; operand
          ((eq type 'operand)
           (when last-was-operand
             ;; two operands next to each other often means "and" implicitly
             (unless implicit-and
               (error 'proposition-parse-error
                      :position token-pos
                      :proposition str
                      :message "expected operator, found operand"))
             (multiple-value-bind (new-oper new-opan pop-count)
                 (apply-lower-precedent (operator-precedence 'and)
                                        operators operands str token-pos)
               (setq operators new-oper
                     operands new-opan)
               (dotimes (i pop-count)
                 (pop oper-poses)))
             (push 'and operators)
             (push token-pos oper-poses))
           (unless (member value '(true false))
             (pushnew value found-vars :test 'equal))
           (push value operands)
           (setq last-was-operand t))
          ;; open and close paren don't touch `last-was-operand'
          ((eq value 'open-paren)
           (push value operators)
           (push token-pos oper-poses))
          ((eq value 'close-paren)
           (loop while (not (eq (car operators) 'open-paren))
                 when (null operators) do
                   (error 'proposition-parse-error
                          :position token-pos
                          :proposition str
                          :message "no matching open parenthesis")
                 do
                    (setf (values operators operands)
                          (apply-one-operator operators operands
                                              str token-pos))
                    (pop oper-poses))
           ;; remove the open-paren
           (pop operators)
           (pop oper-poses))
          ;; operator
          (t
           (multiple-value-bind (new-oper new-opan pop-count)
               (apply-lower-precedent (operator-precedence value)
                                      operators operands str token-pos)
             (setq operators new-oper
                   operands new-opan)
             (dotimes (i pop-count)
               (pop oper-poses)))
           (push value operators)
           (push token-pos oper-poses)
           (setq last-was-operand nil)))))
    (loop while operators
          for oper-pos = (pop oper-poses)
          when (eq (car operators) 'open-paren) do
            (error 'proposition-parse-error
                   :message "no matching closing parenthesis"
                   :proposition str
                   :position oper-pos)
          do
             (setf (values operators operands)
                   (apply-one-operator operators operands
                                       str oper-pos)))
    ;; return variables in the order we found them
    (values (car operands) (nreverse found-vars))))

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

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

(defconstant 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"))
  "Lookup table mapping operators to their LaTeX 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 typeset-proposition (expr &optional
                                   (lookup-table operator-ascii-lookup-alist)
                                   var-name-transform
                                   (parent-prec most-positive-fixnum))
  "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 a variable name
    ((stringp expr)
     (if var-name-transform 
         (funcall var-name-transform expr)
         expr))
    ;; expr is true or false
    ((or (eq expr 'true)
         (eq expr 'false))
     (cdr (assoc expr lookup-table)))
    ;; expr is a compound expression
    (t
     (destructuring-bind (oper first-arg &rest args) 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
                                          var-name-transform our-prec)
                     (cdr prefix-suffix))
             ;; we have many arguments
             (loop for arg in args
                   collect oper-ascii into output
                   collect
                   (typeset-proposition arg lookup-table
                                        var-name-transform our-prec)
                     into output
                   finally
                      (push (typeset-proposition first-arg lookup-table
                                                 var-name-transform our-prec)
                            output)
                      (return (format nil "~A~{~A~^ ~}~A" (car prefix-suffix)
                                      output (cdr prefix-suffix))))))))))

(defun logical-xor (&rest args)
  "Logical xor (not equal) each argument in turn with its following argument.
NOTE: This is NOT a macro, so all arguments, so there is no short circuit
evaluation (all arguments are evaluated no matter what)."
  (loop with result = nil
        for arg in args do
          (setq result (not (eq result arg)))
        finally (return result)))

(defun logical-and (&rest args)
  "Logical and (all true).
NOTE: This is NOT a macro, so all arguments, so there is no short circuit
evaluation (all arguments are evaluated no matter what)."
  (not (member nil args)))

(defun logical-or (&rest args)
  "Logical or (one or more true).
NOTE: This is NOT a macro, so all arguments, so there is no short circuit
evaluation (all arguments are evaluated no matter what)."
  (not (not (member t args))))

(defun logical-implies (prop1 prop2)
  "Evaluate the logical implies operation on PROP1 and PROP2. That is \"if
PROP1, then PROP2\".
NOTE: This is NOT a macro, so all arguments, so there is no short circuit
evaluation (all arguments are evaluated no matter what)."
  (if prop1 ;; only if first is true
      prop2 ;; eval second
      t)) ;; otherwise, just return true

(defun check-operator-argument-count (oper args)
  "Raise an error if OPER cannot be called with ARGS."
  (multiple-value-bind (min max) (operator-argument-count oper)
    (let ((arg-count (length args)))
      (cond
        ((< arg-count min)
         (error 'proposition-eval-error
                :message
                (format nil "~s ~[takes no arguments~;requires one argument~:;~
                                  requires at least ~:*~d arguments~], ~
                             but got ~[none~:;~:*~d~]"
                        oper min arg-count)))
        ((and max (> arg-count max))
         (error 'proposition-eval-error
                :message
                (format nil "~s can take at most ~d argument~:p, but got ~d"
                        oper max arg-count)))))))

(defun keep-unique-expressions (mapping)
  "Keep only unique expressions from MAPPING, which is an alist as returned by
`eval-proposition'."
  (loop for entry in mapping
        unless (assoc (car entry) output :test 'equal)
          collect entry into output
        finally (return output)))

(defun eval-proposition (prop vars)
  "Evaluate the proposition PROP, with the alist VARS mapping variables to their
values. Return the result of the proposition as the first value, and an alist
mapping sub expressions to their results as the second value.
NOTE: the second value does not include individual variables, literal values
(true and false)."
  (cond
    ;; prop is a variable name
    ((stringp prop)
     (let ((entry (assoc prop vars :test 'equal)))
       (unless entry
         (error 'proposition-eval-error
                :message (format nil "unknown variable: ~S~%" prop)))
       (values (cdr entry) '())))
    ;; prop is true or false
    ((eq prop 'true)
     (values t '()))
    ((eq prop 'false)
     (values nil '()))
    ;; prop is a compound expression
    (t
     (loop with (oper . args) = prop
           for arg in args
           for (value sub-map) = (multiple-value-list
                                  (eval-proposition arg vars))
           nconc sub-map into mapping
           collect value into arg-values
           finally
              (check-operator-argument-count oper args)
              (let ((result
                      (case oper
                        ;; avoid using the macros `and' and `or' so we can avoid
                        ;; using `eval'
                        (and
                         (apply 'logical-and arg-values))
                        (nand
                         (not (apply 'logical-and arg-values)))
                        (or
                         (apply 'logical-or arg-values))
                        (nor
                         (not (apply 'logical-or arg-values)))
                        (xor
                         (apply 'logical-xor arg-values))
                        (not
                         (not (car arg-values)))
                        (implies
                         (logical-implies (car arg-values)
                                          (second arg-values)))
                        (converse
                         ;; this is just implies with the arguments flipped
                         (logical-implies (second arg-values)
                                          (car arg-values)))
                        (iff
                         (eq (car arg-values) ;; both must have the same value
                             (second arg-values))))))
                (return (values result
                                (keep-unique-expressions
                                 (cons (cons prop result) mapping)))))))))

(defun discover-variables (prop)
  "Return a list of all the variables in PROP, in left to right order."
  (cond
    ((stringp prop)
     (list prop))
    ((listp prop)
     (mapcan 'discover-variables (cdr prop)))))

(defun permute-variables (vars)
  "Return a list of alists, each with a different permutation of VARS."
  (loop for var in vars
        for perms = (list (list (cons (car vars) t))
                          (list (cons (car vars) nil)))
          then (loop for entry in perms
                     collect (cons (cons var t) entry)
                     collect (cons (cons var nil) entry))
        finally (return (mapcar 'reverse perms))))

(defun create-truth-table (prop &key (vars (discover-variables prop))
                                  (include-intermediate t) (include-vars t))
  "Evaluate PROP with all possible combinations of truth values for its
variables. If supplied VARS should be a list of all the know variables in PORP,
if it is excluded, `discover-variables' will be used to generate it."
  (if (null vars)
      (list (list (cons prop (eval-proposition prop '()))))
      (loop for perm in (permute-variables vars)
            for (value sub-map) = (multiple-value-list
                                   (eval-proposition prop perm))
            collect
            (append (when include-vars perm)
                    (when include-intermediate
                      (delete-if (lambda (item) (equal prop (car item)))
                                 sub-map))
                    (list (cons prop value))))))

(defun extract-truth-table-expressions (table)
  "Extract each expression from TABLE and return them as a list.
NOTE: this just gets each expression from the first row, assuming each row has
the same expressions."
  (loop for (expr . value) in (car table)
        collect expr))

(defun extract-truth-table-values (table)
  "Return a new table, where each row consists of just the value of the
expression that was originally in that spot in TABLE."
  (loop for row in table
        collect (mapcar 'cdr row)))

(defun convert-truth-table-to-latex (table)
  "Convert TABLE, which should be a truth table as returned by
`create-truth-table' to latex.
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 operator-latex-lookup-alist
                                  'latex-var-name-transform))
                               (extract-truth-table-expressions table))))
    (format nil "~
\\begin{tabular}{~{~*|c~}|}~
  \\hline~
  ~{ $ ~A $~^ &~} \\\\~
  \\hline~
  ~{~{ $ ~:[\\bot~;\\top~] $~^ &~} \\\\ ~}~
  \\hline~
\\end{tabular}"
            typeset-exprs
            typeset-exprs
            (extract-truth-table-values table))))

(defconstant 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.")

(defconstant 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)
  "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 length :initial-element horiz))
        when rest do
          (format stream "~c" column))
  (format stream "~c" end))

(defun typeset-table-row (stream lengths row vert)
  "Typeset ROW to STREAM. VERT is the vertical separator. LENGTHS should be the
length of each column."
  (loop for col in row
        for length in lengths
        do
           (format stream "~c~v:@<~a~>" vert length col))
  (format stream "~c" vert))


(defun typeset-truth-table (table &optional
                                    (expr-lookup-table
                                     operator-ascii-lookup-alist)
                                    (box-lookup-table
                                     table-border-ascii-alist))
  "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 expr-lookup-table))
                                (extract-truth-table-expressions table)))
         (col-widths (mapcar (lambda (expr)
                               (+ (length expr) 2))
                             typeset-exprs)))
    (with-output-to-string (str)
      (typeset-table-break str col-widths
                           (cdr (assoc 'horizontal box-lookup-table))
                           (cdr (assoc 'top-left box-lookup-table))
                           (cdr (assoc 'down box-lookup-table))
                           (cdr (assoc 'top-right box-lookup-table)))
      (terpri str)
      (typeset-table-row str col-widths typeset-exprs
                         (cdr (assoc 'vertical box-lookup-table)))
      (terpri str)
      (typeset-table-break str col-widths
                           (cdr (assoc 'horizontal box-lookup-table))
                           (cdr (assoc 'right box-lookup-table))
                           (cdr (assoc 'cross box-lookup-table))
                           (cdr (assoc 'left box-lookup-table)))
      (terpri str)
      (dolist (row (extract-truth-table-values table))
        (typeset-table-row str col-widths
                           ;; convert t or nil to strings
                           (mapcar (lambda (entry)
                                     (cdr (assoc (if entry
                                                     'true
                                                     'false)
                                                 expr-lookup-table)))
                                   row)
                           (cdr (assoc 'vertical box-lookup-table)))
        (terpri str))
      (typeset-table-break str col-widths
                           (cdr (assoc 'horizontal box-lookup-table))
                           (cdr (assoc 'bottom-left box-lookup-table))
                           (cdr (assoc 'up box-lookup-table))
                           (cdr (assoc 'bottom-right box-lookup-table))))))

(defconstant command-line-spec
    '((#\h "help" help nil "print this message, then exit")
      (#\f "format" format t "specify the output format (*unicode*, ascii, or latex)")
      (#\s "subexps" subexps nil "include sub-expressions in the output table")
      (#\n "no-vars" no-vars nil "do not include variables in the output table")
      (#\m "multi-char" multi-char nil "allow multi-character variable names")
      (#\i "no-implicit" no-implicit nil "do not use implicit 'and' operations"))
  "Specification for `parse-command-line'. This is of the format:
(short long symbol has-arg-p desc).")

(defconstant cli-parse-continue-string
  "Continue paring arguments normally."
  "String to use for `cerror' during argument parsing.")

(defun parse-long-option (spec arg next-arg)
  "Parse the long option ARG. Return a list of its symbol, its value (or t if
it did not have one), and weather it consumed NEXT-ARG or not."
  (destructuring-bind (name &optional value)
      (uiop:split-string (subseq arg 2)
                         :max 2
                         :separator "=")
    (loop for (short long symbol has-arg-p dest) in spec
          when (equal name long) do
            (if has-arg-p
                (cond
                  (value
                   (return (list symbol value nil)))
                  (next-arg
                   (return (list symbol next-arg t)))
                  (t
                   (cerror cli-parse-continue-string
                           'option-no-arg-error :opt name)
                   (return (list symbol nil nil))))
                (return (list symbol t nil)))
          finally
             (cerror cli-parse-continue-string
                     'unknown-option-error :opt name)
             (return (list symbol nil nil)))))

(defun parse-short-option (spec arg next-arg)
  "Parse the short options in ARG according to SPEC. Return a list of options
with each entry being similar to the return value of `parse-long-option'."
  (loop with output = '()
        for i from 1 to (1- (length arg))
        for char = (elt arg i)
        for (short long symbol has-arg-p desc) = (assoc char spec) do
          (cond
            (has-arg-p
             (cond
               ((< i (1- (length arg)))
                (push (list symbol (subseq arg (1+ i)) nil) output)
                (return output))
               (next-arg
                (push (list symbol next-arg t) output)
                (return output))
               (t
                (cerror cli-parse-continue-string
                        'option-no-arg-error :opt char))))
            (short
             (push (list symbol t nil) output))
            (t
             (cerror cli-parse-continue-string
                     'unknown-option-error :opt char)))
        finally (return output)))

(defun parse-command-line (spec argv)
  "Parse command line arguments in ARGV according to SPEC. Return an alist with
the car being the option's symbol (as specified in SPEC), and the cdr being
the argument it had on the command line, or t if it had none. The rest of the
arguments will be placed in a list at the beginning of the alist."
  (let ((output-opts '())
        (output-other '()))
    (loop for (arg . rest) = argv then rest
        while (and arg (not (equal arg "--"))) do
          (cond
            ((uiop:string-prefix-p "--" arg)
             (destructuring-bind (symbol value skip-next-p)
                 (parse-long-option spec arg (car rest))
               (push (cons symbol value) output-opts)
               (when skip-next-p
                 (setq rest (cdr rest)))))
            ((uiop:string-prefix-p "-" arg)
             (loop for (symbol value skip-next-p) in (parse-short-option
                                                      spec arg (car rest))
                   do
                      (push (cons symbol value) output-opts)
                      (when skip-next-p
                        (setq rest (cdr rest)))))
            (t
             (push arg output-other)))
          finally (setf output-other (nconc (nreverse rest) output-other)))
    (cons (nreverse output-other) output-opts)))

(defun print-usage (stream spec)
  "Print the command line usage corresponding to SPEC to STREAM."
  (format stream "usage: truth-table [options] <propositions...>~%~%")
  (loop with longest-option
          = (apply 'max (mapcar
                         (lambda (entry)
                           (destructuring-bind (short long sym has-arg-p &rest other)
                               entry
                             (declare (ignorable other sym))
                             (+ (if short 2 0)
                                (if long (+ 2 (length long)) 0)
                                (if (and short long) 2 0)
                                (if has-arg-p 6 0))))
                         spec))
        for (short long symbol has-arg-p desc) in spec
        do
           (format stream "  ~v@<~@[-~c~]~@[, ~*~]~@[--~a~]~@[=<arg>~*~]~>  ~a~%"
                   longest-option
                   short (or short long) long has-arg-p desc))
  (format stream "~%The choice surrounded by '*' is the default. Arguments to long
options are also required for their short variant.~%"))

(defun combine-tables (table1 table2)
  "Join TABLE1 and TABLE2. Both tables must have the same number of rows.
TABLE1 is modified during this process."
  (loop for row1 in table1
        for row2 in table2
        do
           (setf (cdr (last row1)) row2))
  (mapcar 'keep-unique-expressions table1))

(defun create-combined-truth-table (props vars &key (include-intermediate nil)
                                                 (include-vars t))
  "Create a large truth table from all the propositions in PROPS. The other
arguments are as they are in `create-truth-table'."
  (loop with output-table = (create-truth-table
                             (car props)
                             :vars vars
                             :include-intermediate include-intermediate
                             :include-vars include-vars)
        for prop in (cdr props)
        for first-iter = t then nil do
          (setq output-table
                (combine-tables output-table
                                (create-truth-table
                                 prop :vars vars
                                 :include-intermediate include-intermediate
                                 :include-vars nil)))
        finally (return output-table)))

(defun option-value (opt opts)
  "Get the value of command line option OPT from OTPS, which is an alist as
returned as the second output of `parse-command-line'."
  (cdr (assoc opt opts)))

(defun typeset-table-to-format (table format)
  "Typeset TABLE into FORMAT, or error if FORMAT is not a know format."
  (cond 
    ((or (not format)
         (zerop (length format))
         (equal format "unicode"))
     (typeset-truth-table table operator-unicode-lookup-alist
                          table-border-unicode-alist))
    ((equal format "ascii")
     (typeset-truth-table table operator-ascii-lookup-alist
                          table-border-ascii-alist))
    ((equal format "latex")
     (convert-truth-table-to-latex table))
    (t (error 'command-line-error
              :message (format nil "unknown format: ~a"
                               format)))))

(defconstant more-help-error-message
  ""
  "Message to display when exiting because of command line errors.")

(defun eval-and-typeset-propositions (prop-strs &key (format "unicode")
                                                  (implicit-and t)
                                                  multi-char-names
                                                  include-intermediate
                                                  (include-vars t))
  "Evaluate and then typeset PROP-STRS as a table, which is a list of
proposition strings. For a description of the key parameters, see each of the
functions involved in evaluating and typesetting."
  (loop with vars = '()
        for prop-str in prop-strs
        for (parsed-exp parsed-vars)
          = (multiple-value-list
             (parse-proposition-string prop-str
                                       :implicit-and implicit-and
                                       :multi-char-names multi-char-names))
        collect parsed-exp into exps
        do (dolist (var parsed-vars)
             (unless (member var vars :test 'equal)
               (setq vars (nconc vars (list var)))))
        finally
           (let ((table (create-combined-truth-table
                         exps vars
                         :include-intermediate include-intermediate
                         :include-vars include-vars)))
             (return (typeset-table-to-format table format)))))

(defun main (argv)
  (let ((cmdline-error nil))
    (handler-bind
        (((or proposition-parse-error proposition-eval-error)
           (lambda (c)
             (format *error-output* "error: ~a~%" c)
             (uiop:quit 1)))
         (command-line-error
           (lambda (c) ;; finish parsing command line before exiting
             (format *error-output* "error: ~a~%" c)
             (setq cmdline-error t)
             (invoke-restart 'continue))))
      (destructuring-bind ((&rest prop-strs) &rest opts)
          (parse-command-line command-line-spec argv)
        (when (option-value 'help opts)
          (print-usage t command-line-spec)
          (uiop:quit (if cmdline-error 1 0)))
        (when (null prop-strs)
          (cerror cli-parse-continue-string 'no-input-error))
        (when cmdline-error
          (format *error-output* "Try -h or --help for more information.~%")
          (uiop:quit 1))
        (princ (eval-and-typeset-propositions
                prop-strs :format (option-value 'format opts)
                          :implicit-and (not (option-value 'no-implicit opts))
                          :multi-char-names (option-value 'multi-char opts)
                          :include-vars (not (option-value 'no-vars opts))))
        (terpri)))))

(defun toplevel ()
  (handler-case
      (with-user-abort:with-user-abort
        (main (uiop:command-line-arguments)))
    (with-user-abort:user-abort ()
      (format *error-output* "Keyboard interrupt~%")
      (uiop:quit 1))))