judge (empty) → 0.1.2.0
raw patch · 22 files changed
+3923/−0 lines, 22 filesdep +aesondep +ansi-wl-pprintdep +attoparsecsetup-changed
Dependencies added: aeson, ansi-wl-pprint, attoparsec, base, bytestring, containers, directory, filepath, judge, mtl, optparse-applicative, pointedlist, terminal-size, texmath, text, transformers, unordered-containers, utf8-string, vector, yaml
Files
- CHANGELOG.md +54/−0
- LICENSE +674/−0
- README.md +57/−0
- Setup.hs +2/−0
- app/CLI.hs +215/−0
- app/Main.hs +108/−0
- formulas.txt +20/−0
- judge.cabal +74/−0
- logic/J-ghari.yml +81/−0
- logic/J.yml +38/−0
- logic/LP.yml +46/−0
- src/Logic/Judge/Formula.hs +29/−0
- src/Logic/Judge/Formula/Datastructure.hs +320/−0
- src/Logic/Judge/Formula/Parser.hs +341/−0
- src/Logic/Judge/Formula/Substitution.hs +218/−0
- src/Logic/Judge/PointedList.hs +62/−0
- src/Logic/Judge/Prover/Tableau.hs +785/−0
- src/Logic/Judge/Prover/Tableau/Analytics.hs +52/−0
- src/Logic/Judge/Prover/Yaml.hs +154/−0
- src/Logic/Judge/Writer.hs +92/−0
- src/Logic/Judge/Writer/LaTeX.hs +158/−0
- src/Logic/Judge/Writer/Plain.hs +343/−0
+ CHANGELOG.md view
@@ -0,0 +1,54 @@+Changelog for judge+===============================================================================++All notable changes to this project will be documented in this file.++The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)+and this project adheres to the [Haskell Package Versioning +Policy](https://pvp.haskell.org/).++Unreleased+----------++[0.1.2.0] - 2018-01-19+----------------------++### Changed++ * Logic files in the designated data directories can now be specified + without extension, but must not occur in a subdirectory.++### Removed++ * Many previously exposed internal functions are now hidden.++++[0.1.1.0] - 2018-01-18+----------------------++### Added++ * Tableaux are now postprocessed to remove obviously superfluous rules.+ * Tableaux now document which formulas triggered branch closure.++### Removed++ * The `negation` and `contradicts` functions have been removed. + +### Changed++ * Closure is now exclusively triggered on properly signed formulas --- no + longer on finding `[T] A` and `[T] A -> 0`, and no longer on finding + `[T] A` for some assumption `A`.++++[0.1.0.0] - 2018-01-17+----------------------++### Added++ * First versioned release. Although it is the first version, the + application has been incubating for a while and should be mostly stable. + The commit history will take you deeper into the past.
+ LICENSE view
@@ -0,0 +1,674 @@+ GNU GENERAL PUBLIC LICENSE+ Version 3, 29 June 2007++ Copyright (C) 2007 Free Software Foundation, Inc. <http://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 <http://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:++ {project} Copyright (C) {year} {fullname}+ 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+<http://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+<http://www.gnu.org/philosophy/why-not-lgpl.html>.
+ README.md view
@@ -0,0 +1,57 @@+judge+==============================================================================++`judge` is a modular implementation of a decision procedure for classical and +justification logics, through a tableau-based theorem prover. ++++Installation+------------------------------------------------------------------------------++After cloning the repository, the recommended installation method is through +[Stack](https://www.stackage.org/):++ stack install judge++Alternatively, `judge` can be installed through +[Cabal](https://www.haskell.org/cabal/users-guide/).++++Usage+-------------------------------------------------------------------------------++`judge` expects a logical system to be defined in the [YAML](http://yaml.org/) +or [JSON](http://json.org/) format. This file will specify the type of proof +system and the logical family (although at the moment, only the respective +values `tableau` and `justification` are recognised). It also provides the +rules of inference. See the [logic](logic) directory for examples.++If no target formula(s) are provided via `-g`, formulas are read off the +standard input. If no output file is provided via `-o`, the result is written +to the standard output. By default, the format is plain text; add `-f LaTeX` +to obtain LaTeX code instead. ++For example, the following will construct proofs for [theorems](formulas.txt) +of the logic [Jcs](logic/J.yml) (with `c:(A→B→A) ∊ CS`), and produces a PDF +file to visualise them:++ judge logic/J.yml \+ -a "c:(A->B->A)" \+ -f LaTeX \+ < formulas.txt \+ | pdflatex++++Contributing+-------------------------------------------------------------------------------++Notable missing features are detailed on the [issue +tracker](https://github.com/slakkenhuis/judge/issues) +([export](https://api.github.com/repos/slakkenhuis/judge/issues)).++Contributions that extend `judge` to different logical families (modal, first +order...) or proof systems (sequent, natural deduction...) are welcomed.+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/CLI.hs view
@@ -0,0 +1,215 @@+{-|+Module : CLI+Description : Options to judge's command-line interface.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental+-}++{-# LANGUAGE PackageImports #-}+module CLI where++import Prelude hiding (getContents)++import "base" Data.Char (toLower)+import "base" Data.List (intercalate)+import "base" Data.Monoid ((<>))+import "base" Data.Version (showVersion)+import "base" Control.Applicative ((*>),(<*),(<|>))+import "base" Control.Monad (void, forM)+import "base" System.Info (os)+import "base" System.IO (FilePath, IOMode(WriteMode))+import "base" System.IO.Error (catchIOError)+import "base" GHC.IO.Handle (Handle, hIsTerminalDevice)+import "base" GHC.IO.Handle.FD (stdout, stderr, stdin, openFile)+import "text" Data.Text (Text, pack, unpack)+import "text" Data.Text.IO (getContents)+import qualified "filepath" System.FilePath as FP+import qualified "directory" System.Directory as D+import qualified "optparse-applicative" Options.Applicative as O+import qualified "attoparsec" Data.Attoparsec.Text as P+import qualified "ansi-wl-pprint" Text.PrettyPrint.ANSI.Leijen as PP++import Paths_judge (getDataDir, version) -- automatically generated+import Logic.Judge.Formula.Parser (parse, Parseable)+import qualified Logic.Judge.Writer as W++data Arguments = Arguments + { verbose :: Bool+ , _goals :: [String]+ , _assumptions :: [String]+ , _outfile :: Maybe String+ , format :: W.Format+ , _infile :: String+ }+++arguments :: IO Arguments+arguments = do+ logics <- map FP.takeBaseName <$> findLogics+ O.execParser (prog logics) ++ where++ prog logics = O.info+ ( O.helper <*> infoOptions logics <*> runOptions )+ ( O.fullDesc + <> O.progDescDoc (return description)+ <> O.header "judge - Decision procedure for formal logics" + <> O.footer "2017-2018, Utrecht University"+ )++ infoOptions logics = + O.infoOption + ("judge - version " ++ showVersion version)+ ( O.short 'V'+ <> O.long "version"+ <> O.help "Show version of the software and exit"+ ) + <*> O.infoOption + ("Available logical systems: " ++ intercalate ", " logics)+ ( O.short 'l'+ <> O.long "list-logics"+ <> O.help "List logical systems available in the data \n\+ \directories and exit"+ ) + + runOptions = Arguments+ <$> O.switch + ( O.short 'v'+ <> O.long "verbose"+ <> O.help "Show diagnostics"+ ) + <*> O.many+ ( O.strOption+ ( O.short 'g'+ <> O.long "goal"+ <> O.metavar "EXPR"+ <> O.help "Set target formula(s). May be provided multiple \n\+ \times (default: standard input)"+ )+ )+ <*> O.many+ ( O.strOption+ ( O.short 'a'+ <> O.long "assumption"+ <> O.metavar "EXPR"+ <> O.help "Add assumption(s). May be provided multiple times"+ )+ )+ <*> O.optional+ ( O.strOption+ ( O.short 'o'+ <> O.long "output"+ <> O.metavar "PATH"+ <> O.help "Output file (default: standard output)"+ )+ )+ <*> ( O.option O.auto+ ( O.short 'f' + <> O.long "format" + <> O.metavar "FORMAT"+ <> O.value W.Plain + <> O.showDefault+ <> O.help "Output format"+ )+ )+ <*> ( O.argument O.str (O.metavar "LOGIC"))++ description :: PP.Doc+ description = + (PP.line <>) + . PP.fillSep + . map PP.text + . words + $ "Decides whether given logical formulas are provable in some \n\+ \logical system. Takes a YAML or JSON file as input. Refer to \n\+ \README.md for more information."+++-- | Find all paths to logics in the resource directories.+findLogics :: IO [FilePath]+findLogics = do+ dat <- (FP.</> "logic") <$> getDataDir + xdg <- D.getXdgDirectory D.XdgData "judge"+ findFiles ["json", "yml", "yaml"] [xdg, dat]+++-- | Find all files with the given extensions in the given directories. If a+-- directory does not exist or has permission issues, it is simply ignored.+findFiles :: [String] -> [FilePath] -> IO [FilePath]+findFiles extensions dirs = concat <$> forM dirs findFiles++ where+ -- | Find all relevant files in the given directory.+ findFiles :: FilePath -> IO [FilePath]+ findFiles dir = do + { files <- filter correctExtension <$> D.listDirectory dir+ ; return $ map (dir FP.</>) files+ } `catchIOError` (\e -> return [])+++ -- | Check if the filepath has any of the accepted extensions.+ correctExtension :: FilePath -> Bool+ correctExtension path = flip any extensions $ + (/= Nothing) . + flip FP.stripExtension (map toLower path)+ +++-- | Return input file name, or, if it doesn't exist, check if it matches any+-- name in the resource directories.+infile :: Arguments -> IO String+infile args = do+ let name = _infile args+ exists <- D.doesFileExist name+ if exists+ then return name+ else do+ logics <- filter (match name) <$> findLogics+ case logics of+ (filename:_) -> return filename+ _ -> return name++ where++ match :: String -> FilePath -> Bool+ match name path = name `elem` [FP.takeBaseName path, FP.takeFileName path]++++-- | Obtain and open file handle for output file.+outfile :: Arguments -> IO Handle+outfile arg = maybe (return stdout) (flip openFile WriteMode) (_outfile arg)+++-- | Obtain additional assumptions. Taken from command line arguments.+assumptions :: Parseable f => Arguments -> IO [f]+assumptions arg = mapM (parse . pack) (_assumptions arg)+++-- | Obtain goal formulas. Taken from command line arguments or standard input.+goals :: Parseable f => Arguments -> IO [f]+goals arg = case _goals arg of+ [] -> do+ terminal <- hIsTerminalDevice stdin+ if terminal+ then W.prettyprint stderr notification+ else return ()+ getContents >>= parse+ xs -> mapM (parse . pack) xs++ where+ notification :: PP.Doc+ notification = + PP.text "Reading formulas from standard input" PP.<+>+ PP.lparen PP.<>+ eof PP.<+>+ PP.text "to finish" PP.<>+ PP.rparen++ eof :: PP.Doc+ eof = PP.bold . PP.text $ case os of+ "windows" -> "CTRL-Z"+ _ -> "CTRL-D"
+ app/Main.hs view
@@ -0,0 +1,108 @@+{-|+Module : Main+Description : Main module+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental+-}++{-# LANGUAGE PackageImports #-}+{-# LANGUAGE OverloadedStrings #-}++import "base" GHC.IO.Handle (Handle, hClose)+import "base" GHC.IO.Handle.FD (stdout, stderr)+import "base" Control.Monad (forM_)+import "base" Data.Maybe (fromJust)+import "text" Data.Text (Text, pack, unpack)+import qualified "yaml" Data.Yaml as Y+import qualified "unordered-containers" Data.HashMap.Strict as M2+import qualified "ansi-wl-pprint" Text.PrettyPrint.ANSI.Leijen as PP++import qualified CLI++import qualified Logic.Judge.Formula as F+import qualified Logic.Judge.Prover.Yaml as TY+import qualified Logic.Judge.Prover.Tableau as T+import qualified Logic.Judge.Prover.Tableau.Analytics as TX+import qualified Logic.Judge.Writer as W+++main :: IO ()+main = do+ arg <- CLI.arguments+ filename <- CLI.infile arg+ + W.prettyprint stderr $ + PP.bold (PP.string "Selected logical system:") PP.<+> + PP.string filename++ yaml <- deserialiseGeneric filename++ case yaml .: "logic" of+ "justification" -> case yaml .: "system" of+ "tableau" -> do+ sys <- addAssumptions + <$> (deserialise yaml :: IO (T.TableauSystem F.Justification))+ <*> (CLI.assumptions arg :: IO [F.FormulaJL])++ -- Tableau system is not prettyprinted well, so won't be shown+ -- even in verbose mode for now+ --if CLI.verbose arg+ -- then write stderr $ pretty sys+ -- else return ()++ targets <- CLI.goals arg :: IO [F.FormulaJL]+ file <- CLI.outfile arg+ let format = CLI.format arg ++ W.writeHeader file format+ forM_ targets $ \φ -> do++ if CLI.verbose arg+ then W.prettyprint stderr $ TX.analysis sys φ+ else return ()+ + W.writeBody file format (T.decide sys φ)+ W.writeFooter file format++ if file /= stdout+ then hClose file+ else return ()+++ value -> unknown value "system"+ value -> unknown value "logic"+ ++ where++ addAssumptions :: T.TableauSystem ext -> [F.Formula ext] -> T.TableauSystem ext+ addAssumptions system assumptions = + system { T.assumptions' = assumptions ++ T.assumptions' system }++ unknown :: Text -> Text -> IO ()+ unknown value key =+ fail $ "value '" ++ unpack value ++ "' for '" ++ unpack key ++ "' is unknown."+++-- | Get value from a YAML map at a key. If it doesn't exist, return @"undefined"@.+(.:) :: Y.Value -> Text -> Text+(Y.Object object) .: key = + let asText (Y.String s) = Just s+ asText _ = Nothing+ in maybe "undefined" id $ M2.lookup key object >>= asText +_ .: _ = "undefined"+++-- | Read a filename into a generic YAML value.+deserialiseGeneric :: String -> IO Y.Value+deserialiseGeneric path = either report return =<< Y.decodeFileEither path+ where report = fail . Y.prettyPrintParseException+-- make into handle++-- | Evaluate generic YAML into a typed value.+deserialise :: Y.FromJSON a => Y.Value -> IO a+deserialise = either (fail . show) return . Y.parseEither Y.parseJSON ++
+ formulas.txt view
@@ -0,0 +1,20 @@+##############################################################################+# This file contains some example formulas to try #+##############################################################################++# A simple propositional test+(~r → p) & (r → q) -> (p | q)++# The Application axiom should derive instantly in both j0-new and j0-ghari+x:A → y:(A → B) -> y*x:B++# ... and this one should fail instantly+x:A → y:(A → B) -> x*y:B++# This is a good one: it works in both j0-new and j0-ghari, but inspects about +# 18000 formulas in the latter (or 8000 if x:A is in the CS instead of the+# antecedent)+x:A → y:(A → B) → y*(x+x'):B++# ... And this one just gets too complex to find at all+x:A → y:(A → B) → (y+y')*x:B
+ judge.cabal view
@@ -0,0 +1,74 @@+name: judge+version: 0.1.2.0+synopsis: Tableau-based theorem prover.+description: An implementation of a decision procedure for classical + logic and justification logic.+homepage: https://github.com/slakkenhuis/judge#readme+license: GPL-3+license-file: LICENSE+author: ns@slak.ws+maintainer: ns@slak.ws+category: Logic+build-type: Simple+extra-source-files: README.md+ , CHANGELOG.md+ , formulas.txt+data-files: logic/J.yml+ , logic/LP.yml+ , logic/J-ghari.yml+cabal-version: >=1.10++library+ hs-source-dirs: src+ exposed-modules: Logic.Judge.PointedList+ , Logic.Judge.Formula+ , Logic.Judge.Formula.Datastructure+ , Logic.Judge.Formula.Parser+ , Logic.Judge.Formula.Substitution+ , Logic.Judge.Prover.Yaml + , Logic.Judge.Prover.Tableau+ , Logic.Judge.Prover.Tableau.Analytics+ , Logic.Judge.Writer+ , Logic.Judge.Writer.Plain+ , Logic.Judge.Writer.LaTeX+ build-depends: base >=4.7 && <5+ , text ==1.2.2.2+ , bytestring >=0.10.8.1 && <0.10.8.3+ , containers >= 0.5.7.1 && <0.5.10.3+ , unordered-containers ==0.2.8.0+ , vector >=0.11.0.0 && <0.12.0.2+ , attoparsec >=0.13.1.0 && <0.13.3.0+ , aeson >= 0.11.3.0 && <1.2.3.1+ , yaml >=0.8.23 && <0.8.26+ , pointedlist ==0.6.1+ , transformers ==0.5.2.0+ , mtl ==2.2.1+ , ansi-wl-pprint >=0.6.7.3 && <0.6.8.1+ , terminal-size ==0.3.2.1+ , utf8-string ==1.0.1.1+ , texmath >=0.10.1 && <0.11.0+ default-language: Haskell2010+++executable judge+ hs-source-dirs: app+ main-is: Main.hs+ other-modules: CLI+ , Paths_judge+ build-depends: base+ , judge+ , directory >=1.3.0.0 && <1.3.2.0+ , filepath >=1.4.1.1 && <1.4.2.0+ , text ==1.2.2.2+ , yaml >=0.8.23 && <=0.8.26+ , attoparsec >=0.13.1.0 && <0.13.3.0+ , ansi-wl-pprint >=0.6.7.3 && <0.6.8.1+ , optparse-applicative >=0.12.1.0 && <0.14.0.0+ , unordered-containers ==0.2.8.0+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ default-language: Haskell2010+++source-repository head+ type: git+ location: https://github.com/slakkenhuis/judge
+ logic/J-ghari.yml view
@@ -0,0 +1,81 @@+logic: justification+system: tableau+name: J₀+description: |+ This system stays mostly faithful to the one described in Ghari 2016. The + CSr rule was not present in the original; it emulates closure upon+ encountering [F] φ on the branch for some φ ∊ CS.+rules:+ - name: "Te"+ consume: ["[T] T:A"]+ produce:+ - ["[T, e] T:A"]++ - name: "Fe"+ consume: ["[F] T:A"]+ produce:+ - ["[F, e] T:A"]++ - name: "F→"+ consume: ["[F] A → B"]+ produce: + - ["[T] A", "[F] B"]++ - name: "T→"+ consume: ["[T] A -> B"]+ produce:+ - ["[F] A"]+ - ["[T] B"]++ - name: "F+"+ consume: ["[F, e] T+S:A"]+ produce:+ - ["[F, e] T:A", "[F, e] S:A"]++ - name: "T·"+ consume: ["[T, e] S:(A → B)", "[T, e] T:A"]+ produce:+ - ["[T, e] (S * T) : B"]+ restrict:+ and:+ - match: "A → B"+ with: [subterms, formulas]+ in:+ union: [root, assumptions]+ - match: "S * T"+ with: subterms+ in: root+ - name: "CSr"+ consume: []+ produce:+ - ["[T] A"]+ generate:+ match: "A"+ with: all+ in: assumptions+ - name: "PBe"+ consume: []+ produce:+ - ["[T, e] T:A"]+ - ["[F, e] T:A"]+ generate:+ and:+ - match: "A"+ with: [subterms, formulas]+ in: + union: [root, assumptions]+ - match: "T"+ with: [subterms, justifications]+ in: root++ - name: "PBf"+ consume: []+ produce:+ - ["[T] A"]+ - ["[F] A"]+ generate:+ match: "A"+ with: [subterms, formulas]+ in: + union: [root, assumptions]+
+ logic/J.yml view
@@ -0,0 +1,38 @@+logic: justification+system: tableau+name: J₀+description: |+ This is the system described in my thesis.+rules:+ - name: "F→"+ consume: ["[F] A → B"]+ produce: + - ["[T] A", "[F] B"]+ - name: "F+"+ consume: ["[F] T+S:A"]+ produce: + - ["[F] T:A", "[F] S:A"]+ - name: "T→"+ consume: ["[T] A -> B"]+ produce:+ - ["[F] A"]+ - ["[T] B"]+ - name: "F·"+ consume: ["[F] (S * T) : B"]+ produce:+ - ["[F] S:(A → B)"]+ - ["[F] T:A"]+ generate:+ match: "A → B"+ with: [subterms, formulas]+ in:+ union: [root, assumptions]+ - name: "CSr"+ consume: []+ produce:+ - ["[T] A"]+ generate:+ match: "A"+ with: all+ in: assumptions+assumptions: []
+ logic/LP.yml view
@@ -0,0 +1,46 @@+logic: justification+system: tableau+name: Logic of proofs+description: |+ This is the system for LP described in my thesis.+rules:+ - name: "F→"+ consume: ["[F] A → B"]+ produce: + - ["[T] A", "[F] B"]+ - name: "F+"+ consume: ["[F] T+S:A"]+ produce: + - ["[F] T:A", "[F] S:A"]+ - name: "e"+ consume: ["[T] T:A"]+ produce:+ - ["[T] A"]+ - name: "!"+ consume: ["[F] !T:T:A"]+ produce:+ - ["[F] T:A"]+ - name: "T→"+ consume: ["[T] A -> B"]+ produce:+ - ["[F] A"]+ - ["[T] B"]+ - name: "F·"+ consume: ["[F] (S * T) : B"]+ produce:+ - ["[F] S:(A → B)"]+ - ["[F] T:A"]+ generate:+ match: "A → B"+ with: [subterms, formulas]+ in:+ union: [root, assumptions]+ - name: "CSr"+ consume: []+ produce:+ - ["[T] A"]+ generate:+ match: "A"+ with: all+ in: assumptions+assumptions: []
+ src/Logic/Judge/Formula.hs view
@@ -0,0 +1,29 @@+{-|+Module : Logic.Judge.Formula+Description : Re-export of datastructure and class instances.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental++Re-export of the 'Formula' datastructure, including class instances.+-}++module Logic.Judge.Formula+ ( module Logic.Judge.Formula.Datastructure+ , module Logic.Judge.Formula.Parser+ , Extension+ ) where++import Logic.Judge.Formula.Datastructure+import Logic.Judge.Formula.Parser+import Logic.Judge.Formula.Substitution+++-- | Any extension of logical formulas is parseable, its extension+-- terms are subterms of its formulas, and they can be substituted into.+--+-- This encompassing class shortens class constraints and also avoids +-- UndecidableInstances in some cases.+class (Eq e, Ord e, Parseable e, Subterm e e, HasVariables e, Substitutable e e) => Extension e+instance Extension Justification
+ src/Logic/Judge/Formula/Datastructure.hs view
@@ -0,0 +1,320 @@+{-|+Module : Logic.Judge.Formula.Datastructure+Description : Basic datastructures and instances.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental++Plain datastructures, class instances and operations on logical formulas.+-}++{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PackageImports #-}+module Logic.Judge.Formula.Datastructure (+ -- * Datastructures+ -- ** Formulas+ Formula(..)+ , Marked(..)+ , Term(..)+ , Ambiguous(..)+ -- ** Extensions+ , Proposition+ , Predicate+ , FormulaML+ , FormulaJL+ , Classical+ , Quantifier(..)+ , Modality(..)+ , Justification(..)+ -- * Operations+ , simplify+ , asTerm+ , isFormula+ , isExtension+ , isMarkedFormula+ -- * Classes+ , Subterm(..)+ , HasVariables(..)+ ) where++import "base" Data.List (nub)++-- | For our purposes, a @Formula@ is a structure that is built upon a formula+-- of classical propositional logic. It has all the standard connectives, plus+-- an optional 'Extension' that may hold quantifiers, modalities, etcetera.+--+-- Note that it is generally expected that formulas will be 'simplify'ed+-- before being processed.+data Formula ext+ = Variable String -- a, b, c...+ | Constant Bool -- ⊥, ⊤ (Unicode: Mathematical Operators)+ | Extend ext (Formula ext) -- :+ | Negation (Formula ext) -- ¬~ (Unicode: Latin-1 Supplement)+ | Conjunction (Formula ext) (Formula ext) -- ∧&+ | Disjunction (Formula ext) (Formula ext) -- ∨|+ | XDisjunction (Formula ext) (Formula ext) -- ⊻^+ | Implication (Formula ext) (Formula ext) -- →-> (Unicode: Arrows)+ | BiImplication (Formula ext) (Formula ext) -- <->↔ (Unicode: Arrows)+ deriving (Eq, Ord)+++-- | Formulas of propositional logic.+type Proposition = Formula Classical++-- | Formulas of predicate logic.+type Predicate = Formula Quantifier ++-- | Formulas of modal logic.+type FormulaML = Formula Modality ++-- | Formulas of justification logic.+type FormulaJL = Formula Justification +++-- | The formula extension for classical propositional logic is empty.+type Classical = ()++-- | Predicate logic is extended with quantifiers (and relation symbols,+-- unimplemented).+data Quantifier+ = Universal String -- ∀x (Unicode: Mathematical Operators)+ | Existential String -- ∃x (Unicode: Mathematical Operators)+ deriving (Eq)+++-- | Standard modal logics have two (dual) unary modal operators.+data Modality+ = Necessary -- □, K, ... (Unicode: Geometric Shapes)+ | Possible -- ◇, B, ... (Unicode: Geometric Shapes)+ deriving (Eq, Ord)+++-- | Justification logics are extended with justification terms.+data Justification+ = ProofVariable String -- x, y, z...+ | ProofConstant String -- a, b, c...+ | ProofChecker Justification -- !+ | Application Justification Justification -- ⋅ (Unicode: Latin-1 Supplement)+ | Sum Justification Justification -- ++ deriving (Eq, Ord)+++-- MARKS ---------------------------------------------------------------------++-- | A marked formula is simply a formula with zero or more string annotations.+-- This makes for easy generalisation: marks can carry the polarity of a+-- formula, as well as state information specific to a particular tableau+-- system.+data Marked formula = Marked + { marks :: [String]+ , unmarked :: formula+ } deriving (Eq, Ord)++instance Functor Marked where+ fmap f (Marked marks x) = Marked marks (f x)++--mark :: [String] -> Marked a -> Marked a+--mark new (Marked old x) = Marked (new ++ old) x++++-- BASIC MANIPULATIONS -------------------------------------------------------++-- | Simplify formulae to only falsehood, implication and justification. This+-- reduces the number of rules that need implementation.+simplify :: Formula ext -> Formula ext+simplify formula = case formula of+ Variable v -> Variable v+ Constant False -> Constant False+ Constant True -> Implication (Constant False) (Constant False)+ Extend e f -> Extend e (simplify f)+ Implication f1 f2 -> Implication (simplify f1) (simplify f2)+ Negation f -> Implication (simplify f) (Constant False)+ Disjunction f1 f2 -> simplify $ Implication (Negation f1) f2+ Conjunction f1 f2 -> simplify $ Negation (Implication f1 (Negation f2)) + XDisjunction f1 f2 -> simplify $ Conjunction (Implication (Negation f1) f2) (Implication (Negation f2) f1)+ BiImplication f1 f2 -> simplify $ Conjunction (Implication f1 f2) (Implication f2 f1)++++-- SUBTERMS ------------------------------------------------------------------++-- | The term datastructure disambiguates between terms of the logical language+-- and terms of the logical extension language (e.g. justifications).+--+-- The alternative to carrying this information at the value level is to have +-- a multi-parameter @Substructure sub base@ class relative to which operations +-- like @pattern@ing or the @occurs@ check are defined. Although that seemed +-- prettier in theory, it made the code a whole lot more complicated.+data Term ext+ = Formula (Formula ext)+ | Extension ext+ | MarkedFormula (Marked (Formula ext))+ deriving (Eq, Ord)++-- | Return true if and only if the term is a formula.+isFormula :: Term ext -> Bool+isFormula (Formula f) = True+isFormula _ = False++-- | Return true iff the term is a formula extension.+isExtension :: Term ext -> Bool+isExtension (Extension e) = True+isExtension _ = False++-- | Return true iff the term is a marked formula.+isMarkedFormula :: Term ext -> Bool+isMarkedFormula (MarkedFormula _) = True+isMarkedFormula _ = False+++-- | Interpret a marked formula as a choice of terms. Note that it is not+-- always clear whether a value from 'Terms' is meant as the marked or the+-- unmarked version — so we offer both.+asTerm :: Marked (Formula ext) -> [Term ext]+asTerm φ = [MarkedFormula φ, Formula . unmarked $ φ]++++-- | A parsed term may be ambiguous: "S" can be parsed as a Formula or as a+-- Justification. Such ambiguous are stored in an Ambiguous type to be resolved+-- later.+newtype Ambiguous term = Ambiguous [term]++++-- | The @Subterm@ class represents a relation between terms based on an+-- extension @ext@ (that is, formulas or extensions of formulas) and subterms +-- that may occur within those @ext@-terms.+class (Subterm ext) term where+ + -- | Return all the subterms occurring in a term. Note: May contain+ -- duplicates.+ subterms :: term -> [Term ext]++instance Subterm ext ext => Subterm ext (Term ext) where+ subterms (Formula f) = subterms f+ subterms (Extension e) = subterms e+ subterms (MarkedFormula f) = subterms f++instance Subterm ext ext => Subterm ext (Marked (Formula ext)) where+ subterms t@(Marked _ f) = (MarkedFormula t) : subterms f++instance Subterm ext ext => Subterm ext (Ambiguous (Term ext)) where+ subterms (Ambiguous terms) = terms >>= subterms++instance Subterm ext ext => Subterm ext (Formula ext) where+ subterms term = case term of+ t@(Variable var) -> [Formula t]+ t@(Constant a) -> [Formula t]+ t@(Implication a b) -> Formula t:subterms a ++ subterms b+ t@(Extend e a) -> Formula t:subterms e ++ subterms a++instance Subterm Justification Justification where+ subterms term = case term of+ t@(ProofVariable var) -> [Extension t]+ t@(ProofConstant c) -> [Extension t]+ t@(ProofChecker s) -> Extension t:subterms s+ t@(Application s u) -> Extension t:subterms s ++ subterms u+ t@(Sum s u) -> Extension t:subterms s ++ subterms u+++-- | The @HasVariables@ class is applicable to formulas and formula extensions+-- that consist of substructures with variables and constants, and operators to+-- combine them.+class HasVariables term where+ -- | Return the variables occurring in a term. Note: May contain+ -- duplicates.+ variables :: term -> [String]++ -- | Return true if the term is a variable.+ isVariable :: term -> Bool++ -- | Return true if the term is a constant.+ isConstant :: term -> Bool++ -- | Return true if the term is atomary.+ isAtomary :: term -> Bool+ isAtomary t = isConstant t || isVariable t++ -- | Return the number of operators in the term.+ size :: term -> Int+++instance HasVariables ext => HasVariables (Term ext) where+ variables (Formula f) = variables f+ variables (Extension e) = variables e+ variables (MarkedFormula f) = variables f++ isVariable (Formula f) = isVariable f+ isVariable (Extension e) = isVariable e+ isVariable (MarkedFormula f) = False++ isConstant (Formula f) = isConstant f+ isConstant (Extension e) = isConstant e+ isConstant (MarkedFormula f) = False++ size (Formula f) = size f+ size (Extension e) = size e+ size (MarkedFormula f) = size f+++instance HasVariables ext => HasVariables (Ambiguous (Term ext)) where+ variables (Ambiguous terms) = terms >>= variables++ isVariable (Ambiguous terms) = any isConstant terms++ isConstant (Ambiguous terms) = any isConstant terms++ size (Ambiguous []) = 0+ size (Ambiguous (t:_)) = size t++instance HasVariables term => HasVariables (Marked term) where+ variables (Marked _ f) = variables f++ isVariable (Marked _ f) = isVariable f++ isConstant (Marked _ f) = isConstant f++ size (Marked m f) = length m + size f++instance HasVariables ext => HasVariables (Formula ext) where+ variables term = case term of+ Variable var -> [var]+ Constant a -> []+ Implication a b -> variables a ++ variables b+ Extend e a -> variables e ++ variables a++ isVariable (Variable _) = True+ isVariable _ = False++ isConstant (Constant _) = True+ isConstant _ = False++ size term = case term of+ Implication a b -> 1 + size a + size b+ Extend a b -> 1 + size a + size b+ _ -> 0++instance HasVariables Justification where+ variables term = case term of+ ProofVariable var -> [var]+ ProofConstant c -> []+ ProofChecker s -> variables s+ Application s u -> variables s ++ variables u+ Sum s u -> variables s ++ variables u++ isVariable (ProofVariable _) = True+ isVariable _ = True++ isConstant (ProofConstant _) = True+ isConstant _ = False++ size term = case term of+ ProofChecker s -> 1 + size s+ Application a b -> 1 + size a + size b+ Sum a b -> 1 + size a + size b+ _ -> 0
+ src/Logic/Judge/Formula/Parser.hs view
@@ -0,0 +1,341 @@+{-|+Module : Logic.Judge.Formula.Parser+Description : Parser for formulas.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental++Attoparsec-based parser for various logical (sub)structures.+-}++{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PackageImports #-}+module Logic.Judge.Formula.Parser+ (+ -- * Parser typeclass+ Parseable(..)+ , parse+ -- * Formula parsers+ , formula+ , modality+ , justification+ , quantifier+ -- * Auxiliary parsers+ , named+ , marked+ , identifier+ , boolean+ , comments+ -- * Generic parser building+ , Operator+ , expression+ , ambiguity+ ) where++import Prelude hiding (length)+import "base" Data.List (tails, sortBy, groupBy)+import "base" Data.Function (on)+import "base" Data.Maybe (catMaybes, listToMaybe)+import "base" Data.Char (isAlphaNum, isUpper)+import "base" Control.Applicative ((<|>), (<*), (*>), liftA2)+import "text" Data.Text (Text, pack, unpack, empty, length)+import "attoparsec" Data.Attoparsec.Combinator ((<?>))+import qualified "attoparsec" Data.Attoparsec.Combinator as P (lookAhead)+import qualified "attoparsec" Data.Attoparsec.Text as P++import qualified Logic.Judge.Formula.Datastructure as F++--------------------------------------------------------------------------------+-- * Parser typeclass++-- | A Parseable is something with an associated Attoparsec 'P.Parser'.+class Parseable a where++ -- | A parser for type @a@.+ parser :: P.Parser a++ -- | In some cases, the parser for a type must be embellished with some+ -- other symbols when it occurs as part of a parser of a different type,+ -- but not when it occurs on its own. This parser allows us to specify this+ -- alternative.+ parserEmbedded :: P.Parser a+ parserEmbedded = parser+++instance Parseable f => Parseable [f] where+ parser = comments *> P.many1 (parser <* comments)+++instance Parseable F.Classical where+ parser = fail "proposition has no extension"+++instance Parseable F.Modality where+ parser = modality+++instance Parseable F.Quantifier where+ parser = quantifier+++instance Parseable F.Justification where+ parser = justification+ parserEmbedded = parser <* (spaced $ P.char ':')+++instance Parseable e => Parseable (F.Formula e) where+ parser = formula parserEmbedded+++instance Parseable f => Parseable (F.Marked f) where+ parser = marked parser+++instance Parseable e => Parseable (F.Ambiguous (F.Term e)) where+ -- Ambiguities encountered when parsing a 'F.Term' can only be resolved+ -- when the context is known, that is, when we know where the term will be+ -- used. Therefore, the ambiguity will have to be retained during parsing.+ parser = F.Ambiguous <$> ambiguity + [ F.Formula <$> parser+ , F.Extension <$> parser + , F.MarkedFormula <$> parser ]+++-- | Read a text into a parseable structure.+parse :: (Monad m, Parseable a) => Text -> m a+parse = either fail return . P.parseOnly (parser <* P.endOfInput)+++-------------------------------------------------------------------------------+-- * Generic parser builders++-- | Auxiliary: Compose a parser of a list of functions into a single function.+compose, composeReverse :: P.Parser [a -> a] -> P.Parser (a -> a)+compose = fmap $ foldr (.) id+composeReverse = fmap $ foldl (flip (.)) id+++-- | Operators wrap a parser for a function in additional information. Note+-- that the function they wrap must take arguments of the same type.+data Operator a = Infix Associativity (P.Parser (a -> a -> a))+ | Prefix (P.Parser (a -> a))+ | Postfix (P.Parser (a -> a))+data Associativity = L | R++-- | Build a parser for a recursive expression with prefix-, infix- and postfix+-- operators. Note: To avoid ambiguous left/right associative operators, don't +-- put multiple operators of different associative direction into one+-- precedence bucket.+expression :: [[ Operator a ]] ->+ P.Parser a + -> P.Parser a+expression buckets base = spaced $ foldl buildUpon (spaced base) buckets' where++ -- Associate all looser, 'pending' operators with each bucket + buckets' = zip buckets (map concat . tail . tails $ buckets)++ -- Build operators of looser precedence upon existing parser+ buildUpon tighterParser (current, pending) =+ let infixL = spaced $ P.choice [ p | Infix L p <- current ]+ infixR = spaced $ P.choice [ p | Infix R p <- current ]+ postfix = spaced $ P.choice [ p | Postfix p <- current ]+ prefix = spaced $ P.choice [ p | Prefix p <- current ]+ prefixLooser = spaced $ P.choice [ p | Prefix p <- pending ]++ -- Looser prefix operators are considered in @loosePrefix@ at this + -- level already, because we want to allow situations in which such+ -- an operator occurs immediately after a tighter one. After all,+ -- such occurrences are unambiguous whether they are in a sequence+ -- of prefixes or occurring in an infix expression. To illustrate,+ -- consider consider infix operators ⊙ₚ and prefix operators ⊡ₚ+ -- with precedence p (lower is tighter). The following readings + -- are the only reasonable ones:+ -- 'a ⊙₂ ⊡₃ b ⊙₁ c' → 'a ⊙₂ (⊡₃ (b ⊙₁ c))'+ -- 'a ⊙₁ ⊡₂ b ⊙₃ c' → '(a ⊙₁ (⊡₂ b)) ⊙₃ c'+ + postfixes = composeReverse $ P.many' postfix+ prefixesLooser = compose $ P.many' prefixLooser+ prefixes = compose $ (:) + <$> prefix+ <*> P.many' (prefixLooser <|> prefix)+ <|> return []++ continueL x = do f <- infixL+ g <- prefixesLooser+ y <- tighterParser+ continueL (x `f` g y) <|> return (x `f` g y)+ + continueR x = do f <- infixR+ g <- prefixesLooser+ y' <- tighterParser+ y <- continueR y' <|> return y'+ return $ x `f` g y+ + in do f <- prefixes+ x <- tighterParser+ g <- postfixes+ let y = g (f x) in continueL y <|> continueR y <|> return y++++-- | Given a number of parsers that introduce an ambiguity (e.g. parsers that+-- may succeed on precisely the same text), collects the results of all+-- successful parses, provided that at least one succceeds.+ambiguity :: [P.Parser a] -> P.Parser [a]+ambiguity options = do+ (n, results) <- longestParses =<< consider options+ P.take n+ return results+ where + + -- | Try to apply a parser without actually consuming input. This will+ -- tell us whether the parse would succeed, what text it would consume+ -- and what its result would be.+ whatIf :: P.Parser a -> P.Parser (Maybe (Text, a))+ whatIf p = P.option Nothing (Just <$> P.lookAhead (P.match p))++ -- | Consider what would happen if we ran the given parsers. Collect the+ -- ones that would succeed, remembering what they would consume.+ consider :: [P.Parser a] -> P.Parser [(Text, a)]+ consider = fmap catMaybes . sequence . map whatIf++ -- | There may be multiple successful parses. The longest parse is the + -- 'real' one; ambiguity only exists if there are multiple such parses,+ -- since it would otherwise already have been resolved by whatever suffix + -- the shorter parses were unable to process. This function finds the+ -- longest parses among a list of parse results produced by 'consider', and+ -- also tells us how many characters would be consumed.+ longestParses :: [(Text, a)] -> P.Parser (Int, [a])+ longestParses =+ maybe (fail "failed at ambiguity") return . + fmap (\xs -> (fst $ head xs, map snd xs)) . + listToMaybe .+ groupBy ((==) `on` fst) . + reverse .+ sortBy (compare `on` fst) .+ map (\(x, y) -> (length x, y))++++-------------------------------------------------------------------------------+-- * Formula parsers+++-- | Builds a parser for formulas of classical propositional logic extended+-- with some type @e@.+formula :: P.Parser ext -> P.Parser (F.Formula ext)+formula extension = expression operators base ++ where+ operators = + [ [ Prefix (oneOf ['~','¬'] >> return F.Negation) ]+ , [ Infix L (oneOf ['&','∧'] >> return F.Conjunction) ]+ , [ Infix L (oneOf ['|','∨'] >> return F.Disjunction) ]+ , [ Infix L (oneOf ['^','⊻'] >> return F.XDisjunction) ]+ , [ Infix R (oneOf' ["->", "→"] >> return F.Implication) ]+ , [ Infix R (oneOf' ["<-", "←"] >> return (flip F.Implication)) ]+ , [ Infix R (oneOf' ["<->", "↔"] >> return F.BiImplication) ]+ ]+ + base = (F.Extend <$> extension <*> (optPrefixed <*> base) )+ <|> (F.Constant <$> boolean)+ <|> (F.Variable <$> identifier)+ <|> (P.char '(' *> formula extension <* P.char ')')+ <?> "formula term"++ -- Parser that parses and applies zero or more prefixes. This exists+ -- because prefixes need not be wrapped in parentheses when they occur+ -- directly after the extension operator.+ optPrefixed = + compose . P.many' . P.choice $ + [ p | bucket <- operators, Prefix p <- bucket ]+++-- | Parser for modal operators of modal logic.+modality :: P.Parser F.Modality+modality = (oneOf' ["[]","□"] >> return F.Necessary) + <|> (oneOf' ["<>","◇"] >> return F.Possible)+++-- | Parser for quantifiers of first-order predicate logic.+quantifier :: P.Parser F.Quantifier+quantifier = quantor <*> identifier <* P.char '.' + where+ quantor = (oneOf' ["\\A","∀"] >> return F.Universal) + <|> (oneOf' ["\\E","∃"] >> return F.Existential)+++-- | Parser for justification terms of justification logic.+justification :: P.Parser F.Justification+justification = expression operators base ++ where+ operators = + [ [ Prefix (oneOf ['!'] >> return (F.ProofChecker)) ]+ , [ Infix L (oneOf ['+'] >> return (F.Sum)) ]+ , [ Infix L (oneOf ['*','⋅','·'] >> return (F.Application)) ]+ ]++ base = (toAtom <$> identifier)+ <|> (P.char '(' *> justification <* P.char ')')+ <?> "justification term"++ toAtom s | isUpper (head s) = F.ProofVariable s+ | otherwise = F.ProofConstant s++++-------------------------------------------------------------------------------+-- * Auxiliary parsers+++-- | Auxiliary: Parser that accepts and returns any @Char@ in a given list of @Char@s.+oneOf :: [Char] -> P.Parser Char+oneOf c = P.satisfy (`elem` c)+++-- | Auxiliary: Parser that accepts and returns any string in a given list of strings.+oneOf' :: [String] -> P.Parser String+oneOf' s = fmap unpack $ P.choice (map (P.string . pack) s)+++-- | Auxiliary: Skip surrounding spaces.+spaced :: P.Parser a -> P.Parser a+spaced p = P.skipSpace *> p <* P.skipSpace+++-- | Parser that accepts and returns any string that starts with a letter.+identifier :: P.Parser String+identifier = liftA2 (:) P.letter (unpack <$> P.takeWhile (\x -> isAlphaNum x || x == '\''))+ <?> "identifier"+++-- | Parser that accepts a boolean (as binary number or unicode ⊥, ⊤).+boolean :: P.Parser Bool+boolean = (oneOf "⊥0" >> return False) <|> (oneOf "⊤1" >> return True)+ <?> "boolean"+++-- | Make a parser for something that is named by prepending it with an +-- identifier and a = sign.+named :: P.Parser x -> P.Parser (String, x)+named p = (,) + <$> (identifier <* (spaced $ P.char '=')) + <*> p+++-- | Parser for a marked formula.+marked :: P.Parser formula -> P.Parser (F.Marked formula)+marked p = F.Marked <$> P.option [] marks <*> p where + marks = (spaced $ P.char '[') + *> P.sepBy' identifier (spaced $ P.char ',') <* + (spaced $ P.char ']')+++-- | Parser for comments.+comments :: P.Parser ()+comments = + P.skipSpace *> P.skipMany (+ P.char '#' *> P.manyTill P.anyChar P.endOfLine <* P.skipSpace+ )
+ src/Logic/Judge/Formula/Substitution.hs view
@@ -0,0 +1,218 @@+{-|+Module : Logic.Judge.Formula.Substitution+Description : Obtain variable assignments and apply substitutions.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental++This module makes it possible to obtain variable assignments by comparing +'Formula's, and to apply substitutions based on them.++The idea is similar to, but /not the same as/ unification. When we pattern @x@ +to @y@, the former is schematic and the latter is literal. Even though their+variables can be structurally identical, they are really different, in that,+for example, @Var "x"@ may well pattern with @Implication (Var "x") (Var "x")@,+resulting in the substitution @[("x", Implication "x" "x")]@.++Nevertheless, see @subsumes@ from @Control.Unification@. They are not related +by code, but the purpose is similar.+-}++{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PackageImports #-}+module Logic.Judge.Formula.Substitution + ( Substitution+ , Substitutable(substitute, pattern, patternContinue)+ , merge+ ) where++import "base" Control.Monad (void, when, sequence, ap)+import "transformers" Control.Monad.Trans.Class (lift, MonadTrans)+import "transformers" Control.Monad.Trans.State.Lazy (StateT(StateT), execStateT, get, put, evalStateT)+import qualified "containers" Data.Map as M++import Logic.Judge.Formula.Datastructure+++-- | A substitution maps identifiers to terms of a logic.+type Substitution ext = M.Map String (Term ext)+++-- | Monad that supports state and failure.+type StateFail state result = StateT state Maybe result+++-- | The 'Substitutable' class represents a relation between terms based on an +-- extension @ext@ (that is, formulas or extensions of formulas) and subterms +-- that may be substituted for variables inside those @ext@-terms.+class Substitutable ext term where++ -- | Apply a substitution to a term.+ --+ -- Note that at the time of writing, there is no fundamental distinction+ -- between variables and schematic variables.+ substitute :: Monad m + => Substitution ext + -> term+ -> m term+++ -- | @a `pattern` b@ tries to find a substitution such that @a@ matches+ -- @b@. The @a@ formula is taken as a schematic formula, where variables+ -- represent gaps to be filled in, and @b@ is a "normal" formula, in which+ -- variables represent literals.+ --+ -- For simplicity, this function assumes that the formulas have been + -- 'simplify'ed. The intention is to make this explicit via a @newtype@ at+ -- some point.+ pattern :: (Monad m)+ => term -- ^ The 'pattern' formula to be filled in.+ -> term -- ^ The formula to fill in the pattern.+ -> m (Substitution ext)+ pattern = patternContinue M.empty+++ -- | Same as 'pattern', but starts patterning from a given starting state.+ patternContinue :: (Monad m)+ => Substitution ext+ -> term+ -> term+ -> m (Substitution ext)+ patternContinue m a b = maybe (fail "pattern failed") return $ execStateT (patternM a b) m+++ -- | Auxiliary monad, accompanying the 'pattern' function: assign variables+ -- from the first formula to subformulas of the second formula, step by + -- step, so as to obtain a substitution that would make the former equal to + -- the latter. In order to be able to short-circuit as early as possible, + -- this is done in a combination of the Maybe and State monads.+ patternM :: ()+ => term + -> term + -> StateFail (Substitution ext) ()++++instance (Eq ext, Substitutable ext a) => Substitutable ext (Marked a) where+ patternM (Marked m1 x1) (Marked m2 x2) = do+ when (not $ all (`elem` m2) m1 && all (`elem` m1) m2) shortcircuit+ patternM x1 x2++ substitute subst (Marked marks x) = Marked marks <$> substitute subst x++++instance (Eq ext, Substitutable ext ext) => Substitutable ext (Term ext) where+ patternM (Formula f1) (Formula f2) = patternM f1 f2+ patternM (Extension e1) (Extension e2) = patternM e1 e2+ patternM (MarkedFormula f1) (MarkedFormula f2) = patternM f1 f2+ patternM _ _ = shortcircuit++ substitute subst (Formula f) = Formula <$> substitute subst f+ substitute subst (Extension e) = Extension <$> substitute subst e+ substitute subst (MarkedFormula f) = MarkedFormula <$> substitute subst f+++instance (Eq ext, Substitutable ext ext) => Substitutable ext (Formula ext) where++ patternM (Variable var) term = + var `binds` Formula term+ patternM (Implication a1 a2) (Implication b1 b2) = do+ a1 `patternM` b1+ a2 `patternM` b2+ patternM (Extend e a) (Extend e' a') = do+ e `patternM` e'+ a `patternM` a'+ patternM (Constant a) (Constant b) = + when (a /= b) shortcircuit+ patternM _ _ = shortcircuit++ substitute subst term = case term of+ Variable var -> case M.lookup var subst of+ Just (Formula t') -> return t'+ Just _ -> fail $ "gap requires different type at '" ++ var ++ "'"+ _ -> fail $ "variable '" ++ var ++ "' undefined"+ Constant a -> return $ Constant a+ Implication a b -> Implication <$> substitute subst a <*> substitute subst b+ Extend e a -> Extend <$> substitute subst e <*> substitute subst a++++instance Substitutable Justification Justification where++ patternM (ProofVariable var) term = + var `binds` Extension term+ patternM (ProofChecker a) (ProofChecker b) = + a `patternM` b+ patternM (Application a1 a2) (Application b1 b2) = do+ a1 `patternM` b1+ a2 `patternM` b2+ patternM (Sum a1 a2) (Sum b1 b2) = do+ a1 `patternM` b1+ a2 `patternM` b2+ patternM (ProofConstant a) (ProofConstant b) = + when (a /= b) shortcircuit+ patternM _ _ = shortcircuit++ substitute subst term = case term of+ ProofVariable var -> case M.lookup var subst of+ Just (Extension t') -> return t'+ Just _ -> fail $ "gap requires different type at '" ++ var ++ "'"+ _ -> fail $ "variable '" ++ var ++ "' undefined"+ ProofConstant c -> return (ProofConstant c)+ ProofChecker s -> ProofChecker <$> substitute subst s+ Application s t -> Application <$> substitute subst s <*> substitute subst t+ Sum s t -> Sum <$> substitute subst s <*> substitute subst t+++++-- | Auxiliary: Lifts failure from an underlying Maybe monad from within a+-- monad transformer.+shortcircuit :: MonadTrans t => t Maybe a+shortcircuit = lift Nothing+++-- | Auxiliary: Try to add or verify a binding to a substitution monad. Fail+-- if the binding conflicts with an existing one in the substitution state.+binds :: (Eq ext)+ => String+ -> Term ext + -> StateFail (Substitution ext) ()+binds k v = maybe (shortcircuit) (void . put) . insert k v =<< get+++-- | Insert value @v@ at key @k@. If there is already a value at @k@, this will+-- fail, unless the existing value at @k@ is identical to the new one.+insert :: (Ord k, Eq v, Monad m) => k -> v -> M.Map k v -> m (M.Map k v)+insert k v m = sequence $ M.insertWith identical k (return v) (fmap return m)+++-- | Combine two substitutions, but fail if they are conflicting. +--+-- Note: The union is more efficient if the biggest set is the first argument.+merge :: (Ord k, Eq v, Monad m) => M.Map k v -> M.Map k v -> m (M.Map k v)+merge a b = sequence $ M.unionWith identical (return <$> a) (return <$> b)+++-- | Fail if the results of two actions are not the same. In the context of the+-- Maybe monad: only return a value if the first and second argument values+-- are present and equal to eachother.+identical :: (Eq a, Monad m) => m a -> m a -> m a+identical xm ym = do+ x <- xm+ y <- ym+ if x == y then return x + else fail "Conflicting assignment."+++-- | Execute our state monad given a start state, and collect both its final +-- state and its result.+execute :: state -> StateFail state result -> Maybe (state, result)+execute startstate monad = flip evalStateT startstate $ do+ result <- monad+ state <- get+ return (state, result)
+ src/Logic/Judge/PointedList.hs view
@@ -0,0 +1,62 @@+{-|+Module : Logic.Judge.PointedList+Description : Re-export 'Data.List.PointedList' with convenience functions.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental++Re-export 'Data.List.PointedList' with convenience functions.+-}++{-# LANGUAGE PackageImports #-}+module Logic.Judge.PointedList + ( module L+ , asList+ , toList+ , current+ , insertAll+ , focus+ , modify+ , update+ ) where++import "pointedlist" Data.List.PointedList as L hiding (focus)+import "base" Data.Foldable (toList)++-- | Turn a 'PointedList' into a non-pointed list, assuming no particular+-- ordering.+asList :: L.PointedList a -> [a]+asList (L.PointedList prefix x postfix) = x : prefix ++ postfix+++-- | Get the current focus of a 'PointedList'.+current :: L.PointedList a -> a+current = L._focus+++-- | Add a number of entries to a possibly empty 'PointedList'.+insertAll :: Traversable t => t a -> Maybe (L.PointedList a) -> Maybe (L.PointedList a)+insertAll xs Nothing = L.fromList . toList $ xs+insertAll xs (Just l) = return . foldr L.insertLeft l $ xs+++-- | Create a list of variations of the provided 'PointedList', one for each+-- element to take focus. +--+-- This function is a bit sloppy. It assumes no particular order. Note that using+-- 'toList' instead can cause longer (or shorter?) running times.+focus :: L.PointedList a -> [L.PointedList a]+focus = asList . L.positions+++-- | Update the focused element of a 'PointedList' using a function that+-- returns 'Just' the new value, or 'Nothing' for deletion.+modify :: L.PointedList a -> (a -> Maybe a) -> Maybe (L.PointedList a)+modify xs f = maybe (L.delete xs) (Just . flip L.replace xs) . f $ current xs+++-- | Update the focused element of a 'PointedList' with the value of the+-- 'Just', or delete the element if that value is 'Nothing'.+update :: L.PointedList a -> Maybe a -> Maybe (L.PointedList a)+update xs = modify xs . const
+ src/Logic/Judge/Prover/Tableau.hs view
@@ -0,0 +1,785 @@+{-|+Module : Logic.Judge.Prover.Tableau+Description : A tableau-based decision algorithm.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental++A generic decision algorithm based on the method of analytic tableaux.+-}++{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PackageImports #-}+module Logic.Judge.Prover.Tableau (+ -- * Input structures+ TableauSystem(..)+ , Constraint(..)+ , Compositor(..)+ , Rule(..)+ , RuleUninstantiated+ -- ** Term specification+ , PrimitiveDynamicTerms(..)+ , PrimitiveStaticTerms(..)+ , Terms(..)+ , DynamicTerms+ , StaticTerms+ -- * Decision algorithm+ , decide+ , initial+ -- ** Intermediate structures+ , TableauSettings(..)+ , Ref(..)+ , Branch(..)+ , BranchFormula+ , RuleInstantiated+ -- ** Output structures+ , Result(..)+ , Tableau(..)+ -- ** Postprocessors+ , shorten+ , renumber+ , rewrite+ -- * Auxiliaries+ , greedy+ , intersection+ , combinations+ ) where++import "base" Debug.Trace (trace, traceShow, traceM, traceShowM)++import "base" Data.Maybe (listToMaybe, mapMaybe, catMaybes, fromJust)+import "base" Data.List (intersect, partition, lookup, nub, sortBy, (\\))+import "base" Data.Function (on)+import "base" Control.Applicative (Alternative, empty, (<|>))+import "base" Control.Monad (foldM, guard, forM, forM_, join)+import qualified "containers" Data.Tree as R+import qualified "containers" Data.Map as M+import qualified "containers" Data.Set as S+import qualified "transformers" Control.Monad.Trans.State.Lazy as ST++import qualified Logic.Judge.PointedList as L+import qualified Logic.Judge.Formula as F+import qualified Logic.Judge.Formula.Substitution as Fσ+++-- | Formulas on the branch are decorated by their reference number and marks.+type BranchFormula ext = Ref Int (F.Marked (F.Formula ext))+++-- | Relates values to their identifiers.+data Ref ref val = (:=) { reference :: ref, value :: val }+infixr 7 :=++++-- | Like 'Either', but remembers the original input in the 'Right' case, too.+data Result input output+ = Success input output+ | Failure input+++ +-- | A proof in a tableau system is a rose tree, containing sets of formulas+-- and the rule applications used to obtain them.+data Tableau ext+ = Node [BranchFormula ext] (Tableau ext)+ | Application String [Int] [Tableau ext]+ | Closure [Int]++++-- | Before initialisation, the tableau system is read into this structure.+data TableauSystem ext = TableauSystem+ { title :: String+ , rules :: [RuleUninstantiated ext]+ , assumptions' :: [F.Formula ext]+ }++++-- | The global state of the tableau — settings that will remain static after +-- initialisation.+data TableauSettings ext = TableauSettings+ { rulesC :: [RuleInstantiated ext]+ -- ^ The consumer rules are those rules that take a consumption from the+ -- branch. They are always available.+ , root :: F.Marked (F.Formula ext)+ -- ^ The root of the tableau.+ , assumptions :: [F.Formula ext]+ -- ^ The assumptions or the constant specification.+ }+++-- | A constraint is placed on a tableau rule to restrict the values to which+-- its variables can be bound. This means that some applications of the rule+-- will be blocked; but also that any "free" or "generative" variables (that +-- is, variables that occur in the rule's productions but not in its+-- consumptions) can now be associated with a set of possible assignments, +-- thereby making it possible to, essentially, generate a /choice/ of multiple +-- /instantiations/ of a single rule.+data Constraint primitive ext+ = None+ -- | Demand that the pattern occurs in a particular set of terms.+ | Bind (F.Ambiguous (F.Term ext)) (Terms primitive ext)+ -- | Constraint holds if one of the subconstraints hold.+ | Choose [Constraint primitive ext]+ -- | Constraint holds if all subconstraints hold.+ | Merge [Constraint primitive ext]+++-- | Indicates how to handle the situation where multiple rule instantiations+-- are applicable to the same formula.+--+-- Due to their computational complexity, rules that do not take any +-- consumptions are handled greedily regardless of the value of the +-- compositor.+data Compositor = Greedy | Nondeterministic+++-- | Before instantiation, a generator is /described/ by a constraint. This+-- constraint can only refer to static terms.+type RuleUninstantiated ext = Rule (Constraint PrimitiveStaticTerms ext) ext+++-- | After instantiation, a generator consists of all variable assignments that+-- it allows.+type RuleInstantiated ext = Rule (L.PointedList (Fσ.Substitution ext)) ext+++-- | A rule describes which formulas it consumes and which it produces. In its+-- basic form, it can represent both instantiated and uninstantiated tableau+-- rules (see 'RuleInstantiated' and 'RuleUninstantiated').+data Rule generator ext = Rule + { name :: String+ -- ^ Identifier by which the rule shall be known.+ , consumptions :: [ F.Marked (F.Formula ext) ]+ -- ^ The consumptions (also: premises, antecedents, conditions) are+ -- formulas that are to be present on the branch before the rule may be+ -- applied.+ , productions :: [[ F.Marked (F.Formula ext) ]]+ -- ^ The productions (also: conclusions, consequents, results) are the+ -- formulas that will be created on the branch when the rule is applied. + -- Represents a disjunction of conjunctions.+ , generator :: generator+ -- ^ A generator is a "permissive constraint", which represents a choice + -- between possible variable assignments. This approach is necessary to be+ -- able to handle free variables in the productions: such variables+ -- do not have a pre-existing binding to check for compliance, so they + -- need to be created. This also makes it possible to keep track of which + -- bindings have already been attempted over the course of an algorithm,+ -- thus allowing for termination guarantees in case termination is not+ -- certain otherwise.+ -- + -- The limitation of the generator is that it is not very efficient and+ -- that no variable may be bound to terms from a dynamic set, since the + -- generator has to generate its instances at the beginning of the + -- algorithm. (Note that the last point can be dropped if we do not need to+ -- keep track of which bindings have already been used.)+ , constraint :: Constraint PrimitiveDynamicTerms ext+ -- ^ Although the generator /does/ also restrict bound variables (with + -- brute force: a variable's previous binding will block all conflicting + -- assignments), it is more computationally efficient to simply check + -- already known values for compliance, during runtime. + --+ -- The limitation of restrictive constraints is that they cannot deal with+ -- /free/ variables. + , compositor :: Compositor+ -- ^ The compositor indicates how to handle the case where multiple + -- instances are suggested by the generator.+ }+++-- | A @Branch@ keeps track of the leaf of a single branch of the tableau, and+-- all that came before.+data Branch ext = Branch+ { rulesA :: Maybe (L.PointedList (RuleInstantiated ext))+ -- ^ The ascetic rules are those rules that do not take a consumption from+ -- the branch. In order to guarantee termination, they can be used only+ -- once per branch — we therefore keep track of which rules can still be+ -- used.+ , actives :: Maybe (L.PointedList (BranchFormula ext))+ -- ^ Which formulas still lie unprocessed on the branch?+ , inactives :: [BranchFormula ext]+ -- ^ Which formulas have been processed on the branch?+ , new :: [BranchFormula ext]+ -- ^ Which formulas were the last to be introduced?+ , counter :: Int+ -- ^ The next identifier never to have occurred on the branch before.+ }+++-- | A @Match@ keeps track of information that is required when we are checking+-- the applicability of a rule to a branch.+data Match ext = Match+ { matched :: [BranchFormula ext]+ -- ^ Which formulas (including their IDs) have been matched?+ , assignment :: Fσ.Substitution ext+ -- ^ Variable assignments forced by the match so far.+ , remainder :: Maybe (L.PointedList (BranchFormula ext))+ -- ^ Formulas remaining active on the branch after this match.+ , rule :: RuleInstantiated ext+ -- ^ Which rule was applied during the match?+ , rule' :: Maybe (RuleInstantiated ext)+ -- ^ If application of the rule changes the rule, that is recorded here. + }++++-- | Determine if the most recent additions to the branch cause the branch to+-- close by causing a contradiction.+closes :: forall ext . Eq ext + => Branch ext + -> Maybe [Int]+closes π@(Branch {new, actives, inactives}) =++ first (map contradiction new) <|>+ contradict new new <|>+ contradict new inactives <|>+ contradict new (maybe [] L.asList actives)+ + where++ first :: Foldable t => t (Maybe a) -> Maybe a+ first = foldl (<|>) Nothing++ contradict :: [BranchFormula ext] -> [BranchFormula ext] -> Maybe [Int]+ contradict xs ys = first (xs >>= \x -> return $ first (map (contradicts x) ys))++ hasF = any (=="F")++ contradiction :: BranchFormula ext -> Maybe [Int]+ contradiction (i := (F.Marked marks formula)) = case formula of+ F.Constant True -> if hasF marks + then Just [i] + else Nothing+ F.Constant False -> if not $ hasF marks + then Just [i] + else Nothing+ _ -> Nothing++ contradicts :: BranchFormula ext -> BranchFormula ext -> Maybe [Int]+ contradicts (i := F.Marked m1 f1) (j := F.Marked m2 f2) = + if ((hasF m1 && not (hasF m2)) || (hasF m2 && not (hasF m1))) && f1 == f2+ then Just [i, j]+ else Nothing++++-- | Check that a variable assignment does not conflict with a constraint.+respects :: forall ext . (F.Extension ext)+ => (DynamicTerms ext -> [F.Term ext])+ -> Fσ.Substitution ext+ -> Constraint PrimitiveDynamicTerms ext+ -> Bool+respects concretise σ ι = case ι of+ None -> True+ Choose ιs -> any (respects concretise σ) ιs + Merge ιs -> all (respects concretise σ) ιs+ Bind scheme τ -> anyMatching scheme τ++ where + anyMatching :: F.Ambiguous (F.Term ext) -> DynamicTerms ext -> Bool+ anyMatching (F.Ambiguous schemes) τ = not . null . catMaybes $ + [ Fσ.patternContinue σ scheme target+ | scheme <- schemes+ , target <- concretise τ+ ]+++++-------------------------------------------------------------------------------+-- * Initialisation+++-- | Instantiate a rule. Instantiation entails the following:+--+-- 1. Sort the order of its premises in decreasing order of size. +-- 2. Generating the variable assignments as specified by the generator.+--+-- Note that a rule is useless if there is not a single appropriate assignment +-- for the generator.+instantiateRule :: forall ext . (F.Extension ext)+ => (StaticTerms ext -> [F.Term ext])+ -> RuleUninstantiated ext+ -> Maybe (RuleInstantiated ext)+instantiateRule concretise ρ@Rule {generator, consumptions} = + fmap + (\instances -> ρ { generator = instances + , consumptions = ordered consumptions })+ (L.fromList . assign $ generator)++ where++ -- | The consumptions should be sorted in order of decreasing complexity,+ -- since matching the most complex formula first (in `matchRule`) decreases+ -- the number of subsequent matches the most and will thus be more+ -- efficient.+ ordered :: [F.Marked (F.Formula ext)] -> [F.Marked (F.Formula ext)]+ ordered = reverse . sortBy (compare `on` F.size)++ -- | Turn a specification of a generator into an actual set of possible+ -- assignments.+ assign :: Constraint PrimitiveStaticTerms ext -> [Fσ.Substitution ext]+ assign ι = nub $ case ι of+ None -> [mempty]+ Choose ιs -> concat $ map assign ιs+ Merge ιs -> merge $ map assign ιs+ Bind (F.Ambiguous schemes) terms -> catMaybes $ + [ Fσ.pattern scheme target + | scheme <- schemes+ , target <- concretise terms+ ]++ -- | Create a single generator that respects multiple generators + -- simultaneously. To see that this is valid, observe that a generator is + -- really just a list of possible assignments, e.g., a disjunction. To + -- rearrange a conjunction of disjunctions into a single disjunction, we+ -- find every way to draw a single disjunct from each conjunct, and merge+ -- every non-conflicting combination we thus find.+ merge :: [[Fσ.Substitution ext]] -> [Fσ.Substitution ext]+ merge = mapMaybe (foldM Fσ.merge mempty) . combinations++++++-- | Construct the initial branch and settings for the decision algorithm.+initial :: forall ext . (F.Extension ext) + => TableauSystem ext+ -> F.Formula ext+ -> (TableauSettings ext, Branch ext)+initial system goal = (initκ, initπ)++ where++ -- | Initial settings+ initκ :: TableauSettings ext+ initκ = TableauSettings+ { rulesC = rulesC+ , root = value $ L.current root+ , assumptions = assumptions' system+ }++ -- | Initial branch+ initπ :: Branch ext+ initπ = Branch + { actives = return root+ , inactives = []+ , rulesA = L.fromList rulesA+ , new = L.toList root+ , counter = 1+ }++ -- | Root of the tableau.+ root :: L.PointedList (BranchFormula ext)+ root = L.singleton (0 := F.Marked ["F"] (F.simplify goal))++ -- | Rules are seperated into ascetic rules and consumer rules. To preserve+ -- termination, the former may be applied only once per branch, while the+ -- latter can be applied any number of times.+ (rulesA, rulesC) = + partition (null . consumptions) + . mapMaybe (instantiateRule (concretiser (static initκ)))+ . rules + $ system++++-------------------------------------------------------------------------------+-- * Matching branches++-- | A tableau rule has zero or more formula schemes that represent+-- consumptions. These must be matched against the concrete formulas that+-- remain on the branch unprocessed. This function provides all possible +-- 'Match'es, but does not further instantiate the matches.+--+-- For efficiency, the "biggest" consumptions should be the first to be +-- matched.+matchRule :: forall ext . (F.Extension ext)+ => Branch ext+ -> RuleInstantiated ext+ -> [Match ext]+matchRule π ρ@Rule {consumptions} =+ foldM match μ₀ consumptions+ + where++ -- | Initial match.+ μ₀ :: Match ext+ μ₀ = Match + { matched = mempty+ , assignment = mempty+ , remainder = actives π+ , rule = ρ+ , rule' = Just ρ+ }++ -- | Obtain all possibilities for matching one additional formula to an+ -- existing partial match.+ match :: Match ext -> F.Marked (F.Formula ext) -> [Match ext]+ match μ@(Match {matched, assignment, remainder}) scheme = do+ activeF <- maybe [] L.focus remainder+ let ν@(_ := formula) = L.current activeF+ σ <- Fσ.patternContinue assignment scheme formula+ return μ + { matched = ν : matched+ , remainder = L.delete activeF+ , assignment = σ+ }++++-- | Generate a match for every instance of the rule that was partially+-- matched.+instantiateMatch :: forall ext . (F.Extension ext)+ => TableauSettings ext+ -> Branch ext+ -> Match ext + -> [Match ext]+instantiateMatch κ π+ μ@(Match { assignment+ , rule'=Just (ρ@Rule { constraint+ , generator })+ }) = do+ σF <- L.focus generator+ σ <- Fσ.merge assignment (L.current σF)+ guard (respects (concretiser (dynamic κ π)) σ constraint)+ return μ + { assignment = σ+ , rule' = fmap (\g -> ρ { generator = g}) (L.delete σF)+ }++++-- | Greedily pick a consumer rule and consumptions to work with, but obtain+-- all possible instantiations of said rule. This way, nondeterminism is kept+-- at the level of generated instances.+--+-- Note that consumer rules are always picked in the order that they are+-- specified in the 'TableauSettings'.+matchFirst :: forall ext . (F.Extension ext)+ => TableauSettings ext + -> Branch ext + -> [Match ext]+matchFirst κ@(TableauSettings {rulesC}) π = join $ do + μs <- greedy+ . filter (not . null) + . map (instantiateMatch κ π)+ $ rulesC >>= matchRule π+ case compositor . rule . head $ μs of+ Greedy -> greedy <$> return μs+ Nondeterministic -> return μs++++-------------------------------------------------------------------------------+-- * Decision algorithm+++-- | Provide all possibilities for expanding a single branch once: greedily+-- selecting the rules and formulas to apply them to, but possibly keeping the+-- rule instance nondeterministic.+expand1 :: forall ext . (F.Extension ext)+ => TableauSettings ext+ -> Branch ext+ -> [(Match ext, [Branch ext])]+expand1 κ@(TableauSettings {rulesC, assumptions})+ π@(Branch {rulesA, inactives, counter}) =+ if null consumers+ then ascetics+ else consumers+ + where++ mapM2 :: Monad m => (a -> m b) -> [[a]] -> m [[b]]+ mapM2 = mapM . mapM++ -- | All instances of a greedily picked rule for expanding a branch using+ -- a consumer rule.+ consumers :: [(Match ext, [Branch ext])]+ consumers = do+ -- Greedily pick a rule and formulas on the branch, and, depending on+ -- the rule, nondeterministically pick an instance of that rule.+ μ@(Match {matched, remainder, assignment, rule}) <- matchFirst κ π+ -- Instantiate and unwrap the productions of the match we picked+ disjunction <- Fσ.substitute assignment `mapM2` productions rule+ -- Present the newly created branches+ return $ (,) μ+ [ π { actives = L.insertAll conjunction remainder+ , inactives = matched ++ inactives+ , new = conjunction+ , counter = counter + length conjunction+ }+ | conjunction <- zipWith (:=) [counter..] <$> disjunction + ]+ + -- | An ascetic rule must always be greedy.+ ascetics :: [(Match ext, [Branch ext])]+ ascetics = greedy $ do+ ρF <- maybe [] L.focus rulesA+ let ρ = L.current ρF+ μ@(Match {matched, remainder, assignment, rule, rule'}) <- + matchRule π ρ >>= instantiateMatch κ π+ disjunction <- Fσ.substitute assignment `mapM2` productions rule+ return $ (,) μ+ [ π { actives = L.insertAll conjunction remainder+ , inactives = matched ++ inactives+ , new = conjunction+ , counter = counter + length conjunction+ , rulesA = L.update ρF rule'+ }+ | conjunction <- zipWith (:=) [counter..] <$> disjunction+ ]++++-- | Recursively expand a branch and obtain the first closed tableau that+-- can be constructed in this way.+expand :: forall ext . (F.Extension ext) + => TableauSettings ext+ -> Branch ext + -> Maybe (Tableau ext)+expand κ = greedy . expand'++ where ++ -- | Nondeterministically and recursively expand the given branch into its + -- subtableaux.+ expand' :: Branch ext -> [Tableau ext]+ expand' π@(Branch {new}) = Node new <$> case closes π of+ Just xs -> return $ Closure xs+ Nothing -> do+ -- Pick a possible set of branch expansions+ (Match {matched, rule}, πs) <- expand1 κ π+ -- Determine which rule led to the expansions+ let n = name rule + let refs = map reference matched+ -- Recursively expand those branch expansions, too+ Application n refs <$> mapM expand' πs++++-- | Decide the validity of the target formula within the given logical system.+-- A branch closes when it internally contradicts. A branch that is neither +-- closed nor expandable corresponds to a satisfying assignment of the negation+-- of the target formula, and constitutes a counter-model. Otherwise, we have+-- successfully shown the formula's validity and can return a 'Tableau'.+decide :: forall ext . (F.Extension ext) + => TableauSystem ext+ -> F.Formula ext+ -> Result (F.Formula ext) (Tableau ext)+decide system goal =+ let postprocess = renumber 1 . rewrite goal . shorten+ result = uncurry expand (initial system goal)+ in maybe (Failure goal) (Success goal) $ postprocess <$> result ++++-------------------------------------------------------------------------------+-- * Post-processing+++-- | Eliminate rule applications that do not produce any formulas that are +-- involved in closing any branch. +--+-- Note that this will not eliminate all unnecessary applications (let alone+-- find the shortest proof) — it will only remove rules that are not involved+-- in any closure. For example, for justification logic, if @c:φ@ and @d:ψ@ +-- are in the CS but only @d:ψ@ has to be introduced via CSr, then this will+-- remove any redundant CSr application — but if a formula is introduced via+-- a restricted cut, it could do nothing because the cut-formula IS involved in+-- the closure of a branch, even though it was pointless to do the cut in the+-- first place. It would be nice to think of a stronger method.+shorten :: Tableau ext + -> Tableau ext+shorten = flip ST.evalState S.empty . shorten'++ where+ -- | The boolean keeps track of whether the application above produced+ -- anything helpful; the set keeps track of relevant formula references.+ -- It is a bit opaque and not as succinct as I think it could be --- a+ -- rewrite is welcome.+ shorten' :: Tableau ext -> ST.State (S.Set Int) (Tableau ext)+ shorten' tableau = case tableau of+ Closure refs -> do+ ST.modify $ \s -> foldr S.insert s refs+ return tableau+ Application name refs θs -> do+ (relevances, θs') <- fmap unzip . forM θs $ \(Node φs θ) -> do+ θ' <- shorten' θ+ relevantRefs <- ST.get + relevant <- forM φs $ \(i := _) -> do+ if S.member i relevantRefs+ then ST.modify (S.delete i) >> return True+ else return False+ return (or relevant, Node φs θ')+ if or relevances+ then do+ ST.modify (\s -> foldr S.insert s refs) + return $ Application name refs θs'+ else case θs' of+ (Node φs θ'' : _) -> return θ''+ _ -> error "This should not be possible."+ Node φs θ -> Node φs <$> shorten' θ++++-- | Make the reference numbers on the formulas heterogeneous, even if they +-- are on different branches. This is done in a single step at the end so that +-- we do not have the mental (and computational) burden of carrying a +-- 'ST.State' monad everywhere. +renumber :: Int + -> Tableau ext + -> Tableau ext+renumber start = flip ST.evalState (start, []) . renumber'++ where+ -- The renumbering is done by keeping track of the number of times we+ -- traversed up a branch. We also remember the translation table for the+ -- current branch. The latter could probably be done implicitly, but this+ -- is easier to grasp.+ renumber' :: Tableau ext -> ST.State (Int, [(Int,Int)]) (Tableau ext)+ renumber' tableau = do+ θ' <- case tableau of+ Closure refs -> do+ (_, assoc) <- ST.get+ refs' <- forM refs $ return . fromJust . flip lookup assoc+ return $ Closure refs'+ Node φs θ -> do+ φs' <- forM φs $ \(i := φ) -> do+ (j, assoc) <- ST.get+ ST.put (j+1, (i,j):assoc)+ return $ j := φ+ ν <- Node φs' <$> renumber' θ+ ST.modify (fmap . drop $ length φs')+ return ν+ Application name refs θs -> do+ (_, assoc) <- ST.get+ refs' <- forM refs $ return . fromJust . flip lookup assoc+ Application name refs' <$> mapM renumber' θs+ return θ'++++-- | If the root formula is not exactly equal to the input formula, there was +-- supposedly a rewriting step. Add this step to the tableau explicitly, to +-- show what happened.+rewrite :: F.Extension ext + => F.Formula ext + -> Tableau ext + -> Tableau ext+rewrite φ θ@(Node [i := F.Marked m ψ] _) = + if φ == ψ+ then θ+ else Node [subtract 1 i := F.Marked m φ] + $ Application "rewrite" [i-1] [θ]++++-------------------------------------------------------------------------------+-- * Term specifications++-- | Represent sets of primitive source formulas to be used in restrictive +-- constraints. +data PrimitiveDynamicTerms + = Static PrimitiveStaticTerms+ -- | Active terms, currently not processed on the branch. + | Processed+ -- | Inactive terms, currently processed on the branch.+ | Unprocessed+++-- | Represent sets of primitive source formulas to be used in generators+-- and restrictive constraints. +data PrimitiveStaticTerms + -- | Goal formula.+ = Root+ -- | Assumption formulas or constant specification.+ | Assumption+++-- | Represent complex sets of source terms, to be turned into concrete terms+-- at a point where it is known what they should refer to. Static terms are +-- known at the start of the tableau procedure, whereas dynamic terms should+-- be evaluated dynamically.+data Terms primitive ext+ = Primitive primitive+ -- | Keep terms that occur in at least one constituent.+ | Union [Terms primitive ext]+ -- | Keep only terms that occur in all constituents.+ | Intersection [Terms primitive ext]+ -- | Apply a transformation to terms.+ | Transform String ([F.Term ext] -> [F.Term ext]) (Terms primitive ext)+++-- | Shorthand for a specification of complex dynamic terms.+type DynamicTerms = Terms PrimitiveDynamicTerms+++-- | Shorthand for a specification of complex static terms.+type StaticTerms = Terms PrimitiveStaticTerms+++-- | Generic concretiser to convert a specification of terms into concrete+-- terms.+concretiser :: forall ext primitive . (Eq ext, Fσ.Substitutable ext ext)+ => (primitive -> [F.Term ext])+ -> Terms primitive ext+ -> [F.Term ext]+concretiser primitive τ = nub $ case τ of+ Primitive τ -> primitive τ+ Transform _ f τ -> f $ concretiser primitive τ+ Union τs -> concat $ map (concretiser primitive) τs+ Intersection τs -> intersection $ map (concretiser primitive) τs+++-- | Convert a primitive static term specification into concrete terms.+static :: TableauSettings ext+ -> PrimitiveStaticTerms+ -> [F.Term ext]+static κ@(TableauSettings {root, assumptions}) τ = case τ of+ Root -> F.asTerm root+ Assumption -> map F.Formula assumptions+++-- | Convert a primitive dynamic term specification into concrete terms.+dynamic :: TableauSettings ext+ -> Branch ext+ -> PrimitiveDynamicTerms+ -> [F.Term ext]+dynamic κ π τ = case τ of+ Static τ' -> static κ τ'+ Unprocessed -> map value (maybe [] L.asList $ actives π) + >>= F.asTerm+ Processed -> map value (inactives π) + >>= F.asTerm++++-------------------------------------------------------------------------------+-- * Auxiliaries++-- | Take the first option from a list of options.+greedy :: (Alternative f) => [a] -> f a+greedy [] = empty+greedy (x:_) = pure x+++-- | Take the intersection of all given lists.+intersection :: (Eq a) => [[a]] -> [a]+intersection [] = []+intersection xs = foldr1 intersect xs+++-- | A variation on permutations: given a list that describes the possible+-- elements at each position, give all possible element combinations. In a+-- sense, this is a @transpose@ operation.+--+-- Example: @[[1,2],[3,4]] -> [[1,3],[1,4],[2,3],[2,4]]@+combinations :: [[a]] -> [[a]]+combinations [] = []+combinations zs = foldr (\xs xss -> [ y:ys | y <- xs, ys <- xss ]) [[]] zs+
+ src/Logic/Judge/Prover/Tableau/Analytics.hs view
@@ -0,0 +1,52 @@+{-|+Module : Logic.Judge.Prover.Tableau.Analytics+Description : Analysis of the complexity of the system.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental++This module performs rudimentary analysis of the combinatorial complexity of +given tableau systems.+-}++{-# LANGUAGE PackageImports #-}+{-# LANGUAGE NamedFieldPuns #-}+module Logic.Judge.Prover.Tableau.Analytics + ( analysis + ) where++import Prelude hiding ((<$>))+import "ansi-wl-pprint" Text.PrettyPrint.ANSI.Leijen ((<>), (<+>), (</>), (<$>), (<$$>), (<//>))+import qualified "ansi-wl-pprint" Text.PrettyPrint.ANSI.Leijen as PP++import Logic.Judge.Prover.Tableau (Ref((:=)))+import qualified Logic.Judge.PointedList as L+import qualified Logic.Judge.Formula as F+import qualified Logic.Judge.Prover.Tableau as T++-- | Produce a 'PP.Doc' indicating the number of instances of each rule of a+-- tableau system. This function is a stub.+analysis :: F.Extension ext+ => T.TableauSystem ext + -> F.Formula ext + -> PP.Doc+analysis system goal = + PP.string "Number of consumer rule instantiations:" <$>+ PP.indent 4 (+ PP.vsep $ map instances rulesC+ ) <$>+ PP.string "Number of ascetic rule instantiations:" <$>+ PP.indent 4 (+ PP.vsep $ map instances (maybe [] L.toList rulesA)+ )++ where + + (T.TableauSettings {T.rulesC}, T.Branch {T.rulesA}) = T.initial system goal++ instances :: T.RuleInstantiated ext + -> PP.Doc+ instances (T.Rule {T.name, T.generator}) = + PP.string name <> PP.colon <+> PP.int (length generator)+
+ src/Logic/Judge/Prover/Yaml.hs view
@@ -0,0 +1,154 @@+{-|+Module : Logic.Judge.Tableau.Yaml+Description : YAML- and JSON-parsing.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental++This module provides instances for parsing tableau systems in YAML- and +JSON-representation, via 'Y.FromJSON'.+-}++{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PackageImports #-}+module Logic.Judge.Prover.Yaml + () where++import "base" Data.List (delete)+import "base" Data.Maybe (fromMaybe)+import "base" Control.Monad (foldM)+import "base" Control.Applicative ((<|>), liftA2)+import "text" Data.Text (Text, empty, pack, unpack)+import "yaml" Data.Yaml ((.:),(.:?),(.!=))+import qualified "yaml" Data.Yaml as Y+import qualified "aeson" Data.Aeson.Types as Y (typeMismatch, withText, withObject)++import Logic.Judge.Prover.Tableau (Ref((:=)))+import qualified Logic.Judge.Formula as F+import qualified Logic.Judge.Prover.Tableau as T+++instance (F.Extension ext) => Y.FromJSON (T.TableauSystem ext) where+ parseJSON = Y.withObject "tableau system" $ \o ->+ T.TableauSystem+ <$> o .:? "name" .!= "untitled"+ <*> o .: "rules"+ <*> o .:? "assumptions" .!= mempty++++instance {-# OVERLAPPABLE #-} (Monoid a, Y.FromJSON a, Y.FromJSON b) => Y.FromJSON (T.Ref a b) where+ parseJSON = Y.withObject "named object" $ \o -> + (:=) + <$> o .:? "id" .!= mempty+ <*> Y.parseJSON (Y.Object o)++++instance (F.Extension ext, Y.FromJSON primitive) => Y.FromJSON (T.Rule (T.Constraint primitive ext) ext) where+ parseJSON = Y.withObject "tableau rule" $ \o ->+ T.Rule+ <$> o .: "name"+ <*> o .: "consume"+ <*> o .: "produce"+ <*> o .:? "generate" .!= T.None+ <*> o .:? "restrict" .!= T.None+ <*> o .:? "compose" .!= T.Nondeterministic++++instance Y.FromJSON T.Compositor where+ parseJSON = Y.withText expected $ \s -> case s of+ "nondeterministic" -> return T.Nondeterministic+ "greedy" -> return T.Greedy+ invalid -> Y.typeMismatch expected (Y.String invalid)++ where expected = "compositor"++++instance Y.FromJSON T.PrimitiveStaticTerms where+ parseJSON = Y.withText expected $ \s -> case s of+ "root" -> return T.Root+ "assumptions" -> return T.Assumption+ invalid -> Y.typeMismatch expected (Y.String invalid)++ where expected = "term"+++instance Y.FromJSON T.PrimitiveDynamicTerms where+ parseJSON = Y.withText "term" $ \s -> case s of+ "processed" -> return T.Processed+ "unprocessed" -> return T.Unprocessed+ other -> T.Static <$> Y.parseJSON (Y.String s)++++instance (F.Extension ext, Y.FromJSON primitive) => Y.FromJSON (T.Terms primitive ext) where+ parseJSON (Y.Object o) + = T.Union <$> o .: "union" + <|> T.Intersection <$> o .: "intersection" + <|> T.Transform <$> (o .: "with" >>= stringify) <*> o .: "with" <*> o .: "in"+ <|> fail "expected term specification"++ where+ stringify :: Y.Value -> Y.Parser String+ stringify (Y.String string) = return (unpack string)+ stringify (Y.Array vector) = return "<combined>" -- TODO+ stringify _ = fail "could not stringify transformation function"++ parseJSON (Y.String s) = T.Primitive <$> Y.parseJSON (Y.String s)+ parseJSON other = Y.typeMismatch "term specification" other+ ++instance (F.Extension ext) => Y.FromJSON ([F.Term ext] -> [F.Term ext]) where+ parseJSON (Y.Array vector) = foldM fold id vector++ where + fold :: (F.Extension ext) + => ([F.Term ext] -> [F.Term ext]) + -> Y.Value + -> Y.Parser ([F.Term ext] -> [F.Term ext]) + fold fs f = (. fs) <$> Y.parseJSON f+ ++ parseJSON (Y.String s) = case s of+ "all" -> return id+ "subterms" -> return (>>= F.subterms)+ "formulas" -> return (filter F.isFormula)+ "marked" -> return (filter F.isMarkedFormula)+ "extensions" -> return (filter F.isExtension)+ "modalities" -> return (filter F.isExtension)+ "justifications" -> return (filter F.isExtension)+ "atomary" -> return (filter F.isAtomary)+ "complex" -> return (filter $ not . F.isAtomary)+ "constants" -> return (filter F.isConstant)+ "variables" -> return (filter F.isVariable)+ invalid -> fail ("unknown: " ++ unpack invalid)++ parseJSON invalid = Y.typeMismatch "transformation function" invalid+++instance (F.Extension ext, Y.FromJSON primitive) => Y.FromJSON (T.Constraint primitive ext) where+ parseJSON = Y.withObject "constraint or generator" $ \o ->+ T.Choose <$> o .: "or"+ <|> T.Merge <$> o .: "and"+ <|> T.Bind <$> o .: "match" <*> Y.parseJSON (Y.Object o)+ <|> fail "expected constraint or generator"+++instance F.Parseable ext => Y.FromJSON (F.Ambiguous (F.Term ext)) where+ parseJSON = Y.withText "term" F.parse+++instance F.Parseable ext => Y.FromJSON (F.Formula ext) where+ parseJSON = Y.withText "formula" F.parse+++instance F.Parseable term => Y.FromJSON (F.Marked term) where+ parseJSON = Y.withText "marked formula" F.parse++
+ src/Logic/Judge/Writer.hs view
@@ -0,0 +1,92 @@+{-|+Module : Logic.Judge.Writer+Description : Producing output.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental++This module contains operations and class instances for writing to files or +terminals.+-}++{-# LANGUAGE PackageImports #-}+module Logic.Judge.Writer + ( Format(LaTeX, Plain)+ , writeHeader+ , writeBody+ , writeFooter+ , write+ , plainprint+ , prettyprint+ ) where++import "base" GHC.IO.Handle (Handle, hIsTerminalDevice)+import "base" GHC.IO.Handle.FD (stdout, stderr)+import "bytestring" Data.ByteString (hPut)+import "terminal-size" System.Console.Terminal.Size (size, width)+import qualified "ansi-wl-pprint" Text.PrettyPrint.ANSI.Leijen as PP+import qualified "utf8-string" Data.ByteString.UTF8 as UTF8++import Logic.Judge.Writer.Plain (Printable, pretty)+import Logic.Judge.Writer.LaTeX (LaTeX, latexHeader, latexFooter, latex)++-- | A data type representing the supported file formats.+data Format + = LaTeX + | Plain + deriving (Show, Read)+++-- | Write the header associated with a file format to a file.+writeHeader :: Handle -> Format -> IO ()+writeHeader file format = case format of+ LaTeX -> write file latexHeader+ _ -> return ()+++-- | Write an object to a file in the given format.+writeBody :: (LaTeX a, Printable a) => Handle -> Format -> a -> IO ()+writeBody file format = write file . case format of+ LaTeX -> latex+ Plain -> pretty+++-- | Write the footer associated with a file format to a file.+writeFooter :: Handle -> Format -> IO ()+writeFooter file format = case format of+ LaTeX -> write file latexFooter+ _ -> return ()+++-- | Write a document to some file handle. Automatically chooses `prettyprint`+-- or `plainprint` based on whether we are writing to a terminal or not.+write :: Handle -> PP.Doc -> IO ()+write file doc = do+ terminal <- hIsTerminalDevice file+ if terminal+ then prettyprint file doc+ else plainprint file doc+++-- | Print ANSI-colorised document to file handle.+prettyprint :: Handle -> PP.Doc -> IO ()+prettyprint file doc = do+ columns <- maybe 79 width `fmap` size+ PP.displayIO file + . (PP.renderPretty 1.0 columns) + . (PP.<> PP.line)+ . PP.fill columns+ $ doc+++-- | Print UTF-8 encoded, plain document to file handle.+plainprint :: Handle -> PP.Doc -> IO ()+plainprint file doc = hPut file + . UTF8.fromString+ . flip PP.displayS "" + . (PP.renderPretty 1.0 255) + . PP.plain+ . (PP.<> PP.line)+ $ doc+
+ src/Logic/Judge/Writer/LaTeX.hs view
@@ -0,0 +1,158 @@+{-|+Module : Logic.Judge.Writer.LaTeX+Description : Instances for LaTeX output.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental++This module provides instances for LaTeX output in 'PP.Doc'-format.+-}++{-# LANGUAGE PackageImports #-}+{-# LANGUAGE FlexibleInstances #-}+module Logic.Judge.Writer.LaTeX + ( LaTeX+ , latex+ , latexHeader+ , latexFooter+ ) where++import Prelude hiding ((<$>))+import "texmath" Text.TeXMath.TeX (renderTeX)+import "texmath" Text.TeXMath.Unicode.ToTeX (getTeXMath)+import "ansi-wl-pprint" Text.PrettyPrint.ANSI.Leijen ((<>), (<+>), (</>), (<$>), (<$$>), (<//>))+import qualified "ansi-wl-pprint" Text.PrettyPrint.ANSI.Leijen as PP++import Logic.Judge.Writer.Plain (Printable, pretty)+import Logic.Judge.Prover.Tableau (Ref((:=)))+import qualified Logic.Judge.Formula as F+import qualified Logic.Judge.Prover.Tableau as T++++-- | Instances of this class can be represented as LaTeX code.+class LaTeX a where++ -- | Produce a 'PP.Doc' representing LaTeX code.+ latex :: a -> PP.Doc++++instance (LaTeX input, Printable ext) => LaTeX (T.Result input (T.Tableau ext)) where+ latex result = wrap $ case result of+ T.Failure input ->+ PP.string "Failed to satisfy goal: $" <+> latex input <> PP.char '$'+ T.Success input output ->+ latex output++ where+ wrap result = + PP.string "\\begin{result}" <$> + result <$> + PP.string "\\end{result}"+++instance LaTeX a => LaTeX (Ref Int a) where+ latex (i := φ) = + PP.char '$' <> + latex φ <> + PP.char '$' <+> + cmd "n" (PP.int i)+++instance LaTeX a => LaTeX (F.Marked a) where+ latex (F.Marked m φ) = + cmd "marked" (+ PP.encloseSep PP.lbrace PP.rbrace PP.comma $ map (PP.text . unicode2tex) m+ ) <+> latex φ++instance Printable ext => LaTeX (F.Formula ext) where+ latex = PP.string . unicode2tex . show . PP.plain . pretty+++instance (Printable ext) => LaTeX (T.Tableau ext) where+ latex θ = + PP.string "\\begin{forest}" <$> + PP.string "tableau" <$> + latex' θ <$> + PP.string "\\end{forest}"++ where+ latex' θ = case θ of+ T.Closure refs -> + PP.string ", closed={" <>+ cmd "n" (PP.tupled $ map PP.int refs) <>+ PP.string "}"+ T.Application name refs θs -> + PP.string ", apply=$\\sf " <> + PP.string (unicode2tex name) <+> + PP.string "$\\ " <> + cmd "n" (PP.tupled $ map PP.int refs) <$> + PP.indent 4 (PP.vsep $ map latex' θs)+ T.Node (φ:φs) θ -> + PP.lbracket <+> latex φ <> + foldr (\φ doc -> + PP.line <> PP.indent 4 (+ PP.lbracket <+> latex φ <> PP.string ", clamp" <> + doc <$> + PP.rbracket+ )+ ) (latex' θ) φs <$> + PP.rbracket+++-- | Convenience function for writing LaTeX commands.+cmd :: String -> PP.Doc -> PP.Doc+cmd s doc = PP.char '\\' <> PP.string s <> PP.lbrace <> doc <> PP.rbrace+++-- | Header for LaTeX output.+latexHeader :: PP.Doc+latexHeader = PP.vsep $ map PP.string + [ "\\documentclass[multi=result,margin=1cm]{standalone}"+ , "\\usepackage{forest,color}"+ , "\\forestset{"+ , "tableau/.style={"+ , " for tree={"+ , " parent anchor=south, child anchor=north,"+ , " s sep=0.1cm, l sep=0.8cm, inner sep=0.2cm"+ , " },"+ , "},"+ , "closed/.style={"+ , " fit=band, label=below:{$\\otimes$ #1},"+ , "},"+ , "clamp/.style={"+ , " no edge, before computing xy={l=\\baselineskip}"+ , "},"+ , "apply/.style={"+ , " for last={"+ , " edge label={"+ , " node[very near end, anchor=south west, xshift=0.1cm, font=\\small]{#1}"+ , " }"+ , " }"+ , "},"+ , "}"+ , "\\newcommand{\\marked}[1]{\\texttt{\\footnotesize[#1]\\ }}"+ , "\\newcommand{\\n}[1]{\\textcolor{gray}{{\\tiny{#1}}}}"+ , "\\begin{document}"+ ]+++-- | Footer for LaTeX output.+latexFooter :: PP.Doc+latexFooter = PP.text "\\end{document}"+++-- | Convert Unicode strings (@φ → ψ@) to LaTeX (@\psi \rightarrow \phi@).+unicode2tex :: String -> String+unicode2tex str = stripHardSpaces $ getTeXMath str [] >>= flip renderTeX ""++ where+ -- Some hacks to fix TeXMath's output+ stripHardSpaces :: String -> String+ stripHardSpaces string = case string of+ ('\\':'n':'e':'g':xs) -> "\\neg " ++ xs+ ('\\':' ':xs) -> ' ':stripHardSpaces xs+ (x:xs) -> x:stripHardSpaces xs+ [] -> []
+ src/Logic/Judge/Writer/Plain.hs view
@@ -0,0 +1,343 @@+{-|+Module : Logic.Judge.Writer.Plain+Description : Instances for prettyprinted output.+Copyright : (c) 2017, 2018 N Steenbergen+License : GPL-3+Maintainer : ns@slak.ws+Stability : experimental++This module provides instances for prettyprinted output in 'PP.Doc'-format.+-}++{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PackageImports #-}+module Logic.Judge.Writer.Plain + ( Printable+ , pretty+ , prettyEmbedded+ , prettyRecursive+ ) where++import Prelude hiding ((<$>))+import "base" Control.Monad (foldM)++import "text" Data.Text (Text, pack, unpack)+import "ansi-wl-pprint" Text.PrettyPrint.ANSI.Leijen ((<>), (<+>), (</>), (<$>), (<$$>), (<//>))+import qualified "ansi-wl-pprint" Text.PrettyPrint.ANSI.Leijen as PP+import qualified "containers" Data.Tree as R+import qualified "containers" Data.Map as M1+import qualified "unordered-containers" Data.HashMap.Strict as M2++import qualified Logic.Judge.Formula.Datastructure as F+import Logic.Judge.Prover.Tableau (Ref((:=)))+import qualified Logic.Judge.Formula as F+import qualified Logic.Judge.Prover.Tableau as T++styleForm = id+styleOp = PP.bold+styleVar = PP.green+styleConst = id+styleMark = PP.yellow+styleTitle = PP.bold +styleSubtitle = PP.underline+styleName = PP.red . PP.dquotes+styleComment = PP.cyan+styleAnnotation = PP.magenta+++-- | Produce a document representing a comma-seperated list.+list :: Printable a => [a] -> PP.Doc+list [] = PP.empty+list xs = (PP.empty <+>) . PP.fillSep . PP.punctuate (PP.char ',') . map pretty $ xs+++-- | Produce a document for each word.+phrase :: String -> PP.Doc+phrase = PP.fillSep . map PP.text . words+++-- | Produce a string-seperated list.+seperates :: String -> [PP.Doc] -> PP.Doc+seperates str = PP.fillSep . PP.punctuate (PP.text $ ' ':str)+++-- | Fold function for String maps+foldEntry :: Printable a => String -> a -> [PP.Doc] -> [PP.Doc]+foldEntry k v acc = (PP.text k <+> PP.align (pretty v)) : acc+++-- | Helper for prettyprinting unary operators.+unary :: Printable a => Char -> a -> PP.Doc+unary c p = (styleOp . PP.char) c <> prettyRecursive p+++-- | Helper for prettyprinting binary operators.+binary :: (Printable a, Printable b) => a -> Char -> b -> PP.Doc+binary p c q = + prettyRecursive p <+> + (styleOp $ PP.char c) <+> + prettyRecursive q+++-- | Instances of this class can be prettyprinted.+class Printable a where++ -- | Produce a 'PP.Doc' representing LaTeX code.+ pretty :: a -> PP.Doc+++ -- | In some cases, the representation for a type must be embellished with + -- some other symbols when it occurs as part of a representation of a+ -- different type, but not when it occurs on its own. This printer allows + -- us to specify this alternative.+ prettyEmbedded :: a -> PP.Doc+ prettyEmbedded = pretty+++ -- | Prettyprinting below the top level can optionally have a different+ -- procedure - for adding parentheses, for example.+ prettyRecursive :: a -> PP.Doc+ prettyRecursive = pretty+++instance {-# OVERLAPS #-} Printable String where+ pretty = phrase++instance Printable Bool where+ pretty True = PP.bold . PP.green . PP.char $ '✓'+ pretty False = PP.bold . PP.red . PP.char $ '×'+++instance Printable Text where+ pretty = phrase . unpack+++instance Printable Int where+ pretty = PP.int+++instance Printable a => Printable (Maybe a) where+ pretty = maybe PP.empty pretty++instance (Printable a, Printable b) => Printable (Either a b) where+ pretty = either (left . pretty) (right . pretty)+ + where+ left, right :: PP.Doc -> PP.Doc+ right = (<$$>) (PP.bold . PP.green . PP.text $ "Success:") . PP.indent 4+ left = (<$$>) (PP.bold . PP.red . PP.text $ "Failure:") . PP.indent 4+++instance (Printable a, Printable b) => Printable (a,b) where+ pretty (x, y) = + PP.parens $ pretty x <+> PP.comma <+> pretty y++instance Printable a => Printable [a] where+ pretty = PP.vcat . map ((PP.char '-' <+>) . prettyRecursive)++instance Printable a => Printable (M1.Map String a) where+ pretty m = PP.vcat (M1.foldrWithKey foldEntry [] m)++instance Printable a => Printable (M2.HashMap String a) where+ pretty m = PP.vcat (M2.foldrWithKey foldEntry [] m)+++instance Printable a => Printable (R.Tree a) where+ pretty (R.Node x []) = pretty x+ pretty (R.Node x xs) = pretty x <$> pretties xs++ where+ pretties trees' = case trees' of+ [] -> PP.empty+ [x] -> nest x+ (x:xs) -> nest x <$$> pretties xs++ nest x = PP.char '╷' <$$> PP.text "└── " <> PP.nest 4 (pretty x)+++instance Printable f => Printable (F.Marked f) where+ pretty (F.Marked [] formula) = pretty formula+ pretty (F.Marked marks formula) = prettify marks <+> pretty formula + where+ prettify = + styleMark . PP.brackets . PP.cat . + PP.punctuate (PP.comma <> PP.space) . + map PP.text+++instance Printable term => Printable (F.Ambiguous term) where+ pretty (F.Ambiguous (t:_)) = pretty t+ pretty (F.Ambiguous []) = error $+ "Ambiguous term has no readings. Please report this as a bug."+++instance Printable ext => Printable (F.Term ext) where+ pretty (F.Formula f) = pretty f+ pretty (F.Extension e) = pretty e+ pretty (F.MarkedFormula f) = pretty f+++instance (Printable ext) => Printable (F.Formula ext) where+ prettyRecursive el = styleForm $ case el of+ F.Constant _ -> pretty el+ F.Variable _ -> pretty el+ F.Negation _ -> pretty el+ _ -> PP.parens $ pretty el++ pretty el = styleForm $ case el of+ F.Constant True -> styleConst $ PP.char '⊤'+ F.Constant False -> styleConst $ PP.char '⊥'+ F.Variable s -> styleVar $ PP.text s+ F.Negation p -> unary '¬' p+ F.Disjunction p q -> binary p '∨' q+ F.Conjunction p q -> binary p '∧' q+ F.XDisjunction p q -> binary p '⊻' q+ F.Implication p q -> binary p '→' q+ F.BiImplication p q -> binary p '↔' q+ F.Extend j p -> prettyEmbedded j <> prettyRecursive p++++instance Printable F.Justification where++ prettyEmbedded x = pretty x <> (styleOp $ PP.text " : ")+ + pretty el = styleForm $ case el of+ F.ProofConstant s -> styleConst $ PP.text s+ F.ProofVariable s -> styleVar $ PP.text s+ F.ProofChecker j -> unary '!' j+ F.Application j k -> binary j '⋅' k+ F.Sum j k -> binary j '+' k++ + prettyRecursive el = case el of+ F.Application j k -> PP.parens $ pretty el+ F.Sum j k -> PP.parens $ pretty el+ _ -> pretty el+ +++instance Printable F.Modality where+ pretty el = PP.char $ case el of+ F.Necessary -> '□'+ F.Possible -> '◇'+++ +instance Printable F.Quantifier where+ pretty el = PP.text $ case el of+ F.Universal x -> "∀" ++ x ++ ". "+ F.Existential x -> "∃" ++ x ++ ". "++++instance Printable ext => Printable (T.Tableau ext) where+ pretty θ = case θ of+ T.Closure refs -> pretty False <+> styleAnnotation (list refs)+ T.Node φs subθ -> PP.vsep (map pretty φs) <$> pretty subθ+ T.Application name refs θs -> branch+ (styleAnnotation $ pretty name <> list refs)+ (map pretty θs)+ + where+ branch :: PP.Doc -> [PP.Doc] -> PP.Doc+ branch rule children = PP.vsep $ map (\child ->+ PP.char '╷' <+> rule <$> + PP.text "└── " <> PP.nest 4 child) children++++instance (Printable input, Printable ext) => Printable (T.Result input (T.Tableau ext)) where+ pretty result = case result of+ T.Failure input ->+ PP.red (PP.string "Failed to satisfy goal:") <+> pretty input+ T.Success input output ->+ PP.green (PP.string "Success:") <$>+ pretty output++++instance Printable b => Printable (Ref Int b) where+ pretty (i := v) = + pretty v <+> (styleAnnotation . PP.braces . pretty $ i)+++instance (Printable ext, Printable primitive) => Printable (T.Terms primitive ext) where+ pretty terms = case terms of+ T.Primitive s -> pretty s+ T.Union ts -> "or" `seperates` map prettyRecursive ts+ T.Intersection ts -> "and simultaneously" `seperates` map prettyRecursive ts+ T.Transform s _ t -> phrase "one of the" <+> phrase s <+> phrase "of" <+> pretty t+++instance Printable T.PrimitiveStaticTerms where+ pretty source = phrase $ case source of+ T.Root -> "a root node"+ T.Assumption -> "an assumption"+++instance Printable T.PrimitiveDynamicTerms where+ pretty source = case source of+ T.Unprocessed -> phrase "an unprocessed node on the branch"+ T.Processed -> phrase "a processed node on the branch"+ T.Static s -> pretty s+++instance (Printable ext, Printable primitive) => Printable (T.Constraint primitive ext) where++ pretty T.None = PP.empty+ pretty constraint = styleComment $ + PP.empty <$$> + phrase "where" <+> prettyRecursive constraint <$$> + PP.empty++ prettyRecursive constraint = case constraint of+ T.None -> PP.empty+ T.Bind pattern terms -> pretty pattern <+> phrase "matches" <+> prettyRecursive terms+ T.Choose cs -> "or alternatively" `seperates` map prettyRecursive cs+ T.Merge cs -> "while simultaneously" `seperates` map prettyRecursive cs+ + +instance (Printable ext) => Printable (T.RuleUninstantiated ext) where+ pretty T.Rule {T.name, T.productions, T.consumptions} =+ comment name <$$>+ comment "if the branch contains:" <$$>+ pretty consumptions <$$>+ PP.empty <$$>+ comment "then it may be extended with:" <$$>+ pretty (tree $ productions)+ + where+ comment :: String -> PP.Doc+ comment = styleComment . phrase++ -- | Represent a conjunction of disjunctions as a tree.+ tree :: [[a]] -> R.Tree (Maybe a)+ tree = R.Node Nothing . map conjunctiveTree+ + -- | Represent a conjunction as a tree.+ conjunctiveTree :: [a] -> R.Tree (Maybe a)+ conjunctiveTree [] = R.Node Nothing []+ conjunctiveTree [x] = R.Node (Just x) []+ conjunctiveTree (x:xs) = R.Node (Just x) [conjunctiveTree xs]+ ++instance (Printable ext) => Printable (T.TableauSystem ext) where+ pretty tableau = + (styleTitle . PP.text $ "Tableau for logic " ++ T.title tableau) <$$>+ PP.empty <$$>+ PP.indent 2 (+ subtitle "Assumptions" <$$> + PP.empty <$$>+ pretty (T.assumptions' tableau) <$$>+ PP.empty <$$>+ subtitle "Rules" <$$> + PP.empty <$$>+ pretty (T.rules tableau) <$$>+ PP.empty+ )++ where + subtitle = styleSubtitle . PP.text+ title = styleTitle . PP.text