Initial commit
This commit is contained in:
		
							
								
								
									
										1
									
								
								.gitignore
									
									
									
									
										vendored
									
									
										Normal file
									
								
							
							
						
						
									
										1
									
								
								.gitignore
									
									
									
									
										vendored
									
									
										Normal file
									
								
							| @ -0,0 +1 @@ | |||||||
|  | truth-table | ||||||
							
								
								
									
										674
									
								
								LICENSE
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										674
									
								
								LICENSE
									
									
									
									
									
										Normal file
									
								
							| @ -0,0 +1,674 @@ | |||||||
|  |                     GNU GENERAL PUBLIC LICENSE | ||||||
|  |                        Version 3, 29 June 2007 | ||||||
|  |  | ||||||
|  |  Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/> | ||||||
|  |  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. | ||||||
|  |  | ||||||
|  |     <one line to give the program's name and a brief idea of what it does.> | ||||||
|  |     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 | ||||||
|  |     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/>. | ||||||
|  |  | ||||||
|  | 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". | ||||||
|  |  | ||||||
|  |   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 | ||||||
|  | <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>. | ||||||
							
								
								
									
										11
									
								
								Makefile
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										11
									
								
								Makefile
									
									
									
									
									
										Normal file
									
								
							| @ -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 | ||||||
							
								
								
									
										15
									
								
								build.lisp
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										15
									
								
								build.lisp
									
									
									
									
									
										Normal file
									
								
							| @ -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") | ||||||
							
								
								
									
										980
									
								
								truth-table.lisp
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										980
									
								
								truth-table.lisp
									
									
									
									
									
										Normal file
									
								
							| @ -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] <proposition>~%~%") | ||||||
