diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -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.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,674 @@
+ GNU GENERAL PUBLIC LICENSE
+ Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc.
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+ Preamble
+
+ The GNU General Public License is a free, copyleft license for
+software and other kinds of works.
+
+ The licenses for most software and other practical works are designed
+to take away your freedom to share and change the works. By contrast,
+the GNU General Public License is intended to guarantee your freedom to
+share and change all versions of a program--to make sure it remains free
+software for all its users. We, the Free Software Foundation, use the
+GNU General Public License for most of our software; it applies also to
+any other work released this way by its authors. You can apply it to
+your programs, too.
+
+ When we speak of free software, we are referring to freedom, not
+price. Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+them if you wish), that you receive source code or can get it if you
+want it, that you can change the software or use pieces of it in new
+free programs, and that you know you can do these things.
+
+ To protect your rights, we need to prevent others from denying you
+these rights or asking you to surrender the rights. Therefore, you have
+certain responsibilities if you distribute copies of the software, or if
+you modify it: responsibilities to respect the freedom of others.
+
+ For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must pass on to the recipients the same
+freedoms that you received. You must make sure that they, too, receive
+or can get the source code. And you must show them these terms so they
+know their rights.
+
+ Developers that use the GNU GPL protect your rights with two steps:
+(1) assert copyright on the software, and (2) offer you this License
+giving you legal permission to copy, distribute and/or modify it.
+
+ For the developers' and authors' protection, the GPL clearly explains
+that there is no warranty for this free software. For both users' and
+authors' sake, the GPL requires that modified versions be marked as
+changed, so that their problems will not be attributed erroneously to
+authors of previous versions.
+
+ Some devices are designed to deny users access to install or run
+modified versions of the software inside them, although the manufacturer
+can do so. This is fundamentally incompatible with the aim of
+protecting users' freedom to change the software. The systematic
+pattern of such abuse occurs in the area of products for individuals to
+use, which is precisely where it is most unacceptable. Therefore, we
+have designed this version of the GPL to prohibit the practice for those
+products. If such problems arise substantially in other domains, we
+stand ready to extend this provision to those domains in future versions
+of the GPL, as needed to protect the freedom of users.
+
+ Finally, every program is threatened constantly by software patents.
+States should not allow patents to restrict development and use of
+software on general-purpose computers, but in those that do, we wish to
+avoid the special danger that patents applied to a free program could
+make it effectively proprietary. To prevent this, the GPL assures that
+patents cannot be used to render the program non-free.
+
+ The precise terms and conditions for copying, distribution and
+modification follow.
+
+ TERMS AND CONDITIONS
+
+ 0. Definitions.
+
+ "This License" refers to version 3 of the GNU General Public License.
+
+ "Copyright" also means copyright-like laws that apply to other kinds of
+works, such as semiconductor masks.
+
+ "The Program" refers to any copyrightable work licensed under this
+License. Each licensee is addressed as "you". "Licensees" and
+"recipients" may be individuals or organizations.
+
+ To "modify" a work means to copy from or adapt all or part of the work
+in a fashion requiring copyright permission, other than the making of an
+exact copy. The resulting work is called a "modified version" of the
+earlier work or a work "based on" the earlier work.
+
+ A "covered work" means either the unmodified Program or a work based
+on the Program.
+
+ To "propagate" a work means to do anything with it that, without
+permission, would make you directly or secondarily liable for
+infringement under applicable copyright law, except executing it on a
+computer or modifying a private copy. Propagation includes copying,
+distribution (with or without modification), making available to the
+public, and in some countries other activities as well.
+
+ To "convey" a work means any kind of propagation that enables other
+parties to make or receive copies. Mere interaction with a user through
+a computer network, with no transfer of a copy, is not conveying.
+
+ An interactive user interface displays "Appropriate Legal Notices"
+to the extent that it includes a convenient and prominently visible
+feature that (1) displays an appropriate copyright notice, and (2)
+tells the user that there is no warranty for the work (except to the
+extent that warranties are provided), that licensees may convey the
+work under this License, and how to view a copy of this License. If
+the interface presents a list of user commands or options, such as a
+menu, a prominent item in the list meets this criterion.
+
+ 1. Source Code.
+
+ The "source code" for a work means the preferred form of the work
+for making modifications to it. "Object code" means any non-source
+form of a work.
+
+ A "Standard Interface" means an interface that either is an official
+standard defined by a recognized standards body, or, in the case of
+interfaces specified for a particular programming language, one that
+is widely used among developers working in that language.
+
+ The "System Libraries" of an executable work include anything, other
+than the work as a whole, that (a) is included in the normal form of
+packaging a Major Component, but which is not part of that Major
+Component, and (b) serves only to enable use of the work with that
+Major Component, or to implement a Standard Interface for which an
+implementation is available to the public in source code form. A
+"Major Component", in this context, means a major essential component
+(kernel, window system, and so on) of the specific operating system
+(if any) on which the executable work runs, or a compiler used to
+produce the work, or an object code interpreter used to run it.
+
+ The "Corresponding Source" for a work in object code form means all
+the source code needed to generate, install, and (for an executable
+work) run the object code and to modify the work, including scripts to
+control those activities. However, it does not include the work's
+System Libraries, or general-purpose tools or generally available free
+programs which are used unmodified in performing those activities but
+which are not part of the work. For example, Corresponding Source
+includes interface definition files associated with source files for
+the work, and the source code for shared libraries and dynamically
+linked subprograms that the work is specifically designed to require,
+such as by intimate data communication or control flow between those
+subprograms and other parts of the work.
+
+ The Corresponding Source need not include anything that users
+can regenerate automatically from other parts of the Corresponding
+Source.
+
+ The Corresponding Source for a work in source code form is that
+same work.
+
+ 2. Basic Permissions.
+
+ All rights granted under this License are granted for the term of
+copyright on the Program, and are irrevocable provided the stated
+conditions are met. This License explicitly affirms your unlimited
+permission to run the unmodified Program. The output from running a
+covered work is covered by this License only if the output, given its
+content, constitutes a covered work. This License acknowledges your
+rights of fair use or other equivalent, as provided by copyright law.
+
+ You may make, run and propagate covered works that you do not
+convey, without conditions so long as your license otherwise remains
+in force. You may convey covered works to others for the sole purpose
+of having them make modifications exclusively for you, or provide you
+with facilities for running those works, provided that you comply with
+the terms of this License in conveying all material for which you do
+not control copyright. Those thus making or running the covered works
+for you must do so exclusively on your behalf, under your direction
+and control, on terms that prohibit them from making any copies of
+your copyrighted material outside their relationship with you.
+
+ Conveying under any other circumstances is permitted solely under
+the conditions stated below. Sublicensing is not allowed; section 10
+makes it unnecessary.
+
+ 3. Protecting Users' Legal Rights From Anti-Circumvention Law.
+
+ No covered work shall be deemed part of an effective technological
+measure under any applicable law fulfilling obligations under article
+11 of the WIPO copyright treaty adopted on 20 December 1996, or
+similar laws prohibiting or restricting circumvention of such
+measures.
+
+ When you convey a covered work, you waive any legal power to forbid
+circumvention of technological measures to the extent such circumvention
+is effected by exercising rights under this License with respect to
+the covered work, and you disclaim any intention to limit operation or
+modification of the work as a means of enforcing, against the work's
+users, your or third parties' legal rights to forbid circumvention of
+technological measures.
+
+ 4. Conveying Verbatim Copies.
+
+ You may convey verbatim copies of the Program's source code as you
+receive it, in any medium, provided that you conspicuously and
+appropriately publish on each copy an appropriate copyright notice;
+keep intact all notices stating that this License and any
+non-permissive terms added in accord with section 7 apply to the code;
+keep intact all notices of the absence of any warranty; and give all
+recipients a copy of this License along with the Program.
+
+ You may charge any price or no price for each copy that you convey,
+and you may offer support or warranty protection for a fee.
+
+ 5. Conveying Modified Source Versions.
+
+ You may convey a work based on the Program, or the modifications to
+produce it from the Program, in the form of source code under the
+terms of section 4, provided that you also meet all of these conditions:
+
+ a) The work must carry prominent notices stating that you modified
+ it, and giving a relevant date.
+
+ b) The work must carry prominent notices stating that it is
+ released under this License and any conditions added under section
+ 7. This requirement modifies the requirement in section 4 to
+ "keep intact all notices".
+
+ c) You must license the entire work, as a whole, under this
+ License to anyone who comes into possession of a copy. This
+ License will therefore apply, along with any applicable section 7
+ additional terms, to the whole of the work, and all its parts,
+ regardless of how they are packaged. This License gives no
+ permission to license the work in any other way, but it does not
+ invalidate such permission if you have separately received it.
+
+ d) If the work has interactive user interfaces, each must display
+ Appropriate Legal Notices; however, if the Program has interactive
+ interfaces that do not display Appropriate Legal Notices, your
+ work need not make them do so.
+
+ A compilation of a covered work with other separate and independent
+works, which are not by their nature extensions of the covered work,
+and which are not combined with it such as to form a larger program,
+in or on a volume of a storage or distribution medium, is called an
+"aggregate" if the compilation and its resulting copyright are not
+used to limit the access or legal rights of the compilation's users
+beyond what the individual works permit. Inclusion of a covered work
+in an aggregate does not cause this License to apply to the other
+parts of the aggregate.
+
+ 6. Conveying Non-Source Forms.
+
+ You may convey a covered work in object code form under the terms
+of sections 4 and 5, provided that you also convey the
+machine-readable Corresponding Source under the terms of this License,
+in one of these ways:
+
+ a) Convey the object code in, or embodied in, a physical product
+ (including a physical distribution medium), accompanied by the
+ Corresponding Source fixed on a durable physical medium
+ customarily used for software interchange.
+
+ b) Convey the object code in, or embodied in, a physical product
+ (including a physical distribution medium), accompanied by a
+ written offer, valid for at least three years and valid for as
+ long as you offer spare parts or customer support for that product
+ model, to give anyone who possesses the object code either (1) a
+ copy of the Corresponding Source for all the software in the
+ product that is covered by this License, on a durable physical
+ medium customarily used for software interchange, for a price no
+ more than your reasonable cost of physically performing this
+ conveying of source, or (2) access to copy the
+ Corresponding Source from a network server at no charge.
+
+ c) Convey individual copies of the object code with a copy of the
+ written offer to provide the Corresponding Source. This
+ alternative is allowed only occasionally and noncommercially, and
+ only if you received the object code with such an offer, in accord
+ with subsection 6b.
+
+ d) Convey the object code by offering access from a designated
+ place (gratis or for a charge), and offer equivalent access to the
+ Corresponding Source in the same way through the same place at no
+ further charge. You need not require recipients to copy the
+ Corresponding Source along with the object code. If the place to
+ copy the object code is a network server, the Corresponding Source
+ may be on a different server (operated by you or a third party)
+ that supports equivalent copying facilities, provided you maintain
+ clear directions next to the object code saying where to find the
+ Corresponding Source. Regardless of what server hosts the
+ Corresponding Source, you remain obligated to ensure that it is
+ available for as long as needed to satisfy these requirements.
+
+ e) Convey the object code using peer-to-peer transmission, provided
+ you inform other peers where the object code and Corresponding
+ Source of the work are being offered to the general public at no
+ charge under subsection 6d.
+
+ A separable portion of the object code, whose source code is excluded
+from the Corresponding Source as a System Library, need not be
+included in conveying the object code work.
+
+ A "User Product" is either (1) a "consumer product", which means any
+tangible personal property which is normally used for personal, family,
+or household purposes, or (2) anything designed or sold for incorporation
+into a dwelling. In determining whether a product is a consumer product,
+doubtful cases shall be resolved in favor of coverage. For a particular
+product received by a particular user, "normally used" refers to a
+typical or common use of that class of product, regardless of the status
+of the particular user or of the way in which the particular user
+actually uses, or expects or is expected to use, the product. A product
+is a consumer product regardless of whether the product has substantial
+commercial, industrial or non-consumer uses, unless such uses represent
+the only significant mode of use of the product.
+
+ "Installation Information" for a User Product means any methods,
+procedures, authorization keys, or other information required to install
+and execute modified versions of a covered work in that User Product from
+a modified version of its Corresponding Source. The information must
+suffice to ensure that the continued functioning of the modified object
+code is in no case prevented or interfered with solely because
+modification has been made.
+
+ If you convey an object code work under this section in, or with, or
+specifically for use in, a User Product, and the conveying occurs as
+part of a transaction in which the right of possession and use of the
+User Product is transferred to the recipient in perpetuity or for a
+fixed term (regardless of how the transaction is characterized), the
+Corresponding Source conveyed under this section must be accompanied
+by the Installation Information. But this requirement does not apply
+if neither you nor any third party retains the ability to install
+modified object code on the User Product (for example, the work has
+been installed in ROM).
+
+ The requirement to provide Installation Information does not include a
+requirement to continue to provide support service, warranty, or updates
+for a work that has been modified or installed by the recipient, or for
+the User Product in which it has been modified or installed. Access to a
+network may be denied when the modification itself materially and
+adversely affects the operation of the network or violates the rules and
+protocols for communication across the network.
+
+ Corresponding Source conveyed, and Installation Information provided,
+in accord with this section must be in a format that is publicly
+documented (and with an implementation available to the public in
+source code form), and must require no special password or key for
+unpacking, reading or copying.
+
+ 7. Additional Terms.
+
+ "Additional permissions" are terms that supplement the terms of this
+License by making exceptions from one or more of its conditions.
+Additional permissions that are applicable to the entire Program shall
+be treated as though they were included in this License, to the extent
+that they are valid under applicable law. If additional permissions
+apply only to part of the Program, that part may be used separately
+under those permissions, but the entire Program remains governed by
+this License without regard to the additional permissions.
+
+ When you convey a copy of a covered work, you may at your option
+remove any additional permissions from that copy, or from any part of
+it. (Additional permissions may be written to require their own
+removal in certain cases when you modify the work.) You may place
+additional permissions on material, added by you to a covered work,
+for which you have or can give appropriate copyright permission.
+
+ Notwithstanding any other provision of this License, for material you
+add to a covered work, you may (if authorized by the copyright holders of
+that material) supplement the terms of this License with terms:
+
+ a) Disclaiming warranty or limiting liability differently from the
+ terms of sections 15 and 16 of this License; or
+
+ b) Requiring preservation of specified reasonable legal notices or
+ author attributions in that material or in the Appropriate Legal
+ Notices displayed by works containing it; or
+
+ c) Prohibiting misrepresentation of the origin of that material, or
+ requiring that modified versions of such material be marked in
+ reasonable ways as different from the original version; or
+
+ d) Limiting the use for publicity purposes of names of licensors or
+ authors of the material; or
+
+ e) Declining to grant rights under trademark law for use of some
+ trade names, trademarks, or service marks; or
+
+ f) Requiring indemnification of licensors and authors of that
+ material by anyone who conveys the material (or modified versions of
+ it) with contractual assumptions of liability to the recipient, for
+ any liability that these contractual assumptions directly impose on
+ those licensors and authors.
+
+ All other non-permissive additional terms are considered "further
+restrictions" within the meaning of section 10. If the Program as you
+received it, or any part of it, contains a notice stating that it is
+governed by this License along with a term that is a further
+restriction, you may remove that term. If a license document contains
+a further restriction but permits relicensing or conveying under this
+License, you may add to a covered work material governed by the terms
+of that license document, provided that the further restriction does
+not survive such relicensing or conveying.
+
+ If you add terms to a covered work in accord with this section, you
+must place, in the relevant source files, a statement of the
+additional terms that apply to those files, or a notice indicating
+where to find the applicable terms.
+
+ Additional terms, permissive or non-permissive, may be stated in the
+form of a separately written license, or stated as exceptions;
+the above requirements apply either way.
+
+ 8. Termination.
+
+ You may not propagate or modify a covered work except as expressly
+provided under this License. Any attempt otherwise to propagate or
+modify it is void, and will automatically terminate your rights under
+this License (including any patent licenses granted under the third
+paragraph of section 11).
+
+ However, if you cease all violation of this License, then your
+license from a particular copyright holder is reinstated (a)
+provisionally, unless and until the copyright holder explicitly and
+finally terminates your license, and (b) permanently, if the copyright
+holder fails to notify you of the violation by some reasonable means
+prior to 60 days after the cessation.
+
+ Moreover, your license from a particular copyright holder is
+reinstated permanently if the copyright holder notifies you of the
+violation by some reasonable means, this is the first time you have
+received notice of violation of this License (for any work) from that
+copyright holder, and you cure the violation prior to 30 days after
+your receipt of the notice.
+
+ Termination of your rights under this section does not terminate the
+licenses of parties who have received copies or rights from you under
+this License. If your rights have been terminated and not permanently
+reinstated, you do not qualify to receive new licenses for the same
+material under section 10.
+
+ 9. Acceptance Not Required for Having Copies.
+
+ You are not required to accept this License in order to receive or
+run a copy of the Program. Ancillary propagation of a covered work
+occurring solely as a consequence of using peer-to-peer transmission
+to receive a copy likewise does not require acceptance. However,
+nothing other than this License grants you permission to propagate or
+modify any covered work. These actions infringe copyright if you do
+not accept this License. Therefore, by modifying or propagating a
+covered work, you indicate your acceptance of this License to do so.
+
+ 10. Automatic Licensing of Downstream Recipients.
+
+ Each time you convey a covered work, the recipient automatically
+receives a license from the original licensors, to run, modify and
+propagate that work, subject to this License. You are not responsible
+for enforcing compliance by third parties with this License.
+
+ An "entity transaction" is a transaction transferring control of an
+organization, or substantially all assets of one, or subdividing an
+organization, or merging organizations. If propagation of a covered
+work results from an entity transaction, each party to that
+transaction who receives a copy of the work also receives whatever
+licenses to the work the party's predecessor in interest had or could
+give under the previous paragraph, plus a right to possession of the
+Corresponding Source of the work from the predecessor in interest, if
+the predecessor has it or can get it with reasonable efforts.
+
+ You may not impose any further restrictions on the exercise of the
+rights granted or affirmed under this License. For example, you may
+not impose a license fee, royalty, or other charge for exercise of
+rights granted under this License, and you may not initiate litigation
+(including a cross-claim or counterclaim in a lawsuit) alleging that
+any patent claim is infringed by making, using, selling, offering for
+sale, or importing the Program or any portion of it.
+
+ 11. Patents.
+
+ A "contributor" is a copyright holder who authorizes use under this
+License of the Program or a work on which the Program is based. The
+work thus licensed is called the contributor's "contributor version".
+
+ A contributor's "essential patent claims" are all patent claims
+owned or controlled by the contributor, whether already acquired or
+hereafter acquired, that would be infringed by some manner, permitted
+by this License, of making, using, or selling its contributor version,
+but do not include claims that would be infringed only as a
+consequence of further modification of the contributor version. For
+purposes of this definition, "control" includes the right to grant
+patent sublicenses in a manner consistent with the requirements of
+this License.
+
+ Each contributor grants you a non-exclusive, worldwide, royalty-free
+patent license under the contributor's essential patent claims, to
+make, use, sell, offer for sale, import and otherwise run, modify and
+propagate the contents of its contributor version.
+
+ In the following three paragraphs, a "patent license" is any express
+agreement or commitment, however denominated, not to enforce a patent
+(such as an express permission to practice a patent or covenant not to
+sue for patent infringement). To "grant" such a patent license to a
+party means to make such an agreement or commitment not to enforce a
+patent against the party.
+
+ If you convey a covered work, knowingly relying on a patent license,
+and the Corresponding Source of the work is not available for anyone
+to copy, free of charge and under the terms of this License, through a
+publicly available network server or other readily accessible means,
+then you must either (1) cause the Corresponding Source to be so
+available, or (2) arrange to deprive yourself of the benefit of the
+patent license for this particular work, or (3) arrange, in a manner
+consistent with the requirements of this License, to extend the patent
+license to downstream recipients. "Knowingly relying" means you have
+actual knowledge that, but for the patent license, your conveying the
+covered work in a country, or your recipient's use of the covered work
+in a country, would infringe one or more identifiable patents in that
+country that you have reason to believe are valid.
+
+ If, pursuant to or in connection with a single transaction or
+arrangement, you convey, or propagate by procuring conveyance of, a
+covered work, and grant a patent license to some of the parties
+receiving the covered work authorizing them to use, propagate, modify
+or convey a specific copy of the covered work, then the patent license
+you grant is automatically extended to all recipients of the covered
+work and works based on it.
+
+ A patent license is "discriminatory" if it does not include within
+the scope of its coverage, prohibits the exercise of, or is
+conditioned on the non-exercise of one or more of the rights that are
+specifically granted under this License. You may not convey a covered
+work if you are a party to an arrangement with a third party that is
+in the business of distributing software, under which you make payment
+to the third party based on the extent of your activity of conveying
+the work, and under which the third party grants, to any of the
+parties who would receive the covered work from you, a discriminatory
+patent license (a) in connection with copies of the covered work
+conveyed by you (or copies made from those copies), or (b) primarily
+for and in connection with specific products or compilations that
+contain the covered work, unless you entered into that arrangement,
+or that patent license was granted, prior to 28 March 2007.
+
+ Nothing in this License shall be construed as excluding or limiting
+any implied license or other defenses to infringement that may
+otherwise be available to you under applicable patent law.
+
+ 12. No Surrender of Others' Freedom.
+
+ If conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License. If you cannot convey a
+covered work so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you may
+not convey it at all. For example, if you agree to terms that obligate you
+to collect a royalty for further conveying from those to whom you convey
+the Program, the only way you could satisfy both those terms and this
+License would be to refrain entirely from conveying the Program.
+
+ 13. Use with the GNU Affero General Public License.
+
+ Notwithstanding any other provision of this License, you have
+permission to link or combine any covered work with a work licensed
+under version 3 of the GNU Affero General Public License into a single
+combined work, and to convey the resulting work. The terms of this
+License will continue to apply to the part which is the covered work,
+but the special requirements of the GNU Affero General Public License,
+section 13, concerning interaction through a network will apply to the
+combination as such.
+
+ 14. Revised Versions of this License.
+
+ The Free Software Foundation may publish revised and/or new versions of
+the GNU General Public License from time to time. Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+ Each version is given a distinguishing version number. If the
+Program specifies that a certain numbered version of the GNU General
+Public License "or any later version" applies to it, you have the
+option of following the terms and conditions either of that numbered
+version or of any later version published by the Free Software
+Foundation. If the Program does not specify a version number of the
+GNU General Public License, you may choose any version ever published
+by the Free Software Foundation.
+
+ If the Program specifies that a proxy can decide which future
+versions of the GNU General Public License can be used, that proxy's
+public statement of acceptance of a version permanently authorizes you
+to choose that version for the Program.
+
+ Later license versions may give you additional or different
+permissions. However, no additional obligations are imposed on any
+author or copyright holder as a result of your choosing to follow a
+later version.
+
+ 15. Disclaimer of Warranty.
+
+ THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY
+APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT
+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY
+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,
+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM
+IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF
+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+ 16. Limitation of Liability.
+
+ IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS
+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY
+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE
+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF
+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD
+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),
+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGES.
+
+ 17. Interpretation of Sections 15 and 16.
+
+ If the disclaimer of warranty and limitation of liability provided
+above cannot be given local legal effect according to their terms,
+reviewing courts shall apply local law that most closely approximates
+an absolute waiver of all civil liability in connection with the
+Program, unless a warranty or assumption of liability accompanies a
+copy of the Program in return for a fee.
+
+ END OF TERMS AND CONDITIONS
+
+ How to Apply These Terms to Your New Programs
+
+ If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+ To do so, attach the following notices to the program. It is safest
+to attach them to the start of each source file to most effectively
+state the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+ {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 .
+
+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
+.
+
+ The GNU General Public License does not permit incorporating your program
+into proprietary programs. If your program is a subroutine library, you
+may consider it more useful to permit linking proprietary applications with
+the library. If this is what you want to do, use the GNU Lesser General
+Public License instead of this License. But first, please read
+.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -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.
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/app/CLI.hs b/app/CLI.hs
new file mode 100644
--- /dev/null
+++ b/app/CLI.hs
@@ -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"
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -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
+
+
diff --git a/formulas.txt b/formulas.txt
new file mode 100644
--- /dev/null
+++ b/formulas.txt
@@ -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
diff --git a/judge.cabal b/judge.cabal
new file mode 100644
--- /dev/null
+++ b/judge.cabal
@@ -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
diff --git a/logic/J-ghari.yml b/logic/J-ghari.yml
new file mode 100644
--- /dev/null
+++ b/logic/J-ghari.yml
@@ -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]
+
diff --git a/logic/J.yml b/logic/J.yml
new file mode 100644
--- /dev/null
+++ b/logic/J.yml
@@ -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: []
diff --git a/logic/LP.yml b/logic/LP.yml
new file mode 100644
--- /dev/null
+++ b/logic/LP.yml
@@ -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: []
diff --git a/src/Logic/Judge/Formula.hs b/src/Logic/Judge/Formula.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Judge/Formula.hs
@@ -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
diff --git a/src/Logic/Judge/Formula/Datastructure.hs b/src/Logic/Judge/Formula/Datastructure.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Judge/Formula/Datastructure.hs
@@ -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
diff --git a/src/Logic/Judge/Formula/Parser.hs b/src/Logic/Judge/Formula/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Judge/Formula/Parser.hs
@@ -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
+ )
diff --git a/src/Logic/Judge/Formula/Substitution.hs b/src/Logic/Judge/Formula/Substitution.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Judge/Formula/Substitution.hs
@@ -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)
diff --git a/src/Logic/Judge/PointedList.hs b/src/Logic/Judge/PointedList.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Judge/PointedList.hs
@@ -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
diff --git a/src/Logic/Judge/Prover/Tableau.hs b/src/Logic/Judge/Prover/Tableau.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Judge/Prover/Tableau.hs
@@ -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
+
diff --git a/src/Logic/Judge/Prover/Tableau/Analytics.hs b/src/Logic/Judge/Prover/Tableau/Analytics.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Judge/Prover/Tableau/Analytics.hs
@@ -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)
+
diff --git a/src/Logic/Judge/Prover/Yaml.hs b/src/Logic/Judge/Prover/Yaml.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Judge/Prover/Yaml.hs
@@ -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 "" -- 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
+
+
diff --git a/src/Logic/Judge/Writer.hs b/src/Logic/Judge/Writer.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Judge/Writer.hs
@@ -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
+
diff --git a/src/Logic/Judge/Writer/LaTeX.hs b/src/Logic/Judge/Writer/LaTeX.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Judge/Writer/LaTeX.hs
@@ -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
+ [] -> []
diff --git a/src/Logic/Judge/Writer/Plain.hs b/src/Logic/Judge/Writer/Plain.hs
new file mode 100644
--- /dev/null
+++ b/src/Logic/Judge/Writer/Plain.hs
@@ -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