Zander671/truth-table
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Refactor to use ASDF

Browse Source
This commit is contained in:
Alexander Rosenberg 2024-09-04 03:14:57 -07:00
parent 24c1a03b35
commit 24904e73b5
Signed by: Zander671
GPG Key ID: 5FD0394ADBD72730
11 changed files with 1264 additions and 1122 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

141
LICENSE
View File

@ -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. <https://fsf.org/>
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) <year> <name of author>
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 <https://www.gnu.org/licenses/>.
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:
<program> Copyright (C) <year> <name of author>
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
<https://www.gnu.org/licenses/>.
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
<https://www.gnu.org/licenses/why-not-lgpl.html>.

12
Makefile
View File

@ -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

24
build.lisp
View File

@ -1,15 +1,19 @@
(ql:quickload '(:uiop :with-user-abort))
;; This file should be run as follows:
;; sbcl --load build.lisp --eval '(<BUILD FUNCTION>)'
;; where <BUILD FUNCTION> 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)))

241
cli.lisp Normal file
View File

@ -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 <https://www.gnu.org/licenses/>.
(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] <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 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))))

160
eval.lisp Normal file
View File

@ -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 <https://www.gnu.org/licenses/>.
(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)))))))))

52
packages.lisp Normal file
View File

@ -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))

336
parse.lisp Normal file
View File

@ -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 <https://www.gnu.org/licenses/>.
(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))))

93
table.lisp Normal file
View File

@ -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 <https://www.gnu.org/licenses/>.
(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)))

24
truth-table.asd Normal file
View File

@ -0,0 +1,24 @@
(defsystem #:truth-table
:description "Tools for working with logical propositions and truth tables"
:author "Alexander Rosenberg <zanderpkg@pm.me>"
: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")))

1031
truth-table.lisp
View File

File diff suppressed because it is too large Load Diff

272
typeset.lisp Normal file
View File

@ -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 <https://www.gnu.org/licenses/>.
(in-package :truth-table/base)
(define-condition table-format-error (error)
((format :initarg :format
:accessor table-format-error-format))
(:report
(lambda (con stream)
(format stream "unknown table format: ~a"
(table-format-error-format con)))))
(defparameter *operator-ascii-lookup-alist*
'((and . "&")
(nand . "nand")
(or . "|")
(nor . "nor")
(xor . "^")
(not . "~")
(implies . "->")
(converse . "<-")
(iff . "<->")
(open-paren . "(")
(close-paren . ")")
(true . "T")
(false . "F"))
"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))))