|  |   (loop with longest-option | ||||||
|  |           = (apply 'max (mapcar | ||||||
|  |                          (lambda (entry) | ||||||
|  |                            (destructuring-bind (short long sym has-arg-p &rest other) | ||||||
|  |                                entry | ||||||
|  |                              (declare (ignorable other sym)) | ||||||
|  |                              (+ (if short 2 0) | ||||||
|  |                                 (if long (+ 2 (length long)) 0) | ||||||
|  |                                 (if (and short long) 2 0) | ||||||
|  |                                 (if has-arg-p 6 0)))) | ||||||
|  |                          spec)) | ||||||
|  |         for (short long symbol has-arg-p desc) in spec | ||||||
|  |         do | ||||||
|  |            (format stream "  ~v@<~@[-~c~]~@[, ~*~]~@[--~a~]~@[=<arg>~*~]~>  ~a~%" | ||||||
|  |                    longest-option | ||||||
|  |                    short (or short long) long has-arg-p desc)) | ||||||
|  |   (format stream "~%The choice surrounded by '*' is the default. Arguments to long | ||||||
|  | options are also required for their short variant.~%")) | ||||||
|  |  | ||||||
|  | (defun combine-tables (table1 table2) | ||||||
|  |   "Join TABLE1 and TABLE2. Both tables must have the same number of rows. | ||||||
|  | TABLE1 is modified during this process." | ||||||
|  |   (loop for row1 in table1 | ||||||
|  |         for row2 in table2 | ||||||
|  |         do | ||||||
|  |            (setf (cdr (last row1)) row2)) | ||||||
|  |   (mapcar 'keep-unique-expressions table1)) | ||||||
|  |  | ||||||
|  | (defun create-combined-truth-table (props vars &key (include-intermediate nil) | ||||||
|  |                                                  (include-vars t)) | ||||||
|  |   "Create a large truth table from all the propositions in PROPS. The other | ||||||
|  | arguments are as they are in `create-truth-table'." | ||||||
|  |   (loop with output-table = (create-truth-table | ||||||
|  |                              (car props) | ||||||
|  |                              :vars vars | ||||||
|  |                              :include-intermediate include-intermediate | ||||||
|  |                              :include-vars include-vars) | ||||||
|  |         for prop in (cdr props) | ||||||
|  |         for first-iter = t then nil do | ||||||
|  |           (setq output-table | ||||||
|  |                 (combine-tables output-table | ||||||
|  |                                 (create-truth-table | ||||||
|  |                                  prop :vars vars | ||||||
|  |                                  :include-intermediate include-intermediate | ||||||
|  |                                  :include-vars nil))) | ||||||
|  |         finally (return output-table))) | ||||||
|  |  | ||||||
|  | (defun option-value (opt opts) | ||||||
|  |   "Get the value of command line option OPT from OTPS, which is an alist as | ||||||
|  | returned as the second output of `parse-command-line'." | ||||||
|  |   (cdr (assoc opt opts))) | ||||||
|  |  | ||||||
|  | (defun typeset-table-to-format (table format) | ||||||
|  |   "Typeset TABLE into FORMAT, or error if FORMAT is not a know format." | ||||||
|  |   (cond  | ||||||
|  |     ((or (not format) | ||||||
|  |          (zerop (length format)) | ||||||
|  |          (equal format "unicode")) | ||||||
|  |      (typeset-truth-table table operator-unicode-lookup-alist | ||||||
|  |                           table-border-unicode-alist)) | ||||||
|  |     ((equal format "ascii") | ||||||
|  |      (typeset-truth-table table operator-ascii-lookup-alist | ||||||
|  |                           table-border-ascii-alist)) | ||||||
|  |     ((equal format "latex") | ||||||
|  |      (convert-truth-table-to-latex table)) | ||||||
|  |     (t (error 'command-line-error | ||||||
|  |               :message (format nil "unknown format: ~a" | ||||||
|  |                                format))))) | ||||||
|  |  | ||||||
|  | (defconstant more-help-error-message | ||||||
|  |   "" | ||||||
|  |   "Message to display when exiting because of command line errors.") | ||||||
|  |  | ||||||
|  | (defun eval-and-typeset-propositions (prop-strs &key (format "unicode") | ||||||
|  |                                                   (implicit-and t) | ||||||
|  |                                                   multi-char-names | ||||||
|  |                                                   include-intermediate | ||||||
|  |                                                   (include-vars t)) | ||||||
|  |   "Evaluate and then typeset PROP-STRS as a table, which is a list of | ||||||
|  | proposition strings. For a description of the key parameters, see each of the | ||||||
|  | functions involved in evaluating and typesetting." | ||||||
|  |   (loop with vars = '() | ||||||
|  |         for prop-str in prop-strs | ||||||
|  |         for (parsed-exp parsed-vars) | ||||||
|  |           = (multiple-value-list | ||||||
|  |              (parse-proposition-string prop-str | ||||||
|  |                                        :implicit-and implicit-and | ||||||
|  |                                        :multi-char-names multi-char-names)) | ||||||
|  |         collect parsed-exp into exps | ||||||
|  |         do (dolist (var parsed-vars) | ||||||
|  |              (unless (member var vars :test 'equal) | ||||||
|  |                (setq vars (nconc vars (list var))))) | ||||||
|  |         finally | ||||||
|  |            (let ((table (create-combined-truth-table | ||||||
|  |                          exps vars | ||||||
|  |                          :include-intermediate include-intermediate | ||||||
|  |                          :include-vars include-vars))) | ||||||
|  |              (return (typeset-table-to-format table format))))) | ||||||
|  |  | ||||||
|  | (defun main (argv) | ||||||
|  |   (let ((cmdline-error nil)) | ||||||
|  |     (handler-bind | ||||||
|  |         (((or proposition-parse-error proposition-eval-error) | ||||||
|  |            (lambda (c) | ||||||
|  |              (format *error-output* "error: ~a~%" c) | ||||||
|  |              (uiop:quit 1))) | ||||||
|  |          (command-line-error | ||||||
|  |            (lambda (c) ;; finish parsing command line before exiting | ||||||
|  |              (format *error-output* "error: ~a~%" c) | ||||||
|  |              (setq cmdline-error t) | ||||||
|  |              (invoke-restart 'continue)))) | ||||||
|  |       (destructuring-bind ((&rest prop-strs) &rest opts) | ||||||
|  |           (parse-command-line command-line-spec argv) | ||||||
|  |         (when (option-value 'help opts) | ||||||
|  |           (print-usage t command-line-spec) | ||||||
|  |           (uiop:quit (if cmdline-error 1 0))) | ||||||
|  |         (when (null prop-strs) | ||||||
|  |           (cerror cli-parse-continue-string 'no-input-error)) | ||||||
|  |         (when cmdline-error | ||||||
|  |           (format *error-output* "Try -h or --help for more information.~%") | ||||||
|  |           (uiop:quit 1)) | ||||||
|  |         (princ (eval-and-typeset-propositions | ||||||
|  |                 prop-strs :format (option-value 'format opts) | ||||||
|  |                           :implicit-and (not (option-value 'no-implicit opts)) | ||||||
|  |                           :multi-char-names (option-value 'multi-char opts) | ||||||
|  |                           :include-vars (not (option-value 'no-vars opts)))) | ||||||
|  |         (terpri))))) | ||||||
|  |  | ||||||
|  | (defun toplevel () | ||||||
|  |   (handler-case | ||||||
|  |       (with-user-abort:with-user-abort | ||||||
|  |         (main (uiop:command-line-arguments))) | ||||||
|  |     (with-user-abort:user-abort () | ||||||
|  |       (format *error-output* "Keyboard interrupt~%") | ||||||
|  |       (uiop:quit 1)))) | ||||||
		Reference in New Issue
	
	Block a user