commit 62347e8b4dad124e55b0d2a6e30d464d621dbcf2 Author: Alexander Rosenberg Date: Tue Sep 3 17:50:58 2024 -0700 Initial commit diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..2bf7a83 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +truth-table \ No newline at end of file diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..f288702 --- /dev/null +++ b/LICENSE @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The GNU General Public License is a free, copyleft license for +software and other kinds of works. + + 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 +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. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +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. + + 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. + + 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. + + 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. + + The precise terms and conditions for copying, distribution and +modification follow. + + TERMS AND CONDITIONS + + 0. Definitions. + + "This License" refers to version 3 of the GNU General Public License. + + "Copyright" also means copyright-like laws that apply to other kinds of +works, such as semiconductor masks. + + "The Program" refers to any copyrightable work licensed under this +License. Each licensee is addressed as "you". "Licensees" and +"recipients" may be individuals or organizations. + + To "modify" a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of an +exact copy. The resulting work is called a "modified version" of the +earlier work or a work "based on" the earlier work. + + A "covered work" means either the unmodified Program or a work based +on the Program. + + To "propagate" a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + + To "convey" a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user through +a computer network, with no transfer of a copy, is not conveying. + + An interactive user interface displays "Appropriate Legal Notices" +to the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + + 1. Source Code. + + The "source code" for a work means the preferred form of the work +for making modifications to it. "Object code" means any non-source +form of a work. + + A "Standard Interface" means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + + The "System Libraries" of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +"Major Component", in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + + The "Corresponding Source" for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. + + The Corresponding Source need not include anything that users +can regenerate automatically from other parts of the Corresponding +Source. + + The Corresponding Source for a work in source code form is that +same work. + + 2. Basic Permissions. + + All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + + You may make, run and propagate covered works that you do not +convey, without conditions so long as your license otherwise remains +in force. You may convey covered works to others for the sole purpose +of having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + + Conveying under any other circumstances is permitted solely under +the conditions stated below. Sublicensing is not allowed; section 10 +makes it unnecessary. + + 3. Protecting Users' Legal Rights From Anti-Circumvention Law. + + No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + + When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such circumvention +is effected by exercising rights under this License with respect to +the covered work, and you disclaim any intention to limit operation or +modification of the work as a means of enforcing, against the work's +users, your or third parties' legal rights to forbid circumvention of +technological measures. + + 4. Conveying Verbatim Copies. + + You may convey verbatim copies of the Program's source code as you +receive it, in any medium, provided that you conspicuously and +appropriately publish on each copy an appropriate copyright notice; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + + You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + + 5. Conveying Modified Source Versions. + + You may convey a work based on the Program, or the modifications to +produce it from the Program, in the form of source code under the +terms of section 4, provided that you also meet all of these conditions: + + a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + + b) The work must carry prominent notices stating that it is + released under this License and any conditions added under section + 7. This requirement modifies the requirement in section 4 to + "keep intact all notices". + + c) You must license the entire work, as a whole, under this + License to anyone who comes into possession of a copy. This + License will therefore apply, along with any applicable section 7 + additional terms, to the whole of the work, and all its parts, + regardless of how they are packaged. This License gives no + permission to license the work in any other way, but it does not + invalidate such permission if you have separately received it. + + d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your + work need not make them do so. + + A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +"aggregate" if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + + 6. Conveying Non-Source Forms. + + You may convey a covered work in object code form under the terms +of sections 4 and 5, provided that you also convey the +machine-readable Corresponding Source under the terms of this License, +in one of these ways: + + a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium + customarily used for software interchange. + + b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a + written offer, valid for at least three years and valid for as + long as you offer spare parts or customer support for that product + model, to give anyone who possesses the object code either (1) a + copy of the Corresponding Source for all the software in the + product that is covered by this License, on a durable physical + medium customarily used for software interchange, for a price no + more than your reasonable cost of physically performing this + conveying of source, or (2) access to copy the + Corresponding Source from a network server at no charge. + + c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This + alternative is allowed only occasionally and noncommercially, and + only if you received the object code with such an offer, in accord + with subsection 6b. + + d) Convey the object code by offering access from a designated + place (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) + that supports equivalent copying facilities, provided you maintain + clear directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + + e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + + A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + + A "User Product" is either (1) a "consumer product", which means any +tangible personal property which is normally used for personal, family, +or household purposes, or (2) anything designed or sold for incorporation +into a dwelling. In determining whether a product is a consumer product, +doubtful cases shall be resolved in favor of coverage. For a particular +product received by a particular user, "normally used" refers to a +typical or common use of that class of product, regardless of the status +of the particular user or of the way in which the particular user +actually uses, or expects or is expected to use, the product. A product +is a consumer product regardless of whether the product has substantial +commercial, industrial or non-consumer uses, unless such uses represent +the only significant mode of use of the product. + + "Installation Information" for a User Product means any methods, +procedures, authorization keys, or other information required to install +and execute modified versions of a covered work in that User Product from +a modified version of its Corresponding Source. The information must +suffice to ensure that the continued functioning of the modified object +code is in no case prevented or interfered with solely because +modification has been made. + + If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + + The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or updates +for a work that has been modified or installed by the recipient, or for +the User Product in which it has been modified or installed. Access to a +network may be denied when the modification itself materially and +adversely affects the operation of the network or violates the rules and +protocols for communication across the network. + + Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + 7. Additional Terms. + + "Additional permissions" are terms that supplement the terms of this +License by making exceptions from one or more of its conditions. +Additional permissions that are applicable to the entire Program shall +be treated as though they were included in this License, to the extent +that they are valid under applicable law. If additional permissions +apply only to part of the Program, that part may be used separately +under those permissions, but the entire Program remains governed by +this License without regard to the additional permissions. + + When you convey a copy of a covered work, you may at your option +remove any additional permissions from that copy, or from any part of +it. (Additional permissions may be written to require their own +removal in certain cases when you modify the work.) You may place +additional permissions on material, added by you to a covered work, +for which you have or can give appropriate copyright permission. + + Notwithstanding any other provision of this License, for material you +add to a covered work, you may (if authorized by the copyright holders of +that material) supplement the terms of this License with terms: + + a) Disclaiming warranty or limiting liability differently from the + terms of sections 15 and 16 of this License; or + + b) Requiring preservation of specified reasonable legal notices or + author attributions in that material or in the Appropriate Legal + Notices displayed by works containing it; or + + c) Prohibiting misrepresentation of the origin of that material, or + requiring that modified versions of such material be marked in + reasonable ways as different from the original version; or + + d) Limiting the use for publicity purposes of names of licensors or + authors of the material; or + + e) Declining to grant rights under trademark law for use of some + trade names, trademarks, or service marks; or + + f) Requiring indemnification of licensors and authors of that + material by anyone who conveys the material (or modified versions of + it) with contractual assumptions of liability to the recipient, for + any liability that these contractual assumptions directly impose on + those licensors and authors. + + All other non-permissive additional terms are considered "further +restrictions" within the meaning of section 10. If the Program as you +received it, or any part of it, contains a notice stating that it is +governed by this License along with a term that is a further +restriction, you may remove that term. If a license document contains +a further restriction but permits relicensing or conveying under this +License, you may add to a covered work material governed by the terms +of that license document, provided that the further restriction does +not survive such relicensing or conveying. + + If you add terms to a covered work in accord with this section, you +must place, in the relevant source files, a statement of the +additional terms that apply to those files, or a notice indicating +where to find the applicable terms. + + Additional terms, permissive or non-permissive, may be stated in the +form of a separately written license, or stated as exceptions; +the above requirements apply either way. + + 8. Termination. + + You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + + However, if you cease all violation of this License, then your +license from a particular copyright holder is reinstated (a) +provisionally, unless and until the copyright holder explicitly and +finally terminates your license, and (b) permanently, if the copyright +holder fails to notify you of the violation by some reasonable means +prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + + Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + + 9. Acceptance Not Required for Having Copies. + + You are not required to accept this License in order to receive or +run a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + + 10. Automatic Licensing of Downstream Recipients. + + Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + + An "entity transaction" is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + + You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + + 11. Patents. + + A "contributor" is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's "contributor version". + + A contributor's "essential patent claims" are all patent claims +owned or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, "control" includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + + Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + + In the following three paragraphs, a "patent license" is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To "grant" such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + + If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. "Knowingly relying" means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + + If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + + A patent license is "discriminatory" if it does not include within +the scope of its coverage, prohibits the exercise of, or is +conditioned on the non-exercise of one or more of the rights that are +specifically granted under this License. You may not convey a covered +work if you are a party to an arrangement with a third party that is +in the business of distributing software, under which you make payment +to the third party based on the extent of your activity of conveying +the work, and under which the third party grants, to any of the +parties who would receive the covered work from you, a discriminatory +patent license (a) in connection with copies of the covered work +conveyed by you (or copies made from those copies), or (b) primarily +for and in connection with specific products or compilations that +contain the covered work, unless you entered into that arrangement, +or that patent license was granted, prior to 28 March 2007. + + Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + + 12. No Surrender of Others' Freedom. + + If conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot convey a +covered work so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you may +not convey it at all. For example, if you agree to terms that obligate you +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. + + 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 +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. + + 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 +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 +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 +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 +public statement of acceptance of a version permanently authorizes you +to choose that version for the Program. + + Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + + 15. Disclaimer of Warranty. + + THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY +APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT +HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY +OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM +IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF +ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. Limitation of Liability. + + IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS +THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY +GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE +USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF +DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD +PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), +EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF +SUCH DAMAGES. + + 17. Interpretation of Sections 15 and 16. + + If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +state the exclusion of warranty; and each file should have at least +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 + 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 . + +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". + + 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 +. + + 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 new file mode 100644 index 0000000..f424a39 --- /dev/null +++ b/Makefile @@ -0,0 +1,11 @@ +LISP ?= sbcl + +all: truth-table + +truth-table: build.lisp truth-table.lisp + $(LISP) --load build.lisp + +clean: + rm -f truth-table + +.PHONY: all clean diff --git a/build.lisp b/build.lisp new file mode 100644 index 0000000..ddaddc7 --- /dev/null +++ b/build.lisp @@ -0,0 +1,15 @@ +(ql:quickload '(:uiop :with-user-abort)) + +(load "truth-table.lisp") + +#+sbcl +(progn + (sb-ext:disable-debugger) + (sb-ext:save-lisp-and-die + "truth-table" + :toplevel 'truth-table:toplevel + :save-runtime-options t + :executable t)) + +#-sbcl +(error "I only know how to build under SBCL") diff --git a/truth-table.lisp b/truth-table.lisp new file mode 100644 index 0000000..101783f --- /dev/null +++ b/truth-table.lisp @@ -0,0 +1,980 @@ +#+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" "&&" "&" "∧" ".") + (or "\\/" "or" "||" "|" "∥" "+" "∨") + (xor "xor" "⊕" "⊻" "↮" "≢" "^" "!=") + (not "¬" "~" "!" "not") + (implies "->" ">" "=>" "⇒" "→" "⊃" "implies") + (iff "<->" "<>" "<=>" "⇔" "↔" "≡" "iff" "=" "==")) + "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) + (xor 3) + (or 4) + (implies 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)) + (iff (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 . "&") + (or . "|") + (xor . "^") + (not . "~") + (implies . "->") + (iff . "<->") + (open-paren . "(") + (close-paren . ")") + (true . "T") + (false . "F")) + "Lookup table mapping operators to their ASCII representation.") + +(defconstant operator-unicode-lookup-alist + '((and . "∧") + (or . "∨") + (xor . "⊕") + (not . "¬") + (implies . "→") + (iff . "↔") + (open-paren . "(") + (close-paren . ")") + (true . "⊤") + (false . "⊥")) + "Lookup table mapping operators to their Unicode representation.") + +(defconstant operator-latex-lookup-alist + '((and . "\\land") + (or . "\\lor") + (xor . "\\oplus") + (not . "\\lnot ") + (implies . "\\to") + (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 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)) + (or + (apply 'logical-or arg-values)) + (xor + (apply 'logical-xor arg-values)) + (not + (not (car arg-values))) + (implies + (if (car arg-values) ;; if first is true + (second arg-values) ;; eval second + t)) ;; otherwise, just return true + (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))))) + +(defconstant more-help-error-message + "" + "Message to display when exiting because of command line errors.") + +(defun eval-and-typeset-propositions (prop-strs &key (format "unicode") + (implicit-and t) + multi-char-names + include-intermediate + (include-vars t)) + "Evaluate and then typeset PROP-STRS as a table, which is a list of +proposition strings. For a description of the key parameters, see each of the +functions involved in evaluating and typesetting." + (loop with vars = '() + for prop-str in prop-strs + for (parsed-exp parsed-vars) + = (multiple-value-list + (parse-proposition-string prop-str + :implicit-and implicit-and + :multi-char-names multi-char-names)) + collect parsed-exp into exps + do (dolist (var parsed-vars) + (unless (member var vars :test 'equal) + (setq vars (nconc vars (list var))))) + finally + (let ((table (create-combined-truth-table + exps vars + :include-intermediate include-intermediate + :include-vars include-vars))) + (return (typeset-table-to-format table format))))) + +(defun main (argv) + (let ((cmdline-error nil)) + (handler-bind + (((or proposition-parse-error proposition-eval-error) + (lambda (c) + (format *error-output* "error: ~a~%" c) + (uiop:quit 1))) + (command-line-error + (lambda (c) ;; finish parsing command line before exiting + (format *error-output* "error: ~a~%" c) + (setq cmdline-error t) + (invoke-restart 'continue)))) + (destructuring-bind ((&rest prop-strs) &rest opts) + (parse-command-line command-line-spec argv) + (when (option-value 'help opts) + (print-usage t command-line-spec) + (uiop:quit (if cmdline-error 1 0))) + (when (null prop-strs) + (cerror cli-parse-continue-string 'no-input-error)) + (when cmdline-error + (format *error-output* "Try -h or --help for more information.~%") + (uiop:quit 1)) + (princ (eval-and-typeset-propositions + prop-strs :format (option-value 'format opts) + :implicit-and (not (option-value 'no-implicit opts)) + :multi-char-names (option-value 'multi-char opts) + :include-vars (not (option-value 'no-vars opts)))) + (terpri))))) + +(defun toplevel () + (handler-case + (with-user-abort:with-user-abort + (main (uiop:command-line-arguments))) + (with-user-abort:user-abort () + (format *error-output* "Keyboard interrupt~%") + (uiop:quit 1))))