diff --git a/LICENSE b/LICENSE index f288702..be3f7b2 100644 --- a/LICENSE +++ b/LICENSE @@ -1,5 +1,5 @@ - GNU GENERAL PUBLIC LICENSE - Version 3, 29 June 2007 + GNU AFFERO GENERAL PUBLIC LICENSE + Version 3, 19 November 2007 Copyright (C) 2007 Free Software Foundation, Inc. Everyone is permitted to copy and distribute verbatim copies @@ -7,17 +7,15 @@ Preamble - The GNU General Public License is a free, copyleft license for -software and other kinds of works. + The GNU Affero General Public License is a free, copyleft license for +software and other kinds of works, specifically designed to ensure +cooperation with the community in the case of network server software. The licenses for most software and other practical works are designed to take away your freedom to share and change the works. By contrast, -the GNU General Public License is intended to guarantee your freedom to +our General Public Licenses are intended to guarantee your freedom to share and change all versions of a program--to make sure it remains free -software for all its users. We, the Free Software Foundation, use the -GNU General Public License for most of our software; it applies also to -any other work released this way by its authors. You can apply it to -your programs, too. +software for all its users. When we speak of free software, we are referring to freedom, not price. Our General Public Licenses are designed to make sure that you @@ -26,44 +24,34 @@ them if you wish), that you receive source code or can get it if you want it, that you can change the software or use pieces of it in new free programs, and that you know you can do these things. - To protect your rights, we need to prevent others from denying you -these rights or asking you to surrender the rights. Therefore, you have -certain responsibilities if you distribute copies of the software, or if -you modify it: responsibilities to respect the freedom of others. + Developers that use our General Public Licenses protect your rights +with two steps: (1) assert copyright on the software, and (2) offer +you this License which gives you legal permission to copy, distribute +and/or modify the software. - For example, if you distribute copies of such a program, whether -gratis or for a fee, you must pass on to the recipients the same -freedoms that you received. You must make sure that they, too, receive -or can get the source code. And you must show them these terms so they -know their rights. + A secondary benefit of defending all users' freedom is that +improvements made in alternate versions of the program, if they +receive widespread use, become available for other developers to +incorporate. Many developers of free software are heartened and +encouraged by the resulting cooperation. However, in the case of +software used on network servers, this result may fail to come about. +The GNU General Public License permits making a modified version and +letting the public access it on a server without ever releasing its +source code to the public. - Developers that use the GNU GPL protect your rights with two steps: -(1) assert copyright on the software, and (2) offer you this License -giving you legal permission to copy, distribute and/or modify it. + The GNU Affero General Public License is designed specifically to +ensure that, in such cases, the modified source code becomes available +to the community. It requires the operator of a network server to +provide the source code of the modified version running there to the +users of that server. Therefore, public use of a modified version, on +a publicly accessible server, gives the public access to the source +code of the modified version. - For the developers' and authors' protection, the GPL clearly explains -that there is no warranty for this free software. For both users' and -authors' sake, the GPL requires that modified versions be marked as -changed, so that their problems will not be attributed erroneously to -authors of previous versions. - - Some devices are designed to deny users access to install or run -modified versions of the software inside them, although the manufacturer -can do so. This is fundamentally incompatible with the aim of -protecting users' freedom to change the software. The systematic -pattern of such abuse occurs in the area of products for individuals to -use, which is precisely where it is most unacceptable. Therefore, we -have designed this version of the GPL to prohibit the practice for those -products. If such problems arise substantially in other domains, we -stand ready to extend this provision to those domains in future versions -of the GPL, as needed to protect the freedom of users. - - Finally, every program is threatened constantly by software patents. -States should not allow patents to restrict development and use of -software on general-purpose computers, but in those that do, we wish to -avoid the special danger that patents applied to a free program could -make it effectively proprietary. To prevent this, the GPL assures that -patents cannot be used to render the program non-free. + An older license, called the Affero General Public License and +published by Affero, was designed to accomplish similar goals. This is +a different license, not a version of the Affero GPL, but Affero has +released a new version of the Affero GPL which permits relicensing under +this license. The precise terms and conditions for copying, distribution and modification follow. @@ -72,7 +60,7 @@ modification follow. 0. Definitions. - "This License" refers to version 3 of the GNU General Public License. + "This License" refers to version 3 of the GNU Affero General Public License. "Copyright" also means copyright-like laws that apply to other kinds of works, such as semiconductor masks. @@ -549,35 +537,45 @@ to collect a royalty for further conveying from those to whom you convey the Program, the only way you could satisfy both those terms and this License would be to refrain entirely from conveying the Program. - 13. Use with the GNU Affero General Public License. + 13. Remote Network Interaction; Use with the GNU General Public License. + + Notwithstanding any other provision of this License, if you modify the +Program, your modified version must prominently offer all users +interacting with it remotely through a computer network (if your version +supports such interaction) an opportunity to receive the Corresponding +Source of your version by providing access to the Corresponding Source +from a network server at no charge, through some standard or customary +means of facilitating copying of software. This Corresponding Source +shall include the Corresponding Source for any work covered by version 3 +of the GNU General Public License that is incorporated pursuant to the +following paragraph. Notwithstanding any other provision of this License, you have permission to link or combine any covered work with a work licensed -under version 3 of the GNU Affero General Public License into a single +under version 3 of the GNU General Public License into a single combined work, and to convey the resulting work. The terms of this License will continue to apply to the part which is the covered work, -but the special requirements of the GNU Affero General Public License, -section 13, concerning interaction through a network will apply to the -combination as such. +but the work with which it is combined will remain governed by version +3 of the GNU General Public License. 14. Revised Versions of this License. The Free Software Foundation may publish revised and/or new versions of -the GNU General Public License from time to time. Such new versions will -be similar in spirit to the present version, but may differ in detail to +the GNU Affero General Public License from time to time. Such new versions +will be similar in spirit to the present version, but may differ in detail to address new problems or concerns. Each version is given a distinguishing version number. If the -Program specifies that a certain numbered version of the GNU General +Program specifies that a certain numbered version of the GNU Affero General Public License "or any later version" applies to it, you have the option of following the terms and conditions either of that numbered version or of any later version published by the Free Software Foundation. If the Program does not specify a version number of the -GNU General Public License, you may choose any version ever published +GNU Affero General Public License, you may choose any version ever published by the Free Software Foundation. If the Program specifies that a proxy can decide which future -versions of the GNU General Public License can be used, that proxy's +versions of the GNU Affero General Public License can be used, that proxy's public statement of acceptance of a version permanently authorizes you to choose that version for the Program. @@ -635,40 +633,29 @@ the "copyright" line and a pointer to where the full notice is found. Copyright (C) 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 + it under the terms of the GNU Affero 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. + GNU Affero General Public License for more details. - You should have received a copy of the GNU General Public License + You should have received a copy of the GNU Affero General Public License along with this program. If not, see . Also add information on how to contact you by electronic and paper mail. - If the program does terminal interaction, make it output a short -notice like this when it starts in an interactive mode: - - Copyright (C) - This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. - This is free software, and you are welcome to redistribute it - under certain conditions; type `show c' for details. - -The hypothetical commands `show w' and `show c' should show the appropriate -parts of the General Public License. Of course, your program's commands -might be different; for a GUI interface, you would use an "about box". + If your software can interact with users remotely through a computer +network, you should also make sure that it provides a way for users to +get its source. For example, if your program is a web application, its +interface could display a "Source" link that leads users to an archive +of the code. There are many ways you could offer source, and different +solutions will be better for different programs; see section 13 for the +specific requirements. You should also get your employer (if you work as a programmer) or school, if any, to sign a "copyright disclaimer" for the program, if necessary. -For more information on this, and how to apply and follow the GNU GPL, see +For more information on this, and how to apply and follow the GNU AGPL, see . - - The GNU General Public License does not permit incorporating your program -into proprietary programs. If your program is a subroutine library, you -may consider it more useful to permit linking proprietary applications with -the library. If this is what you want to do, use the GNU Lesser General -Public License instead of this License. But first, please read -. diff --git a/Makefile b/Makefile index f424a39..8c7bffa 100644 --- a/Makefile +++ b/Makefile @@ -1,11 +1,15 @@ LISP ?= sbcl -all: truth-table +BASE_FILES=packages.lisp parse.lisp table.lisp typeset.lisp eval.lisp +CLI_FILES=cli.lisp -truth-table: build.lisp truth-table.lisp - $(LISP) --load build.lisp +all: cli + +cli: truth-table +truth-table: build.lisp truth-table.asd $(BASE_FILES) $(CLI_FILES) + $(LISP) --load build.lisp --eval '(cli)' clean: rm -f truth-table -.PHONY: all clean +.PHONY: all cli clean diff --git a/build.lisp b/build.lisp index ddaddc7..9ae821c 100644 --- a/build.lisp +++ b/build.lisp @@ -1,15 +1,19 @@ -(ql:quickload '(:uiop :with-user-abort)) +;; This file should be run as follows: +;; sbcl --load build.lisp --eval '()' +;; where is either `cli' or `web' -(load "truth-table.lisp") +#-sbcl (error "Only SBCL is supported right now") -#+sbcl -(progn - (sb-ext:disable-debugger) +(sb-ext:disable-debugger) + +(require :asdf) + +(defun cli () + "Build the CLI application executable." + (asdf:load-system :truth-table/cli) + (require :truth-table/cli) (sb-ext:save-lisp-and-die "truth-table" - :toplevel 'truth-table:toplevel + :executable t :save-runtime-options t - :executable t)) - -#-sbcl -(error "I only know how to build under SBCL") + :toplevel (intern "TOPLEVEL" :truth-table/cli))) diff --git a/cli.lisp b/cli.lisp new file mode 100644 index 0000000..8bd58c5 --- /dev/null +++ b/cli.lisp @@ -0,0 +1,241 @@ +;; cli.lisp -- Command line interface entry point and option parsing +;; 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 . +(in-package :truth-table/cli) + +(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.")) + +(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))))) + +(defparameter *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).") + +(defparameter *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] ~%~%") + (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~]~@[=~*~]~> ~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 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 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 + table-format-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) + (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 + (let ((format (option-value 'format opts))) + (when (or (not format) (zerop (length format))) + (setq format "unicode")) + (princ (eval-and-typeset-propositions + prop-strs :format format + :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)))) diff --git a/eval.lisp b/eval.lisp new file mode 100644 index 0000000..75022a7 --- /dev/null +++ b/eval.lisp @@ -0,0 +1,160 @@ +;; eval.lisp -- Evaluate parsed 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 . +(in-package :truth-table/base) + +(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.")) + +(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 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))))))))) diff --git a/packages.lisp b/packages.lisp new file mode 100644 index 0000000..1f65ce3 --- /dev/null +++ b/packages.lisp @@ -0,0 +1,52 @@ +(defpackage #:truth-table/base + (:use #:common-lisp) + (:export + ;; parse.lsip + #:whitespace-p + #:paren-p + #:delim-p + #:symbol-char-p + #:proposition-parse-error + #:operator-symbol + #:operator-precedence + #:interpret-operand + #:next-token + #:dotokens + #:interpret-token + #:parse-proposition-string + + ;; eval.lisp + #:proposition-eval-error + #:operator-argument-count + #:logical-xor + #:logical-and + #:logical-or + #:logical-implies + #:eval-proposition + + ;; table.lisp + #:discover-variables + #:permute-variables + #:create-truth-table + #:extract-truth-table-expressions + #:extract-truth-table-values + #:combine-tables + #:create-combined-truth-table + + ;; typeset.lisp + #:table-format-error + #:*operator-ascii-lookup-alist* + #:*operator-unicode-lookup-alist* + #:*operator-latex-lookup-alist* + #:latex-var-name-transform + #:typeset-proposition + #:convert-truth-table-to-latex + #:*table-border-ascii-alist* + #:*table-border-unicode-alist* + #:typeset-truth-table + #:*known-formats* + #:typeset-table-to-format)) + +(defpackage #:truth-table/cli + (:use #:common-lisp #:truth-table/base) + (:export #:toplevel #:main)) diff --git a/parse.lisp b/parse.lisp new file mode 100644 index 0000000..2ca1cc9 --- /dev/null +++ b/parse.lisp @@ -0,0 +1,336 @@ +;; parse.lisp -- Proposition string parsing subroutines +;; 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 . +(in-package :truth-table/base) + +(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.")) + +(defparameter *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 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)))) diff --git a/table.lisp b/table.lisp new file mode 100644 index 0000000..3a3bad8 --- /dev/null +++ b/table.lisp @@ -0,0 +1,93 @@ +;; table.lisp -- Generate tables from parsed propositions +;; 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 . +(in-package :truth-table/base) + +(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 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))) diff --git a/truth-table.asd b/truth-table.asd new file mode 100644 index 0000000..45901b3 --- /dev/null +++ b/truth-table.asd @@ -0,0 +1,24 @@ +(defsystem #:truth-table + :description "Tools for working with logical propositions and truth tables" + :author "Alexander Rosenberg " + :license "AGPL3" + :depends-on ()) + +(defsystem #:truth-table/base + :version "0.0.1" + :serial t + :components + ((:file "packages") + (:file "parse") + (:file "eval") + (:file "table") + (:file "typeset"))) + +(defsystem #:truth-table/cli + :depends-on (#:uiop + #:with-user-abort + #:truth-table/base) + :serial t + :components + ((:file "packages") + (:file "cli"))) diff --git a/truth-table.lisp b/truth-table.lisp deleted file mode 100644 index b431b95..0000000 --- a/truth-table.lisp +++ /dev/null @@ -1,1031 +0,0 @@ -;; 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 . -#+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] ~%~%") - (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~]~@[=~*~]~> ~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)))) diff --git a/typeset.lisp b/typeset.lisp new file mode 100644 index 0000000..0fd1e0b --- /dev/null +++ b/typeset.lisp @@ -0,0 +1,272 @@ +;; 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 . +(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")) + "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 . "⊥")) + "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")) + "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 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)))) + +(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) + "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)))))) + +(defparameter *known-formats* + '("unicode" "ascii" "latex") + "The known formats that `typeset-table-to-format' can take.") + +(defun typeset-table-to-format (table format) + "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*)) + ((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 'table-format-error :format format))))