1032 lines
42 KiB
Common Lisp
1032 lines
42 KiB
Common 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)))))
|
||
|
||
(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)
|
||
"The main entry point to the program. ARGV is the list of command line
|
||
arguments."
|
||
(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)
|
||
(cond
|
||
((option-value 'help opts)
|
||
(print-usage t command-line-spec)
|
||
(uiop:quit (if cmdline-error 1 0)))
|
||
((null prop-strs)
|
||
(cerror cli-parse-continue-string 'no-input-error))
|
||
(cmdline-error
|
||
(format *error-output* "Try -h or --help for more information.~%")
|
||
(uiop:quit 1))
|
||
(t
|
||
(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))
|
||
:include-intermediate (option-value 'subexps opts)))
|
||
(terpri)))))))
|
||
|
||
(defun toplevel ()
|
||
"Top-level function to be passed to `save-lisp-and-die'."
|
||
(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))))
|