diff --git a/ChangeLog b/ChangeLog
new file mode 100644
--- /dev/null
+++ b/ChangeLog
@@ -0,0 +1,3 @@
+2017-09-29 Ferdinand van Walree 0.1.0
+
+* Initial release.
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/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/sessiontypes.cabal b/sessiontypes.cabal
new file mode 100644
--- /dev/null
+++ b/sessiontypes.cabal
@@ -0,0 +1,90 @@
+name: sessiontypes
+version: 0.1.0
+synopsis: Session types library
+description: This packages provides a deep embedded domain-specific language for writing session typed program.
+ A session typed program is a program annotated with session types. A session type describes a communication protocol at the type-level.
+ The motivation for doing so is that it gives you a static guarantee that a program correctly implements a protocol.
+ It may even guarantee that no deadlocking can occur.
+homepage: https://github.com/Ferdinand-vW/sessiontypes#readme
+license: GPL-3
+license-file: LICENSE
+author: Ferdinand van Walree
+maintainer: Ferdinand van Walree
+copyright: 2017 Ferdinand van Walree
+category: Control
+build-type: Simple
+extra-source-files: ChangeLog
+cabal-version: >=1.10
+
+library
+ hs-source-dirs: src
+ exposed-modules: Control.SessionTypes
+ , Control.SessionTypes.Codensity
+ , Control.SessionTypes.Visualize
+ , Control.SessionTypes.Debug
+ , Control.SessionTypes.MonadSession
+ , Control.SessionTypes.Normalize
+ , Control.SessionTypes.Indexed
+ , Control.SessionTypes.Interactive
+ , Control.SessionTypes.STTerm
+ , Control.SessionTypes.Types
+ ghc-options: -fno-warn-partial-type-signatures
+ build-depends: base >= 4.7 && < 5
+ , deepseq >= 1.4 && < 1.5
+ , diagrams-lib >= 1.4 && < 1.5
+ , diagrams-svg >= 1.4 && < 1.5
+ , mtl >= 2.2 && < 2.3
+ , transformers >= 0.5 && < 0.6
+ , vector >= 0.12 && < 0.13
+ default-language: Haskell2010
+
+
+test-suite sessiontypes-debug
+ type: exitcode-stdio-1.0
+ main-is: Test/Debug/Main.hs
+ hs-source-dirs: test
+ other-modules: Test.Program.Simple
+ , Test.Program.FileServer
+ build-depends: base >= 4.7 && < 5
+ , sessiontypes
+ , hspec >= 2.4.4 && < 2.5
+ , directory >= 1.3 && < 1.4
+ ghc-options: -threaded -rtsopts -with-rtsopts=-N
+ default-language: Haskell2010
+
+test-suite sessiontypes-normalize
+ type: exitcode-stdio-1.0
+ main-is: Test/Normalize/Main.hs
+ hs-source-dirs: test
+ other-modules: Test.Program.Normalizable
+ build-depends: base >= 4.7 && < 5
+ , sessiontypes
+ , hspec >= 2.4.4 && < 2.5
+ , directory >= 1.3 && < 1.4
+ ghc-options: -threaded -rtsopts -with-rtsopts=-N
+ default-language: Haskell2010
+
+
+test-suite sessiontypes-interactive
+ type: exitcode-stdio-1.0
+ main-is: Test/Interactive/Main.hs
+ hs-source-dirs: test
+ other-modules: Test.Program.FileServer
+ build-depends: base >= 4.7 && < 5
+ , sessiontypes
+ , hspec >= 2.4.4 && < 2.5
+ , directory >= 1.3 && < 1.4
+ , exceptions >= 0.8.3 && < 0.9.0
+ ghc-options: -threaded -rtsopts -with-rtsopts=-N
+ default-language: Haskell2010
+
+Executable test-visualizer
+ main-is: Test/Visualize/Main.hs
+ hs-source-dirs: test
+ build-depends: base
+ , sessiontypes
+ default-language: Haskell2010
+
+source-repository head
+ type: git
+ location: https://github.com/Ferdinand-vW/sessiontypes
diff --git a/src/Control/SessionTypes.hs b/src/Control/SessionTypes.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/SessionTypes.hs
@@ -0,0 +1,132 @@
+-- | This packages provides a deep embedded domain-specific language for writing session typed program.
+--
+-- A session typed program is a program annotated with session types. A session type describes a communication protocol at the type-level.
+--
+-- The motivation for doing so is that it gives you a static guarantee that a program correctly implements a protocol. It may even guarantee that no deadlocking can occur.
+--
+-- The following constitutes the most important parts of this library for writing session typed programs.
+--
+-- * `STTerm`: A GADT representing the terms of the DSL. The constructors represent the different session types and are annotated with session types.
+-- * `ST`: A protomoted data type describing the different session types.
+-- * `MonadSession`: A type class exposing the interface of the DSL.
+-- * "Control.SessionTypes.Indexed": A custom prelude module replacing common type classes with indexed type classes
+--
+-- This package also implements a couple interpreters that evaluate an abstract-syntax tree consisting of `STTerm` constructors:
+--
+-- * "Control.SessionTypes.Debug": Purely evaluation
+-- * "Control.SessionTypes.Interactive": Interactive evaluation
+-- * "Control.SessionTypes.Normalize": Rewrites `STTerm` programs to a normal form
+-- * "Control.SessionTypes.Visualize": Visualizes a session type
+module Control.SessionTypes (
+ -- * STTerm
+ STTerm (..),
+ inferIdentity,
+ -- * MonadSession
+ -- ** Primitives
+ MonadSession (..),
+ -- ** Combinators
+ empty,
+ empty0,
+ selN,
+ selN1,
+ selN2,
+ selN3,
+ selN4,
+ Select(sel),
+ (<&),
+ (<&>),
+ offer,
+ recurseFix,
+ recurse0,
+ weaken0,
+ var0,
+ eps0,
+ -- * Types
+ -- ** Session Types
+ ST(..),
+ Cap(..),
+ GetST,
+ GetCtx,
+ -- ** Duality
+ Dual,
+ DualST,
+ MapDual,
+ -- ** Removing
+ RemoveSend,
+ RemoveSendST,
+ MapRemoveSend,
+ RemoveRecv,
+ RemoveRecvST,
+ MapRemoveRecv,
+ -- ** Applying Constraints
+ HasConstraint,
+ HasConstraintST,
+ MapHasConstraint,
+ HasConstraints,
+ -- ** Boolean functions
+ IfThenElse,
+ Not,
+ Or,
+ -- ** Product type
+ Prod (..),
+ Left,
+ Right,
+ -- ** Other
+ Nat(..),
+ Ref(..),
+ TypeEqList,
+ Append
+) where
+
+import Control.SessionTypes.STTerm (
+ STTerm (..),
+ inferIdentity
+ )
+import Control.SessionTypes.Types (
+ ST(..),
+ Cap(..),
+ GetST,
+ GetCtx,
+ Dual,
+ DualST,
+ MapDual,
+ RemoveSend,
+ RemoveSendST,
+ MapRemoveSend,
+ RemoveRecv,
+ RemoveRecvST,
+ MapRemoveRecv,
+ HasConstraint,
+ HasConstraintST,
+ MapHasConstraint,
+ HasConstraints,
+ IfThenElse,
+ Not,
+ Or,
+ Prod (..),
+ Left,
+ Right,
+ Nat(..),
+ Ref(..),
+ TypeEqList,
+ Append
+ )
+import Control.SessionTypes.MonadSession (
+ MonadSession (..),
+ empty,
+ empty0,
+ selN,
+ selN1,
+ selN2,
+ selN3,
+ selN4,
+ Select(sel),
+ (<&),
+ (<&>),
+ offer,
+ recurseFix,
+ recurse0,
+ weaken0,
+ var0,
+ eps0
+ )
diff --git a/src/Control/SessionTypes/Codensity.hs b/src/Control/SessionTypes/Codensity.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/SessionTypes/Codensity.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RebindableSyntax #-}
+-- | This module defines a new type for constructing more efficient `STTerm` programs.
+module Control.SessionTypes.Codensity where
+
+import Control.SessionTypes.STTerm
+import Control.SessionTypes.MonadSession
+import Control.SessionTypes.Indexed hiding (abs)
+
+-- | We define an indexed codensity monad that allows us to reduce quadratic complexity
+-- from repeated use of (>>=) in a session typed program to linear complexity.
+newtype IxC m s r a = IxC { runIxC :: forall b k. (a -> STTerm m r k b) -> STTerm m s k b }
+
+instance IxFunctor (IxC m) where
+ fmap f (IxC x) = IxC $ \c -> x (c . f)
+
+instance IxApplicative (IxC m) where
+ pure = return
+ (<*>) = ap
+
+instance IxMonad (IxC m) where
+ return a = IxC $ \h -> h a
+ (IxC h) >>= f = IxC $ \c -> h $ \a -> runIxC (f a) c
+
+instance Monad m => MonadSession (IxC m) where
+ send a = IxC $ \h -> send a >>= h
+ recv = IxC $ \h -> recv >>= h
+ sel1 = IxC $ \h -> sel1 >>= h
+ sel2 = IxC $ \h -> sel2 >>= h
+ offZ (IxC f) = IxC $ \h -> offZ (f h)
+ offS (IxC f) (IxC g) = IxC $ \h -> offS (f h) (g h)
+ recurse (IxC f) = IxC $ \h -> recurse $ f h
+ weaken (IxC f) = IxC $ \h -> weaken $ f h
+ var (IxC f) = IxC $ \h -> var $ f h
+ eps a = IxC $ \h -> h a
+
+-- | Turns the `IxC` representation of a program to the `STTerm` representation.
+--
+-- The idea is to apply `abs` on a `IxC` program to make the resulting `STTerm` program more efficient.
+abs :: Monad m => IxC m s r a -> STTerm m s r a
+abs (IxC f) = f $ \a -> return a
+
+-- | Transforms an `STTerm` program into a `IxC` representation.
+--
+-- Note that applying this function to a session typed program and then
+-- applying `abs` to the result will not be more efficient.
+--
+-- This is because applying `rep` already induces quadratic complexity.
+rep :: Monad m => STTerm m s r a -> IxC m s r a
+rep m = IxC $ \h -> m >>= h
diff --git a/src/Control/SessionTypes/Debug.hs b/src/Control/SessionTypes/Debug.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/SessionTypes/Debug.hs
@@ -0,0 +1,268 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+-- | This module describes an interpreter for purely evaluating session typed programs
+--
+-- that is based on the paper /Beauty in the beast/ by /Swierstra, W., & Altenkirch, T./
+--
+-- Impurity in a session typed programs mainly comes from three things: receives, branching and lifting.
+--
+-- Using the session type we can easily determine the type of the message that each receive should expect.
+--
+-- This information allows us to define a stream of values of different types that provides input for each receive.
+--
+-- In the sessiontyped-distributed library we send and receive booleans to enable branching.
+--
+-- It is also possible to provide some kind of input that makes this choice.
+--
+-- The current structure of the `Lift` constructor does not allow us to purely evaluate a `Lift`.
+--
+-- As such a session typed program may not contain a lift for it to be purely evaluated. See `runM` as an alternative.
+module Control.SessionTypes.Debug (
+ -- * Pure
+ run,
+ runAll,
+ runSingle,
+ runM,
+ runAllM,
+ runSingleM,
+ -- * Input
+ Stream(..),
+ -- * Output
+ Output(..)
+) where
+
+import Control.SessionTypes
+import qualified Control.SessionTypes.Indexed as I
+
+import Control.DeepSeq (NFData, rnf)
+import Data.Kind (Type)
+
+
+
+-- | Purely evaluates a given `STTerm` using the input defined by `Stream`.
+--
+-- The output is described in terms of the session type actions within the given program
+--
+-- An example of how to use this function goes as follows:
+--
+-- @
+-- prog :: STTerm Identity ('Cap '[] (Int :!> String :?> Eps)) ('Cap '[] Eps) String
+-- prog = send 5 >> recv >>= eps
+--
+-- strm = S_Send $ S_Recv "foo" S_Eps
+-- @
+--
+-- >>> run prog strm
+-- O_Send 5 $ O_Recv "foo" $ O_Eps "foo"
+run :: HasConstraint Show s => STTerm m s ('Cap ctx 'Eps) a -> Stream s -> Output s a
+run st inp = (run' $ st) inp
+
+-- | Instead of describing the session typed actions, it returns a list of the results
+-- of all branches of all offerings.
+--
+-- @
+-- prog = offer (eps 10) (eps 5)
+-- strm = S_OffS S_Eps S_Eps
+-- @
+--
+-- >>> runAll prog strm
+-- [10,5]
+runAll :: HasConstraint Show s => STTerm m s ('Cap ctx 'Eps) a -> Stream s -> [a]
+runAll st stm = evalOutput $ run st stm
+
+-- | Same as `runAll` but applies `head` to the resulting list
+--
+-- >>> runSingle prog strm
+-- 10
+runSingle :: HasConstraint Show s => STTerm m s ('Cap ctx 'Eps) a -> Stream s -> a
+runSingle st stm = head $ evalOutput $ run st stm
+
+run' :: (HasConstraint Show s) => STTerm m s r a -> Stream s -> Output s a
+run' (Send a r) (S_Send s_r) = O_Send a $ run' r s_r
+run' (Recv c) (S_Recv a s_r) = O_Recv a $ run' (c a) s_r
+run' (Sel1 s) (S_Sel1 s_s) = O_Sel1 $ run' s s_s
+run' (Sel2 r) (S_Sel2 s_r) = O_Sel2 $ run' r s_r
+run' (OffZ s) (S_OffZ s_s) = O_OffZ $ run' s s_s
+run' (OffS s r) (S_OffS s_s s_r) = O_OffS (run' s s_s) (run' r s_r)
+run' (OffZ s) (S_Off1 s_s) = O_Off1 $ run' s s_s
+run' (OffS s r) (S_Off2 s_r) = O_Off2 $ run' r s_r
+run' (OffS s r) (S_Off1 s_s) = O_Off1 $ run' s s_s
+run' (Rec r) (S_Rec s_r) = O_Rec $ run' r s_r
+run' (Weaken r) (S_Weaken s_r) = O_Weaken $ run' r s_r
+run' (Var r) (S_Var s_r) = O_Var $ run' r s_r
+run' (Ret a) S_Eps = O_Eps a
+run' (Lift _) _ = error "Cannot run' O_Lift operations. Use runM' instead or remove all lifts"
+
+
+-- | `run` cannot deal with lifted computations. This makes it limited to session typed programs without any use of lift.
+--
+-- This function allows us to evaluate lifted computations, but as a consequence is no longer entirely pure.
+runM :: (Monad m, HasConstraint Show s) => STTerm m s ('Cap ctx 'Eps) a -> Stream s -> m (Output s a)
+runM st inp = runM' (st I.>>= eps) inp
+
+-- | Monadic version of `runAll`.
+runAllM :: (Monad m, HasConstraint Show s) => STTerm m s ('Cap ctx 'Eps) a -> Stream s -> m [a]
+runAllM st stm = fmap evalOutput $ runM st stm
+
+-- | Monad version of `runSingle`
+runSingleM :: (Monad m, HasConstraint Show s) => STTerm m s ('Cap ctx 'Eps) a -> Stream s -> m a
+runSingleM st stm = fmap (head . evalOutput) $ runM st stm
+
+runM' :: (HasConstraint Show s, Monad m) => STTerm m s r a -> Stream s -> m (Output s a)
+runM' (Send a r) (S_Send s_r) = fmap (O_Send a) $ runM' r s_r
+runM' (Recv c) (S_Recv a s_r) = fmap (O_Recv a) $ runM' (c a) s_r
+runM' (Sel1 s) (S_Sel1 s_s) = fmap O_Sel1 $ runM' s s_s
+runM' (Sel2 r) (S_Sel2 s_r) = fmap O_Sel2 $ runM' r s_r
+runM' (OffZ s) (S_OffZ s_s) = fmap O_OffZ $ runM' s s_s
+runM' (OffS s r) (S_OffS s_s s_r) = pure O_OffS <*> (runM' s s_s) <*> (runM' r s_r)
+runM' (OffZ s) (S_Off1 s_s) = fmap O_Off1 $ runM' s s_s
+runM' (OffS s r) (S_Off2 s_r) = fmap O_Off2 $ runM' r s_r
+runM' (OffS s r) (S_Off1 s_s) = fmap O_Off1 $ runM' s s_s
+runM' (Rec r) (S_Rec s_r) = fmap O_Rec $ runM' r s_r
+runM' (Weaken r) (S_Weaken s_r) = fmap O_Weaken $ runM' r s_r
+runM' (Var r) (S_Var s_r) = fmap O_Var $ runM' r s_r
+runM' (Ret a) S_Eps = return $ O_Eps a
+runM' (Lift m) stm = m >>= \st -> fmap O_Lift $ runM' st stm
+
+
+-- | We use the `Stream` data type to supply input for the receives
+-- in a session typed programs.
+--
+-- We annotate a `Stream` with a capability for the following three reasons:
+--
+-- 1. Each `recv` may return a value of a different type.
+--
+-- 2. Given reason 1 and that we can have branching, we must also be able to branch in the stream.
+--
+-- 3. We can now write a function that recursively generates input for a recursive program
+--
+--
+-- Similar to `STTerm`, `Stream` has a constructor for each session type.
+-- Each constructor takes an argument that is another `Stream` type, except
+-- for `S_Recv` that takes an additional argument that will be used as input, and
+-- `S_Eps` that denotes the end of the stream.
+--
+--
+-- At first it might be confusing which constructors and in what order these constructors
+-- should be placed to form a `Stream` that can be used as input for some `STTerm`.
+--
+-- This is actually not that difficult at all. A `Stream` is session typed and that
+-- session type must be equal to the session type of the `STTerm`. As such one merely needs to
+-- create a `Stream` that has the same session type and if you don't the type checker will tell you
+-- what it incorrect.
+--
+-- There are two things that you need to be aware of when constructor a `Stream`.
+--
+-- * The `Stream` constructors for offering (S_OffZ and S_OffS) require that you define input for all branches
+-- of the offering. This can be quite cumbersome, so we include a `S_Off1` and `S_Off2` constructor that behave
+-- similarly to `S_Sel1` and `S_Sel2`.
+--
+-- * You are not guaranteed that a `Stream` can be used for all session typed programs that have the same session type.
+-- Specifically when it comes to selection can we not guarantee this. The session type for selection only tells us
+-- about which branches could be selected. It does not tell us which branch was selected as this is runtime dependent.
+--
+data Stream :: Cap Type -> Type where
+ S_Send :: Stream ('Cap ctx s) -> Stream ('Cap ctx (a :!> s))
+ S_Recv :: a -> Stream ('Cap ctx s) -> Stream ('Cap ctx (a :?> s))
+ S_Sel1 :: Stream ('Cap ctx s) -> Stream ('Cap ctx (Sel (s ': xs)))
+ S_Sel2 :: Stream ('Cap ctx (Sel (t ': xs))) -> Stream ('Cap ctx (Sel (s ': t ': xs)))
+ S_OffZ :: Stream ('Cap ctx s) -> Stream ('Cap ctx (Off '[s]))
+ S_OffS :: Stream ('Cap ctx s) -> Stream ('Cap ctx (Off (t ': xs))) -> Stream ('Cap ctx (Off (s ': t ': xs)))
+ S_Off1 :: Stream ('Cap ctx s) -> Stream ('Cap ctx (Off (s ': xs)))
+ S_Off2 :: Stream ('Cap ctx (Off (t ': xs))) -> Stream ('Cap ctx (Off (s ': t ': xs)))
+ S_Rec :: Stream ('Cap (s ': ctx) s) -> Stream ('Cap ctx (R s))
+ S_Weaken :: Stream ('Cap ctx s) -> Stream ('Cap (t ': ctx) (Wk s))
+ S_Var :: Stream ('Cap (s ': ctx) s) -> Stream ('Cap (s ': ctx) V)
+ S_Eps :: Stream ('Cap '[] Eps)
+
+-- | The `Output` data type describes the session type actions that were done
+data Output :: Cap Type -> Type -> Type where
+ O_Send :: a -> Output ('Cap ctx r) b -> Output ('Cap ctx (a :!> r)) b
+ O_Recv :: a -> Output ('Cap ctx r) b -> Output ('Cap ctx (a :?> r)) b
+ O_Sel1 :: Output ('Cap ctx s) b -> Output ('Cap ctx (Sel (s ': xs))) b
+ O_Sel2 :: Output ('Cap ctx (Sel xs)) b -> Output ('Cap ctx (Sel (s ': xs))) b
+ O_OffZ :: Output ('Cap ctx s) a -> Output ('Cap ctx (Off '[s])) a
+ O_OffS :: Output ('Cap ctx s) b -> Output ('Cap ctx (Off (t ': xs))) b -> Output ('Cap ctx (Off (s ': t ': xs))) b
+ O_Off1 :: Output ('Cap ctx s) a -> Output ('Cap ctx (Off (s ': xs))) a
+ O_Off2 :: Output ('Cap ctx (Off (t ': xs))) a -> Output ('Cap ctx (Off (s ': t ': xs))) a
+ O_Rec :: Output ('Cap (s ': ctx) s) b -> Output ('Cap ctx (R s)) b
+ O_Var :: Output ('Cap (s ': ctx) s) b -> Output ('Cap (s ': ctx) V) b
+ O_Weaken :: Output ('Cap ctx s) b -> Output ('Cap (t ': ctx) (Wk s)) b
+ O_Eps :: b -> Output ('Cap ctx Eps) b
+ O_Lift :: Output s b -> Output s b
+
+-- | Extracts all result values from a given `Output`
+evalOutput :: Output s a -> [a]
+evalOutput (O_Send _ r) = evalOutput r
+evalOutput (O_Recv _ r) = evalOutput r
+evalOutput (O_Sel1 s) = evalOutput s
+evalOutput (O_Sel2 r) = evalOutput r
+evalOutput (O_OffZ s) = evalOutput s
+evalOutput (O_OffS s r) = evalOutput s ++ evalOutput r
+evalOutput (O_Off1 s) = evalOutput s
+evalOutput (O_Off2 r) = evalOutput r
+evalOutput (O_Rec s) = evalOutput s
+evalOutput (O_Var r) = evalOutput r
+evalOutput (O_Weaken r) = evalOutput r
+evalOutput (O_Eps a) = [a]
+evalOutput (O_Lift s) = evalOutput s
+
+
+deriving instance (HasConstraint Show s, Show a) => Show (Output s a)
+deriving instance (HasConstraint Eq s, Eq a) => Eq (Output s a)
+deriving instance (HasConstraint Show s) => Show (Stream s)
+deriving instance (HasConstraint Eq s) => Eq (Stream s)
+--deriving instance (HasConstraint Ord s, Ord a) => Ord (Output s a)
+
+
+instance (HasConstraint NFData s, NFData a) => NFData (Output s a) where
+ rnf (O_Send a b) = (rnf a) `seq` (rnf b)
+ rnf (O_Recv a r) = rnf a `seq` rnf r
+ rnf (O_Sel1 s) = rnf s
+ rnf (O_Sel2 r) = rnf r
+ rnf (O_OffZ s) = rnf s
+ rnf (O_OffS s r) = rnf s `seq` rnf r
+ rnf (O_Off1 s) = rnf s
+ rnf (O_Off2 r) = rnf r
+ rnf (O_Rec s) = rnf s
+ rnf (O_Var s) = rnf s
+ rnf (O_Weaken s) = rnf s
+ rnf (O_Eps a) = rnf a
+ rnf (O_Lift s) = rnf s
+
+instance (HasConstraint NFData s) => NFData (Stream s) where
+ rnf (S_Send r) = rnf r
+ rnf (S_Recv a r) = rnf a `seq` rnf r
+ rnf (S_Sel1 s) = rnf s
+ rnf (S_Sel2 r) = rnf r
+ rnf (S_OffZ s) = rnf s
+ rnf (S_OffS s r) = rnf s `seq` rnf r
+ rnf (S_Off1 s) = rnf s
+ rnf (S_Off2 r) = rnf r
+ rnf (S_Rec s) = rnf s
+ rnf (S_Var s) = rnf s
+ rnf (S_Weaken s) = rnf s
+ rnf (S_Eps) = ()
+
+
+rec2 = S_Rec . S_Rec
+rec4 = rec2 . rec2
+rec8 = rec4 . rec4
+rec16 = rec8 . rec8
+rec32 = rec16 . rec16
+rec64 = rec32 . rec32
+rec128 = rec64 . rec64
+rec100 = rec64 . rec32 . rec4
+
+wk2 = S_Weaken . S_Weaken
+wk4 = wk2 . wk2
+wk8 = wk4 . wk4
+wk16 = wk8 . wk8
+wk32 = wk16 . wk16
+wk64 = wk32 . wk32
+wk128 = wk64 . wk64
+wk100 = wk64 . wk32 . wk4
diff --git a/src/Control/SessionTypes/Indexed.hs b/src/Control/SessionTypes/Indexed.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/SessionTypes/Indexed.hs
@@ -0,0 +1,122 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE FunctionalDependencies #-}
+-- | This module provides a set of indexed type classes (IxFunctor, IxApplicative, IxMonad, etc..) that correspond to existing type classes (Functor, Applicative, Monad, etc..)
+--
+-- The intent of this module is to replace the use of non-indexed type classes with indexed type class.
+--
+-- For that reason the indexed type classes expose functions that are named the same as the functions exposed by a corresponding non-indexed type class.
+--
+-- There are two ways to use this module:
+--
+-- @
+-- import SessionTypes
+-- import qualified SessionTypes.Indexed as I
+--
+-- prog = send 5 I.>> eps0
+-- @
+--
+-- @
+-- {-\# LANGUAGE RebindableSyntax \#-}
+-- import SessionTypes
+-- import SessionTypes.Indexed
+--
+-- prog = do
+-- send 5
+-- eps0
+-- @
+--
+-- With `RebindableSyntax` we construct a custom do notation by rebinding (>>=) with (>>=) of `IxMonad`.
+-- Rebinding is not limited to only (>>=), but also all other functions in Prelude.
+--
+-- We do not want to force importing Prelude if you use `RebindableSyntax`.
+-- Therefore this module also exports Prelude that hides functions already defined by
+-- the indexed type classes.
+module Control.SessionTypes.Indexed (
+ -- * Classes
+ IxFunctor(..),
+ IxApplicative(..),
+ IxMonad(..),
+ -- ** Transformers
+ IxMonadT(..),
+ IxMonadIxT(..),
+ -- ** Mtl
+ IxMonadReader(..),
+ -- ** Exception
+ IxMonadThrow(..),
+ IxMonadCatch(..),
+ IxMonadMask(..),
+ -- ** MonadIO
+ IxMonadIO(..),
+ -- * Combinators
+ ap,
+ -- * Rebind
+ ifThenElse,
+ module PH,
+) where
+
+import Control.Exception
+import Data.Kind (Type)
+import Prelude as PH hiding ((>>=),(>>), return, fail, fmap, pure, (<*>))
+
+class IxFunctor (f :: p -> p -> Type -> Type) where
+ fmap :: (a -> b) -> f j k a -> f j k b
+
+class IxFunctor f => IxApplicative (f :: p -> p -> Type -> Type) where
+ pure :: a -> f i i a
+ (<*>) :: f s r (a -> b) -> f r k a -> f s k b
+
+infixl 1 >>=
+infixl 1 >>
+
+class IxApplicative m => IxMonad (m :: p -> p -> Type -> Type) where
+ (>>=) :: m s t a -> (a -> m t k b) -> m s k b
+ (>>) :: m s t a -> m t k b -> m s k b
+ return :: a -> m i i a
+ fail :: String -> m i i a
+ m1 >> m2 = m1 >>= \_ -> m2
+ fail = error
+
+-- | Type class for lifting monadic computations
+class IxMonad (t m) => IxMonadT t m where
+ lift :: m a -> t m s s a
+
+-- | Type class for lifting indexed monadic computations
+class IxMonad (t m) => IxMonadIxT t m where
+ ilift :: m s r a -> t m s r a
+
+-- | Type class representing the indexed monad reader
+class IxMonad m => IxMonadReader r m | m -> r where
+ ask :: m s s r
+ local :: (r -> r) -> m s t a -> m s t a
+ reader :: (r -> a) -> m i i a
+
+-- | Type class for indexed monads in which exceptions may be thrown.
+class IxMonad m => IxMonadThrow m s where
+ -- | Provide an `Exception` to be thrown
+ throwM :: Exception e => e -> m s s a
+
+-- | Type class for indexed monads to allow catching of exceptions.
+class IxMonadThrow m s => IxMonadCatch m s where
+ -- | Provide a handler to catch exceptions.
+ catch :: Exception e => m s s a -> (e -> m s s a) -> m s s a
+
+-- | Type class for indexed monads that may mask asynchronous exceptions.
+class IxMonadCatch m s => IxMonadMask m s where
+ -- | run an action that disables asynchronous exceptions. The provided function can be used to restore the occurrence of asynchronous exceptions.
+ mask :: ((m s s b -> m s s b) -> m s s b) -> m s s b
+ -- | Ensures that even interruptible functions may not raise asynchronous exceptions.
+ uninterruptibleMask :: ((m s s b -> m s s b) -> m s s b) -> m s s b
+
+-- | Type class for indexed monads that may lift IO computations.
+class IxMonadIO m where
+ liftIO :: IO a -> m s s a
+
+ifThenElse :: Bool -> t -> t -> t
+ifThenElse True b1 _ = b1
+ifThenElse False _ b2 = b2
+
+-- # Combinators
+
+ap :: IxMonad m => m s r (a -> b) -> m r k a -> m s k b
+ap f g = f >>= \f' -> g >>= \g' -> return (f' g')
diff --git a/src/Control/SessionTypes/Interactive.hs b/src/Control/SessionTypes/Interactive.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/SessionTypes/Interactive.hs
@@ -0,0 +1,162 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+-- | This module exposes two functions for interactively evaluation a session typed program
+--
+-- To run a session you must have two participating actors. In our context, the actors are session typed programs.
+--
+-- Using this module the user will act as one of the actors in the session by suppling values to a receive
+--
+-- and selecting a branch for offerings.
+module Control.SessionTypes.Interactive (
+ interactive,
+ interactiveStep
+) where
+
+import Control.SessionTypes.STTerm
+import Control.SessionTypes.Types
+import qualified Control.SessionTypes.Indexed as I
+import Control.SessionTypes.MonadSession
+
+import Control.Monad.Trans.Maybe (MaybeT(..), runMaybeT)
+import Control.Monad.IO.Class (MonadIO, liftIO)
+import Data.Proxy (Proxy (..))
+import Data.Typeable (Typeable, typeRep)
+import Text.Read (readMaybe)
+
+-- | For this function tThe user will act as the dual to the given `STTerm`. User interaction is only required
+-- when the given program does a receive or an offer.
+--
+-- A possible interaction goes as follows:
+--
+-- @
+-- prog = do
+-- send 5
+-- x <- recv
+-- offer (eps x) (eps "")
+--
+-- main = interactive prog
+-- @
+--
+-- >> Enter value of type String: "test"
+-- >> (L)eft or (R)ight: L
+-- > "test"
+interactive :: (MonadIO m, HasConstraints '[Read, Show, Typeable] s, Show a) => STTerm m s r a -> m a
+interactive (Send _ r) = interactive r
+interactive r@(Recv c) = do
+ liftIO $ putStr $ "Enter value of type " ++ typeShow r ++ ": "
+ ma <- liftIO $ fmap readMaybe getLine
+ case ma of
+ Nothing -> interactive r
+ Just a -> interactive $ c a
+ where typeShow :: forall m ctx a r k b. Typeable a => STTerm m ('Cap ctx (a :?> r)) k b -> String
+ typeShow _ = show $ typeRep (Proxy :: Proxy a)
+interactive (Sel1 s) = interactive s
+interactive (Sel2 r) = interactive r
+interactive (OffZ s) = interactive s
+interactive (OffS s xs) = do
+ liftIO $ putStr $ "(L)eft or (R)ight: "
+ lr <- liftIO getLine
+ case lr of
+ "L" -> interactive s
+ "Left" -> interactive s
+ "R" -> interactive xs
+ "Right" -> interactive xs
+ _ -> do
+ liftIO $ putStrLn "Invalid option"
+ interactive (OffS s xs)
+interactive (Rec s) = interactive s
+interactive (Weaken s) = interactive s
+interactive (Var s) = interactive s
+interactive (Lift m) = m >>= interactive
+interactive (Ret a) = return a
+
+-- | Different from `interactive` is that this function gives the user the choice to abort the session
+-- after each session typed action.
+--
+-- Furthermore, it also prints additional output describing which session typed action occurred.
+interactiveStep :: (MonadIO m, HasConstraints '[Read, Show, Typeable] s, Show a) => STTerm m s r a -> m (Maybe a)
+interactiveStep st = runMaybeT (interactiveStep' st)
+
+
+-- Implements interactive stepping. Essentially for every constructor we print a message,
+-- and then allow the user to abort or continue.
+-- For receiving and branching we also require more input that needs to be given before allowing to abort/continue.
+interactiveStep' :: (MonadIO m, HasConstraints '[Read, Show, Typeable] s, Show a) => STTerm m s r a -> MaybeT m a
+interactiveStep' s@(Send a r) = do
+ printST s
+ waitStep
+ interactiveStep' r
+interactiveStep' s@(Recv r) = do
+ printST s
+ ma <- liftIO $ fmap readMaybe getLine
+ case ma of
+ Nothing -> interactiveStep' s
+ Just a -> waitStep >> interactiveStep' (r a)
+interactiveStep' s@(Sel1 r) = do
+ printST s
+ waitStep
+ interactiveStep' r
+interactiveStep' s@(Sel2 r) = do
+ printST s
+ waitStep
+ interactiveStep' r
+interactiveStep' (OffZ r) = interactiveStep' r -- If we see a OffZ then we have already chosen a branch
+interactiveStep' s@(OffS r xs) = do
+ printST s
+ lr <- liftIO getLine
+ if lr `elem` ["L","Left"]
+ then waitStep >> interactiveStep' r
+ else if lr `elem` ["R","Right"]
+ then waitStep >> interactiveStep' xs
+ else do
+ liftIO $ putStrLn "Invalid option"
+ interactiveStep' (OffS s xs)
+interactiveStep' s@(Rec r) = do
+ printST s
+ waitStep
+ interactiveStep' r
+interactiveStep' s@(Weaken r) = do
+ printST s
+ waitStep
+ interactiveStep' r
+interactiveStep' s@(Var r) = do
+ printST s
+ waitStep
+ interactiveStep' r
+interactiveStep' s@(Lift m) = do
+ printST s
+ waitStep
+ MaybeT $ m >>= \st -> runMaybeT $ interactiveStep' st
+interactiveStep' s@(Ret a) = do
+ printST s
+ return a
+
+-- Prints a different message for each constructor of `STTerm`
+printST :: (MonadIO m, HasConstraints [Typeable, Show] s, Show a) => STTerm m s r a -> MaybeT m ()
+printST (Send a _) = liftIO $ putStrLn $ "> Send value " ++ show a
+printST r@(Recv _) = liftIO $ putStr $ "?> Enter value of type " ++ typeShow r ++ ": "
+ where typeShow :: forall m ctx a r k b. Typeable a => STTerm m ('Cap ctx (a :?> r)) k b -> String
+ typeShow _ = show $ typeRep (Proxy :: Proxy a)
+printST (Sel1 _) = liftIO $ putStrLn "> Select1"
+printST (Sel2 _) = liftIO $ putStrLn "> Select2"
+printST (OffZ _) = return ()
+printST (OffS _ _) = liftIO $ putStr $ "?> (L)eft or (R)ight: "
+printST (Rec _) = liftIO $ putStrLn "> Recurse"
+printST (Weaken _) = liftIO $ putStrLn "> Weaken"
+printST (Var _) = liftIO $ putStrLn "> Var"
+printST (Lift _) = liftIO $ putStrLn $ "> Lifted"
+printST (Ret a) = liftIO $ putStrLn $ "> Returned: " ++ show a
+
+-- Gives the user the option to quit early by pressing q
+-- or to continue by pressing n.
+-- We use the maybe monad to implement aborting early.
+waitStep :: MonadIO m => MaybeT m ()
+waitStep = do
+ liftIO $ putStrLn "?> Press n to continue or q to quit."
+ line <- liftIO $ getLine
+ case line of
+ "n" -> return ()
+ "q" -> MaybeT $ return Nothing
+ _ -> waitStep
diff --git a/src/Control/SessionTypes/MonadSession.hs b/src/Control/SessionTypes/MonadSession.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/SessionTypes/MonadSession.hs
@@ -0,0 +1,188 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+-- | This module provides an interface for writing session typed programs
+module Control.SessionTypes.MonadSession (
+ -- * Primitives
+ MonadSession (..),
+ -- * Combinators
+ empty,
+ empty0,
+ selN,
+ selN1,
+ selN2,
+ selN3,
+ selN4,
+ Select(sel),
+ (<&),
+ (<&>),
+ offer,
+ recurseFix,
+ recurse0,
+ weaken0,
+ var0,
+ eps0
+) where
+
+import Control.SessionTypes.Indexed as I
+import Control.SessionTypes.Types
+
+import Data.Function (fix)
+import Data.Typeable (Proxy(..))
+
+-- | The `MonadSession` type class exposes a set of functions that composed together form a session typed program
+--
+-- A type that is an instance of `MonadSession` must therefore also be an instance of `IxMonad`.
+--
+-- The functions themselves are generally defined as wrappers over corresponding `STTerm` constructors.
+class IxMonad m => MonadSession m where
+ send :: a -> m ('Cap ctx (a :!> r)) ('Cap ctx r) ()
+ recv :: m ('Cap ctx (a :?> r)) ('Cap ctx r) a
+ sel1 :: m ('Cap ctx (Sel (s ': xs))) ('Cap ctx s) ()
+ sel2 :: m ('Cap ctx (Sel (s ': t ': xs))) ('Cap ctx (Sel (t ': xs))) ()
+ offZ :: m ('Cap ctx s) r a -> m ('Cap ctx (Off '[s])) r a
+ offS :: m ('Cap ctx s) r a -> m ('Cap ctx (Off (t ': xs))) r a -> m ('Cap ctx (Off (s ': t ': xs))) r a
+ recurse :: m ('Cap (s ': ctx) s) r a -> m ('Cap ctx (R s)) r a
+ weaken :: m ('Cap ctx s) r a -> m ('Cap (t ': ctx) (Wk s)) r a
+ var :: m ('Cap (s ': ctx) s) r a -> m ('Cap (s ': ctx) V) r a
+ eps :: a -> m ('Cap ctx Eps) ('Cap ctx Eps) a
+
+-- | A session typed program that is polymorphic in its context can often not be used by interpreters.
+--
+-- We can apply `empty` to the session typed program before passing it to an interpreter to instantiate that the context is empty.
+empty :: MonadSession m => m ('Cap '[] s) r a -> m ('Cap '[] s) r a
+empty = id
+
+-- | Monadic composable definition of `empty`
+--
+-- Prefix a session typed program with (empty >>) to instantiate the context to be empty.
+empty0 :: MonadSession m => m ('Cap '[] r) ('Cap '[] r) ()
+empty0 = I.return ()
+
+-- | Allows indexing of selections.
+--
+-- The given `Ref` type can be used as an indexed to select a branch. This circumvents the need to sequence a bunch of `sel1` and `sel2` to select a branch.
+--
+-- @
+-- prog :: MonadSession m => m ('Cap ctx (Sel '[a,b,c,d])) ('Cap ctx Eps) ()
+--
+-- MonadSession m => m ('Cap ctx b) ('Cap ctx Eps) ()
+-- prog2 = prog >> selN (RefS RefZ)
+-- @
+--
+selN :: MonadSession m => Ref s xs -> m ('Cap ctx (Sel xs)) ('Cap ctx s) ()
+selN RefZ = sel1
+selN (RefS r) = sel2 I.>> selN r
+
+-- | Select the first branch of a selection.
+selN1 :: MonadSession m => m ('Cap ctx (Sel (s ': xs))) ('Cap ctx s) ()
+selN1 = sel1
+
+-- | Select the second branch of a selection.
+selN2 :: MonadSession m => m ('Cap ctx (Sel (s ': t ': xs))) ('Cap ctx t) ()
+selN2 = sel2 I.>> sel1
+
+-- | Select the third branch of a selection.
+selN3 :: MonadSession m => m ('Cap ctx (Sel (s ': t ': k ': xs))) ('Cap ctx k) ()
+selN3 = sel2 I.>> sel2 I.>> sel1
+
+-- | Select the fourth branch of a selection.
+selN4 :: MonadSession m => m ('Cap ctx (Sel (s ': t ': k ': r ': xs))) ('Cap ctx r) ()
+selN4 = sel2 I.>> sel2 I.>> sel2 I.>> sel1
+
+-- | Type class for selecting a branch through injection.
+--
+-- Selects the first branch that matches the given session type.
+--
+-- @
+-- prog :: MonadSession m => m ('Cap ctx (Sel '[Eps, String :!> Eps, Int :!> Eps])) ('Cap ctx Eps) ()
+-- prog = sel >> send "c" >>= eps
+-- @
+--
+-- It should be obvious that you cannot select a branch using `sel` if that branch has the same session type as a previous branch.
+class Select xs s where
+ sel :: MonadSession m => m ('Cap ctx (Sel xs)) ('Cap ctx s) ()
+
+instance (tl ~ TypeEqList xs s, Select' xs s tl) => Select xs s where
+ sel = sel' (Proxy :: Proxy tl)
+
+class Select' xs s (tl :: k) | xs tl -> s where
+ sel' :: MonadSession m => Proxy tl -> m ('Cap ctx (Sel xs)) ('Cap ctx s) ()
+
+instance Select' (s ': xs) s ('True ': tl) where
+ sel' _ = sel1
+
+instance Select' (r ': xs) t tl => Select' (s ': r ': xs) t ('False ': tl) where
+ sel' _ = sel2 I.>> sel' (Proxy :: Proxy tl)
+
+-- | Takes two session typed programs and constructs an offering consisting of two branches
+offer :: MonadSession m => m ('Cap ctx s) r a -> m ('Cap ctx t) r a -> m ('Cap ctx (Off '[s, t])) r a
+offer s r = offS s (offZ r)
+
+-- | Infix synonym for `offS`
+infixr 1 <&
+(<&) :: MonadSession m => m ('Cap ctx s) r a -> m ('Cap ctx (Off (t ': xs))) r a -> m ('Cap ctx (Off (s ': t ': xs))) r a
+(<&) = offS
+
+-- | Infix synonym for `offer`
+--
+-- Using both `<&` and `<&>` we can now construct an offering as follows:
+--
+-- @
+-- branch1
+-- \<& branch2
+-- \<& branch3
+-- \<&\> branch4
+-- @
+--
+-- This will be parsed as
+--
+-- @
+-- (branch1
+-- \<& (branch2
+-- \<& (branch3
+-- \<&\> branch4)))
+-- @
+infix 2 <&>
+(<&>) :: MonadSession m => m ('Cap ctx s) r a -> m ('Cap ctx t) r a -> m ('Cap ctx (Off '[s, t])) r a
+s <&> r = offS s (offZ r)
+
+-- | A fixpoint combinator for recursion
+--
+-- The argument function must take a recursion variable as an argument that can be used to denote the point of recursion.
+--
+-- For example:
+--
+-- @
+-- prog = recurseFix \\f -> do
+-- send 5
+-- f
+-- @
+--
+-- This program will send the number 5 an infinite amount of times.
+recurseFix :: MonadSession m => (m ('Cap (s ': ctx) V) r a -> m ('Cap (s ': ctx) s) r a) -> m ('Cap ctx (R s)) r a
+recurseFix s = recurse $ fix (\f -> s $ var f)
+
+-- | Monadic composable definition of `recurse`
+recurse0 :: MonadSession m => m ('Cap ctx (R s)) ('Cap (s ': ctx) s) ()
+recurse0 = recurse $ I.return ()
+
+-- | Monadic composable definition of `weaken`
+weaken0 :: MonadSession m => m ('Cap (t ': ctx) (Wk s)) ('Cap ctx s) ()
+weaken0 = weaken $ I.return ()
+
+-- | Monadic composable definition of `var`
+var0 :: MonadSession m => m ('Cap (s ': ctx) V) ('Cap (s ': ctx) s) ()
+var0 = var $ I.return ()
+
+-- | Monadic composable definition of `eps`
+eps0 :: MonadSession m => m ('Cap ctx Eps) ('Cap ctx Eps) ()
+eps0 = eps ()
diff --git a/src/Control/SessionTypes/Normalize.hs b/src/Control/SessionTypes/Normalize.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/SessionTypes/Normalize.hs
@@ -0,0 +1,571 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
+-- | This module provides a type class for normalizing session typed programs.
+--
+-- With normalizing we mean that we apply rewrites to a session typed program until we can no longer do so
+-- and that do not change the semantics of the program.
+--
+-- The motivation for this module is that for two session typed programs to run a session they must be dual.
+-- Sometimes, one of these programs might not have a session type that is dual to the session type of the other program,
+--
+-- but we can rewrite the program and therefore also the session type such that it is. It is of course important that we do not
+-- alter the semantics of the program when rewriting it. For that reason, any rewrite that we may apply must be isomorphic.
+--
+-- A rewrite is isomorphic if we have two programs \p\ and \p'\, we can do a rewrite from \p\ to \p'\ and from \p'\ to \p\.
+--
+-- For now two types of rewrites are applied: Elimination of recursive types and flattening of branches.
+module Control.SessionTypes.Normalize (
+ Normalize(..),
+ Flatten(..),
+ ElimRec(..),
+) where
+
+import Control.SessionTypes.STTerm
+import Control.SessionTypes.Types
+import Data.Proxy (Proxy (..))
+
+-- | Type class for rewriting an `STTerm` to its normal form
+--
+-- The type class has a single instance that is constrained with two type classes.
+-- One for each type of rewrite.
+class Normalize s s'' | s -> s'' where
+ normalize :: Monad m => STTerm m s ('Cap '[] Eps) a -> STTerm m s'' ('Cap '[] Eps) a
+
+instance (Flatten s s', ElimRec s' s'') => Normalize s s'' where
+ normalize = elimRec . flatten
+
+
+-------------------------------------------
+-- Eliminates unused recursion constructors
+-------------------------------------------
+
+-- | Type class for eliminating unused recursive types.
+--
+-- The function `elimRec` traverses a given `STTerm`. While doing so, it will attempt to remove constructors annotated with `R` or `Wk` from the program
+-- if in doing so does not change the behavior of the program.
+--
+-- For example, in the following session type we may remove the inner `R` and the `Wk`.
+--
+-- > R (R (Wk V))
+--
+-- We have that the outer `R` matches the recursion variable because of the use of `Wk`.
+--
+-- That means the inner `R` does not match any recursion variable (the `R` is unused) and therefore may it and its corresponding constructor be removed from the `STTerm` program.
+--
+-- We also remove the `Wk`, because the session type pushed into the context by the inner `R` has also been removed.
+--
+-- The generated session type is
+--
+-- > R V
+class ElimRec s s' | s -> s' where
+ elimRec :: Monad m => STTerm m s r a -> STTerm m s' r a
+
+instance (el ~ ElimRecAllPath s, ElimRec' s s' el) => ElimRec s s' where
+ elimRec = elimRec' (Proxy :: Proxy el)
+
+
+-- Type class that does the actual rewriting of the AST
+-- It takes an extra type parameter, which tells us when to remove a `R`
+-- or a `Wk`. This is computed using the type family `ElimRecAllPath`
+class ElimRec' s s' (rml :: Cap Bool) | s rml -> s' where
+ elimRec' :: Monad m => Proxy rml -> STTerm m s r a -> STTerm m s' r a
+
+
+-- The only instances of interest are those of `R` and `Wk`. The other
+-- instances only traverse the AST
+instance ElimRec' ('Cap ctx r) ('Cap ctx' r') rml =>
+ ElimRec' ('Cap ctx (a :!> r)) ('Cap ctx' (a :!> r')) rml where
+ elimRec' rml (Send a r) = Send a $ elimRec' rml r
+
+instance ElimRec' ('Cap ctx r) ('Cap ctx' r') rml =>
+ ElimRec' ('Cap ctx (a :?> r)) ('Cap ctx' (a :?> r')) rml where
+ elimRec' rml (Recv r) = Recv $ \a -> elimRec' rml (r a)
+
+-- We need two instances for each branching session type
+-- One handling the singleton case and another for having at least
+-- two branches.
+instance ElimRec' ('Cap ctx s)
+ ('Cap ctx' s')
+ ('Cap rmctx rm) =>
+ ElimRec' ('Cap ctx (Sel '[s]))
+ ('Cap ctx' (Sel '[s']))
+ ('Cap rmctx (Sel '[rm])) where
+ elimRec' _ (Sel1 s) = Sel1 $ elimRec' (Proxy :: Proxy ('Cap rmctx rm)) s
+
+instance (ElimRec' ('Cap ctx s)
+ ('Cap ctx' s')
+ ('Cap rmctx rm),
+ ElimRec' ('Cap ctx (Sel (t ': xs)))
+ ('Cap ctx' (Sel (t' ': xs')))
+ ('Cap rmctx (Sel rmxs))) =>
+ ElimRec' ('Cap ctx (Sel (s ': t ': xs)))
+ ('Cap ctx' (Sel (s' ': t' ': xs')))
+ ('Cap rmctx (Sel (rm ': rmxs))) where
+ elimRec' _ (Sel1 s) = Sel1 $ elimRec' (Proxy :: Proxy ('Cap rmctx rm)) s
+ elimRec' _ (Sel2 xs) = Sel2 $ elimRec' (Proxy :: Proxy ('Cap rmctx (Sel rmxs))) xs
+
+instance ElimRec' ('Cap ctx s)
+ ('Cap ctx' s')
+ ('Cap rmctx rm) =>
+ ElimRec' ('Cap ctx (Off '[s]))
+ ('Cap ctx' (Off '[s']))
+ ('Cap rmctx (Off '[rm])) where
+ elimRec' _ (OffZ s) = OffZ $ elimRec' (Proxy :: Proxy ('Cap rmctx rm)) s
+
+instance (ElimRec' ('Cap ctx s) ('Cap ctx' s') ('Cap rmctx rm),
+ ElimRec' ('Cap ctx (Off (t ': xs)))
+ ('Cap ctx' (Off (t' ': xs')))
+ ('Cap rmctx (Off rmxs))) =>
+ ElimRec' ('Cap ctx (Off (s ': t ': xs)))
+ ('Cap ctx' (Off (s' ': t' ': xs')))
+ ('Cap rmctx (Off (rm ': rmxs))) where
+ elimRec' _ (OffS s xs) =
+ OffS (elimRec' (Proxy :: Proxy ('Cap rmctx rm)) s)
+ (elimRec' (Proxy :: Proxy ('Cap rmctx (Off rmxs))) xs)
+
+-- For this instance we have computed that we must not remove this `R`
+-- So we write a `Rec` and do a recursive call on its argument
+instance (ElimRec' ('Cap (s ': ctx) s)
+ ('Cap (s' ': ctx') s')
+ ('Cap (rml ': rmctx) rml)) =>
+ ElimRec' ('Cap ctx (R s))
+ ('Cap ctx' (R s'))
+ ('Cap rmctx ('True :!> rml)) where
+ elimRec' _ (Rec s) = Rec $ elimRec' (Proxy :: Proxy ('Cap (rml ': rmctx) rml)) s
+
+-- In this case we have determined that the `R` must be removed.
+-- So all we do is a recursive call on `s`
+instance (ElimRec' ('Cap (s ': ctx) s)
+ ('Cap ctx' s')
+ ('Cap rmctx rml)) =>
+ ElimRec' ('Cap ctx (R s))
+ ('Cap ctx' s')
+ ('Cap rmctx ('False :!> rml)) where
+ elimRec' _ (Rec s) = elimRec' (Proxy :: Proxy ('Cap rmctx rml)) s
+
+-- When keeping the `Wk` we must account for the possibility that
+-- an other `R` or `Wk` lower in the AST may have been removed. In that case
+-- we can't keep `t` on top of the context as it will still contain that `R`
+-- and `Wk`. We use `ApplyElimRecPath` to compute which `R` and `Wk` are supposed
+-- to be removed from `t`. The result is then placed on top of the context.
+instance (ApplyElimRecPath t rm' ~ t',
+ ElimRec' ('Cap ctx s)
+ ('Cap ctx' s')
+ ('Cap rmctx rml)) =>
+ ElimRec' ('Cap (t ': ctx) (Wk s))
+ ('Cap (t' ': ctx') (Wk s'))
+ ('Cap (rm' ': rmctx) ('True :!> rml)) where
+ elimRec' _ (Weaken s) = Weaken $ elimRec' (Proxy :: Proxy ('Cap rmctx rml)) s
+
+instance (ElimRec' ('Cap ctx s)
+ ('Cap ctx' s')
+ ('Cap rmctx rml)) =>
+ ElimRec' ('Cap (t ': ctx) (Wk s))
+ ('Cap ctx' s')
+ ('Cap rmctx ('False :!> rml)) where
+ elimRec' _ (Weaken s) = elimRec' (Proxy :: Proxy ('Cap rmctx rml)) s
+
+instance ElimRec' ('Cap (s ': ctx) s)
+ ('Cap (s' ': ctx') s')
+ ('Cap (rm ': rmctx) rm) =>
+ ElimRec' ('Cap (s ': ctx) V)
+ ('Cap (s' ': ctx') V)
+ ('Cap (rm ': rmctx) V) where
+ elimRec' _ (Var s) = Var $ elimRec' (Proxy :: Proxy ('Cap (rm ': rmctx) rm)) s
+
+instance ElimRec' ('Cap '[] Eps) ('Cap '[] Eps) ('Cap '[] Eps) where
+ elimRec' _ (Ret a) = Ret a
+ elimRec' _ (Lift m) = error "was a lift"
+
+---------------------------------------------------------------------
+-- Type families used to compute which R's and Wk's should be removed
+---------------------------------------------------------------------
+
+-- Type family to be applied to a capability that calculates a session type
+-- that tells us if an `R` or a `Wk` should be removed.
+type family ElimRecAllPath c where
+ ElimRecAllPath ('Cap ctx s) = 'Cap (MapElimRecAllPath ctx Z) (ElimRecAllPathST s Z)
+
+
+type family ElimRecAllPathST s n where
+ ElimRecAllPathST (a :!> r) n = ElimRecAllPathST r n
+ ElimRecAllPathST (a :?> r) n = ElimRecAllPathST r n
+ ElimRecAllPathST (Sel xs) n = Sel (MapElimRecAllPath xs n)
+ ElimRecAllPathST (Off xs) n = Off (MapElimRecAllPath xs n)
+-- An `R` may only be removed if it does not correspond to a `V`
+ ElimRecAllPathST (R s) n = KeepRPath (R s) (HasPathToV s (S Z)) n
+-- An `Wk` may only be removed if an `R` above it was removed
+ ElimRecAllPathST (Wk s) (S n) = KeepWkPath (Wk s) (HasPathToV s n) (S n)
+ ElimRecAllPathST (Wk s) n = 'False :!> ElimRecAllPathST s n
+ ElimRecAllPathST V n = V
+ ElimRecAllPathST Eps n = Eps
+
+type family MapElimRecAllPath xs n where
+ MapElimRecAllPath '[] n = '[]
+ MapElimRecAllPath (s ': xs) n = ElimRecAllPathST s n ': MapElimRecAllPath xs n
+
+-- If we remove a `R` we also have to consider removing any corresponding `Wk`.
+-- However, a `Wk` might be incorrectly marked to not be removed since
+-- it could be matched to an outer `R`. We use `DeleteWkPath` to also account for this
+type family KeepRPath s b n where
+ KeepRPath (R s) 'True n = ('True :!> (ElimRecAllPathST s (S n)))
+ KeepRPath (R s) 'False n = ('False :!> ((ElimRecAllPathST s n) `MergePath` (DeleteWkPath s (S Z) n)))
+
+type family KeepWkPath s b n where
+ KeepWkPath (Wk s) 'True (S n) = ('True :!> (ElimRecAllPathST s n))
+ KeepWkPath (Wk s) 'False n = ('True :!> ElimRecAllPathST s (S n))
+
+-- Type family that can calcuate for an `R` whether there exists a recursion
+-- variable that corresponds to that `R`. The type family assumes that it is applied
+-- to the body of the `R`.
+-- It takes two arguments: a session type and a natural number.
+-- The natural number is incremented on seeing a `R`
+-- and decremented on seeing a `Wk`. Then if it is (S Z)
+-- we know that we have incremented as often as decremented.
+-- We therefore also know that the R from where this type family
+-- was called reaches a V
+type family HasPathToV s n :: Bool where
+ HasPathToV (a :!> r) n = HasPathToV r n
+ HasPathToV (a :?> r) n = HasPathToV r n
+ HasPathToV (Sel '[s]) n = HasPathToV s n
+ HasPathToV (Sel (s ': xs)) n = HasPathToV s n `Or` HasPathToV (Sel xs) n
+ HasPathToV (Off '[s]) n = HasPathToV s n
+ HasPathToV (Off (s ': xs)) n = HasPathToV s n `Or` HasPathToV (Off xs) n
+ HasPathToV (R s) n = HasPathToV s (S n)
+ HasPathToV (Wk s) (S n) = HasPathToV s n
+ HasPathToV (Wk s) n = 'False
+ HasPathToV V (S Z) = 'True
+ HasPathToV V n = 'False
+ HasPathToV Eps n = 'False
+
+
+
+-- Determines whether a `Wk` should be removed
+-- It takes three arguments: a session type and two natural numbers.
+-- The first Nat
+type family DeleteWkPath s n k where
+ DeleteWkPath (a :!> r) n k = DeleteWkPath r n k
+ DeleteWkPath (a :?> r) n k = DeleteWkPath r n k
+ DeleteWkPath (Sel xs) n k = Sel (MapDeleteWkPath xs n k)
+ DeleteWkPath (Off xs) n k = Off (MapDeleteWkPath xs n k)
+ DeleteWkPath (R s) n k = 'True :!> (DeleteWkPath s (S n) (S k))
+ DeleteWkPath (Wk Eps) (S Z) (S Z) = 'True :!> Eps
+ DeleteWkPath (Wk s) (S Z) k = 'False :!> Eps
+ DeleteWkPath (Wk s) (S n) (S k) = 'True :!> (DeleteWkPath s n k)
+ DeleteWkPath V n k = V
+ DeleteWkPath Eps n k = Eps
+
+type family MapDeleteWkPath xs n k where
+ MapDeleteWkPath '[] n k = '[]
+ MapDeleteWkPath (s ': xs) n k = DeleteWkPath s n k ': MapDeleteWkPath xs n k
+
+type family MergePath l r where
+ MergePath (b1 :!> l) (b2 :!> r) = Not (Not b1 `Or` Not b2) :!> MergePath l r
+ MergePath (Sel xs) (Sel ys) = Sel (MapMergePath xs ys)
+ MergePath (Off xs) (Off ys) = Off (MapMergePath xs ys)
+ MergePath Eps s = s
+ MergePath s Eps = s
+ MergePath V s = s
+ MergePath s V = s
+
+type family MapMergePath l r where
+ MapMergePath '[] '[] = '[]
+ MapMergePath (s ': xs) (r ': ys) = MergePath s r ': MapMergePath xs ys
+
+-- Given a session type that marks which `R` and `Wk` should be removed
+-- we rewrite the session type
+type family ApplyElimRecPath s ml where
+ ApplyElimRecPath (a :!> r) ml = a :!> ApplyElimRecPath r ml
+ ApplyElimRecPath (a :?> r) ml = a :?> ApplyElimRecPath r ml
+ ApplyElimRecPath (Sel xs) (Sel ml) = Sel (MapApplyElimRecPath xs ml)
+ ApplyElimRecPath (Off xs) (Off ml) = Off (MapApplyElimRecPath xs ml)
+ ApplyElimRecPath (R s) ('True :!> ml) = R (ApplyElimRecPath s ml)
+ ApplyElimRecPath (R s) ('False :!> ml) = ApplyElimRecPath s ml
+ ApplyElimRecPath (Wk s) ('True :!> ml) = Wk (ApplyElimRecPath s ml)
+ ApplyElimRecPath (Wk s) ('False :!> ml) = ApplyElimRecPath s ml
+ ApplyElimRecPath s ml = s
+
+type family MapApplyElimRecPath xs ml where
+ MapApplyElimRecPath '[] '[] = '[]
+ MapApplyElimRecPath (s ': xs) (m ': ml) = ApplyElimRecPath s m ': MapApplyElimRecPath xs ml
+
+
+-- | Type class for flattening branches
+--
+-- The function `flatten` takes and traverses a `STTerm`.
+-- If it finds a branching session type that has a branch
+-- starting with another branching of the same type, then it will extract the branches of the inner branching
+-- and inserts these into the outer branching. This is similar to flattening a list of lists to a larger list.
+--
+-- For example:
+--
+-- > Sel '[a,b, Sel '[c,d], e]
+--
+-- becomes
+--
+-- > Sel '[a,b,c,d,e]
+--
+-- This only works if the inner branching has the same type as the outer branch (Sel in Sel or Off in Off).
+--
+-- Also, for now this rewrite only works if one of the branching of the outer branch starts with a new branching.
+--
+-- For example:
+--
+-- > Sel '[a,b, Int :!> Sel '[c,d],e]
+--
+-- does not become
+--
+-- > Sel '[a,b,Int :!> c, Int :!> d, e]
+--
+-- This is something that will be added in the future.
+class Flatten s s' | s -> s' where
+ flatten :: Monad m => STTerm m s r a -> STTerm m s' r a
+
+instance (rwl ~ ListRewrites s, Flatten' s s' rwl) => Flatten s s' where
+ flatten = flatten' (Proxy :: Proxy rwl)
+
+class Flatten' s s' rwl | s rwl -> s' where
+ flatten' :: Monad m => Proxy rwl -> STTerm m s r a -> STTerm m s' r a
+
+
+instance Flatten' ('Cap ctx (Sel ys))
+ ('Cap ctx' (Sel ys'))
+ ('Cap nctx rwl) =>
+ Flatten' ('Cap ctx (Sel '[Sel ys]))
+ ('Cap ctx' (Sel ys'))
+ ('Cap nctx ((Sel '[ 'True :!> rwl]))) where
+ flatten' _ (Sel1 s) = flatten' (Proxy :: Proxy ('Cap nctx rwl)) s
+
+instance (Flatten' ('Cap ctx (Sel '[y]))
+ ('Cap ctx' (Sel '[y']))
+ ('Cap nctx rw_y),
+ Flatten' ('Cap ctx (Sel (x ': xs)))
+ ('Cap ctx' (Sel (x' ': xs')))
+ ('Cap nctx (Sel rw_xs))) =>
+ Flatten' ('Cap ctx (Sel (Sel '[y] ': x ': xs)))
+ ('Cap ctx' (Sel (y' ': x' ': xs')))
+ ('Cap nctx (Sel ('True :!> rw_y ': rw_xs))) where
+ flatten' _ (Sel1 s) =
+ case flatten' (Proxy :: Proxy ('Cap nctx rw_y)) s of
+ Sel1 s' -> Sel1 s'
+ flatten' _ (Sel2 s) = Sel2 $ flatten' (Proxy :: Proxy ('Cap nctx (Sel rw_xs))) s
+
+instance (Flatten' ('Cap ctx (Sel '[s]))
+ ('Cap ctx' (Sel '[s']))
+ ('Cap nctx (Sel '[rw_s])),
+ Flatten' ('Cap ctx (Sel (Sel (z ': ys) ': x ': xs)))
+ ('Cap ctx' (Sel (z' ': xss)))
+ ('Cap nctx (Sel (True :!> (Sel rw_ys) ': rw_xss)))) =>
+ Flatten' ('Cap ctx (Sel (Sel (s ': z ': ys) ': x ': xs)))
+ ('Cap ctx' (Sel (s' ': z' ': xss)))
+ ('Cap nctx (Sel ('True :!> Sel (rw_s ': rw_ys) ': rw_xss))) where
+ -- Using singleSel we enforce the branching denoted by `Sel1 s` to describe
+ -- only a single branch. Otherwise, there would be an ambigeous type variable representing
+ -- the 'other branches', which do not exist. This would prevent us from using flatten on (Sel1 s),
+ -- since we would not be able to describe a constraint matching this application.
+ flatten' _ (Sel1 (Sel1 s)) = Sel1 $ singleSel (Sel1 s) (Proxy :: Proxy ('Cap nctx (Sel '[rw_s])))
+ flatten' _ (Sel1 (Sel2 s)) = Sel2 $ flatten' (Proxy :: Proxy ('Cap nctx (Sel (True :!> Sel rw_ys ': rw_xss))))
+ (instSelApp (Sel1 s) (Proxy :: Proxy (x ': xs)))
+ flatten' _ (Sel2 s) = Sel2 $ flatten' (Proxy :: Proxy ('Cap nctx (Sel (True :!> Sel rw_ys ': rw_xss))))
+ (instSelPrep (Proxy :: Proxy (Sel (z ': ys))) s)
+
+singleSel :: Monad m => Flatten' ('Cap ctx (Sel '[s])) ('Cap ctx' (Sel '[s'])) ('Cap nctx (Sel '[rw_s])) =>
+ STTerm m ('Cap ctx (Sel '[s])) r a -> Proxy ('Cap nctx (Sel '[rw_s])) -> STTerm m ('Cap ctx' s') r a
+singleSel st p = case flatten' p st of
+ (Sel1 s') -> s'
+
+-- Helper functions for append and prepending to a select when this can not only be done using
+-- the constructors of STTerm
+instSelApp :: STTerm m ('Cap ctx (Sel '[x])) r a -> Proxy ys -> STTerm m ('Cap ctx (Sel (x ': ys))) r a
+instSelApp (Sel1 s) _ = Sel1 s
+
+instSelPrep :: Proxy y -> STTerm m ('Cap ctx (Sel (x ': xs))) r a -> STTerm m ('Cap ctx (Sel (y ': x ': xs))) r a
+instSelPrep _ s = Sel2 s
+
+instance Flatten' ('Cap ctx (Off ys))
+ ('Cap ctx' (Off ys'))
+ ('Cap nctx rwl) =>
+ Flatten' ('Cap ctx (Off '[Off ys]))
+ ('Cap ctx' (Off ys'))
+ ('Cap nctx (Off '[ 'True :!> rwl])) where
+ flatten' _ (OffZ s) = flatten' (Proxy :: Proxy ('Cap nctx rwl)) s
+
+instance (Flatten' ('Cap ctx (Off '[s]))
+ ('Cap ctx' (Off '[s']))
+ ('Cap nctx rwl_s),
+ Flatten' ('Cap ctx (Off (x ': xs)))
+ ('Cap ctx' (Off (x' ': xs')))
+ ('Cap nctx (Off rwl_xs))) =>
+ Flatten' ('Cap ctx (Off (Off '[s] ': x ': xs)))
+ ('Cap ctx' (Off (s' ': x' ': xs')))
+ ('Cap nctx (Off ('True :!> rwl_s ': rwl_xs))) where
+ flatten' _ (OffS (OffZ s) xs) =
+ case flatten' (Proxy :: Proxy ('Cap nctx rwl_s)) (OffZ s) of
+ (OffZ s') -> OffS s' (flatten' (Proxy :: Proxy ('Cap nctx (Off rwl_xs))) xs)
+
+instance (Flatten' ('Cap ctx (Off '[s]))
+ ('Cap ctx' (Off '[s']))
+ ('Cap nctx (Off '[rwl_s])),
+ Flatten' ('Cap ctx (Off (Off (z ': ys) ': x ': xs)))
+ ('Cap ctx' (Off (z' ': xss)))
+ ('Cap nctx (Off ('True :!> (Off rwl_ys) ': rw_xs)))) =>
+ Flatten' ('Cap ctx (Off (Off (s ': z ': ys) ': x ': xs)))
+ ('Cap ctx' (Off (s' ': z' ': xss)))
+ ('Cap nctx (Off ('True :!> (Off (rwl_s ': rwl_ys)) ': rw_xs))) where
+ flatten' _ (OffS (OffS s ys) xs) =
+ case flatten' (Proxy :: Proxy ('Cap nctx (Off '[rwl_s]))) (OffZ s) of
+ OffZ s' -> OffS s' $ flatten' (Proxy :: Proxy ('Cap nctx (Off ('True :!> (Off rwl_ys) ': rw_xs)))) (OffS ys xs)
+
+------------------------------------------------------------
+-- Traverse AST and apply flatten'
+------------------------------------------------------------
+
+instance Flatten' ('Cap ctx s)
+ ('Cap ctx' s')
+ ('Cap nctx rwl) =>
+ Flatten' ('Cap ctx (Sel '[s]))
+ ('Cap ctx' (Sel '[s']))
+ ('Cap nctx (Sel '[ 'False :!> rwl])) where
+ flatten' _ (Sel1 s) = Sel1 $ flatten' (Proxy :: Proxy ('Cap nctx rwl)) s
+
+instance (Flatten' ('Cap ctx s)
+ ('Cap ctx' s')
+ ('Cap nctx rw_s),
+ Flatten' ('Cap ctx (Sel (r ': xs)))
+ ('Cap ctx' (Sel (r' ': xs')))
+ ('Cap nctx (Sel rw_xs))) =>
+ Flatten' ('Cap ctx (Sel (s ': r ': xs)))
+ ('Cap ctx' (Sel (s' ': r' ': xs')))
+ ('Cap nctx (Sel ('False :!> rw_s ': rw_xs))) where
+ flatten' _ (Sel1 s) = Sel1 $ flatten' (Proxy :: Proxy ('Cap nctx rw_s)) s
+ flatten' _ (Sel2 s) = Sel2 $ flatten' (Proxy :: Proxy ('Cap nctx (Sel rw_xs))) s
+
+instance Flatten' ('Cap ctx s)
+ ('Cap ctx' s')
+ ('Cap nctx rwl) =>
+ Flatten' ('Cap ctx (Off '[s]))
+ ('Cap ctx' (Off '[s']))
+ ('Cap nctx (Off '[ 'False :!> rwl])) where
+ flatten' _ (OffZ s) = OffZ $ flatten' (Proxy :: Proxy ('Cap nctx rwl)) s
+
+instance (Flatten' ('Cap ctx s)
+ ('Cap ctx' s')
+ ('Cap nctx rwl_s),
+ Flatten' ('Cap ctx (Off (t ': xs)))
+ ('Cap ctx' (Off (t' ': xs')))
+ ('Cap nctx (Off rwl_r))) =>
+ Flatten' ('Cap ctx (Off (s ': t ': xs)))
+ ('Cap ctx' (Off (s' ': t' ': xs')))
+ ('Cap nctx (Off ('False :!> rwl_s ': rwl_r))) where
+ flatten' _ (OffS s xs) =
+ OffS (flatten' (Proxy :: Proxy ('Cap nctx rwl_s)) s)
+ (flatten' (Proxy :: Proxy ('Cap nctx (Off rwl_r))) xs)
+
+instance Flatten' ('Cap ctx r)
+ ('Cap ctx' r')
+ rwl =>
+ Flatten' ('Cap ctx (a :!> r))
+ ('Cap ctx' (a :!> r'))
+ rwl where
+ flatten' p (Send a (Lift m)) = Send a $ Lift $ do
+ st <- m
+ return $ flatten' p st
+ flatten' p (Send a r) = Send a $ flatten' p r
+
+instance Flatten' ('Cap ctx r)
+ ('Cap ctx' r')
+ rwl =>
+ Flatten' ('Cap ctx (a :?> r))
+ ('Cap ctx' (a :?> r'))
+ rwl where
+ flatten' p (Recv r) = Recv $ \x ->
+ case r x of
+ (Lift m) -> Lift $ do
+ st <- m
+ return $ flatten' p st
+ _ -> flatten' p $ r x
+
+instance Flatten' ('Cap (s ': ctx) s)
+ ('Cap (s' ': ctx') s')
+ ('Cap (norm ': nctx) norm) =>
+ Flatten' ('Cap ctx (R s))
+ ('Cap ctx' (R s'))
+ ('Cap nctx norm) where
+ flatten' _ (Rec s) = Rec $ flatten' (Proxy :: Proxy ('Cap (norm ': nctx) norm)) s
+
+-- Similar to the ElimRec case,
+-- the `t` at the top of the context might be invalidated after
+-- rewriting the argument to `Wk`. Hence, we also have to rewrite
+-- `t`.
+instance (RewriteTypes t ~ t',
+ Flatten' ('Cap ctx s)
+ ('Cap ctx' s')
+ ('Cap nctx norm)) =>
+ Flatten' ('Cap (t ': ctx) (Wk s))
+ ('Cap (t' ': ctx') (Wk s'))
+ ('Cap (k ': nctx) norm) where
+ flatten' _ (Weaken s) = Weaken $ flatten' (Proxy :: Proxy ('Cap nctx norm)) s
+
+instance Flatten' ('Cap (s ': ctx) s)
+ ('Cap (s' ': ctx') s')
+ ('Cap (norm ': nctx) norm) =>
+ Flatten' ('Cap (s ': ctx) V)
+ ('Cap (s' ': ctx') V)
+ ('Cap (norm ': nctx) V) where
+ flatten' _ (Var s) = Var $ flatten' (Proxy :: Proxy ('Cap (norm ': nctx) norm)) s
+
+instance Flatten' ('Cap ctx Eps) ('Cap ctx Eps) ('Cap nctx Eps) where
+ flatten' _ (Ret a) = Ret a
+
+
+type family ListRewrites c where
+ ListRewrites ('Cap ctx s) = 'Cap (MapListRewritesCtx ctx) (ListRewritesST s)
+
+type family MapListRewritesCtx ctx where
+ MapListRewritesCtx '[] = '[]
+ MapListRewritesCtx (s ': xs) = ListRewritesST s ': MapListRewritesCtx xs
+
+-- Returns a session type marking where we can do an flatteniative rewrite
+type family ListRewritesST s where
+ ListRewritesST (Sel xs) = Sel (RewriteFlatten (MapListRewritesCtx xs))
+ ListRewritesST (Off xs) = Off (RewriteFlatten (MapListRewritesCtx xs))
+ ListRewritesST (a :!> r) = ListRewritesST r
+ ListRewritesST (a :?> r) = ListRewritesST r
+ ListRewritesST (R s) = ListRewritesST s
+ ListRewritesST (Wk s) = ListRewritesST s
+ ListRewritesST V = V
+ ListRewritesST Eps = Eps
+
+-- Determines whether we can do a flatteniative rewrite
+type family RewriteFlatten s where
+ RewriteFlatten '[] = '[]
+ RewriteFlatten (Sel xs ': ys) = ('True :!> Sel xs) ': RewriteFlatten ys
+ RewriteFlatten (Off xs ': ys) = ('True :!> Off xs) ': RewriteFlatten ys
+ RewriteFlatten (s ': ys) = ('False :!> s) ': RewriteFlatten ys
+
+
+-- Does a full flatteniative rewrite
+type family RewriteTypes s where
+ RewriteTypes (a :!> r) = a :!> RewriteTypes r
+ RewriteTypes (a :?> r) = a :?> RewriteTypes r
+ RewriteTypes (Sel (Sel xs ': ys)) = RewriteTypes (Sel (xs `Append` ys))
+ RewriteTypes (Sel (x ': xs)) = Sel (x ': MapRewriteTypes xs)
+ RewriteTypes (Off (Off xs ': ys)) = RewriteTypes (Off (xs `Append` ys))
+ RewriteTypes (Off (x ': xs)) = Off (x ': MapRewriteTypes xs)
+ RewriteTypes (R s) = R (RewriteTypes s)
+ RewriteTypes (Wk s) = Wk (RewriteTypes s)
+ RewriteTypes V = V
+ RewriteTypes Eps = Eps
+
+type family MapRewriteTypes xs where
+ MapRewriteTypes '[] = '[]
+ MapRewriteTypes (s ': xs) = RewriteTypes s ': MapRewriteTypes xs
diff --git a/src/Control/SessionTypes/STTerm.hs b/src/Control/SessionTypes/STTerm.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/SessionTypes/STTerm.hs
@@ -0,0 +1,157 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+-- | This module defines a GADT `STTerm` that is the very core of this library
+--
+-- Session typed programs are constructed by composing the constructors of `STTerm`.
+--
+-- Each constructor is annotated with a specific session type (except for `Ret` and `Lift`).
+--
+-- By passing a constructor to another constructor as an argument their session types are joined
+-- to form a larger session type.
+--
+-- We do not recommend explicitly composing the `STTerm` constructors. Instead make use of the functions defined in the "Control.SessionTypes.MonadSession" module.
+--
+-- Of course a `STTerm` program in itself is not very useful as it is devoid of any semantics.
+-- However, an interpreter function can give meaning to a `STTerm` program.
+--
+-- We define a couple in this library: "Control.SessionTypes.Debug", "Control.SessionTypes.Interactive", "Control.SessionTypes.Normalize" and "Control.SessionTypes.Visualize".
+module Control.SessionTypes.STTerm (
+ STTerm (..),
+ inferIdentity
+) where
+
+import Control.SessionTypes.MonadSession
+import Control.SessionTypes.Types
+import qualified Control.SessionTypes.Indexed as I
+
+import Control.Monad.IO.Class
+import Data.Functor.Identity (Identity)
+import Data.Kind
+import Data.Typeable
+
+-- | The STTerm GADT
+--
+-- Although we say that a `STTerm` is annotated with a session type, it is actually annotated with a capability (`Cap`).
+--
+-- The capability contains a context that is necessary for recursion and the session type.
+--
+-- The constructors can be split in four different categories:
+--
+-- * Communication: `Send` and `Recv` for basic communication
+-- * Branching: `Sel1`, `Sel2`, `OffZ` and `OffS`
+-- * Recursion: `Rec`, `Weaken` and `Var`
+-- * Unsession typed: `Ret` and `Lift`
+data STTerm :: (Type -> Type) -> Cap a -> Cap a -> Type -> Type where
+ -- | The constructor for sending messages. It is annotated with the send session type (`:!>`).
+ --
+ -- It takes as an argument, the message to send, of type equal to the first argument of `:!>` and the continuing `STTerm` that is session typed with the second argument of `:!>`.
+ Send :: a -> STTerm m ('Cap ctx r) r' b -> STTerm m ('Cap ctx (a :!> r)) r' b
+ -- | The constructor for receiving messages. It is annotated with the receive session type (`:?>`)
+ --
+ -- It takes a continuation that promises to deliver a value that may be used in the rest of the program.
+ Recv :: (a -> STTerm m ('Cap ctx r) r' b) -> STTerm m ('Cap ctx (a :?> r)) r' b
+ -- | Selects the first branch in a selection session type.
+ --
+ -- By selecting a branch, that selected session type must then be implemented.
+ Sel1 :: STTerm m ('Cap ctx s) r a -> STTerm m ('Cap ctx (Sel (s ': xs))) r a
+ -- | Skips a branch in a selection session type.
+ --
+ -- If the first branch in the selection session type is not the one we want to implement
+ -- then we may use `Sel2` to skip this.
+ Sel2 :: STTerm m ('Cap ctx (Sel (t ': xs))) r a -> STTerm m ('Cap ctx (Sel (s ': t ': xs))) r a
+ -- | Dually to selection there is also offering branches.
+ --
+ -- Unlike selection, where we may only implement one branch, an offering asks you to implement all branches. Which is chosen depends
+ -- on how an interpreter synchronizes selection with offering.
+ --
+ -- This constructor denotes the very last branch that may be offered.
+ OffZ :: STTerm m ('Cap ctx s) r a -> STTerm m ('Cap ctx (Off '[s])) r a
+ -- | offers a branch and promises at least one more branch to be offered.
+ OffS :: STTerm m ('Cap ctx s) r a -> STTerm m ('Cap ctx (Off (t ': xs))) r a -> STTerm m ('Cap ctx (Off (s ': t ': xs))) r a
+ -- | Constructor for delimiting the scope of recursion
+ --
+ -- The recursion constructors also modify or at least make use of the context in the capability.
+ --
+ -- The `Rec` constructor inserts the session type argument to `R` into the context of the capability of its `STTerm` argument.
+ --
+ -- This is necessary such that we remember the session type of the body of code that we may want to recurse over and thus avoiding
+ -- infinite type occurrence errors.
+ Rec :: STTerm m ('Cap (s ': ctx) s) r a -> STTerm m ('Cap ctx (R s)) r a
+ -- | Constructor for weakening (expanding) the scope of recusion
+ --
+ -- This constructor does the opposite of `R` by popping a session type from the context.
+ --
+ -- Use this constructor to essentially exit a recursion
+ Weaken :: STTerm m ('Cap ctx t) r a -> STTerm m ('Cap (s ': ctx) (Wk t)) r a
+ -- | Constructor that denotes the recursion variable
+ --
+ -- It assumes the context to be non-empty and uses the session type at the top of the context to determine what should be implemented after `Var`.
+ Var :: STTerm m ('Cap (s ': ctx) s) t a -> STTerm m ('Cap (s ': ctx) V) t a
+ -- | Constructor that makes `STTerm` a (indexed) monad
+ Ret :: (a :: Type) -> STTerm m s s a
+ -- | Constructor that makes `STTerm` a (indexed) monad transformer
+ Lift :: m (STTerm m s r a) -> STTerm m s r a
+
+deriving instance Typeable (STTerm m s r a)
+
+instance Functor (STTerm m s s) where
+ fmap f (Ret a) = Ret $ f a
+
+instance Applicative (STTerm m s s) where
+ pure x = Ret x
+ (Ret f) <*> (Ret a) = Ret $ f a
+
+instance Monad (STTerm m s s) where
+ return x = Ret x
+ (Ret x) >>= f = f x
+
+instance I.IxFunctor (STTerm m) where
+ fmap f (Send a r) = Send a (I.fmap f r)
+
+instance Monad m => I.IxApplicative (STTerm m) where
+ pure x = Ret x
+ (<*>) = I.ap
+
+instance Monad m => I.IxMonad (STTerm m) where
+ return x = Ret x
+ (Send a r) >>= f = Send a (r I.>>= f)
+ (Recv x) >>= f = Recv $ \c -> x c I.>>= f
+ (Sel1 s) >>= f = Sel1 $ s I.>>= f
+ (Sel2 xs) >>= f = Sel2 $ xs I.>>= f
+ (OffZ s) >>= f = OffZ (s I.>>= f)
+ (OffS s xs) >>= f = OffS (s I.>>= f) (xs I.>>= f)
+ (Rec s) >>= f = Rec $ s I.>>= f
+ (Var s) >>= f = Var $ s I.>>= f
+ (Weaken s) >>= f = Weaken $ s I.>>= f
+ (Lift m) >>= f = Lift $ do
+ st <- m
+ return $ st I.>>= f
+ (Ret x) >>= f = f x
+
+instance Monad m => I.IxMonadT (STTerm) m where
+ lift m = Lift $ m >>= return . Ret
+
+instance MonadIO m => I.IxMonadIO (STTerm m) where
+ liftIO m = I.lift $ liftIO m
+
+instance Monad m => MonadSession (STTerm m) where
+ send a = Send a (Ret ())
+ recv = Recv Ret
+ sel1 = Sel1 $ Ret ()
+ sel2 = Sel2 $ Ret ()
+ offZ = OffZ
+ offS = OffS
+ recurse = Rec
+ weaken = Weaken
+ var = Var
+ eps = Ret
+
+-- | This function can be used if we do not use `lift` in a program
+-- but we must still disambiguate `m`.
+inferIdentity :: STTerm Identity s r a -> STTerm Identity s r a
+inferIdentity = id
diff --git a/src/Control/SessionTypes/Types.hs b/src/Control/SessionTypes/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/SessionTypes/Types.hs
@@ -0,0 +1,222 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+-- | This module provides a collection of types and type families.
+--
+-- Specifically it defines the session type data type, capability data type and type families that compute using session types or capabilities as arguments.
+module Control.SessionTypes.Types (
+ -- * Session Types
+ ST(..),
+ Cap(..),
+ GetST,
+ GetCtx,
+ -- * Duality
+ Dual,
+ DualST,
+ MapDual,
+ -- * Removing
+ RemoveSend,
+ RemoveSendST,
+ MapRemoveSend,
+ RemoveRecv,
+ RemoveRecvST,
+ MapRemoveRecv,
+ -- * Applying Constraints
+ HasConstraint,
+ HasConstraintST,
+ MapHasConstraint,
+ HasConstraints,
+ -- * Boolean functions
+ IfThenElse,
+ Not,
+ Or,
+ -- * Product type
+ Prod (..),
+ Left,
+ Right,
+ -- * Other
+ Nat(..),
+ Ref(..),
+ TypeEqList,
+ Append
+) where
+
+import Data.Kind
+import Data.Typeable
+
+infixr 6 :?>
+infixr 6 :!>
+
+-- | The session type data type
+--
+-- Each constructor denotes a specific session type. Using the `DataKinds` pragma the constructors are promoted to types and `ST` is promoted to a kind.
+data ST a = (:?>) a (ST a) -- ^ Send a value
+ | (:!>) a (ST a) -- ^ Recv a value
+ | Sel [ST a] -- ^ Selection of branches
+ | Off [ST a] -- ^ Offering of branches
+ | R (ST a) -- ^ Delimit the scope of recursion
+ | Wk (ST a) -- ^ Weaken the scope of recursion
+ | V -- ^ Recursion variable
+ | Eps -- ^ End of the session
+ deriving Typeable
+
+-- | A capability that stores a context/scope that is a list of session types and a session type
+data Cap a = Cap [ST a] (ST a) deriving Typeable
+
+-- | Retrieves the session type from the capability
+type family GetST s where
+ GetST ('Cap ctx s) = s
+
+-- | Retrieves the context from the capability
+type family GetCtx s where
+ GetCtx ('Cap ctx s) = ctx
+
+-- | Type family for calculating the dual of a session type. It may be applied to a capability.
+--
+-- We made `Dual` injective to support calculating the dual of a selection that contains
+-- an ambiguous branch. Of course that does require that the dual of that ambiguous branch must be known.
+type family Dual s = r | r -> s where
+ Dual ('Cap ctx s) = 'Cap (MapDual ctx) (DualST s)
+
+-- | Type family for calculating the dual of a session type. It may be applied to the actual session type.
+type family DualST (a :: ST c) = (b :: ST c) | b -> a where
+ DualST (s :!> r) = s :?> DualST r
+ DualST (s :?> r) = s :!> DualST r
+ DualST (Sel xs) = Off (MapDual xs)
+ DualST (Off xs) = Sel (MapDual xs)
+ DualST (R s) = R (DualST s)
+ DualST (Wk s) = Wk (DualST s)
+ DualST V = V
+ DualST Eps = Eps
+
+-- | Type family for calculating the dual of a list of session types.
+type family MapDual xs = ys | ys -> xs where
+ MapDual '[] = '[]
+ MapDual (s ': xs) = DualST s ': MapDual xs
+
+-- | Type family for removing the send session type from the given session type. It may be applied to a capability.
+type family RemoveSend s where
+ RemoveSend ('Cap ctx s) = 'Cap (MapRemoveSend ctx) (RemoveSendST s)
+
+-- | Type family for removing the send session type from the given session type. It may be applied to a session type.
+type family RemoveSendST s where
+ RemoveSendST (a :!> r) = RemoveSendST r
+ RemoveSendST (a :?> r) = a :?> RemoveSendST r
+ RemoveSendST (Sel xs) = Sel (MapRemoveSend xs)
+ RemoveSendST (Off xs) = Off (MapRemoveSend xs)
+ RemoveSendST (R s) = R (RemoveSendST s)
+ RemoveSendST (Wk s) = Wk (RemoveSendST s)
+ RemoveSendST s = s
+
+-- | Type family for removing the send session type from a list of session types.
+type family MapRemoveSend ctx where
+ MapRemoveSend '[] = '[]
+ MapRemoveSend (s ': ctx) = RemoveSendST s ': MapRemoveSend ctx
+
+-- | Type family for removing the receive session type from the given session type. It may be applied to a capability.
+type family RemoveRecv s where
+ RemoveRecv ('Cap ctx s) = 'Cap (MapRemoveRecv ctx) (RemoveRecvST s)
+
+-- | Type family for removing the receive session type from the given session type. It may be applied to a session type.
+type family MapRemoveRecv ctx where
+ MapRemoveRecv '[] = '[]
+ MapRemoveRecv (s ': ctx) = RemoveRecvST s ': MapRemoveRecv ctx
+
+-- | Type family for removing the receive session type from a list of session types.
+type family RemoveRecvST s where
+ RemoveRecvST (a :!> r) = a :!> RemoveRecvST r
+ RemoveRecvST (a :?> r) = RemoveRecvST r
+ RemoveRecvST (Sel xs) = Sel (MapRemoveRecv xs)
+ RemoveRecvST (Off xs) = Off (MapRemoveRecv xs)
+ RemoveRecvST (R s) = R (RemoveRecvST s)
+ RemoveRecvST (Wk s) = Wk (RemoveRecvST s)
+ RemoveRecvST s = s
+
+
+-- | Type family for applying a constraint to types of kind `Type` in a session type. It may be applied to a capability.
+type family HasConstraint (c :: Type -> Constraint) s :: Constraint where
+ HasConstraint c ('Cap ctx s) = (HasConstraintST c s, MapHasConstraint c ctx)
+
+-- | Type family for applying a constraint to types of kind `Type` in a session type. It may be applied to a session type.
+type family MapHasConstraint (c :: Type -> Constraint) ss :: Constraint where
+ MapHasConstraint c '[] = ()
+ MapHasConstraint c (s ': ss) = (HasConstraintST c s, MapHasConstraint c ss)
+
+-- | Type family for applying a constraint to types of kind `Type` in a list of session types.
+type family HasConstraintST (c :: Type -> Constraint) s :: Constraint where
+ HasConstraintST c (a :!> r) = (c a, HasConstraintST c r)
+ HasConstraintST c (a :?> r) = (c a, HasConstraintST c r)
+ HasConstraintST c (Sel '[]) = ()
+ HasConstraintST c (Sel (s ': xs)) = (HasConstraintST c s, HasConstraintST c (Sel xs))
+ HasConstraintST c (Off '[]) = ()
+ HasConstraintST c (Off (s ': xs)) = (HasConstraintST c s, HasConstraintST c (Off xs))
+ HasConstraintST c (R s) = HasConstraintST c s
+ HasConstraintST c (Wk s) = HasConstraintST c s
+ HasConstraintST c V = ()
+ HasConstraintST c s = ()
+
+-- | Type family for applying zero or more constraints to types of kind `Type` in a list of session types. It may be applied to a capability.
+type family HasConstraints (cs :: [Type -> Constraint]) s :: Constraint where
+ HasConstraints '[] s = ()
+ HasConstraints (c ': cs) s = (HasConstraint c s, HasConstraints cs s)
+
+-- | Type family for applying zero or more constraints to types of kind `Type` in a list of session types. It may be applied to a session type.
+type family HasConstraintsST (cs :: [Type -> Constraint]) s :: Constraint where
+ HasConstraintsST '[] s = ()
+ HasConstraintsST (c ': cs) s = (HasConstraintST c s, HasConstraintsST cs s)
+
+-- | Type family for applying zero or more constraints to types of kind `Type` in a list of session types. It may be applied to a list of session types.
+type family MapHasConstraints (cs :: [Type -> Constraint]) ctx :: Constraint where
+ MapHasConstraints '[] ctx = ()
+ MapHasConstraints (c ': cs) ctx = (MapHasConstraint c ctx, MapHasConstraints cs ctx)
+
+-- | Promoted `ifThenElse`
+type family IfThenElse (b :: Bool) (l :: k) (r :: k) :: k where
+ IfThenElse 'True l r = l
+ IfThenElse 'False l r = r
+
+-- | Promoted `not`
+type family Not b :: Bool where
+ Not 'True = 'False
+ Not 'False = 'True
+
+-- | Promoted `||`
+type family Or b1 b2 :: Bool where
+ Or 'True b = 'True
+ Or b 'True = 'True
+ Or b1 b2 = 'False
+
+-- | Data type that takes a kind as an argument. Its sole constructor takes two capabilities parameterized by the kind argument.
+--
+-- This data type is useful if it is necessary for an indexed monad to be indexed by four parameters.
+data Prod t = (:*:) (Cap t) (Cap t)
+
+-- | Type family for returning the first argument of a product.
+type family Left p where
+ Left (l :*: r) = l
+
+-- | Type family for returning the second argument of a product.
+type family Right p where
+ Right (l :*: r) = r
+
+-- | Data type defining natural numbers
+data Nat = Z | S Nat deriving (Show, Eq, Ord)
+
+-- | Data type that can give us proof of membership of an element in a list of elements.
+data Ref s xs where
+ RefZ :: Ref s (s ': xs)
+ RefS :: Ref s (k ': xs) -> Ref s (t ': k ': xs)
+
+-- | Type family for computing which types in a list of types are equal to a given type.
+type family TypeEqList xs s where
+ TypeEqList '[s] s = '[True]
+ TypeEqList '[r] s = '[False]
+ TypeEqList (s ': xs) s = 'True ': TypeEqList xs s
+ TypeEqList (r ': xs) s = 'False ': TypeEqList xs s
+
+-- | Promoted `++`
+type family Append xs ys where
+ Append '[] ys = ys
+ Append (x ': xs) ys = x ': xs `Append` ys
diff --git a/src/Control/SessionTypes/Visualize.hs b/src/Control/SessionTypes/Visualize.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/SessionTypes/Visualize.hs
@@ -0,0 +1,635 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+-- | This module defines an interpreter for visualizing session types.
+--
+-- Using `visualize` or `visualizeP` you can create a diagram that displays a session type using a set of nodes and arrows that connect these nodes.
+module Control.SessionTypes.Visualize (
+ visualize,
+ visualizeP,
+ MkDiagram
+) where
+
+import Control.SessionTypes.MonadSession
+import Control.SessionTypes.Types as ST
+
+import Diagrams.Prelude hiding (Coordinates, loc)
+import Diagrams.Backend.SVG.CmdLine
+import Control.Monad.State
+import qualified Data.Vector as V
+import Data.Proxy (Proxy (..))
+import Data.Typeable (Typeable, typeRep)
+
+-- | Visualizes the session type of a given `STTerm`
+-- You may use this function in the following way
+--
+-- > main = visualize st
+--
+-- Then the following command will generate a diagram named "sessiontype.png"
+--
+-- > stack exec vis-sessiontype -- -o sessiontype.png -w 400
+--
+-- For more information on how to generate a diagram please visit the
+-- package
+visualize :: forall m ctx s r a. (MonadSession m, MkDiagram s) => m ('Cap ctx s) r a -> IO ()
+visualize _ = mainWith $ mkDiagram (Proxy :: Proxy s)
+
+-- | Visualizes a given session type denoted by a Proxy.
+visualizeP :: forall s. MkDiagram s => Proxy s -> IO ()
+visualizeP p = mainWith $ mkDiagram p
+
+
+
+
+-- We define a grid as a vector of vectors of nodes
+type Grid = V.Vector (V.Vector Node)
+
+newGrid :: Int -> Int -> Grid
+newGrid x y = V.map (\_ -> V.replicate (x + 1) empNode) $ V.replicate (y + 1) V.empty
+
+gridIndex :: Grid -> (Int, Int) -> Maybe Node
+gridIndex g (x,y) = g V.!? y >>= \v -> v V.!? x
+
+gridIndex' :: Grid -> (Int, Int) -> Node
+gridIndex' g (x,y) = g V.! y V.! x
+
+-- We define a data type to represent Nodes
+-- Nodes are named such that later on we can place arrows between them
+-- They also have a type, which is necessary to determine whether an arrow should be placed
+-- Each node must also have a Diagram representation
+data Node = Node {name :: String, nodeType :: NodeType, nodeDiag :: Diagram B }
+-- The different node types
+data NodeType = N_Send | N_Recv | N_B | N_Anch | N_CR | N_End | N_Emp | T | N_R | N_V | N_W deriving (Eq, Show)
+
+data Orientation = Horizontal | Vertical
+
+------------ Basic Diagrams
+
+diagSize :: Double
+diagSize = 1
+
+newDiag :: String -> Diagram B
+newDiag s = (text s <> circle diagSize) # fontSize (local diagSize)
+
+pointDiag :: Diagram B
+pointDiag = circle 0.01 # lw none
+
+arrBetween_noHead :: String -> String -> Diagram B -> Diagram B
+arrBetween_noHead s1 s2 d = (connectOutside' (with & arrowHead .~ noHead )) s1 s2 d
+
+----------- Node for each session type
+
+sendNode, recvNode, endNode, empNode, crNode, anchNode, offNode, selNode, rNode, vNode, wNode :: Node
+sendNode = Node "" N_Send $ newDiag ":!>"
+recvNode = Node "" N_Recv $ newDiag ":?>"
+endNode = Node "end" N_End $ newDiag "End"
+empNode = Node "" N_Emp $ newDiag "" # lw none
+crNode = Node "" N_CR $ pointDiag
+anchNode = Node "" N_Anch $ pointDiag
+offNode = Node "" N_B $ newDiag "Off"
+selNode = Node "" N_B $ newDiag "Sel"
+rNode = Node "" N_R $ newDiag "R"
+vNode = Node "" N_V $ newDiag "V"
+wNode = Node "" N_W $ newDiag "Wk"
+
+----------- Other node types
+
+encase :: Node -> Node
+encase (Node n nt d) = Node n nt (d <> (circle diagSize # lw none))
+
+typeBox :: String -> Node
+typeBox s = Node "" T $ newDiag s # lw none
+
+{-
+
+ DIAGRAM API
+
+-}
+
+-- When building the diagram we will need to keep track of several things
+data DState = DState {
+ counter :: Int, -- ^ Used to make unique name
+ weakenN :: Int, -- ^ Number of weakenings
+ loc :: (Int, Int), -- ^ current position in the grid
+ diag :: Diagram B, -- ^ Diagram that we build
+ grid :: Grid -- ^ Grid that will contain nodes
+ }
+
+
+newDState :: Grid -> DState
+newDState = DState 0 0 (0,0) mempty
+
+-- | We use a State monad to modify the diagram
+type DiagramM a = StateT DState IO a
+
+runDiagramM :: DState -> DiagramM a -> IO (a, DState)
+runDiagramM state m = runStateT m state
+
+-- Creates a Diagram from a given grid
+gridToDiagram :: Grid -> Diagram B
+gridToDiagram g = vsep (2 * diagSize) $ V.toList $ V.map (hsep (2 * diagSize) . map nodeDiag . V.toList) g
+
+-- | Returns a unique name
+newName :: DiagramM String
+newName = do
+ (DState n w xy d g) <- get
+ put (DState (n + 1) w xy d g)
+ return $ show n
+
+-- | Name a given node
+nameNode :: Node -> DiagramM Node
+nameNode (Node _ t d) = do
+ name <- newName
+ return $ Node name t $ d # named name
+
+-- | Checks the current position and returns the name of the node
+getNameAtCurr :: DiagramM String
+getNameAtCurr = do
+ loc <- getLoc
+ grid <- getGrid
+ let (Node name _ _) = gridIndex' grid loc
+ return name
+
+-- | Returns current location
+getLoc :: DiagramM (Int, Int)
+getLoc = fmap loc get
+
+-- | Update the current location with a new location
+saveLoc :: (Int, Int) -> DiagramM ()
+saveLoc (x,y) = modify $ \(DState n w _ d g) -> DState n w (x,y) d g
+
+-- | Move up by one
+incrLocY :: DiagramM ()
+incrLocY = modify $ \(DState n w (x,y) d g) -> DState n w (x, y + 1) d g
+
+-- | Move down by one
+decrLocY :: DiagramM ()
+decrLocY = modify $ \(DState n w (x,y) d g) -> DState n w (x, y - 1) d g
+
+-- | Move to the right by one
+incrLocX :: DiagramM ()
+incrLocX = modify $ \(DState n w (x,y) d g) -> DState n w (x + 1, y) d g
+
+-- | Keep moving to the right until
+incrLocXWhile :: (Node -> Bool) -> DiagramM ()
+incrLocXWhile f = do
+ incrLocX
+ loc <- getLoc
+ grid <- getGrid
+ let mn = gridIndex grid loc
+ case mn of
+ Nothing -> return ()
+ Just n | f n -> incrLocXWhile f
+ | otherwise -> return ()
+
+-- | Increase the number of weakenings
+incrWk :: DiagramM ()
+incrWk = modify $ \(DState n w loc d g) -> DState n (w + 1) loc d g
+
+-- | decrease the number of weakenings
+decrWk :: DiagramM ()
+decrWk = modify $ \(DState n w loc d g) -> DState n (w - 1) loc d g
+
+-- | Get current number of weakenings
+getWk :: DiagramM Int
+getWk = fmap weakenN get
+
+-- | Insert new number of weaknings into state
+saveWk :: Int -> DiagramM ()
+saveWk w = modify $ \(DState n _ loc d g) -> DState n w loc d g
+
+-- | Returns the grid
+getGrid :: DiagramM Grid
+getGrid = fmap grid get
+
+-- | Saves a new grid
+saveGrid :: Grid -> DiagramM ()
+saveGrid g = modify $ \(DState n w loc d _) -> DState n w loc d g
+
+-- | Returns the diagram
+getDiag :: DiagramM (Diagram B)
+getDiag = fmap diag get
+
+-- | Saves a new diagram
+saveDiag :: Diagram B -> DiagramM ()
+saveDiag d = modify $ \(DState n w loc _ g) -> DState n w loc d g
+
+-- | Place a node at the current location
+placeAtCurrM :: Node -> DiagramM ()
+placeAtCurrM sn = do
+ loc <- getLoc
+ placeAtLocM sn loc
+
+-- | Place a node at the given location
+placeAtLocM :: Node -> (Int, Int) -> DiagramM ()
+placeAtLocM sn loc = do
+ grid <- getGrid
+ saveGrid $ placeAtLoc sn loc grid
+
+placeAtLoc :: Node -> (Int, Int) -> Grid -> Grid
+placeAtLoc sn (x,y) grid = grid V.// [(y, (grid V.! y) V.// [(x, sn)])]
+
+-- Internal utility function
+printGrid :: Grid -> IO ()
+printGrid g = forM_ g $ \hv -> do
+ forM_ hv (\(Node n t _) -> putStr (show (n, t) ++ " "))
+ putStrLn ""
+
+{-
+We use a grid to give a visualization of session types. The grid contains nodes
+and is sized by the maximum number of nodes in the X and Y dimension.
+The size is calculated using the `Coordinates` type class.
+
+The grid is initially filled with so called empty nodes that don't show in the generated diagram.
+We will first use the type class `PlaceNodes` to place nodes in the grid that describe the session type.
+Initially we start at location (0,0), which is the left top in the diagram. Then the `PlaceNodes` will independently
+for each partial session type place nodes. After having done so it will update the position that we are at and do a recursive call
+for the second part of the session type if it exists.
+
+We'll shortly describe how nodes are placed for each session type:
+ a :!> r : Places two nodes. First a node describing `a` at the current position.
+ Then a new node describing the operator `:!>` at 1 position below it.
+ The y coordinate of the position is then once more increased before making a recursive call on `r`.
+
+ a :?> r : Similar to `a :!> r`
+
+ Sel '[s] : For each branching session ype we have to write two instances. In this case we only have to make a recursive call on `s`
+
+ Sel (s ': t ': xs): We place a node describing `Sel` at the current position. We then increment y and do a recursive call on `s`, such that
+ the first branch is placed directly below `Sel`. After completion of the recursive call we go back to our original position
+ and move in the X-dimension equal to the size of `s` in its X-dimension + 1. This is necessary to avoid overlap between the two
+ branches. In our new position we place a so called corner node that is essentially invisible, but is necessary for arrows.
+ Finally we increment y and do a recursive call on `Sel (t ': xs)`.
+
+ Off '[s] : Same as `Sel '[s]`
+
+ Off (s ': t ': xs) : Similar to `Sel (s ': t ': xs)`.
+
+ R s : We place a node describing `R` and replace all empty nodes to the right of this node with an anchor node. The anchor node is necessary for a `V` node
+ to connect with this `R` node. Since there can be multiple `V` nodes, we might need more than one anchor. One solution is to calculate exactly at which
+ X-coordinate these `V` nodes are and use these coordinates to place anchor nodes. An easier solution is to simply place anchor nodes at every empty node
+ to the right of this `R` node, since anchor nodes in most cases can be treated as empty nodes. So if one overlaps with a branch, then it will be removed
+ by that branch. After having placed these anchor nodes we do a recursive call on `s`.
+
+ Wk s : Similar to `R`, but without the anchor nodes.
+
+ V : Places two nodes. One at the current position describing `V` and an anchor node directly to the right. This anchor node will connect to an anchor node
+ placed right to a `R` node.
+
+ Eps : A single node describing `Eps`.
+
+
+After all nodes have been placed we will have to connect them.
+We will walk the grid starting from (0,0).
+Depending on the type of the node we know which session type it is describing.
+And as described above, we know exactly where the next nodes are.
+Connecting two nodes using the Diagrams library is done by taking two named diagrams (nodes)
+and constructing a single diagram that contains both nodes with an arrow between them.
+
+For both branching and recursion we have to take a bit more care about how we connect nodes with arrows.
+The corner node of a branching is not directly to the right of the branching node, so we have to walk over all empty
+and anchor nodes until it finds one.
+With recursion we need to consider the number of `R` and `Wk` nodes that we have passed before connecting a `V` node to a `R` node.
+Once that number is known 3 arrows will be placed: from the `V` node to its anchor node, from that anchor node to an anchor of a `R` node and from that anchor
+to that `R` node.
+
+
+-}
+
+-- | Type class for constructing a diagram that visualizes the session types
+class MkDiagram (s :: ST k) where
+ mkDiagram :: Proxy s -> IO (Diagram B)
+
+ default mkDiagram :: (Coordinates s, PlaceNodes s) => Proxy s -> IO (Diagram B)
+ mkDiagram p = do
+ -- place nodes in the grid
+ dstate <- dstateWNodesIO
+ -- connect the grid and build a Diagram
+ (diag, DState n _ _ d g) <- runStateT connectGrid dstate
+ -- Place arrows going from a `V` to a `R`
+ fmap fst $ runStateT connectRecursions (DState n 0 (0,0) diag g)
+ where
+ dstateWNodesIO = fmap snd $ runStateT (placeNodes p) (newDState $ newGrid (getX p) (getY p))
+
+instance (Coordinates s, PlaceNodes s) => MkDiagram s
+
+-- | Determines size of grid based on the session types
+class Coordinates (s :: ST k) where
+ getX :: Proxy s -> Int
+ getY :: Proxy s -> Int
+
+instance Coordinates r => Coordinates (a :!> r) where
+ getY Proxy = 2 + getY (Proxy :: Proxy r)
+ getX Proxy = getX (Proxy :: Proxy r)
+
+instance Coordinates r => Coordinates (a :?> r) where
+ getY Proxy = 2 + getY (Proxy :: Proxy r)
+ getX Proxy = getX (Proxy :: Proxy r)
+
+instance Coordinates t => Coordinates (Sel '[t]) where
+ getY Proxy = getY (Proxy :: Proxy t)
+ getX Proxy = getX (Proxy :: Proxy t)
+
+instance (Coordinates s, Coordinates (Sel (t ': xs))) => Coordinates (Sel (s ': t ': xs)) where
+ getY Proxy = 1 + getY (Proxy :: Proxy s) `max` getY (Proxy :: Proxy (Sel (t ': xs)))
+ getX Proxy = 1 + getX (Proxy :: Proxy s) + getX (Proxy :: Proxy (Sel (t ': xs)))
+
+instance Coordinates t => Coordinates (Off '[t]) where
+ getY Proxy = getY (Proxy :: Proxy t)
+ getX Proxy = getX (Proxy :: Proxy t)
+
+instance (Coordinates s, Coordinates (Off (t ': xs))) => Coordinates (Off (s ': t ': xs)) where
+ getY Proxy = 1 + getY (Proxy :: Proxy s) `max` getY (Proxy :: Proxy (Off (t ': xs)))
+ getX Proxy = 1 + getX (Proxy :: Proxy s) + getX (Proxy :: Proxy (Off (t ': xs)))
+
+instance Coordinates s => Coordinates (R s) where
+ getY _ = 1 + getY (Proxy :: Proxy s)
+ getX _ = getX (Proxy :: Proxy s)
+
+instance Coordinates ST.V where
+ getY _ = 0
+ getX _ = 1
+
+instance Coordinates s => Coordinates (Wk s) where
+ getY _ = 1 + getY (Proxy :: Proxy s)
+ getX _ = getX (Proxy :: Proxy s)
+
+instance Coordinates 'Eps where
+ getY _ = 0
+ getX _ = 0
+
+
+-- | Type class that places the nodes at the correct locations in the grid
+class PlaceNodes (s :: ST k) where
+ placeNodes :: Proxy s -> DiagramM ()
+
+instance (Typeable a, PlaceNodes r) => PlaceNodes (a :!> r) where
+ placeNodes Proxy = operationDiagram sendNode (Proxy :: Proxy a) (Proxy :: Proxy r)
+
+instance (Typeable a, PlaceNodes r) => PlaceNodes (a :?> r) where
+ placeNodes Proxy = operationDiagram recvNode (Proxy :: Proxy a) (Proxy :: Proxy r)
+
+instance PlaceNodes s => PlaceNodes (Sel '[s]) where
+ placeNodes _ = placeNodes (Proxy :: Proxy s)
+
+instance (Coordinates s, PlaceNodes s, PlaceNodes (Sel (t ': xs))) => PlaceNodes (Sel (s ': t ': xs)) where
+ placeNodes _ = branchDiagram selNode (Proxy :: Proxy s) (Proxy :: Proxy (Sel (t ': xs)))
+
+instance PlaceNodes s => PlaceNodes (Off '[s]) where
+ placeNodes _ = placeNodes (Proxy :: Proxy s)
+
+instance (Coordinates s, PlaceNodes s, PlaceNodes (Off (t ': xs))) => PlaceNodes (Off (s ': t ': xs)) where
+ placeNodes _ = branchDiagram offNode (Proxy :: Proxy s) (Proxy :: Proxy (Off (t ': xs)))
+
+instance PlaceNodes s => PlaceNodes (R s) where
+ placeNodes p = do
+ -- create a recursion node
+ rnode' <- nameNode rNode
+ loc <- getLoc
+
+ -- place the node at the current location
+ placeAtCurrM rnode'
+ incrLocY
+
+ -- do a recursive call for the other nodes
+ placeNodes (Proxy :: Proxy s)
+
+ -- place an anchor node
+ saveLoc loc
+ incrLocX
+ placeAnchors (\(x,y) -> (x + 1, y))
+
+instance PlaceNodes ST.V where
+ placeNodes _ = do
+ -- create a recursion variable node
+ -- and place it at the current loc
+ vnode <- nameNode vNode
+ placeAtCurrM vnode
+
+ -- Place an anchor node
+ incrLocX
+ anchnode <- nameNode anchNode
+ placeAtCurrM $ encase anchnode
+
+instance PlaceNodes s => PlaceNodes (Wk s) where
+ placeNodes _ = do
+ wnode <- nameNode wNode
+
+ placeAtCurrM wnode
+ incrLocY
+
+ placeNodes (Proxy :: Proxy s)
+
+instance PlaceNodes 'Eps where
+ placeNodes Proxy = do
+ end <- nameNode endNode
+
+ placeAtCurrM end
+ return ()
+
+-- Places the nodes for the send and receive session type
+operationDiagram :: (Typeable a, PlaceNodes r) => Node -> Proxy a -> Proxy r -> DiagramM ()
+operationDiagram node pr1 pr2 = do
+ tb <- nameNode $ typeBox $ show $ typeRep pr1
+ nnode <- nameNode node
+
+ placeAtCurrM tb
+ incrLocY
+ placeAtCurrM nnode
+ incrLocY
+
+ placeNodes pr2
+
+-- Places the nodes for the branching session types
+branchDiagram :: (Coordinates s, PlaceNodes s, PlaceNodes r) => Node -> Proxy s -> Proxy r -> DiagramM ()
+branchDiagram n pr1 pr2 = do
+ br <- nameNode n
+ cr <- nameNode crNode
+
+ placeAtCurrM br
+ (x,y) <- getLoc
+ incrLocY
+
+ placeNodes pr1
+ saveLoc (x + getX pr1 + 1, y)
+ placeAtCurrM (encase cr)
+ incrLocY
+
+ placeNodes pr2
+
+
+-- Walks the grid in a given direction and replaces
+-- all empty nodes with an anchor node
+placeAnchors :: ((Int, Int) -> (Int, Int)) -> DiagramM ()
+placeAnchors move = do
+ loc <- getLoc
+ g <- getGrid
+ let mn = gridIndex g loc -- get the node at the current position
+ case mn of
+ -- We are out of bounds so we stop recursion
+ Nothing -> return ()
+ -- If empty node then replace it with a anchor
+ Just n | nodeType n == N_Emp -> do
+ nn <- nameNode anchNode
+ placeAtCurrM (encase nn)
+ -- move and do a recursive call
+ saveLoc (move loc)
+ placeAnchors move
+ | otherwise -> return ()
+
+
+-- Top level function for placing arrows between nodes
+-- returns a Diagram that can be displayed
+connectGrid :: DiagramM (Diagram B)
+connectGrid = do
+ grid <- getGrid
+ -- take the grid and turn it into diagram
+ -- the diagram contains the nodes, but does not contain arrows
+ addConn $ gridToDiagram grid
+ where
+ addConn d = do
+ grid <- getGrid
+ -- Takes the existing diagram and will add arrows to this diagram
+ walkGrid (0,0) connectNodes grid d
+
+-- Implements the logic for connecting two nodes
+-- If two nodes are to be connected we add a property on the
+-- diagram that adds an arrow between the nodes
+connectNodes :: Node -> Node -> Orientation -> Diagram B -> DiagramM (Diagram B)
+connectNodes (Node n1 t1 d1) (Node n2 t2 d2) Horizontal d
+ | t1 == N_B && t2 == N_CR = return $ (d # arrBetween_noHead n1 n2)
+ | otherwise = return d
+connectNodes (Node n1 t1 _) (Node n2 t2 _) Vertical d
+ | t2 /= N_CR
+ && t1 /= N_Emp = return $ d # connectOutside n1 n2
+ | otherwise = return d
+
+-- Walkes the grid starting at the given location.
+-- It also takes a function that can connect two nodes, the grid and the diagram that is to be built upon
+-- The function works by taking the current position and walking downwards to see if there are any nodes
+-- If there are it will use the function to place any arrows and then do a recursive call downwards
+-- Otherwise it will return the diagram built so far and tries the same from the original position in a rightward movement
+-- This function is primarily for walking over the grid, whereas the given function implements the logic for adding arrows
+walkGrid :: (Int, Int) -> (Node -> Node -> Orientation -> Diagram B -> DiagramM (Diagram B)) -> Grid -> Diagram B -> DiagramM (Diagram B)
+walkGrid (x,y) f g d = tryVertical d >>= tryHorizontal (x,y)
+ where
+ currNode = gridIndex' g (x,y) -- current node
+ tryHorizontal (x',y') d = do
+ case gridIndex g (x' + 1,y') of
+ Nothing -> return d -- out of bounds
+ -- If its an anchor or empty node there is nothing to connect, but there might be a corner node further to the right
+ -- We don't do a recursive call on walkGrid, because that would try to connect an empty/anchor node to anything below it
+ Just sn | nodeType sn == N_Anch || nodeType sn == N_Emp -> tryHorizontal (x' + 1, y) d
+ -- If we found a corner node we use `f` to add any arrows.
+ -- We can now also stop looking to the right, so we call walkGrid again
+ | nodeType sn == N_CR -> do
+ d' <- f currNode sn Horizontal d
+ walkGrid (x' + 1, y') f g d'
+ | otherwise -> return d
+ -- Vertical movement is much more simple, either there is a node directly below it or there will never be any
+ tryVertical d = case gridIndex g (x, y + 1) of
+ Nothing -> return d
+ Just sn -> do
+ d' <- f currNode sn Vertical d
+ walkGrid (x, y + 1) f g d'
+
+-- Adds arrows going from V to an R
+-- We traverse the grid and upon encountering a V we have to do backtracking
+-- to find the corresponding R
+connectRecursions :: DiagramM (Diagram B)
+connectRecursions = do
+ pos <- getLoc
+ grid <- getGrid
+ let (Node name nt _) = gridIndex' grid pos
+ case nt of
+ N_V -> do
+ -- We move to the anchor node and start backtracking
+ incrLocX
+ backTrack name
+ getDiag
+ N_B -> do
+ incrLocY
+ d <- connectRecursions
+
+ saveDiag d
+ saveLoc pos
+ -- Look for second branch
+ incrLocXWhile (\(Node _ nt _) -> nt /= N_CR)
+ connectRecursions
+ N_W -> do
+ incrLocY
+ -- increment number of weakens we found
+ incrWk
+ wk <- getWk
+ connectRecursions
+ -- ensure that weakenings in one branch don't affect other branches
+ decrWk
+ getDiag
+ N_End -> getDiag
+ _ -> do
+ incrLocY
+ connectRecursions
+
+-- The backtrack function starts at the anchor node of a `V` node
+-- It starts moving upwards. After every increment it will look
+-- for `R` nodes to its left
+-- If there exists one, then if the number of weakenings is at 0 we make an arrow
+-- to its anchor node and from its anchor node to the `R` node itself.
+-- If the number of weakens is higher than zero, then we keep moving upward
+-- while decrementing the number of weakenings.
+-- if there is no `R` node then we also move upwards
+backTrack :: String -> DiagramM ()
+backTrack name = do
+ grid <- getGrid
+
+ pos <- getLoc
+ cname <- getNameAtCurr
+ goUp cname -- need the name of the original anchor node to make a connection
+ saveLoc pos
+ where
+ goUp cname = do
+ ms <- rToLeft -- Looks for `R` node to the left
+ case ms of
+ -- If there is none we move upward
+ Nothing -> do
+ decrLocY
+ goUp cname
+ Just rname -> do
+ wkC <- getWk
+ if wkC == 0 -- we can make a connection
+ then do
+ cname' <- getNameAtCurr
+ d <- getDiag
+ saveDiag (d # arrBetween_noHead name cname
+ # arrBetween_noHead cname cname'
+ # connectOutside cname' rname)
+ else do -- decrement the number of weakenings and move upwards
+ decrWk
+ decrLocY
+ goUp cname
+ saveWk wkC
+
+-- Looks for a `R` node to the left of the current location
+rToLeft :: DiagramM (Maybe String)
+rToLeft = do
+ (x,y) <- getLoc
+ grid <- getGrid
+ let mnode = gridIndex grid (x,y)
+ mn <- case mnode of
+ Nothing -> return Nothing
+ Just (Node name nt _)
+ | nt == N_R -> return $ Just name -- found one
+ | nt == N_Anch || nt == N_Emp -> do -- keep moving left
+ saveLoc (x-1, y)
+ ms <- rToLeft
+ return ms
+ | otherwise -> return Nothing -- could not find any
+
+ saveLoc (x, y) -- set position back to original location
+ return mn
diff --git a/test/Test/Debug/Main.hs b/test/Test/Debug/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Debug/Main.hs
@@ -0,0 +1,79 @@
+import Control.SessionTypes
+import Control.SessionTypes.Debug
+
+import Test.Program.Simple
+import Test.Program.FileServer
+import Test.Hspec
+
+main :: IO ()
+main = hspec $ do
+ describe "runSingle" $ do
+ it "returns True" $
+ runSingle (inferIdentity prog_sendRecv) (S_Send $ S_Recv True S_Eps) `shouldBe` True
+
+ it "returns the value of the first returned value in a program; '()'" $
+ runSingle (inferIdentity prog_branching) (S_Off1 $ S_Send S_Eps) `shouldBe` ()
+
+ it "selects a branch and returns 'c'" $
+ runSingle (inferIdentity prog_branching_dual) (S_Sel1 $ S_Recv "c" S_Eps) `shouldBe` "c"
+
+ it "Recurses until a 10 is given" $
+ runSingle (inferIdentity prog_recursion) (S_Rec $ S_Recv 7 $ S_Sel2 $ S_Sel1 $ S_Var $ S_Recv 10 $ S_Sel1 $ S_Weaken $ S_Eps) `shouldBe` 10
+
+ describe "runAll" $ do
+ it "returns [True]" $
+ runAll (inferIdentity prog_sendRecv) (S_Send $ S_Recv True S_Eps) `shouldBe` [True]
+
+ it "returns the values returned in all branches; [(),(),()]" $
+ runAll (inferIdentity prog_branching) (S_OffS (S_Send S_Eps) $ S_OffS (S_Send S_Eps) $ S_OffZ (S_Send S_Eps)) `shouldBe` [(),(),()]
+
+ it "returns only the final result in a list; [10]" $
+ runAll (inferIdentity prog_recursion) (S_Rec $ S_Recv 7 $ S_Sel2 $ S_Sel1 $ S_Var $ S_Recv 10 $ S_Sel1 $ S_Weaken $ S_Eps) `shouldBe` [10]
+
+ describe "run" $ do
+ it "returns O_Send followed by O_Recv" $
+ run (inferIdentity prog_sendRecv) (S_Send $ S_Recv True S_Eps) `shouldBe` (O_Send "c" $ O_Recv True $ O_Eps True)
+
+ it "describes the second branch" $
+ run (inferIdentity prog_branching) (S_Off2 $ S_Off1 $ S_Send S_Eps) `shouldBe` (O_Off2 $ O_Off1 $ O_Send True $ O_Eps ())
+
+ it "Recurses until a 10 is given" $
+ run (inferIdentity prog_recursion) (S_Rec $ S_Recv 7 $ S_Sel2 $ S_Sel1 $ S_Var $ S_Recv 10 $ S_Sel1 $ S_Weaken $ S_Eps) `shouldBe`
+ (O_Rec $ O_Recv 7 $ O_Sel2 $ O_Sel1 $ O_Var $ O_Recv 10 $ O_Sel1 $ O_Weaken $ O_Eps 10)
+
+ describe "runSingleM" $ do
+ it "can be used to print something to console" $ do
+ s <- runSingleM (client ["test.txt", "doesnotexist.txt"])
+ (S_Rec $ S_Sel1 $ S_Send $ S_Recv (Right "hello") $ S_Var $
+ S_Sel1 $ S_Send $ S_Recv (Left "File does not exist") $ S_Var $
+ S_Sel2 $ S_Sel1 $ S_Weaken $ S_Eps)
+ s `shouldBe` ["hello"]
+
+ it "can do any IO action (like readFile)" $ do
+ let io = runSingleM server
+ (S_Rec $ S_Off1 $ S_Recv "hello.txt" $ S_Send $ S_Var $
+ S_Off1 $ S_Recv "doesnotexist.txt" $ S_Send $ S_Var $
+ S_Off2 $ S_Off1 $ S_Weaken $ S_Eps)
+ io `shouldThrow` anyException
+
+ describe "runAllM" $ do
+ it "returns more than one result" $ do
+ s <- runAllM (client ["text.txt", "doesnotexist.txt"])
+ (S_Rec $ S_Sel1 $ S_Send $ S_Recv (Right "hello") $ S_Var $
+ S_Sel1 $ S_Send $ S_Recv (Right "text") $ S_Var $
+ S_Sel2 $ S_Sel1 $ S_Weaken $ S_Eps)
+ s `shouldBe` [["text", "hello"]]
+
+ describe "runM" $ do
+ it "Also describes Lifts" $ do
+ s <- runM (client ["text.txt", "doesnotexist.txt"])
+ (S_Rec $ S_Sel1 $ S_Send $ S_Recv (Right "hello") $ S_Var $
+ S_Sel1 $ S_Send $ S_Recv (Left "File does not exist") $ S_Var $
+ S_Sel2 $ S_Sel1 $ S_Weaken $ S_Eps)
+ s `shouldBe` (O_Rec $ O_Sel1 $ O_Send "text.txt" $ O_Recv (Right "hello") $ O_Var $
+ O_Sel1 $ O_Send "doesnotexist.txt" $ O_Recv (Left "File does not exist") $ O_Lift $ O_Var $
+ O_Sel2 $ O_Sel1 $ O_Weaken $ O_Eps ["hello"])
+
+
+
+
diff --git a/test/Test/Interactive/Main.hs b/test/Test/Interactive/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Interactive/Main.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+import Control.SessionTypes.Interactive
+import qualified Control.SessionTypes.Indexed as I
+import Control.SessionTypes
+import Test.Program.FileServer
+import Control.Monad.Catch
+
+main = putStrLn "Interactive requires manual testing."
+
+test = do
+ -- If entered Right x then result should be
+ -- > [x]
+ -- If entered Left x then result should be
+ -- > x
+ -- > []
+ res1 <- interactive (empty0 I.>> client ["test.txt"])
+ putStrLn $ show res1
+
+ -- There are two possible execution paths to take (disregarding aborting):
+ -- > Recurse
+ -- ?> Press n to continue or q to quit
+ -- n
+ -- ?> (L)eft or (R)ight: L
+ -- ?> Press n to continue or q to quit
+ -- n
+ -- ?> Enter value of type [Char]: "hello"
+ -- ?> Press n to continue or q to quit.
+ -- n
+ -- > Lifted
+ -- ?> Press n to continue or q to quit
+ -- n
+ -- > Lifted
+ -- ?> Press n to continue or q to quit
+ -- n
+ -- *** Exception: hello: openFile: does not exist (No such file or directory)
+ catch (interactiveStep (empty0 I.>> server) >>= putStrLn . show) $ \(e :: SomeException) -> do
+ putStrLn $ show e
+ -- > Recurse
+ -- ?> Press n to continue or q to quit
+ -- n
+ -- ?> (L)eft or (R)right: Right
+ -- ?> Press n to continue or q to quit
+ -- n
+ -- > Weaken
+ -- ?> Press n to continue or q to quit
+ -- n
+ -- > Returned: ()
+ -- Just ()
+ res2 <- interactiveStep (empty0 I.>> server)
+ putStrLn $ show res2
+ -- It is also possible to abort, in which case we expect 'Nothing' to be printed
+ -- > Recurse
+ -- ?> Press n to continue or q to quit
+ -- q
+ -- Nothing
+ res3 <- interactiveStep (empty0 I.>> server)
+ putStrLn $ show res3
diff --git a/test/Test/Normalize/Main.hs b/test/Test/Normalize/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Normalize/Main.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE DataKinds #-}
+import Control.SessionTypes
+import Control.SessionTypes.Debug
+import Control.SessionTypes.Normalize
+
+import Test.Program.Normalizable
+import Test.Hspec
+
+
+main = hspec $ do
+ describe "Normalize" $ do
+ it "rewrites a left nested offering to a right nested offering" $ do
+ run (normalize (inferIdentity left_nested_offer)) (S_OffS S_Eps $ S_OffS S_Eps $ S_OffZ S_Eps)
+ `shouldBe` run (inferIdentity right_nested_offer) (S_OffS S_Eps $ S_OffS S_Eps $ S_OffZ S_Eps)
+
+ it "rewrites a center nested offering to a right nested offering" $ do
+ run (normalize $ inferIdentity center_nested_offer) (S_OffS S_Eps $ S_OffS S_Eps $ S_OffZ S_Eps)
+ `shouldBe` run (inferIdentity right_nested_offer) (S_OffS S_Eps $ S_OffS S_Eps $ S_OffZ S_Eps)
+
+ it "rewrites a left nested selection to a right nested selection" $ do
+ run (normalize (inferIdentity left_nested_select)) (S_Sel2 $ S_Sel2 $ S_Sel1 S_Eps)
+ `shouldBe` run (inferIdentity right_nested_select) (S_Sel2 $ S_Sel2 $ S_Sel1 S_Eps)
+
+ it "rewrites a center nested selection to a right nested selection" $ do
+ run (normalize $ inferIdentity center_nested_select) (S_Sel2 $ S_Sel2 $ S_Sel1 S_Eps)
+ `shouldBe` run (inferIdentity right_nested_select) (S_Sel2 $ S_Sel2 $ S_Sel1 S_Eps)
+
+ it "eliminates unused R's and Wk's" $ do
+ [run (normalize $ inferIdentity extra_r_and_wk_after) (S_Rec $ S_Sel1 $ S_Var $ S_Sel2 $ S_Sel1 $ S_Weaken S_Eps),
+ run (normalize $ inferIdentity extra_r_and_wk_before) (S_Rec $ S_Sel1 $ S_Var $ S_Sel2 $ S_Sel1 $ S_Weaken S_Eps)]
+ `shouldMatchList`
+ [run (inferIdentity simple_recursion) (S_Rec $ S_Sel1 $ S_Var $ S_Sel2 $ S_Sel1 $ S_Weaken S_Eps),
+ run (inferIdentity simple_recursion) (S_Rec $ S_Sel1 $ S_Var $ S_Sel2 $ S_Sel1 $ S_Weaken S_Eps)]
+
+test = run (normalize (inferIdentity extra_r_and_wk_after)) (S_Rec $ S_Sel1 $ S_Var $ S_Sel2 $ S_Sel1 $ S_Weaken S_Eps)
diff --git a/test/Test/Program/FileServer.hs b/test/Test/Program/FileServer.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Program/FileServer.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module Test.Program.FileServer where
+
+import Control.SessionTypes
+import Control.SessionTypes.Indexed
+import Control.SessionTypes.Debug
+
+import System.Directory
+
+client :: (IxMonadIO m, MonadSession m) => [String] -> m ('Cap ctx (R (Sel '[String :!> Either String String :?> V, Wk Eps]))) ('Cap ctx Eps) [String]
+client fnames = recurse $ client' fnames []
+ where
+ client' [] contents = selN2 >> weaken0 >> eps contents
+ client' (fname:fnames) contents = do
+ sel1
+ send fname
+ eth <- recv
+
+ case eth of
+ Left s -> liftIO (putStrLn s) >> var (client' fnames contents)
+ Right s -> var $ client' fnames (s : contents)
+
+server :: (IxMonadIO m, MonadSession m) => m ('Cap ctx (R (Off '[String :?> Either String String :!> V, Wk Eps]))) ('Cap ctx Eps) ()
+server = recurseFix $ \f -> do
+ offer (do
+ fname <- recv
+
+ b <- liftIO $ doesPathExist fname
+ if b
+ then send (Left "File does not exist") >> f
+ else liftIO (readFile fname) >>= \s -> send (Right s) >> f) $
+ weaken0 >> eps0
+
+prog :: MonadSession m => m ('Cap ctx (Int :!> Sel '[Eps, Int :!> Eps])) r ()
+prog = undefined
+
+prog2 :: MonadSession m => m ('Cap ctx (Sel '[Eps, String :!> Eps, Int :!> Eps])) ('Cap ctx Eps) ()
+prog2 = sel >> send "c" >>= eps
diff --git a/test/Test/Program/Normalizable.hs b/test/Test/Program/Normalizable.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Program/Normalizable.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module Test.Program.Normalizable where
+
+import Control.SessionTypes
+import Control.SessionTypes.Indexed
+
+left_nested_offer :: MonadSession m => m ('Cap ctx (Off '[Off '[Off '[Eps], Eps], Eps])) ('Cap ctx Eps) ()
+left_nested_offer =
+ offer (
+ offer (
+ offZ eps0
+ ) eps0
+ ) eps0
+
+right_nested_offer :: MonadSession m => m ('Cap ctx (Off '[Eps, Eps, Eps])) ('Cap ctx Eps) ()
+right_nested_offer = eps0 <& eps0 <&> eps0
+
+center_nested_offer :: MonadSession m => m ('Cap ctx (Off '[Eps, Off '[Eps], Eps])) ('Cap ctx Eps) ()
+center_nested_offer =
+ eps0
+ <& offZ eps0
+ <&> eps0
+
+
+left_nested_select :: MonadSession m => m ('Cap ctx (Sel '[Sel '[Sel '[Eps], Eps], Eps])) ('Cap ctx Eps) ()
+left_nested_select = sel2 >> sel1 >> eps0
+
+right_nested_select :: MonadSession m => m ('Cap ctx (Sel '[Eps, Eps, Eps])) ('Cap ctx Eps) ()
+right_nested_select = selN3 >> eps0
+
+center_nested_select :: MonadSession m => m ('Cap ctx (Sel '[Eps, Sel '[Eps], Eps])) ('Cap ctx Eps) ()
+center_nested_select = selN3 >> eps0
+
+extra_r_and_wk_after :: MonadSession m => m ('Cap ctx (R (R (Sel '[Wk V, Wk (Wk Eps)])))) ('Cap ctx Eps) ()
+extra_r_and_wk_after = recurse $ go 1
+ where
+ go 0 = recurseFix $ \_ -> sel2 >> sel1 >> weaken0 >> weaken0 >> eps0
+ go n = recurseFix $ \_ -> do
+ sel1
+ weaken0
+ var (go $ n - 1)
+
+extra_r_and_wk_before :: MonadSession m => m ('Cap ctx (R (R (Sel '[V, Wk (Wk Eps)])))) ('Cap ctx Eps) ()
+extra_r_and_wk_before = recurseFix $ \_ -> recurse $ go 1
+ where
+ go 0 = sel2 >> sel1 >> weaken0 >> weaken0 >> eps0
+ go n = do
+ sel1
+ var (go $ n - 1)
+
+simple_recursion :: MonadSession m => m ('Cap ctx (R (Sel '[V, Wk Eps]))) ('Cap ctx Eps) ()
+simple_recursion = recurse $ go 1
+ where
+ go 0 = selN2 >> weaken0 >> eps0
+ go n = sel1 >> var (go $ n - 1)
diff --git a/test/Test/Program/Simple.hs b/test/Test/Program/Simple.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Program/Simple.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module Test.Program.Simple where
+
+import Control.SessionTypes
+import Control.SessionTypes.Indexed
+
+prog_sendRecv :: MonadSession m => m ('Cap ctx (String :!> Bool :?> Eps)) ('Cap ctx Eps) Bool
+prog_sendRecv = do
+ send "c"
+ x <- recv
+ eps x
+
+prog_sendRecv_dual :: MonadSession m => m ('Cap ctx (String :?> Bool :!> Eps)) ('Cap ctx Eps) String
+prog_sendRecv_dual = do
+ x <- recv
+ send True
+ eps x
+
+prog_branching :: MonadSession m => m ('Cap ctx (Off '[String :!> Eps, Bool :!> Eps, Int :!> Eps])) ('Cap ctx Eps) ()
+prog_branching = do
+ send "c" <& send True <&> send 1
+ eps ()
+
+
+prog_branching_dual :: MonadSession m => m ('Cap ctx (Sel '[String :?> Eps, Bool :?> Eps, Int :?> Eps])) ('Cap ctx Eps) String
+prog_branching_dual = do
+ sel1
+ x <- recv
+ eps x
+
+prog_recursion :: MonadSession m => m ('Cap ctx (R (Int :?> Sel '[Wk Eps, V]))) ('Cap ctx Eps) Int
+prog_recursion = recurseFix $ \f -> do
+ x <- recv
+
+ if x < 10
+ then selN2 >> f
+ else sel1 >> weaken0 >> eps x
+
+prog_recursion_dual :: MonadSession m => m ('Cap ctx (R (Int :!> Off '[Wk Eps, V]))) ('Cap ctx Eps) Int
+prog_recursion_dual = recurse $ go 0
+ where
+ go n = do
+ send n
+ (weaken0 >> eps n) <&> (var $ go (n + 1))
diff --git a/test/Test/Visualize/Main.hs b/test/Test/Visualize/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Visualize/Main.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+
+import Control.SessionTypes
+import Control.SessionTypes.Visualize
+import Data.Proxy (Proxy (..))
+
+
+-- This test requires visual verification.
+-- Run the following to generate a diagram:
+-- > stack build
+-- > stack exec test-visualizer -- -o output.svg -w 600 -h 600
+-- Adjust the height and width if necessary
+main = visualizeP p
+
+p :: Proxy (R ( Int :!> Sel '[ Bool :?> Off [Wk Eps, V], R (Sel '[Char :!> V, Wk V])]))
+p = Proxy