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