packages feed

lol-typing (empty) → 1.20160822

raw patch · 49 files changed

+7156/−0 lines, 49 filesdep +basedep +containersdep +directorybuild-type:Customsetup-changed

Dependencies added: base, containers, directory, filepath, ghc-prim, lol-calculus, lol-typing, monad-classes, parsec, tasty, tasty-hunit, text, text-format, transformers, uuagc, uuagc-cabal

Files

+ COPYING 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:++    <program>  Copyright (C) <year>  <name of author>+    This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.+    This is free software, and you are welcome to redistribute it+    under certain conditions; type `show c' for details.++The hypothetical commands `show w' and `show c' should show the appropriate+parts of the General Public License.  Of course, your program's commands+might be different; for a GUI interface, you would use an "about box".++  You should also get your employer (if you work as a programmer) or school,+if any, to sign a "copyright disclaimer" for the program, if necessary.+For more information on this, and how to apply and follow the GNU GPL, see+<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>.
+ Language/LOL/Typing.hs view
@@ -0,0 +1,29 @@+-- | Type inferencer for LOL (λω language).+--+-- __Ressources:__+--+-- * /Top Quality Type Error Messages/, Bastiaan Heeren, 2005,+-- http://www.open.ou.nl/bhr/TopQuality.pdf+--+-- * /Interpreting types as abstract values: a tutorial on Hindley-Milner type inference/,+-- Oleg Kiselyov, Chung-chieh Shan, 2008,+-- http://okmij.org/ftp/Haskell/AlgorithmsH.html#teval+--+-- * /Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism/,+-- Gergő Érdi, 2011,+-- https://gergo.erdi.hu/projects/tandoori/Tandoori-Compositional-Typeclass.pdf+--+-- All submodules, in a topological order.+module    Language.LOL.Typing+ ( module Language.LOL.Typing.Type+ , module Language.LOL.Typing.Solver+ , module Language.LOL.Typing.Constraint+ , module Language.LOL.Typing.Collect+ , module Language.LOL.Typing.Expr+ ) where++import Language.LOL.Typing.Type+import Language.LOL.Typing.Solver+import Language.LOL.Typing.Constraint+import Language.LOL.Typing.Collect+import Language.LOL.Typing.Expr
+ Language/LOL/Typing/Collect.hs view
@@ -0,0 +1,6 @@+-- | All submodules, in a topological order.+module Language.LOL.Typing.Collect+ ( module Language.LOL.Typing.Collect.Constraint+ ) where++import Language.LOL.Typing.Collect.Constraint
+ Language/LOL/Typing/Collect/Constraint.hs view
@@ -0,0 +1,174 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Collect.Constraint where++-- vim: ft=haskell+-- import Data.Bool+-- import Data.Defaults (Defaults(..))+import Data.Either (Either(..))+import Data.Eq (Eq(..))+import Data.Function (($), (.))+import Data.Functor ((<$>))+import qualified Data.List as List+import qualified Data.Foldable as Foldable+import Data.Maybe (Maybe(..))+import Data.Monoid (Monoid(..), (<>))+import Data.Text (Text)+import Data.Text.Buildable (Buildable(..))+import Data.Tuple (fst, snd)+import Text.Show (Show(..))+import Data.Sequence (Seq)+import qualified Data.Sequence as Seq++import Language.LOL.Typing.Type+import Language.LOL.Typing.Expr+import Language.LOL.Typing.Solver+import Language.LOL.Typing.Constraint+import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build++-- * Type 'Collect_Context'++-- | A 'Polytyref' substitution.+type Collect_Context = [(Name, Polytyref)]++-- * Type 'Collect_Constraint'++type Collect_Constraint+ =   Constraint_Either+     Constraint_Monotype+     Constraint_Polytype+     Collect_Infos++-- | Build a 'Constraint_Monotype_Unification' lifted into 'Collect_Constraint'.+unifies_with+ :: (Monotypeable x, Monotypeable y)+ => x -> y+ -> Collect_Info_Grammar -> Collect_Constraint+unifies_with x y info =+	Constraint_Either $ Left $+	Constraint_Monotype_Unification (monotype x) (monotype y) $+	Collect_Infos [Collect_Info_Grammar info]++-- | Build a 'Constraint_Polytype_instantiates_to_Monotype' lifted into 'Collect_Constraint'.+instantiates_to+ :: (Polytyrefable polyty, Monotypeable monoty)+ => polyty -> monoty+ -> Collect_Info_Grammar -> Collect_Constraint+instantiates_to p m info =+	Constraint_Either $ Right $+	Constraint_Polytype_instantiates_to_Monotype (polytyref p) (monotype m) $+	Collect_Infos [Collect_Info_Grammar info]++-- | Build a 'Constraint_Polytype_generalizes_from_Monotype' lifted into 'Collect_Constraint'.+generalizes_from+ :: Monotypeable monoty+ => Polyvar -> monoty -> Collect_Context+ -> Collect_Info_Grammar -> Collect_Constraint+generalizes_from p m ctx info =+	Constraint_Either $ Right $+	Constraint_Polytype_generalizes_from_Monotype+	 p (context_rigtypes ctx, monotype m) $+	Collect_Infos [Collect_Info_Grammar info]++-- | Build a 'Constraint_Polytype_generalized_by_Monotype' lifted into 'Collect_Constraint'.+generalized_by+ :: (Polytyrefable polyty, Monotypeable monoty)+ => polyty -> monoty -> Collect_Context+ -> Collect_Info_Grammar -> Collect_Constraint+generalized_by p m ctx info =+	Constraint_Either $ Right $+	Constraint_Polytype_generalized_by_Monotype+	 (context_rigtypes ctx, polytyref p) (monotype m) $+	Collect_Infos [Collect_Info_Grammar info]++-- * Type 'Collect_Info'++data Collect_Info+ =   Collect_Info_Solver  (Solver_Info Collect_Infos)+ |   Collect_Info_Grammar Collect_Info_Grammar+ deriving (Eq, Show)+newtype Collect_Infos+ =      Collect_Infos [Collect_Info]+ deriving (Eq, Show)++instance Infoable Info_Monotype Collect_Infos where+	info_insert i (Collect_Infos is) =+		Collect_Infos $+		( Collect_Info_Solver $ Solver_Info_Monotype i+		) : is+instance Infoable Info_Polytype Collect_Infos where+	info_insert i (Collect_Infos is) =+		Collect_Infos $+		( Collect_Info_Solver $ Solver_Info_Polytype i+		) : is+instance Infoable (Info_Class Collect_Infos) Collect_Infos where+	info_insert i (Collect_Infos is) =+		Collect_Infos $+		( Collect_Info_Solver $ Solver_Info_Class i+		) : is++instance Buildable Collect_Infos where+	build (Collect_Infos is) = Build.list is+instance Buildable Collect_Info where+	build x =+		case x of+		 Collect_Info_Solver  i -> build i+		 Collect_Info_Grammar i -> build i++-- ** Type 'Collect_Info_Grammar'++data Collect_Info_Grammar+ =   Collect_Info_Grammar_Expr Text+ deriving (Eq, Show)+instance Buildable Collect_Info_Grammar where+	build x =+		case x of+		 Collect_Info_Grammar_Expr t -> build t++-- * Type 'Collect_Error'++data Collect_Error info err+ =   Collect_Error_Solver  [(info, err)]+ |   Collect_Error_Grammar [Collect_Error_Grammar]+ deriving (Eq, Show)++-- ** Type 'Collect_Error_Grammar'++data Collect_Error_Grammar+ =   Collect_Error_Grammar_Variable_not_in_scope Text+ deriving (Eq, Show)++context_insert :: Polytyrefable a => Name -> a -> Collect_Context -> Collect_Context+context_insert i p = ((i, polytyref p) :)++context_lookup :: Name -> Collect_Context -> Maybe Polytyref+context_lookup = List.lookup++context_rigtypes :: Collect_Context -> [Rigtype]+context_rigtypes ctx = Monotype_Var <$> subvars (snd <$> ctx)++hussel :: Seq Collect_Constraint -> Seq Collect_Constraint+hussel = (\(as, bs) -> (snd <$> bs) <> as) . go mempty+	where+	go :: Seq Polyvar -> Seq Collect_Constraint+	 -> (Seq Collect_Constraint, Seq (Polyvar, Collect_Constraint))+	go polyvars cs =+		case Seq.viewl cs of+		 Seq.EmptyL -> mempty+		 (c@(Constraint_Either e) Seq.:< rest) ->+			case e of+			 Right (Constraint_Polytype_instantiates_to_Monotype (Polytyref_Var var) _ _) ->+				let (new, gs)  = go (var Seq.<| polyvars) rest in+				let (gs1, gs2) = Seq.partition ((`Foldable.elem` polyvars) . fst) gs in+				((snd <$> gs2)<>Seq.singleton c<>new, gs1)+			 Right (Constraint_Polytype_generalizes_from_Monotype var _ _)+				| var `Foldable.elem` polyvars ->+				let (new, gs) = go polyvars rest in+				(new, (var,c) Seq.<| gs)+			 _ ->+				let (new, gs)  = go polyvars rest in+				let (gs1, gs2) = Seq.partition ((`Foldable.elem` polyvars) . fst) gs in+				((snd <$> gs2)<>Seq.singleton c<>new, gs1)
+ Language/LOL/Typing/Collect/Grammar.ag view
@@ -0,0 +1,129 @@+-- vim: syntax=haskell+optpragmas {+{-# LANGUAGE OverloadedStrings #-}+}+module {Language.LOL.Typing.Collect.Grammar} {} {+import Data.Function (($))+import Data.Maybe (Maybe(..), maybe)+import Data.Monoid (Monoid(..), (<>))+import Data.Sequence (Seq, (|>), (<|), (><))+import qualified Data.Sequence as Seq+import Prelude (Num(..))++import Language.LOL.Typing.Collect.Constraint+import Language.LOL.Typing.Type+import Language.LOL.Typing.Expr+import Language.LOL.Typing.Lib.Data.Default (Default(..))+import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build+}++include "../Expr/Grammar.ag"++attr Expr+	-- | top-down+	inh polytys :: Collect_Context+	-- | bottom-up+	syn monovar :: Monovar+	syn constraints :: {Seq Collect_Constraint}+	syn errors use {<>} {[]} :: {[Collect_Error_Grammar]}+	-- | both+	chn freshvar :: Freshvar+attr Decl+	-- | top-down+	inh polytys :: Collect_Context+	-- | bottom-up+	syn polyvar :: Polyvar+	syn constraints :: {Seq Collect_Constraint}+	syn errors use {<>} {[]} :: {[Collect_Error_Grammar]}+	-- | both+	chn freshvar :: Freshvar++sem Expr+ | Annot+	lhs.constraints = @body.constraints |>+	                  ((@sig `generalized_by` @body.monovar) @lhs.polytys $+	                   Collect_Info_Grammar_Expr $ "Annot " <> Build.text+	                    (def::Quantification_Build_Options, @sig))+ | Var+	lhs.monovar     = @loc.monovar+	loc.monovar     = @lhs.freshvar+	lhs.freshvar    = @lhs.freshvar + 1+	loc.polyty      = context_lookup @name @lhs.polytys+	-- loc.term        = TeTy_Var_Unknown @name @loc.monovar+	lhs.constraints = case @loc.polyty of+	                   Nothing -> mempty+	                   Just p -> Seq.singleton $+	                              p `instantiates_to` @loc.monovar $+	                               Collect_Info_Grammar_Expr $ "Var " <> @name+	lhs.errors = case @loc.polyty of+	              Nothing -> [Collect_Error_Grammar_Variable_not_in_scope @name]+	              Just _  -> []+ | Abst+	lhs.monovar     = @loc.monovar+	loc.monovar     = @lhs.freshvar+	loc.arg_monovar = @lhs.freshvar + 1+	body.freshvar   = @lhs.freshvar + 2+	body.polytys    = (@name `context_insert` Monotype_Var @loc.arg_monovar) @lhs.polytys+	lhs.constraints = (@loc.monovar `unifies_with`+	                    (Monotype_Var @loc.arg_monovar .->. Monotype_Var @body.monovar) $+	                    Collect_Info_Grammar_Expr $ "Abst(body) " <> @name) <|+	                  maybe mempty (\sig -> Seq.singleton ((sig `unifies_with` @loc.arg_monovar) $+	                   Collect_Info_Grammar_Expr $ "Abst(sig) " <> Build.text sig)) @sig ><+	                  @body.constraints+ | App+	lhs.monovar     = @loc.monovar+	loc.monovar     = @lhs.freshvar+	abst.freshvar   = @lhs.freshvar + 1+	abst.polytys    = @lhs.polytys+	arg.polytys     = @lhs.polytys+	lhs.constraints = @abst.constraints <>+	                  @arg.constraints |>+	                  (@abst.monovar `unifies_with`+	                    (Monotype_Var @arg.monovar .->. Monotype_Var @loc.monovar) $+	                    Collect_Info_Grammar_Expr $ "App")+ | Let+	lhs.monovar      = @loc.monovar+	loc.monovar      = @lhs.freshvar+	loc.decl_polyvar = @lhs.freshvar + 1+	decl.freshvar    = @lhs.freshvar + 2+	decl.polytys     = @lhs.polytys+	body.polytys     = (@name `context_insert` @loc.decl_polyvar) @lhs.polytys+	lhs.constraints  = let info x = Collect_Info_Grammar_Expr $ "Let" <> "(" <> x <> ") " <> @name in+	                   @decl.constraints ><+	                   (@loc.decl_polyvar `generalizes_from` @decl.monovar)+	                    @lhs.polytys (info "decl") <|+	                   maybe mempty (\sig -> Seq.singleton+	                    ((sig `generalized_by` @decl.monovar) @lhs.polytys $+	                    Collect_Info_Grammar_Expr $ "Let(sig) " <>+	                    Build.text (def::Quantification_Build_Options, sig))) @sig ><+	                   (@loc.monovar `unifies_with` @body.monovar) (info "body") <|+	                   @body.constraints+ | Where+	lhs.monovar      = @loc.monovar+	loc.monovar      = @lhs.freshvar+	loc.decl_polyvar = @lhs.freshvar + 1+	body.freshvar    = @lhs.freshvar + 2+	decl.polytys     = @lhs.polytys+	body.polytys     = (@name `context_insert` @loc.decl_polyvar) @lhs.polytys+	lhs.constraints  = let info = Collect_Info_Grammar_Expr $ "Where " <> @name in+	                   @decl.constraints ><+	                   (@loc.decl_polyvar `generalizes_from` @decl.monovar) @lhs.polytys info <|+	                   maybe mempty (\sig -> Seq.singleton ((sig `generalized_by` @decl.monovar) @lhs.polytys $+	                    Collect_Info_Grammar_Expr $ "Where(sig) " <> Build.text+	                     (def::Quantification_Build_Options, sig))) @sig ><+	                   (@loc.monovar `unifies_with` @body.monovar) info <|+	                   @body.constraints++sem Decl+ | Let+	-- loc.monovar      = Monotype_Var @lhs.freshvar+	loc.decl_polyvar = @lhs.freshvar+	decl.freshvar    = @lhs.freshvar + 1+	decl.polytys     = @lhs.polytys+	lhs.polyvar      = @loc.decl_polyvar+	lhs.constraints  = let info x = Collect_Info_Grammar_Expr $ "Let" <> "(" <> x <> ") " <> @name in+	                   @decl.constraints ><+	                   (@loc.decl_polyvar `generalizes_from` @decl.monovar) @lhs.polytys (info "decl") <|+	                   maybe mempty (\sig -> Seq.singleton ((sig `generalized_by` @decl.monovar) @lhs.polytys $+	                    Collect_Info_Grammar_Expr $ "Let(sig) " <> Build.text+	                     (def::Quantification_Build_Options, sig))) @sig
+ Language/LOL/Typing/Constraint.hs view
@@ -0,0 +1,12 @@+-- | All submodules, in a topological order.+module Language.LOL.Typing.Constraint+ ( module Language.LOL.Typing.Constraint.Monotype+ , module Language.LOL.Typing.Constraint.Polytype+ , module Language.LOL.Typing.Constraint.Extra+ , module Language.LOL.Typing.Constraint.Either+ ) where++import Language.LOL.Typing.Constraint.Monotype+import Language.LOL.Typing.Constraint.Polytype+import Language.LOL.Typing.Constraint.Extra+import Language.LOL.Typing.Constraint.Either
+ Language/LOL/Typing/Constraint/Either.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Constraint.Either where++import Data.Either (Either(..), either)+import Data.Function (($), (.))+import Data.Functor (Functor(..))+import Data.Text.Buildable (Buildable(..))+import Text.Show (Show(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Solver++-- ** Type 'Constraint_Either'++newtype Constraint_Either f g info+ =      Constraint_Either (Either (f info) (g info))+ deriving (Show)++instance+ ( Buildable (f info)+ , Buildable (g info)+ ) => Buildable (Constraint_Either f g info) where+	build (Constraint_Either x) = either build build x+instance+ ( Functor f+ , Functor g+ ) => Functor (Constraint_Either f g) where+	fmap f (Constraint_Either x) =+		Constraint_Either $+		either (Left . fmap f) (Right . fmap f) x+instance+ ( Substitutable (f info)+ , Substitutable (g info)+ ) => Substitutable (Constraint_Either f g info) where+	subvars (Constraint_Either x) = either subvars subvars x+	substitute sub (Constraint_Either x) =+		Constraint_Either $+		either+		 (Left  . (sub `substitute`))+		 (Right . (sub `substitute`))+		 x+instance+ ( Solvable (f info) m+ , Solvable (g info) m+ ) => Solvable (Constraint_Either f g info) m where+	constraint_solver (Constraint_Either x) = either constraint_solver constraint_solver x+	constraint_checker (Constraint_Either x) = either constraint_checker constraint_checker x
+ Language/LOL/Typing/Constraint/Extra.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Constraint.Extra where++import Data.Function (($))+import Data.Functor (Functor(..))+import Data.Monoid ((<>))+import Data.Text.Buildable (Buildable(..))+import Text.Show (Show(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Solver++-- * Type 'Constraint_Extra'++data Constraint_Extra info+ =   Constraint_Extra_ToProve Class_Qualifier info+ |   Constraint_Extra_Assume  Class_Qualifier info+ deriving (Show)++instance Functor Constraint_Extra where+	fmap f c =+		case c of+		 Constraint_Extra_ToProve p info -> Constraint_Extra_ToProve p (f info)+		 Constraint_Extra_Assume  p info -> Constraint_Extra_Assume  p (f info)+instance Buildable info => Buildable (Constraint_Extra info) where+	build c =+		case c of+		 Constraint_Extra_ToProve p info ->+			build $ Infoed info $ "Prove (" <> build p <> ")"+		 Constraint_Extra_Assume p info ->+			build $ Infoed info $ "Assume (" <> build p <> ")"+instance Substitutable (Constraint_Extra info) where+	subvars c =+		case c of+		 Constraint_Extra_ToProve p _ -> subvars p+		 Constraint_Extra_Assume  p _ -> subvars p+	sub `substitute` c =+		case c of+		 Constraint_Extra_ToProve p info -> Constraint_Extra_ToProve (sub `substitute` p) info+		 Constraint_Extra_Assume  p info -> Constraint_Extra_Assume  (sub `substitute` p) info+instance+ ( info ~ Info m+ , Show info+ , Buildable info+ , Solver_Class m+ ) => Solvable (Constraint_Extra info) m where+	constraint_solver c =+		case c of+		 Constraint_Extra_ToProve p info -> class_qualifier_toprove info p+		 Constraint_Extra_Assume  p info -> class_qualifier_assume  info p
+ Language/LOL/Typing/Constraint/Monotype.hs view
@@ -0,0 +1,64 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+-- | Constraints for /monomorphic types/.+module Language.LOL.Typing.Constraint.Monotype where++import Control.Applicative (Applicative(..))+import Data.Eq (Eq(..))+import Data.Function (on)+import Data.Functor (Functor(..), (<$>))+import qualified Data.List as List+import Data.Monoid ((<>))+import Data.Text.Buildable (Buildable(..))+import Text.Show (Show(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Solver++-- * Type 'Constraint_Monotype_Unification'++-- | /monotype constraint/.+data Constraint_Monotype info+ =   Constraint_Monotype_Unification Monotype Monotype info+     -- ^ A /monotype unification constraint/.+ deriving (Show)++-- | Infix alias for 'Constraint_Monotype_Unification'.+(.==.) :: Monotype -> Monotype -> info -> Constraint_Monotype info+(.==.) = Constraint_Monotype_Unification++instance Buildable info => Buildable (Constraint_Monotype info) where+	build (Constraint_Monotype_Unification t1 t2 info) =+		build t1 <> " == " <> build t2 <> build_info+		where+		build_info = " {- " <> build info <> " -}"+instance Functor Constraint_Monotype where+	fmap f (Constraint_Monotype_Unification t1 t2 info) =+		Constraint_Monotype_Unification t1 t2 (f info)+instance Substitutable (Constraint_Monotype info) where+	subvars (Constraint_Monotype_Unification t1 t2 _) = subvars t1 `List.union` subvars t2+	sub `substitute` (Constraint_Monotype_Unification t1 t2 info) =+		Constraint_Monotype_Unification (sub `substitute` t1) (sub `substitute` t2) info+instance+ ( info ~ Info m+ , Show info+ , Buildable info+ , Solver_Constraint m+ , Solver_Monotype m+ , Solver_Polytype m+ ) => Solvable (Constraint_Monotype info) m where+	constraint_solver (Constraint_Monotype_Unification t1 t2 info) =+		monotype_unify+		 (info_insert (Info_Monotype_Unification t1 t2) info)+		 t1 t2+	constraint_checker (Constraint_Monotype_Unification t1 t2 _) = do+		Synotype_Substitution{synotypes} <- synotype_substitution+		((==) `on` synexpand synotypes)+		 <$> monotype_substitute t1+		 <*> monotype_substitute t2
+ Language/LOL/Typing/Constraint/Polytype.hs view
@@ -0,0 +1,229 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+-- | Constraints for /parametric polymorphism/ and /type class polymorphism/.+module Language.LOL.Typing.Constraint.Polytype where++import Control.Applicative (Applicative(..))+import Control.Monad (forM_, join)+import Data.Function (($), (.))+import Data.Functor (Functor(..), (<$>))+import qualified Data.List as List+import Data.Monoid ((<>))+import qualified Data.Sequence as Seq+import Data.Text.Buildable (Buildable(..))+import qualified Data.Text.Lazy.Builder as Builder+import Text.Show (Show(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Solver+import Language.LOL.Typing.Constraint.Monotype+import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build++-- * Type 'Constraint_Polytype'++-- | The /polymorphism 'Constraint's/.+data Constraint_Polytype info+ =   Constraint_Polytype_generalizes_from_Monotype Polyvar ([Rigtype], Monotype) info+  -- ^ A /polytype generalization constraint/:+  -- assign a 'Polyvar' to the 'Polytype'+  -- obtained by generalizing a 'Monotype' to a 'Forall' 'Quantification'+  -- over all its 'subvars' except those of the given 'Rigtype's.+  -- These excluded 'Rigtype's are used to avoid generalizing+  -- 'Monovar's appearing in the /typing context/,+  -- since they appear in 'Constraint's that /need/ to be satisfied.+  --+  -- NOTE: a 'Constraint_Polytype_generalizes_from_Monotype' requires+  -- that the 'Polytype'’s 'quantifiers' have at least the 'qualifiers'+  -- of the 'Monotype'’s 'subvars' they generalize. See 'class_polytype_forall'.+ |   Constraint_Polytype_instantiates_to_Monotype Polytyref Monotype info+  -- ^ A /polytype explicit instantiation constraint/+  -- (/explicit/ meaning known when collecting the 'Constraint's):+  -- restricts a 'Monotype' to be /less general/+  -- than a 'Polytype' (from given 'Polytyref')+  -- i.e. to be an /instance/ of it.+  --+  -- NOTE: instantiating a 'Polytyref'+  -- implies that the instantiated 'qualifiers'+  -- are entailed by the 'qualifiers' in the solving 'Substitution'.+ |   Constraint_Polytype_implicit_instantiates_to_Monotype ([Rigtype], Monotype) Monotype info+  -- ^ A /polytype implicit instantiation constraint/:+  -- restrict a 'Monotype' to be an /instance/ of the 'Polytype'+  -- obtained by 'generalize'-ing another 'Monotype'+  -- over all its 'subvars' except those of the given 'Rigtype's.+  --+  -- NOTE: the idea is that such a 'Constraint'+  -- can be solved only if no more deductions+  -- can be found in the remaining 'Constraint's ('state_constraint_constraints')+  -- about the 'quantifiers' of the 'Polytype' returned by 'class_polytype_forall'.+ |   Constraint_Polytype_generalized_by_Monotype ([Rigtype], Polytyref) Monotype info+  -- ^ A /polytype rigidification constraint/:+  -- restricts a 'Monotype' to be /more general/+  -- than a 'Polytype' (from given 'Polytyref').+  --+  -- NOTE: determining this requires to know which 'Monovar's in the 'Monotype'+  -- are 'Polyvar's, and which are 'Monovar's, hence+  -- a set of 'Rigtype's is attached.+  --+  -- NOTE: this 'Constraint' becomes important+  -- to handle /expression/ with /type signature/,+  -- because then the inferred 'Monotype' of the /expression/+  -- should be /more general/ than the /type signature/.+ deriving (Show)++-- | Infix alias for 'Constraint_Polytype_generalized_by_Monotype'.+(.::.) :: Monotype -> Polytyref -> [Rigtype] -> info -> Constraint_Polytype info+(.::.) monoty polyty rigtys = Constraint_Polytype_generalized_by_Monotype (rigtys, polyty) monoty++instance Functor Constraint_Polytype where+	fmap f c =+		case c of+		 Constraint_Polytype_generalizes_from_Monotype polyty monos info ->+			Constraint_Polytype_generalizes_from_Monotype polyty monos (f info)+		 Constraint_Polytype_instantiates_to_Monotype polyref monoty info ->+			Constraint_Polytype_instantiates_to_Monotype polyref monoty (f info)+		 Constraint_Polytype_implicit_instantiates_to_Monotype (monotys, t2) t1 info ->+			Constraint_Polytype_implicit_instantiates_to_Monotype (monotys, t2) t1 (f info)+		 Constraint_Polytype_generalized_by_Monotype ty pair info ->+			Constraint_Polytype_generalized_by_Monotype ty pair (f info)+instance Buildable info => Buildable (Constraint_Polytype info) where+	build c =+		case c of+		 Constraint_Polytype_generalizes_from_Monotype polyty (rigtys, monoty) info ->+			"p" <> build polyty+			 <> " := Generalize"+			 <> Build.tuple [build_rigvars rigtys, build monoty]+			 <> build_info info+		 Constraint_Polytype_instantiates_to_Monotype polyref monoty info ->+			build monoty+			 <> " := Instantiate"+			 <> Build.tuple [build polyref]+			 <> build_info info+		 Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, polyty) monoty info ->+			build monoty+			 <> " := Implicit"+			 <> Build.tuple [build_rigvars rigtys, build polyty]+			 <> build_info info+		 Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty info ->+			build monoty+			 <> " := Rigidify"+			 <> Build.tuple [build_rigvars rigtys, build polyref]+			 <> build_info info+		where+		build_info info = " {- " <> build info <> " -}"+		build_rigvars :: [Monotype] -> Builder.Builder+		build_rigvars = Build.list . (Monotype_Var <$>) . subvars++instance Substitutable (Constraint_Polytype info) where+	subvars c =+		case c of+		 Constraint_Polytype_generalizes_from_Monotype _ (rigtys, monoty) _ ->+			subvars rigtys `List.union` subvars monoty+		 Constraint_Polytype_instantiates_to_Monotype polyref monoty _ ->+			subvars monoty `List.union` subvars polyref+		 Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, t2) t1 _ ->+			subvars t1 `List.union` subvars rigtys `List.union` subvars t2+		 Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty _ ->+			subvars monoty `List.union` subvars rigtys `List.union` subvars polyref+	sub `substitute` c =+		case c of+		 Constraint_Polytype_generalizes_from_Monotype sv (rigtys, monoty) info ->+			Constraint_Polytype_generalizes_from_Monotype sv+			 ( sub `substitute` rigtys+			 , sub `substitute` monoty )+			 info+		 Constraint_Polytype_instantiates_to_Monotype polyref monoty info ->+			Constraint_Polytype_instantiates_to_Monotype+			 (sub `substitute` polyref)+			 (sub `substitute` monoty)+			 info+		 Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, t2) t1 info ->+			Constraint_Polytype_implicit_instantiates_to_Monotype+			 ( sub `substitute` rigtys+			 , sub `substitute` t2 )+			 (sub `substitute` t1)+			 info+		 Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty info ->+			Constraint_Polytype_generalized_by_Monotype+			 ( sub `substitute` rigtys+			 , sub `substitute` polyref )+			 (sub `substitute` monoty)+			 info+instance+ ( info ~ Info m+ , Show info+ , Buildable info+ , Solver_Constraint m+ , Solver_Monotype m+ , Solver_Polytype m+ , Solver_Class m+ ) => Solvable (Constraint_Polytype info) m where+	constraint_solver con =+		case con of+		 Constraint_Polytype_generalizes_from_Monotype polyvar (rigtys, monoty) _ -> do+			-- NOTE: Here 'monotype_substitution'+			-- can be in an inconsistent state,+			-- however 'class_reduction' makes it consistent+			-- (by calling: 'monotype_substitution_consistentify'),+			-- it then applies it to the 'class_qualifiers'+			-- (by calling: 'class_qualifiers_map' 'monotype_substitute').+			class_reduction+			-- NOTE: Apply 'monotype_substitution'+			-- to the 'Monotype's which must remain so,+			-- and to the 'Monotype' before generalizing it.+			polyty <- join $ class_polytype_forall+			 <$> monotype_substitute rigtys+			 <*> monotype_substitute monoty+			-- NOTE: The 'Polyvar' given by the 'Constraint'+			-- is then associated to the just computed 'Polytype',+			-- within 'state_polytype_substitution'.+			polytype_insert polyvar polyty+		+		 Constraint_Polytype_instantiates_to_Monotype polyref monoty info -> do+			polyty <- polytype_lookup polyref+			 -- NOTE: get a (known) 'Polytype' from the given 'Polytyref'.+			Qualification+			 { qualifiers+			 , qualified=inst_monoty+			 } <- polytype_instantiate monoty polyty+			 -- NOTE: instantiate the 'Polytype' into a 'Monotype'+			 -- using the 'polytype_freshvar'.+			let info' = info_insert (Info_Polytype_Instantiated polyty) info+			forM_ qualifiers $+			 -- NOTE: all instantiated 'qualifiers' have to be proven+				class_qualifier_toprove $+				info_insert (Info_Monotype_Unification monoty inst_monoty) info'+			constraint_push $+				constraint (monoty .==. inst_monoty $ info')+			 -- NOTE: add a 'Constraint_Monotype_Unification'+			 -- between the given 'Monotype' and the instantiated 'Polytype',+			 -- using the 'info' to store the original 'Polytype'.+		+		 Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, t2) t1 info -> do+			polyvar <- polytype_freshvar+			constraint_push_many $ constraints $ Seq.fromList+			 [ Constraint_Polytype_generalizes_from_Monotype polyvar (rigtys, t2) info+			 , Constraint_Polytype_instantiates_to_Monotype (Polytyref_Var polyvar) t1 info+			 ]+		+		 Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty info -> do+			polyty <- polytype_lookup polyref+			let info' = info_insert (Info_Polytype_Rigidified rigtys polyty) info+			Qualification+			 { qualifiers+			 , qualified=rigid_polyty+			 } <- polytype_rigvarify info rigtys polyty+			forM_ qualifiers $+			 -- NOTE: all rigidified 'qualifiers' are assumed.+				class_qualifier_assume $+				info_insert (Info_Monotype_Unification rigid_polyty monoty) info'+			 -- FIXME: Top has (monoty, monoty), but (rigid_polyty, monoty)+			 -- seems to be the correct thing to do.+			constraint_push $+				constraint (monoty .==. rigid_polyty $ info')
+ Language/LOL/Typing/Expr.hs view
@@ -0,0 +1,18 @@+-- | All submodules, in a topological order.+--+-- WARNING: this is a rough draft to experiment+-- with the generation of explicitely typed terms+-- from implicitely typed expressions;+-- see @Expr/Test.hs@.+module Language.LOL.Typing.Expr+ ( module Language.LOL.Typing.Expr.Common+ , module Language.LOL.Typing.Expr.Grammar+ , module Language.LOL.Typing.Expr.Utils+ -- , module Language.LOL.Typing.Expr.Write+ ) where++import Language.LOL.Typing.Expr.Calculus ()+import Language.LOL.Typing.Expr.Common+import Language.LOL.Typing.Expr.Grammar+import Language.LOL.Typing.Expr.Utils+import Language.LOL.Typing.Expr.Write ()
+ Language/LOL/Typing/Expr/Calculus.ag view
@@ -0,0 +1,156 @@+-- vim: syntax=haskell+optpragmas {+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TupleSections #-}+{-# OPTIONS_GHC -fno-warn-unused-matches #-}+}+module {Language.LOL.Typing.Expr.Calculus} {} {+import Data.Function (($))+import Data.Eq (Eq(..))+import Data.Maybe (Maybe(..), fromMaybe)+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Prelude (Num(..), error)+import Data.Tuple (fst, snd)+import qualified Data.Foldable as Foldable+++import Language.LOL.Typing.Type+import Language.LOL.Typing.Expr.Common+import Language.LOL.Typing.Expr.Grammar+-- import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build+import qualified Language.LOL.Calculus as Calc+import Data.Monoid ((<>))+import Text.Show (show)+-- import Debug.Trace+}++include "./Grammar.ag"++attr Expr Decl+	-- | top-down+	inh env :: {Calc.Env}+	inh monoconsts :: Monoconsts+	 -- ^ The 'Monoconst's+	 -- bound at the current node.+	inh monotys :: Substitution_Fixpoint+	 -- ^ The inferred 'Monotype's.+	inh polytys :: Polysub+	 -- ^ The inferred 'Polytype's.+	inh quantifiers :: {Map Monovar [Monotype]}+	 -- ^ The 'Monotype's (fully inferred)+	 -- which have been introduced when a 'Polytype'+	 -- has been instanciated to a 'Monovar',+	 -- and thus must be passed to the 'Expr_Var' derived from it.+	inh renames :: {Map Name Name}+	 -- ^ Used to accumulate 'Name's+	 -- bound at the current node+	 -- but conflicting with 'monoconsts_Inh_Expr',+	 -- and thus requiring a rename+	 -- at their corresponding 'Expr_Var' nodes;+	 -- this rename is important because 'quantifiers_Inh_Expr'+	 -- may introduce 'Monoconst's of 'monoconsts_Inh_Expr'.+	+	-- | bottom-up+	syn monovar :: Monovar+	syn term :: {Calc.Term TeTy_Var}+	+	-- | both+	chn freshvar :: Freshvar++sem Expr+ | Annot+ | Var+	lhs.monovar  = @loc.monovar+	loc.monovar  = @lhs.freshvar+	lhs.freshvar = @lhs.freshvar + 1+	loc.name     = Map.findWithDefault @name @name @lhs.renames+	lhs.term     = {-+	               let ty = @lhs.monotys `substitute` Monotype_Var @loc.monovar in+	               let fv = subvars ty in+	               trace ("trace: Var m"<>show @loc.monovar<>+	                " name="<>show @loc.name<>+	                " : "<>Build.string ty<>+	                " ~> "<>show (Build.list <$> Map.lookup @loc.monovar @lhs.quantifiers)) $+	               -}+	               Foldable.foldl+	                (\acc mty -> Calc.TeTy_App acc+	                 (calc_type mty))+	                (Calc.TeTy_Var (TeTy_Var_Name @loc.name))+	                (Map.findWithDefault [] @loc.monovar @lhs.quantifiers)+	               {-case Map.lookup @loc.monovar @lhs.quantifiers of+	                Nothing -> Calc.TeTy_Var (TeTy_Var_Name @name)+	                Just quants ->+	                  Foldable.foldl+	                   (\acc quant -> Calc.TeTy_App acc+	                    (calc_type $ @lhs.monotys `substitute` Monotype_Var quant))+	                   (Calc.TeTy_Var (TeTy_Var_Name @name))+	                   quants-}+ | Abst+	lhs.monovar     = @loc.monovar+	loc.monovar     = @lhs.freshvar+	loc.arg_monovar = @lhs.freshvar + 1+	body.freshvar   = @lhs.freshvar + 2+	loc.consts_name = const_freshify @lhs.monoconsts @name+	body.monoconsts = fst @loc.consts_name+	body.renames    = if @name == snd @loc.consts_name+	                  then @lhs.renames+	                  else Map.insert @name (snd @loc.consts_name) @lhs.renames+	loc.term        = Calc.Term_Abst (Calc.Suggest $ snd @loc.consts_name)+	                   (calc_type $ @lhs.monotys `substitute`+	                                Monotype_Var @loc.arg_monovar) $ -- TODO: cache calc_type+	                   (\v -> case v of+	                    TeTy_Var_Name n | n == snd @loc.consts_name -> Just (Calc.Suggest n)+	                    _ -> Nothing) `Calc.abstract` @body.term+ | App+	lhs.monovar     = @loc.monovar+	loc.monovar     = @lhs.freshvar+	abst.freshvar   = @lhs.freshvar + 1+	lhs.term        = Calc.TeTy_App @abst.term @arg.term+ | Let+	lhs.monovar      = @loc.monovar+	loc.monovar      = @lhs.freshvar+	loc.decl_polyvar = @lhs.freshvar + 1+	decl.freshvar    = @lhs.freshvar + 2+	loc.consts_name  = const_freshify @lhs.monoconsts @name+	body.renames     = if @name == snd @loc.consts_name+	                   then @lhs.renames+	                   else Map.insert @name (snd @loc.consts_name) @lhs.renames+	loc.decl_polyty  = fromMaybe (error $ "Oops, Polytype missing " <> show @loc.decl_polyvar <> " in " <> show @lhs.polytys) $+	                   Map.lookup @loc.decl_polyvar @lhs.polytys+	loc.decl_quants  = quantifiers_freshify @lhs.monoconsts+	                                        (quantifier_hintnames @loc.decl_polyty)+	                                        (quantifiers          @loc.decl_polyty)+	decl.monoconsts  = fst @loc.decl_quants+	body.monoconsts  = fst @loc.consts_name+	lhs.term         = Calc.TeTy_App+	                    (Calc.Term_Abst+	                     (Calc.Suggest $ snd @loc.consts_name)+	                     (Foldable.foldr+	                       (\(quant, qname) ty ->+	                        let nam = Calc.Suggest qname in+	                        Calc.Type_Abst nam+	                         (Calc.Type_Sort Calc.sort_star_mono)+	                         ((\v -> case v of+	                           TeTy_Var_Monovar m | m == quant -> Just nam+	                           _ -> Nothing) `Calc.abstract` ty))+	                       (calc_type (quantified @loc.decl_polyty))+	                       (snd @loc.decl_quants))+	                     ((\v -> case v of+	                      TeTy_Var_Name n | n == snd @loc.consts_name -> Just (Calc.Suggest n)+	                      _ -> Nothing) `Calc.abstract` @body.term))+	                     (Foldable.foldr+	                       (\(quant, qname) te ->+	                        let nam = Calc.Suggest qname in+	                        Calc.Term_Abst nam+	                         (Calc.Type_Sort Calc.sort_star_mono)+	                         ((\v -> case v of+	                           TeTy_Var_Monovar m | m == quant -> Just nam+	                           _ -> Nothing) `Calc.abstract` te))+	                       @decl.term+	                       (snd @loc.decl_quants))+sem Decl+ | Let+	-- loc.monovar      = @lhs.freshvar+	-- loc.decl_polyvar = @lhs.freshvar + 1+	decl.freshvar    = @lhs.freshvar + 1
+ Language/LOL/Typing/Expr/Common.hs view
@@ -0,0 +1,124 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TupleSections #-}+module Language.LOL.Typing.Expr.Common where++import qualified Data.Foldable as Foldable+import Data.Eq (Eq(..))+import Data.Text (Text)+import qualified Data.Text as Text+import Data.Function (const)+import Data.Functor ((<$>))+import Data.Maybe (Maybe(..))+import Data.Text.Buildable (Buildable(..))++import qualified Language.LOL.Calculus as Calc+import Language.LOL.Typing.Type+import Text.Show++type Name = Text++data TeTy_Var+ =   TeTy_Var_Name Calc.Var_Name+ |   TeTy_Var_Monovar Monovar+ deriving (Eq, Show)+instance Buildable TeTy_Var where+	build x =+		case x of+		 TeTy_Var_Name n -> build n+		 TeTy_Var_Monovar v -> build (Monotype_Var v)++class Calc_Type a where+	calc_type :: a -> Calc.Type TeTy_Var+instance Calc_Type Monotype where+	calc_type ty =+		case app_spine_left ty of+		 Monotype_Var v `App_Spine` [] -> Calc.TeTy_Var (TeTy_Var_Monovar v)+		 Monotype_Const c `App_Spine` [] -> Calc.TeTy_Var (TeTy_Var_Name c)+		 Monotype_Const "->" `App_Spine` [t1, t2] ->+			Calc.Type_Abst (Calc.Suggest "")+			 (calc_type t1)+			 (const Nothing `Calc.abstract` calc_type t2)+		 t `App_Spine` tys ->+			Calc.term_apps+			 (calc_type t)+			 (calc_type <$> tys)+calc_of_polytype+ :: Monoconsts+ -> Polytype+ -> (Monoconsts, Calc.Type TeTy_Var)+calc_of_polytype consts_used Quantification+	 { quantifiers+	 , quantifier_hintnames+	 , quantified } =+	Foldable.foldr+	 (\(quant, qname) ty ->+		let nam = Calc.Suggest qname in+		Calc.Type_Abst nam+		 (Calc.Type_Sort Calc.sort_star_mono)+		 ((\x -> case x of+			 TeTy_Var_Monovar v | v == quant-> Just nam+			 _ -> Nothing) `Calc.abstract` ty)+	 ) (calc_type quantified) <$>+	quantifiers_freshify consts_used quantifier_hintnames quantifiers+calc_abst_term_of_polytype+ :: Monoconsts+ -> Polytype+ -> Calc.Term TeTy_Var+ -> (Monoconsts, Calc.Type TeTy_Var)+calc_abst_term_of_polytype consts_used Quantification+	 { quantifiers+	 , quantifier_hintnames } term =+	Foldable.foldr+	 (\(quant, qname) ty ->+		let nam = Calc.Suggest qname in+		Calc.Term_Abst nam+		 (Calc.Type_Sort Calc.sort_star_mono)+		 ((\x -> case x of+			 TeTy_Var_Monovar v | v == quant -> Just nam+			 _ -> Nothing) `Calc.abstract` ty)+	 ) term <$>+	quantifiers_freshify consts_used quantifier_hintnames quantifiers+{-+instance (Show a, Substitutable a, Buildable (Quantification_Build_Options, a), Calc_Type a)+ => Calc_Type ([Monoconst], Forall a) where+	calc_type (consts_used, f@Quantification+	 { quantifiers+	 , quantifier_hintnames+	 , quantified }) =+		let (_consts_used, quants) = quantifiers_freshify consts_used quantifier_hintnames quantifiers in+		let qty = calc_type quantified in+		Foldable.foldr+		 (\(quant, qname) ty ->+			Calc.Type_Abst (Calc.Suggest qname)+			 (Calc.Type_Sort Calc.sort_star_mono)+			 ((\x ->+				case x of+				 TeTy_Var_Name _ -> Nothing+				 TeTy_Var_Monovar v ->+					if v == quant+					then Just (Calc.Suggest qname)+					else Nothing) `Calc.abstract` ty)+		 ) qty $+		trace ("quants: " <> Build.string (Build.list $ (\(x, y) -> Build.tuple [build x, build y]) <$> quants))+		trace ("forall: " <> Build.string (def::Quantification_Build_Options,f))+		trace ("forall: " <> show f)+		trace ("quantified: " <> show quantified)+		quants+-}+instance (Calc_Type a) => Calc_Type (Qualification [Class_Qualifier] a) where+	calc_type Qualification+	 { qualifiers+	 , qualified } =+		Foldable.foldr+		 (\(Class_Qualifier qname qty) ty ->+			Calc.Term_Abst (Calc.Suggest qname)+			 (calc_type qty)+			 ((\x -> case x of+				 TeTy_Var_Name n | Text.toLower n == qname -> Just (Calc.Suggest qname)+				 _ -> Nothing) `Calc.abstract` ty)+		 ) (calc_type qualified) qualifiers+
+ Language/LOL/Typing/Expr/Grammar.ag view
@@ -0,0 +1,43 @@+-- vim: syntax=haskell+optpragmas {+{-# LANGUAGE OverloadedStrings #-}+}+module {Language.LOL.Typing.Expr.Grammar} {} {+import Data.Maybe (Maybe(..))+import Text.Show (Show)++import Language.LOL.Typing.Type+import Language.LOL.Typing.Expr.Common+}++data Expr+ | Var+	name :: Name+ | Abst -- ^ Monomorphic bind+	sig  :: {Maybe Monotype}+	name :: Name+	body :: Expr+ | App+	abst :: Expr+	arg  :: Expr+ | Annot+	body :: Expr+	sig  :: Polytype+ | Let -- ^ Polymorphic bind+	sig  :: {Maybe Polytype}+	name :: Name+	decl :: Expr+	body :: Expr+ | Where+	sig  :: {Maybe Polytype}+	name :: Name+	decl :: Expr+	body :: Expr+deriving Expr : Show++data Decl+ | Let+	sig  :: {Maybe Monotype}+	name :: Name+	decl :: Expr+deriving Decl : Show
+ Language/LOL/Typing/Expr/Test.hs view
@@ -0,0 +1,195 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+module Expr.Test where++import Control.Monad (Monad(..), when)+import Data.Bool+import Data.Functor.Identity (Identity(..))+import Data.Either (Either(..))+import Data.Function (($), (.))+import Data.Functor ((<$>))+import Data.Traversable (Traversable(..))+import Data.Maybe (Maybe(..))+import Data.Eq (Eq(..))+-- import Data.Tuple (fst, snd)+import qualified Data.Foldable as Foldable+import qualified Data.List as List+-- import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Data.Monoid (Monoid(..), (<>))+import Test.Tasty+import Test.Tasty.HUnit+-- import Test.HUnit hiding (test)+import System.IO (IO)+-- import Data.Sequence (Seq)+import Data.Text (Text)+-- import Control.Monad.Trans.Class (lift)+-- import qualified Data.Text    as Text+import qualified Data.Text.IO as Text+import Text.Show (Show(..))+import Prelude (error)+-- import Debug.Trace++import qualified Language.LOL.Calculus as Calc+import qualified Language.LOL.Calculus.Read as Calc+import Language.LOL.Typing+-- import qualified Language.LOL.Typing.Collect.Grammar as Collect+import Language.LOL.Typing.Expr.Calculus+import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build+import Solver.Test (polytys_env, infer)+-- import Solver.Test (write_log, Collect_Constraints(..), Infer_Polytype(..))++tests :: TestTree+tests = testGroup "Expr"+ [ tests_Calculus+ ]++type Test_Solver+ =   Solver_Greedy_Finite Collect_Infos IO++class Calcify a where+	calcify+	 :: Bool -> a+	 -> IO (Either (Collect_Error (Info Test_Solver)+	                              (Error Test_Solver))+	               (Calc.Term TeTy_Var))+instance Calcify Expr where+	calcify logging expr = do+		ty <- infer logging expr+		case ty of+		 Left err -> return $ Left err+		 Right Solver_Result+			 { solver_result_monotypes   = monosub+			 , solver_result_polytypes   = polysub+			 , solver_result_quantifiers = quants+			 } -> do+			let monoty = monosub `substitute` Monotype_Var 0+			let foralls = subvars monoty+			let consts = Map.unions+				 ( (Map.fromList $ (, ()) <$> List.take (List.length foralls) const_pool)+				 : ((\(name, polyty) -> Map.insert name () $ monoconsts polyty) <$> polytys_env) )+			let Syn_Expr+				 { term_Syn_Expr = term+				 } = wrap_Expr (sem_Expr expr) Inh_Expr+				 { env_Inh_Expr         = mempty+				 , freshvar_Inh_Expr    = 0+				 , monoconsts_Inh_Expr  = consts+				 , monotys_Inh_Expr     = monosub+				 , polytys_Inh_Expr     = (monosub `substitute`) <$> polysub+				 , quantifiers_Inh_Expr = (monosub `substitute`) . (Monotype_Var <$>) <$> quants+				 , renames_Inh_Expr     = mempty+				 }+			return $ Right $+				Foldable.foldr+				 (\(quant, const) ->+					Calc.Term_Abst (Calc.Suggest const)+					 (Calc.Type_Sort Calc.sort_star_mono) .+					((\v -> case v of+						 TeTy_Var_Monovar m | m == quant -> Just (Calc.Suggest const)+						 _ -> Nothing) `Calc.abstract`))+				 term+				 (List.zip foralls const_pool)+instance Calcify Decl where+	calcify logging decl = do+		ty <- infer logging decl+		case ty of+		 Left err -> return $ Left err+		 Right Solver_Result+			 { solver_result_monotypes   = monosub+			 , solver_result_polytypes   = polysub+			 , solver_result_quantifiers = quants+			 } -> do+			let monoty  = monosub `substitute` Monotype_Var 1 -- NOTE: decl.freshvar+			let foralls = subvars monoty+			let consts = Map.unions+				 ( (Map.fromList $ (, ()) <$> List.take (List.length foralls) const_pool)+				 : ((\(name, polyty) -> Map.insert name () $ monoconsts polyty) <$> polytys_env) )+			let Syn_Decl+				 { term_Syn_Decl = term+				 } = wrap_Decl (sem_Decl decl) Inh_Decl+				 { env_Inh_Decl         = mempty+				 , freshvar_Inh_Decl    = 0+				 , monoconsts_Inh_Decl  = consts+				 , monotys_Inh_Decl     = monosub+				 , polytys_Inh_Decl     = (monosub `substitute`) <$> polysub+				 , quantifiers_Inh_Decl = (monosub `substitute`) . (Monotype_Var <$>) <$> quants+				 , renames_Inh_Decl     = mempty+				 }+			return $ Right $+				Foldable.foldr+				 (\(quant, const) ->+					Calc.Term_Abst (Calc.Suggest const)+					 (Calc.Type_Sort Calc.sort_star_mono) .+					((\v -> case v of+						 TeTy_Var_Monovar m | m == quant -> Just (Calc.Suggest const)+						 _ -> Nothing) `Calc.abstract`))+				 term+				 (List.zip foralls const_pool)++calc_monovar_close :: Calc.Term TeTy_Var -> Either Monovar (Calc.Term Calc.Var_Name)+calc_monovar_close te =+	traverse go te+	where+		go (TeTy_Var_Monovar v) = Left v+		go (TeTy_Var_Name n) = Right n++tests_Calculus :: TestTree+tests_Calculus = testGroup "Calculus" $+	let test logging input (expected::Text) = do+		when logging $+			Text.putStrLn ("expr: " <> Build.text input)+		let expect_term =+			case runIdentity $ Calc.read Calc.parse_term expected of+			 Left err -> error $ show err+			 Right x -> x+		got_either_term <- calcify logging input+		case got_either_term of+		 got@(Left _) -> got @?= Right (TeTy_Var_Name <$> expect_term)+		 Right got_term ->+			case calc_monovar_close got_term of+			 Left m -> Left ("Monovar remains in term: " <> show m) @?= Right expect_term+			 got -> do+				when logging $ do+					Text.putStrLn ("exp: " <> Build.text expect_term)+					case got of+					 Right ex -> Text.putStrLn ("got: " <> Build.text ex)+					 _ -> return ()+				got @?= Right expect_term in+	let (==>) = test False in+	-- let (==>>) = test True in+ [ testGroup "Expr" $+	 [ testCase "id" $ ("x".-> "x")+	    ==> "λ(a:*) (x:a) -> x"+	 , testCase "id_Int" $ (("x","Int")..-> "x")+	    ==> "λ(x:Int) -> x"+	 , testCase "id_Int" $ ("x".-> ("x".:("Int"::Monotype)))+	    ==> "λ(x:Int) -> x"+	 , testCase "twice" $ ("f".-> "x".-> "f"!("f"!"x"))+	    ==> "λ(a:*) (f:a -> a) (x:a) -> f (f x)"+	 , testCase "const" $ ("x".-> "y".-> "x")+	    ==> "λ(a:*) (b:*) (x:a) (y:b) -> x"+	 , testCase "compose" $ ("f".-> "g".-> "x".-> "f"!("g"!"x"))+	    ==> "λ(a:*) (b:*) (c:*) (f:a -> b) (g:c -> a) (x:c) -> f (g x)"+	 , testCase "equal" $ ("x".-> "f".= "x" $ "f")+	    ==> "λ(a:*) (x:a) -> (λ(f:a) -> f) x"+	 , testCase "equal" $ ("x".-> "f".= ("y".->"x") $ "pair"!("f"!"True")!("f"!"one") )+	    ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> pair a a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)"+	 {-+	 , testCase "equal" $ ("x".-> "f".= ("y".->"x") $ "equal"!("f"!"True")!("f"!"one") )+	    ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)"+	 -}+	 ]+ , testGroup "Decl" $+	 [ testCase "equal" $ Decl_Let Nothing "test"+		("x".-> "f".= ("y".-> "x") $ "equal"!("f"!"True")!("f"!"one") )+	    ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)"+	 -- , testCase "Abst rename" $ Decl_Let Nothing "test" ("Bool".-> "f".= ("y".-> "Bool") $ "equal"!("f"!"True")!("f"!"one") )+	 --    ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)"+	 -- , testCase "Let rename" $ Decl_Let Nothing "test" ("x".-> "Int".= ("y".-> "x") $ "equal"!("Int"!"True")!("Int"!"one") )+	 --    ==> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> a) -> equal a (f Bool True) (f Int one)) (λ(b:*) (y:b) -> x)"+	 -- , testCase "equal" $ Decl_Let Nothing "test" ("x".-> "f".= ("y".-> "g".= ("z".->"y") $ "g"!"x") $ "equal"!("f"!"True")!("f"!"True") )+	 --    ==>> "λ(a:*) (x:a) -> (λ(f:∀(b:*) -> b -> b) -> equal Bool (f Bool True) (f Bool True)) (λ(b:*) (y:b) -> (λ(g:∀(c:*) -> c -> b) -> g a x) (λ(c:*) (z:c) -> y))"+	 ]+ ]
+ Language/LOL/Typing/Expr/Utils.hs view
@@ -0,0 +1,43 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Language.LOL.Typing.Expr.Utils where++import Data.Function (($), (.))+import Data.Maybe (Maybe(..))+import Data.String (IsString(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Expr.Common+import Language.LOL.Typing.Expr.Grammar++-- Convenient instances++instance IsString Expr where+	fromString = Expr_Var . fromString++-- * Convenient 'Expr' constructors++(.->) :: Name -> Expr -> Expr+(.->) = Expr_Abst Nothing+infixr 0 .->+(..->) :: (Name, Monotype) -> Expr -> Expr+(..->) (name, sig) = Expr_Abst (Just sig) name+infixr 0 ..->++(.:) :: Polytypeable sig => Expr -> sig -> Expr+(.:) e = Expr_Annot e . polytype+infixr 0 .:++(.=) :: Name -> Expr -> Expr -> Expr+(.=) = Expr_Let Nothing+infixr 2 .=+(..=) :: Polytypeable sig => (Name, sig) -> Expr -> Expr -> Expr+(..=) (name, sig) = Expr_Let (Just $ polytype sig) name+infixr 2 ..=++(!) :: Expr -> Expr -> Expr+(!) = Expr_App+infixl 5 !++(.$) :: Expr -> Expr -> Expr+(.$) = Expr_App+infixr 3 .$
+ Language/LOL/Typing/Expr/Write.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Language.LOL.Typing.Expr.Write where++import Data.Maybe (Maybe(..))+import Data.Monoid ((<>))+import Data.Text.Buildable (Buildable(..))++import Language.LOL.Typing.Expr.Grammar++instance Buildable Expr where+	build expr =+		case expr of+		 Expr_Var nam -> build nam+		 Expr_App f x ->+			"(" <> build f <> " " <> build x <> ")"+		 Expr_Annot e sig ->+			"(" <> build e <> " : " <> build sig <> ")"+		 Expr_Let sig nam decl e ->+			"let " <> n <> " = " <> build decl <> " in " <> build e+			where n =+				case sig of+				 Just s -> "("<>build nam<>":"<>build s<>")"+				 Nothing -> build nam+		 Expr_Where sig nam decl e ->+			build e <> " where " <> n <> " = " <> build decl+			where n =+				case sig of+				 Just s -> "("<>build nam<>":"<>build s<>")"+				 Nothing -> build nam+		 Expr_Abst sig nam e ->+			"(" <> "\\" <> n <> " -> " <> build e <> ")"+			where n =+				case sig of+				 Just s -> "("<>build nam<>":"<>build s<>")"+				 Nothing -> build nam+instance Buildable Decl where+	build decl =+		case decl of+		 Decl_Let sig nam expr ->+			n <> " = " <> build expr+			where n =+				case sig of+				 Just s -> "("<>build nam<>":"<>build s<>")"+				 Nothing -> build nam
+ Language/LOL/Typing/Lib/Control/Monad/Classes/EffectsFix.hs view
@@ -0,0 +1,18 @@+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE KindSignatures #-}+module Language.LOL.Typing.Lib.Control.Monad.Classes.EffectsFix where+-- | Effects whose state is parameterized by the 'Monad' stack.++-- * Types of effects++-- | Writer effect+data EffWriterFix (w :: {-m-}(* -> *) -> *)++-- | Reader effect+data EffReaderFix (e :: {-m-}(* -> *) -> *)++-- | Local state change effect+data EffLocalFix (e :: {-m-}(* -> *) -> *)++-- | State effect+data EffStateFix (s :: {-m-}(* -> *) -> *)
+ Language/LOL/Typing/Lib/Control/Monad/Classes/Instance.hs view
@@ -0,0 +1,23 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE TypeFamilies #-}+module Language.LOL.Typing.Lib.Control.Monad.Classes.Instance where+import Data.Bool (Bool(..))+import GHC.Prim (Constraint)++-- | A data type to existentially wrap a value of type @ty@,+-- when it is an instance of the type class @cl@.+data Instance (cl:: * -> Constraint)+ = forall ty. cl ty => Instance ty++-- | An open type family to know (at the type level) whether a type @ty@+-- has an instance of the type class @cl@.+--+-- NOTE: currently, users have to manually define type family instances of 'Class'+-- to indicate to the compiler which type support which type class.+-- It is definitively redundant to have to define+-- both a type class instance and a type family instance,+-- but I cannot find a way to automatically synchronize+-- the compiler's knowledge between these two levels.+type family Class (cl:: * -> Constraint) (ty:: *) :: Bool
+ Language/LOL/Typing/Lib/Control/Monad/Classes/StateFix.hs view
@@ -0,0 +1,134 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}++-- | 'MonadState' whose state is parameterized by the 'Monad' stack.+module Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix where++import Control.Applicative (Applicative(..))+import Control.Monad+import Control.Monad.Classes+import Control.Monad.Trans.Class+import qualified Control.Monad.Trans.State.Lazy as SL+-- import qualified Control.Monad.Trans.State.Strict as SS -- TODO: when needed :)+import Data.Bool (Bool(..))+import Data.Function ((.), const)+import Data.Functor.Identity (Identity)+import GHC.Prim (Proxy#, proxy#)+import Prelude (seq)++import Language.LOL.Typing.Lib.Control.Monad.Classes.EffectsFix++-- * Type 'StateLazyFixT'++data StateLazyFixT+ (st::{-StateLazyFixT st m-}(* -> *) -> *)+ (m::{-a-}* -> *)+ (a:: *)+ =   StateLazyFixT+ { unStateLazyFixT :: SL.StateT (st (StateLazyFixT st m)) m a }+ deriving (Functor)+instance Monad m => Applicative (StateLazyFixT st m) where+	pure = return+	(<*>) = ap+instance Monad m => Monad (StateLazyFixT st m) where+	return  = StateLazyFixT . return+	m >>= f = StateLazyFixT (unStateLazyFixT m >>= unStateLazyFixT . f)+instance MonadTrans (StateLazyFixT st) where+	lift = StateLazyFixT . lift++-- ** Type 'StateLazyFix'+type StateLazyFix  st+ =   StateLazyFixT st Identity++-- * Type family 'StateFixCanDo'++type instance CanDo (StateLazyFixT s m) eff+ = StateFixCanDo s eff++type family StateFixCanDo s eff where+	StateFixCanDo s (EffStateFix s)  = 'True+	StateFixCanDo s (EffReaderFix s) = 'True+	StateFixCanDo s (EffLocalFix s)  = 'True+	StateFixCanDo s (EffWriterFix s) = 'True+	StateFixCanDo s eff              = 'False++-- * Class 'MonadStateFixN'++class Monad m => MonadStateFixN (n :: Peano) s m where+	stateFixN :: Proxy# n -> (s m -> (a, s m)) -> m a++-- | Warning: only work when 'StateLazyFixT'+-- is the outermost 'Monad' (i.e. when @n@ @~@ 'Zero'),+-- because the state is paramaterized by this 'Monad'.+instance Monad m => MonadStateFixN 'Zero s (StateLazyFixT s m) where+	stateFixN _ = StateLazyFixT . SL.state++-- ** Type 'MonadStateFixN'++-- | The @'MonadStateFix' s m@ constraint asserts that @m@ is a 'Monad' stack+-- that supports state operations on type @s@+type MonadStateFix (s::(* -> *) -> *) m+ =   MonadStateFixN (Find (EffStateFix s) m) s m++-- | Construct a state 'Monad' computation from a function+stateFix+ :: forall s m a. (MonadStateFix s m)+ => (s m -> (a, s m)) -> m a+stateFix = stateFixN (proxy# :: Proxy# (Find (EffStateFix s) m))++-- | @'put' s@ sets the state within the 'Monad' to @s@+putFix :: MonadStateFix s m => s m -> m ()+putFix s = stateFix (const ((), s))++-- | Fetch the current value of the state within the 'Monad'+getFix :: MonadStateFix s m => m (s m)+getFix = stateFix (\s -> (s, s))++-- | Gets specific component of the state,+-- using a projection function supplied.+getsFix :: MonadStateFix s m => (s m -> a) -> m a+getsFix f = do+	s <- getFix+	return (f s)++-- | Maps an old state to a new state inside a state 'Monad' layer+modifyFix :: MonadStateFix s m => (s m -> s m) -> m ()+modifyFix f = stateFix (\s -> ((), f s))++-- | A variant of 'modify' in which the computation+-- is strict in the new state.+modifyFix' :: MonadStateFix s m => (s m -> s m) -> m ()+modifyFix' f = stateFix (\s -> let s' = f s in s' `seq` ((), s'))++-- Return the 'Monad' parameter and the state.+runStateLazyFix+ :: st (StateLazyFixT st m)+ ->     StateLazyFixT st m  a+ ->                      m (a, st (StateLazyFixT st m))+runStateLazyFix s m = SL.runStateT (unStateLazyFixT m) s++-- Return the 'Monad' parameter.+evalStateLazyFix+ :: Monad m+ => st (StateLazyFixT st m)+ ->     StateLazyFixT st m a+ ->                      m a+evalStateLazyFix s m = SL.evalStateT (unStateLazyFixT m) s++-- Return the state.+execStateLazyFix+ :: Monad m+ => st (StateLazyFixT st m)+ ->     StateLazyFixT st m a+ ->                      m (st (StateLazyFixT st m))+execStateLazyFix s m = SL.execStateT (unStateLazyFixT m) s
+ Language/LOL/Typing/Lib/Control/Monad/Classes/StateInstance.hs view
@@ -0,0 +1,109 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} -- NOTE: for CansMonadStateInstance+{-# OPTIONS_GHC -fno-warn-tabs #-}++-- | Collect in a 'Monad' stack, the states of 'MC.MonadState' 'Monad'+-- which are instances of a given type class.+module Language.LOL.Typing.Lib.Control.Monad.Classes.StateInstance where++import Control.Monad+import qualified Control.Monad.Classes as MC+import Control.Monad.Trans.Class+import qualified Control.Monad.Trans.State.Lazy as SL+import qualified Control.Monad.Trans.State.Strict as SS+import Data.Bool (Bool(..))+import GHC.Prim (Proxy#, proxy#, Constraint)++import Language.LOL.Typing.Lib.Control.Monad.Classes.Instance+import Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix++-- * Class 'MonadStateInstance'++-- ** Type family 'CanMonadStateInstance'++-- | A close type family to know whether a 'Monad' @m@+-- support an effect 'eff' whose state is an instance of the type class @cl@.+--+-- NOTE: the closeness enables to define 'Class' instances+-- only for the states of the 'Monad's in a 'Monad' stack+-- which support the effects 'MC.EffState'.+type family CanMonadStateInstance (cl:: * -> Constraint) (m:: * -> *) (eff:: k) :: Bool where+	CanMonadStateInstance cl (SL.StateT s m) (MC.EffState  _s) = Class cl s+	CanMonadStateInstance cl (SS.StateT s m) (MC.EffState  _s) = Class cl s+	-- CanMonadStateInstance cl (SL.StateT s m) (MC.EffReader _s) = Class cl s+	-- CanMonadStateInstance cl (SS.StateT s m) (MC.EffReader _s) = Class cl s+	CanMonadStateInstance cl (StateLazyFixT s m) (MC.EffState  _s) = Class cl (s m)+	CanMonadStateInstance cl s eff = 'False++-- ** Type family 'CansMonadStateInstance'++-- | A close type family to know which 'Monad's in a 'Monad' stack @stack@+-- support an effect 'eff' whose state is an instance of the type class @cl@.+type family CansMonadStateInstance (cl:: * -> Constraint) (eff :: k) (stack :: * -> *) :: [Bool] where+	CansMonadStateInstance cl eff (t m) = CanMonadStateInstance cl (t m) eff ': CansMonadStateInstance cl eff m+	CansMonadStateInstance cl eff m     = CanMonadStateInstance cl m     eff ': '[]++-- | A type synonym to constrain a 'Monad' @m@+-- to support an 'MC.EffState' whose state is an instance of the type class @cl@.+type MonadStateInstance cl m+ =   MonadStateInstanceN cl (CansMonadStateInstance cl (MC.EffState ()) m) m++getInstance :: forall cl m. MonadStateInstance cl m => m [Instance cl]+getInstance = getInstanceN (proxy# :: Proxy# (CansMonadStateInstance cl (MC.EffState ()) m))++-- ** Class 'MonadStateInstanceN'++-- | A type class to recurse over the 'Monad' stack+-- to collect the states which are instance of the type class @cl@.+class Monad m => MonadStateInstanceN cl (cans::[Bool]) m where+	getInstanceN :: Proxy# cans -> m [Instance cl]++-- | Collect the lazy 'SL.StateT', and recurse.+instance (cl s, Monad m, MonadStateInstanceN cl cans m)+ => MonadStateInstanceN cl ('True ': cans) (SL.StateT s m) where+	getInstanceN _ = do+		s <- SL.get+		ss <- lift (getInstanceN (proxy# :: Proxy# cans))+		return (Instance s : ss)++-- | Collect the strict 'SS.StateT', and recurse.+instance (cl s, Monad m, MonadStateInstanceN cl cans m)+ => MonadStateInstanceN cl ('True ': cans) (SS.StateT s m) where+	getInstanceN _ = do+		s <- SS.get+		ss <- lift (getInstanceN (proxy# :: Proxy# cans))+		return (Instance s : ss)++-- | Collect the 'StateLazyFixT', and recurse.+instance (cl (s (StateLazyFixT s m)), Monad m, MonadStateInstanceN cl cans m)+ => MonadStateInstanceN cl ('True ': cans) (StateLazyFixT s m) where+	getInstanceN _ = do+		s <- StateLazyFixT SL.get+		ss <- lift (getInstanceN (proxy# :: Proxy# cans))+		return (Instance s : ss)++-- | Recurse the 'Monad' stack, passing over 'Monad' @t m@+-- such that 'CanMonadStateInstance' @cl@ @t m@ @MC.EffState ()@ @~@ 'False'.+instance+ ( Monad m+ , Monad (t m)+ , MonadTrans t+ , MonadStateInstanceN cl (can ': cans) m+ ) => MonadStateInstanceN cl ('False ': (can ': cans)) (t m) where+	getInstanceN _ = lift (getInstanceN (proxy# :: Proxy# (can ': cans)))++-- | Terminating instance, when the deepest 'Monad' on the stack+-- is such that 'CanMonadStateInstance' @cl@ @t m@ @MC.EffState ()@ @~@ 'False':+-- then there is no need to recurse,+-- and thus no 'MonadStateInstanceN' @cl@ @[]@ @m@ constraint to impose.+instance Monad m => MonadStateInstanceN cl ('False ': '[]) m where+	getInstanceN _ = return []
+ Language/LOL/Typing/Lib/Data/Default.hs view
@@ -0,0 +1,6 @@+module Language.LOL.Typing.Lib.Data.Default where++-- * Class 'Default'++class Default a where+	def :: a
+ Language/LOL/Typing/Lib/Data/Empty.hs view
@@ -0,0 +1,17 @@+module Language.LOL.Typing.Lib.Data.Empty where++import Data.Maybe (Maybe(..))++-- * Class 'Empty'++class Empty a where+	empty :: a++instance Empty () where+	empty = ()+instance (Empty a, Empty b) => Empty (a, b) where+	empty = (empty, empty)+instance Empty [a] where+	empty = []+instance Empty (Maybe a) where+	empty = Nothing
+ Language/LOL/Typing/Lib/Data/Text/Buildable.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Language.LOL.Typing.Lib.Data.Text.Buildable where++import Data.Function (($), (.))+import Data.Functor ((<$>))+import Data.Foldable (Foldable(..))+import Data.Monoid (Monoid(..), (<>))+import qualified Data.List as List+import Data.String (String)+import Data.Text (Text)+import Data.Text.Buildable (Buildable(..))+import qualified Data.Text.Lazy as TL+import qualified Data.Text.Lazy.Builder as Build+import Data.Text.Lazy.Builder (Builder)++string :: Buildable a => a -> String+string = TL.unpack . Build.toLazyText . build++text :: Buildable a => a -> Text+text = TL.toStrict . Build.toLazyText . build++tuple :: (Foldable f, Buildable a) => f a -> Builder+tuple f = "(" <> mconcat (List.intersperse ", " $ foldr ((:). build) [] f) <> ")"++list :: (Foldable f, Buildable a) => f a -> Builder+list f = "[" <> mconcat (List.intersperse ", " $ foldr ((:). build) [] f) <> "]"++unlines :: (Foldable f, Buildable a) => f a -> Builder+unlines = mconcat . List.intersperse "\n" . foldr ((:). build) []++indent :: Buildable a => Builder -> a -> Builder+indent prefix =+	mconcat . List.intersperse "\n" .+	((prefix <>) . build <$>) . TL.lines .+	Build.toLazyText . build++parens :: Buildable a => a -> Builder+parens a = "(" <> build a <> ")"++{-+instance Buildable a => Buildable [a] where+	build = list+-}
+ Language/LOL/Typing/Solver.hs view
@@ -0,0 +1,18 @@+-- | All submodules, in a topological order.+module Language.LOL.Typing.Solver+ ( module Language.LOL.Typing.Solver.Common+ , module Language.LOL.Typing.Solver.Constraint+ , module Language.LOL.Typing.Solver.Monotype+ , module Language.LOL.Typing.Solver.Polytype+ , module Language.LOL.Typing.Solver.Class+ , module Language.LOL.Typing.Solver.Monad+ , module Language.LOL.Typing.Solver.Greedy+ ) where++import Language.LOL.Typing.Solver.Common+import Language.LOL.Typing.Solver.Constraint+import Language.LOL.Typing.Solver.Monotype+import Language.LOL.Typing.Solver.Polytype+import Language.LOL.Typing.Solver.Class+import Language.LOL.Typing.Solver.Monad+import Language.LOL.Typing.Solver.Greedy
+ Language/LOL/Typing/Solver/Class.hs view
@@ -0,0 +1,478 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+-- | Type inference for /type class polymorphism/+-- (aka. /parametric overloading/).+module Language.LOL.Typing.Solver.Class where++import Control.Monad (Monad(..), forM, forM_, mapM)+import qualified Control.Monad.Classes as MC+import Data.Bool+import Data.Eq (Eq(..))+import qualified Data.Foldable as Foldable+import Data.Function (($), (.))+import Data.Functor ((<$>))+import qualified Data.List as List+import qualified Data.Map.Strict as Map+import Data.Maybe (Maybe(..), isJust)+import Data.Monoid (Monoid(..), (<>))+import Data.Text (Text)+import Data.Text.Buildable (Buildable(..))+import Data.Tuple (fst)+import Text.Show (Show(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Solver.Common+import Language.LOL.Typing.Solver.Constraint+import Language.LOL.Typing.Solver.Monotype+import Language.LOL.Typing.Solver.Polytype+import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC+import Language.LOL.Typing.Lib.Data.Empty (Empty(..))+import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build++-- * Type 'State_Class'++data State_Class info+ =   State_Class+ {   state_class_directives :: [Class_Directive info]+     -- ^ 'Class_Directive's for 'state_class_qualifiers'.+ ,   state_class_env :: Class_Env+     -- ^ Known 'Class'es and 'Class_Instance's.+ ,   state_class_qualifiers :: State_Class_Qualifiers info+     -- ^ 'Class' assertions.+ } deriving (Show)++-- | Make 'State_Class' collectable as a 'State' instance+-- out of a 'Monad' stack.+type instance MC.Class State (State_Class info) = 'True++instance Empty (State_Class info) where+	empty = State_Class+	 { state_class_directives = mempty+	 , state_class_env        = mempty+	 , state_class_qualifiers = empty+	 }+instance Buildable info => State (State_Class info) where+	state_name _ = "State_Class"+	state_show = Build.text+instance Buildable info => Buildable (State_Class info) where+	build State_Class+	 { state_class_directives+	 , state_class_env+	 , state_class_qualifiers+	 } =+		mconcat $ List.intersperse "\n"+		 [ "class directives: "  <> Build.list state_class_directives+		 , "class environment: " <> Build.list (Map.keys state_class_env)+		 , "class qualifiers: "+		 , Build.indent "  " state_class_qualifiers+		 ]++-- ** Type 'State_Class_Qualifiers'++data State_Class_Qualifiers info+ =   State_Class_Qualifiers+ {   state_class_qualifiers_assumed     :: [Infoed info Class_Qualifier]+ ,   state_class_qualifiers_generalized :: [Infoed info Class_Qualifier]+ ,   state_class_qualifiers_toprove     :: [Infoed info Class_Qualifier]+     -- ^ Once the constraints have been solved, this list should be empty.+ } deriving (Show)+ +instance Empty (State_Class_Qualifiers info) where+	empty =+		State_Class_Qualifiers+		 { state_class_qualifiers_assumed     = []+		 , state_class_qualifiers_generalized = []+		 , state_class_qualifiers_toprove     = []+		 }+instance Buildable info => Buildable (State_Class_Qualifiers info) where+	build State_Class_Qualifiers+	 { state_class_qualifiers_assumed+	 , state_class_qualifiers_generalized+	 , state_class_qualifiers_toprove+	 } =+		Build.unlines+		 [ "assumed: "     <> Build.list state_class_qualifiers_assumed+		 , "generalized: " <> Build.list state_class_qualifiers_generalized+		 , "toprove: "     <> Build.list state_class_qualifiers_toprove+		 ]+instance Substitutable (State_Class_Qualifiers info) where+	subvars (State_Class_Qualifiers qs gs as) = subvars (infoed <$> (qs <> gs <> as))+	sub `substitute` State_Class_Qualifiers+	 { state_class_qualifiers_toprove     = ps+	 , state_class_qualifiers_generalized = gs+	 , state_class_qualifiers_assumed     = as+	 } =+		State_Class_Qualifiers+		 { state_class_qualifiers_toprove     = ((sub `substitute`) <$>) <$> ps+		 , state_class_qualifiers_generalized = ((sub `substitute`) <$>) <$> gs+		 , state_class_qualifiers_assumed     = ((sub `substitute`) <$>) <$> as+		 }++-- * Class 'Solver_Class'++class+ ( Solver_Constraint m+ , Solver_Monotype m+ , Solver_Polytype m+ , MC.MonadState (State_Class (Info m)) m+ , Infoable (Info_Class (Info m)) (Info m)+ , Solver_Logable Log_Class m+ ) => Solver_Class m where+	error_class :: Error_Class -> Error m+	+	class_qualifiers :: m (State_Class_Qualifiers (Info m))+	class_qualifiers =+		MC.gets $ \(s::State_Class (Info m)) ->+			state_class_qualifiers s+	class_qualifiers_modify+	 :: (State_Class_Qualifiers (Info m) -> State_Class_Qualifiers (Info m))+	 -> m ()+	class_qualifiers_modify f =+		MC.modify $ \(s::State_Class (Info m)) ->+			s{ state_class_qualifiers =+				f (state_class_qualifiers s) }+	class_qualifier_toprove+	 :: Info m -> Class_Qualifier -> m ()+	class_qualifier_toprove info q = do+		log $ Log_Class_Qualifier_ToProve q+		class_qualifiers_modify $ \quals ->+			quals{ state_class_qualifiers_toprove =+				Infoed info q : state_class_qualifiers_toprove quals }+	class_qualifier_assume+	 :: Info m -> Class_Qualifier -> m ()+	class_qualifier_assume info q = do+		log $ Log_Class_Qualifier_Assume q+		class_qualifiers_modify $ \quals ->+			quals{ state_class_qualifiers_assumed =+				Infoed info q : state_class_qualifiers_assumed quals }+	class_qualifiers_map+	 :: (Class_Qualifier -> m Class_Qualifier) -> m ()+	class_qualifiers_map f = do+		let g = mapM $ \(Infoed info q) ->+			f q >>= \new -> return (Infoed info new)+		state_class_qualifiers_toprove <-+			(>>= g) $+			MC.gets $ \(s::(State_Class (Info m))) ->+				state_class_qualifiers_toprove $+				state_class_qualifiers s+		state_class_qualifiers_generalized <-+			(>>= g) $+			MC.gets $ \(s::(State_Class (Info m))) ->+				state_class_qualifiers_generalized $+				state_class_qualifiers s+		state_class_qualifiers_assumed <-+			(>>= g) $+			MC.gets $ \(s::(State_Class (Info m))) ->+				state_class_qualifiers_assumed $+				state_class_qualifiers s+		class_qualifiers_modify $ \quals ->+			quals+			 { state_class_qualifiers_toprove+			 , state_class_qualifiers_generalized+			 , state_class_qualifiers_assumed+			 }+	+	class_qualifiers_reduced :: m [Class_Qualifier]+	class_qualifiers_reduced = do+		synotys <- synotype_substitution+		clenv <- class_env+		quals <- class_qualifiers+		return $ fst $+			class_context_reduction+			 synotys clenv $ infoed <$> (+				state_class_qualifiers_toprove quals <>+				state_class_qualifiers_generalized quals <>+				state_class_qualifiers_assumed quals+			 )+	+	-- | Generalize a 'Monotype', preserving given 'Rigtype's,+	-- and such that the resulting 'Polytype'+	-- has all the 'Class_Qualifier's from 'state_class_qualifiers_toprove',+	-- when they apply at least on one of the 'quantifiers' of this 'Polytype'.+	class_polytype_forall+	 :: [Rigtype] -> Monotype -> m Polytype+	class_polytype_forall rigtys monoty = do+		State_Class_Qualifiers+		 { state_class_qualifiers_toprove     = quals_toprove+		 , state_class_qualifiers_generalized = quals_generalized+		 } <- class_qualifiers+		let rigvas = subvars rigtys+		let polyvars = subvars monoty List.\\ rigvas+		let has_polyvars = Foldable.any (`List.elem` polyvars) . subvars . infoed+		let (  quals_toprove_poly+		     , quals_toprove_mono+		     ) = List.partition has_polyvars quals_toprove+		let quals_generalized_poly = List.filter has_polyvars quals_generalized+		class_qualifiers_modify $ \quals ->+			quals+			 { state_class_qualifiers_toprove     = quals_toprove_mono+			 , state_class_qualifiers_generalized = quals_toprove_poly <> state_class_qualifiers_generalized quals+			 }+		return $+			forall_but rigvas $+			Qualification+			 (infoed <$> (quals_toprove_poly <> quals_generalized_poly))+			 monoty+	+	class_improve+	 :: Bool -> m [(Info m, Monotype, Monotype)]+	class_improve normal =+		if normal+		then class_improve_normal+		else class_improve_final+	class_improve_normal+	 :: m [(Info m, Monotype, Monotype)]+	class_improve_normal =+		return []+	class_improve_final+	 :: m [(Info m, Monotype, Monotype)]+	class_improve_final =+		return []+	+	class_simplify :: m ()+	class_simplify = do+		State_Class_Qualifiers+		 { state_class_qualifiers_toprove+		 , state_class_qualifiers_assumed+		 } <- class_qualifiers+		synotys <- synotype_substitution+		clenv <- class_env+		cldirs <- MC.gets state_class_directives+		clquals <- simplify synotys clenv cldirs+			 state_class_qualifiers_toprove+		class_qualifiers_modify $ \quals ->+			quals{state_class_qualifiers_toprove =+				List.filter (not . class_entails synotys clenv+				 (infoed <$> state_class_qualifiers_assumed) . infoed) clquals }+		where+		simplify ::+		 ( Solver_Constraint m+		 , Solver_Polytype m+		 ) => Synotype_Substitution+		 -> Class_Env+		 -> [Class_Directive (Info m)]+		 ->   [Infoed (Info m) Class_Qualifier]+		 -> m [Infoed (Info m) Class_Qualifier]+		simplify synotys clenv cldirs clquals = do+			hnf' <- go_insts clquals+			are_disjoints (go_super_class [] hnf')+			where+			go_insts+			 ::   [Infoed (Info m) Class_Qualifier]+			 -> m [Infoed (Info m) Class_Qualifier]+			go_insts ts =+				(List.concat <$>) <$>+				forM ts $+				 \q@(Infoed info clqual@(Class_Qualifier clname _)) ->+					if is_class_qualifier_normalized clqual+					then return [q]+					else case class_env_instance_context synotys clenv clqual of+					 Just inst_context ->+						go_insts $+						 Infoed (info_insert+							 (Info_Class_Qualifier_Parent clqual::Info_Class (Info m))+							 info) <$>+						 inst_context+					 Nothing -> do+						constraint_error_insert+						 (error_class Error_Class_Qualifier_Unresolved) $+						 (case cldirs_never of+							 clql:_ -> info_insert $ Info_Class_Directive_Never clql+							 [] -> case infos_cldirs_close of+								 [i] -> info_insert (Info_Class_Directive_Close (Infoed i clname)::Info_Class (Info m))+								 _   -> info_insert (Info_Class_Qualifier_Unresolved clqual::Info_Class (Info m)))+						 info+						return []+						where+						cldirs_never =+							[ Infoed i clql+							| Class_Directive_Never clql i <- cldirs+							, isJust $ class_qualifier_unification synotys clqual clql+							]+						infos_cldirs_close =+							[ i+							| Class_Directive_Close n i <- cldirs+							, n == clname ]+			+			go_super_class+			 :: [Infoed (Info m) Class_Qualifier]+			 -> [Infoed (Info m) Class_Qualifier]+			 -> [Infoed (Info m) Class_Qualifier]+			go_super_class rs [] = rs+			go_super_class rs (x:xs)+			 | class_entails_super_class clenv+				 (infoed <$> (rs <> xs)) (infoed x) = go_super_class rs xs+			 | otherwise = go_super_class (x:rs) xs+			+			are_disjoints+			 ::   [Infoed (Info m) Class_Qualifier]+			 -> m [Infoed (Info m) Class_Qualifier]+			are_disjoints [] = return []+			are_disjoints (t@(Infoed info (Class_Qualifier className ty)):ts) = do+				let f t'@(Infoed info' (Class_Qualifier className' ty')) =+					case+					 [ i+					 | ty == ty'+					 , Class_Directive_Disjoint ss i <- cldirs+					 , className  `List.elem` ss+					 , className' `List.elem` ss+					 ] of+					 [] -> return ([t'], True)+					 info_directive : _ -> do+						constraint_error_insert+						 (error_class Error_Class_Qualifier_Disjoint) $+							info_insert+							 (Info_Class_Directive_Disjoint+								 (Infoed info className)+								 (Infoed info' className'))+							 info_directive+						return ([], False)+				result <- mapM f ts+				let (list, bs) = List.unzip result+				rest <- are_disjoints (List.concat list)+				return $ if Foldable.and bs then t : rest else rest+	+	class_ambiguous :: m ()+	class_ambiguous = do+		State_Class_Qualifiers+		 { state_class_qualifiers_toprove+		 } <- class_qualifiers+		rigvars_rigtypes <- polytype_rigids+		forM_ state_class_qualifiers_toprove $ \q_toprove ->+			case q_toprove of+			 Infoed _ Class_Qualifier{class_qualifier_type=Monotype_Var v} ->+				case+				 [ info+				 | Infoed info (rigvas, _) <- rigvars_rigtypes+				 , v `List.elem` rigvas+				 ] of+				 info:_ -> err_missing q_toprove info+				 _      -> err_ambiguous q_toprove+			 _ -> err_ambiguous q_toprove+		where+		err_ambiguous (Infoed info p) =+			constraint_error_insert+			 (error_class Error_Class_Qualifier_Ambiguous) $+			info_insert+			 (Info_Class_Qualifier_Ambiguous p::Info_Class (Info m)) info+		err_missing q_toprove info =+			constraint_error_insert+			 (error_class Error_Class_Qualifier_Missing) $+			info_insert+			 (Info_Class_Qualifier_Arising_from q_toprove) info+	+	class_env :: m Class_Env+	class_env =+		MC.gets $ \(s::State_Class (Info m)) ->+			state_class_env s+	class_env_set :: Class_Env -> m ()+	class_env_set state_class_env =+		MC.modify $ \(s::State_Class (Info m)) ->+			s{ state_class_env }++-- | When all 'state_constraint_constraints' have been handled,+-- takes all the remaining 'state_class_qualifiers_toprove',+-- and report them as ambiguities.+class_ambiguities ::+ ( Solver_Constraint m+ , Solver_Monotype m+ , Solver_Polytype m+ , Solver_Class m+ ) => m ()+class_ambiguities = do+	class_reduction+	class_improve_fix False+	class_ambiguous++-- | Perform context reduction on the 'state_class_qualifiers_toprove',+-- and removes the 'Class_Qualifier's+-- which are entailed by 'state_class_qualifiers_assumed'.+class_reduction ::+ ( Solver_Constraint m+ , Solver_Monotype m+ , Solver_Polytype m+ , Solver_Class m+ ) => m ()+class_reduction = do+	monotype_substitution_consistentify+	class_qualifiers_map monotype_substitute+	class_improve_fix True+	class_simplify++class_improve_fix ::+ ( Solver_Constraint m+ , Solver_Monotype m+ , Solver_Polytype m+ , Solver_Class m+ ) => Bool -> m ()+class_improve_fix normal = do+	improvements <- class_improve normal+	case improvements of+	 [] -> return ()+	 _  -> do+		forM_ improvements+		 (\(info, t1, t2) -> monotype_unify info t1 t2)+		monotype_substitution_consistentify+		class_improve_fix normal++-- * Class 'Info_Class'++data Info_Class info+ =   Info_Class_Qualifier_Ambiguous Class_Qualifier+ |   Info_Class_Qualifier_Arising_from (Infoed info Class_Qualifier)+ |   Info_Class_Qualifier_Parent Class_Qualifier+ |   Info_Class_Qualifier_Unresolved Class_Qualifier+ |   Info_Class_Directive_Close (Infoed info Text)+ |   Info_Class_Directive_Disjoint (Infoed info Text) (Infoed info Text)+ |   Info_Class_Directive_Never (Infoed info Class_Qualifier)+ deriving (Eq, Show)++instance Buildable info => Buildable (Info_Class info) where+	build x =+		case x of+		 Info_Class_Qualifier_Ambiguous q ->+			"Info_Class_Qualifier_Ambiguous " <> build q+		 Info_Class_Qualifier_Arising_from q ->+			"Info_Class_Qualifier_Arising_from " <> build q+		 Info_Class_Qualifier_Parent q ->+			"Info_Class_Qualifier_Parent " <> build q+		 Info_Class_Qualifier_Unresolved q ->+			"Info_Class_Qualifier_Unresolved " <> build q+		 Info_Class_Directive_Close n ->+			"Info_Class_Directive_Close " <> build n+		 Info_Class_Directive_Disjoint n1 n2 ->+			"Info_Class_Directive_Disjoint " <> build n1 <> " " <> build n2+		 Info_Class_Directive_Never q ->+			"Info_Class_Directive_Never " <> build q++-- * Type 'Error_Class'++data Error_Class+ =   Error_Class_Qualifier_Ambiguous+     -- ^ Example: @forall a. Eq a => Int -> Int@+ |   Error_Class_Qualifier_Disjoint+ |   Error_Class_Qualifier_Missing+ |   Error_Class_Qualifier_Unresolved+     -- ^ A 'Monotype' is missing a required 'Class_Qualifier'.+ deriving (Eq, Show)++-- ** Type 'Log_Class'++data Log_Class+ =   Log_Class_Qualifier_Assume  Class_Qualifier+ |   Log_Class_Qualifier_ToProve Class_Qualifier+ deriving (Show)+instance Buildable Log_Class where+	build x =+		case x of+		 Log_Class_Qualifier_Assume  q -> "class_qualifier_assume  : " <> build q+		 Log_Class_Qualifier_ToProve q -> "class_qualifier_toprove : " <> build q
+ Language/LOL/Typing/Solver/Common.hs view
@@ -0,0 +1,116 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Solver.Common where++import Control.Monad (Monad(..))+import Data.Bool+import Data.Eq (Eq(..))+import Data.Functor (Functor(..))+import Data.Monoid ((<>))+import Data.Text (Text)+import qualified Data.Text as Text+import Data.Text.Buildable (Buildable(..))+import Text.Show (Show(..))++-- * Class 'Information'++-- | An associated type constructor+-- to attach informations to a 'Constraint'+-- about why it exists.+--+-- NOTE: an 'Information' should be enough to construct+-- an error message if the 'Constraint' it is associated with+-- leads to an inconsistency.+class (Monad m, Buildable (Info m)) => Information m where+	type Info m++-- ** Class 'Infoable'+class Infoable a info where+	info_insert :: a -> info -> info++-- | A data type constructor to gather informations+-- from the 'Monad' stack of a solver.+-- data family Info (m :: * -> *)++-- ** Type 'Infoed'++-- | A data type to associate some @info@ to a value.+data Infoed info a+ =   Infoed+ {   information :: info+ ,   infoed :: a+ } deriving (Eq, Functor, Show)+instance (Buildable info, Buildable a) => Buildable (Infoed info a) where+	build Infoed { information, infoed } =+		build infoed <> " {- " <> build information <> " -}"++-- * Type 'Error'++-- | A data type constructor to gather errors+-- from the 'Monad' stack of a solver.+data family Error (m :: * -> *)++-- * Type 'Solver_Logable'++class Solver_Logable a m where+	log :: a -> m ()++-- * Class 'State'++class State st where+	state_name    :: st -> Text+	state_options :: st -> [Text]+	state_collect :: st -> [(Text, Text)]+	state_show    :: st -> Text+	+	-- state_show       = Text.pack . show+	state_options _  = []+	state_collect st = [(state_name st, state_show st)]++-- * Type 'Option'++data Option a+ =   Option+ {   option_current :: a+ ,   option_default :: a+ ,   option_description :: Text+ }++instance (Show a, Eq a) => Show (Option a) where+	show a =+		Text.unpack (option_description a)+		 <> ": "+		 <> show (option_current a)+		 <> show_default+		where+		show_default | option_current a == option_default a = " (default)"+		             | otherwise = ""+instance (Buildable a, Eq a) => Buildable (Option a) where+	build a =+		build (option_description a)+		 <> ": "+		 <> build (option_current a)+		 <> build_default+		where+		build_default | option_current a == option_default a = " (default)"+		              | otherwise = ""+instance Functor Option where+	fmap f a =+		a{ option_default = f (option_default a)+		 , option_current = f (option_current a) }++option :: a -> Text -> Option a+option a s =+	Option+	 { option_default     = a+	 , option_current     = a+	 , option_description = s+	 }
+ Language/LOL/Typing/Solver/Constraint.hs view
@@ -0,0 +1,256 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Solver.Constraint where++import Control.Monad (Monad(..), filterM, forM_, mapM, unless, when)+import Data.Bool+import qualified Data.Foldable as Foldable+import Data.Function (($), (.))+import Data.Functor (Functor(..), (<$>))+import qualified Data.List as List+import Data.Maybe (Maybe(..))+import Data.Monoid (Monoid(..), (<>))+import Data.Sequence (Seq, (<|))+import qualified Data.Sequence as Seq+import Data.String (String)+import qualified Data.Text as Text+import Data.Text.Buildable (Buildable(..))+import Data.Tuple (fst, snd)+import Prelude (error)+import Text.Show (Show(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Solver.Common+import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC+import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix as MC+import Language.LOL.Typing.Lib.Data.Empty (Empty(..))+import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build++-- * Type 'Constraint'++data Constraint m =+	forall c. (Show c, Buildable c, Substitutable c)+	 => Constraint c+	 (c -> m ()) -- solving strategy+	 (c -> m Bool) -- semantic check++instance Show (Constraint m) where+	show (Constraint c _ _) = show c+instance Buildable (Constraint m) where+	build (Constraint c _ _) = build c+instance Substitutable (Constraint m) where+	subvars (Constraint c _ _) = subvars c+	sub `substitute` (Constraint c f g) =+		Constraint (sub `substitute` c) f g+instance Monad m => Solvable (Constraint m) m where+	constraint_solver  (Constraint c f _) = f c+	constraint_checker (Constraint c _ f) = f c++-- | Return a 'Constraint' from a 'Solvable' instance.+constraint :: Solvable c m => c -> Constraint m+constraint c = Constraint c constraint_solver constraint_checker++constraints :: (Solvable c m, Functor f) => f c -> f (Constraint m)+constraints = (constraint <$>)++constraint_map :: (forall a. m1 a -> m2 a) -> Constraint m1 -> Constraint m2+constraint_map t (Constraint c f g) = Constraint c (t . f) (t . g)++-- ** Class 'Solvable'++-- | A type class for 'Constraint's solvable within a 'Monad'.+class (Show c, Buildable c, Substitutable c, Monad m) => Solvable c m where+	constraint_solver  :: c -> m ()+	constraint_checker :: c -> m Bool+	constraint_checker _ = return True++-- * Type 'State_Constraint'++-- | A 'State_Constraint' is parameterized over the 'Monad'+-- in which the 'Constraint's can be solved.+data State_Constraint m+ =   State_Constraint+ {   state_constraint_constraints  :: Seq (Constraint m)+     -- ^ A stack of 'Constraint's to solve.+ ,   state_constraint_checks       :: [(m Bool, String)]+     -- ^ Conditions to check (for the solved 'Constraint's).+ ,   state_constraint_errors       :: [(Info m, Error m)]+     -- ^ The detected errors.+ ,   state_constraint_option_stop  :: Option Bool+     -- ^ Whether to discard all remaining 'Constraint's after the first error.+ ,   state_constraint_option_check :: Option Bool+     -- ^ Whether to check constraint satisfaction afterwards.+ }++-- | Make 'State_Constraint' collectable as a 'State' instance+-- out of a 'Monad' stack.+type instance MC.Class State (State_Constraint m) = 'True++instance Show (State_Constraint m) where+	show = Build.string+instance Buildable (State_Constraint m) where+	build State_Constraint+	 { state_constraint_constraints+	 , state_constraint_errors+	 , state_constraint_checks } =+		Build.unlines $+		 [ "constraints: " <> Build.tuple+			 [ show (List.length state_constraint_constraints) <> " constraints"+			 , show (List.length state_constraint_errors) <> " errors"+			 , show (List.length state_constraint_checks) <> " checks"+			 ]+		 ] <> (("  " <>) . build <$>+			Foldable.toList state_constraint_constraints)+instance State (State_Constraint m) where+	state_name _ = "State_Constraint"+	state_show = Build.text+	state_options s =+	 [ Text.pack $ show $ state_constraint_option_stop  s+	 , Text.pack $ show $ state_constraint_option_check s+	 ]+instance Empty (State_Constraint m) where+	empty = State_Constraint+	 { state_constraint_constraints  = mempty+	 , state_constraint_errors       = mempty+	 , state_constraint_checks       = mempty+	 , state_constraint_option_stop  = option False "Stop solving at first error"+	 , state_constraint_option_check = option False "Check the solution"+	 }++-- * Class 'Solver_Constraint'++class+ ( MC.MonadStateFix State_Constraint m+ , Information m+ , Solver_Logable Log_Constraint m+ ) => Solver_Constraint m where+	constraint_push :: Constraint m -> m ()+	constraint_push c = do+		log $ Log_Constraint_Push c+		MC.modifyFix $ \(s::State_Constraint m) ->+			s{ state_constraint_constraints =+				c <| state_constraint_constraints s }+	+	constraint_push_many :: Seq (Constraint m) -> m ()+	constraint_push_many cs = do+		forM_ cs $ log . Log_Constraint_Push+		MC.modifyFix $ \(s::State_Constraint m) ->+			s{ state_constraint_constraints =+				cs <> state_constraint_constraints s }+	+	constraint_pop :: m (Maybe (Constraint m))+	constraint_pop = do+		cs <- MC.getsFix $ \(s::State_Constraint m) ->+			state_constraint_constraints s+		case Seq.viewl cs of+		 Seq.EmptyL -> return Nothing+		 (c Seq.:< state_constraint_constraints) -> do+			log $ Log_Constraint_Pop c+			MC.modifyFix (\(s::State_Constraint m) ->+				s{ state_constraint_constraints })+			return (Just c)+	+	constraint_discard :: m ()+	constraint_discard =+		MC.modifyFix $ \(s::State_Constraint m) ->+			s{ state_constraint_constraints = mempty }+	+	constraint_error_insert :: Error m -> Info m -> m ()+	constraint_error_insert err info = do+		MC.modifyFix (\(s::State_Constraint m) ->+			s{ state_constraint_errors =+				(info, err) : state_constraint_errors s })+		stop <- constraint_option_stop+		when (option_current stop)+			constraint_discard+	+	constraint_errors :: m [(Info m, Error m)]+	constraint_errors =+		MC.getsFix $ \(s::State_Constraint m) ->+			state_constraint_errors s+	+	constraint_error_info_update+	 :: (Info m -> m (Info m)) -> m ()+	constraint_error_info_update f = do+		errs <- constraint_errors+		state_constraint_errors <- do+			let g (info, err) = do+				info' <- f info+				return (info', err)+			g `mapM` errs+		MC.modifyFix $ \(s::State_Constraint m) ->+			s{ state_constraint_errors }+	+	-- | Add sanity checks for the solved 'Constraint's,+	-- performed when all 'Constraint's have been solved.+	--+	-- The first argument of 'constraint_check_insert' is+	-- a message, which is reported+	-- when the second argument evaluates+	-- to 'False' (in the 'Monad' @m@).+	constraint_check_insert :: String -> m Bool -> m ()+	constraint_check_insert text check =+		MC.modifyFix $ \(s::State_Constraint m) ->+			s{ state_constraint_checks =+				(check, text) : state_constraint_checks s}+	+	constraint_check_get :: m [(m Bool, String)]+	constraint_check_get =+		MC.getsFix $ \(s::State_Constraint m) ->+			state_constraint_checks s+	+	constraint_option_stop :: m (Option Bool)+	constraint_option_stop =+		MC.getsFix $ \(s::State_Constraint m) ->+			state_constraint_option_stop s+	+	constraint_option_check :: m (Option Bool)+	constraint_option_check =+		MC.getsFix (\(s::State_Constraint m) ->+			state_constraint_option_check s)+	+	constraint_solve :: m ()+	constraint_solve = do+		mc <- constraint_pop+		case mc of+		 Just c -> do+			constraint_solver c+			constraint_check_insert (show c) (constraint_checker c)+			constraint_solve+		 Nothing -> do+			check <- option_current <$> constraint_option_check+			errs <- fmap fst <$> constraint_errors+			when (check && List.null errs)+				constraint_check+	+	constraint_check :: m ()+	constraint_check = do+		ms <- constraint_check_get+		bs <- filterM ((not <$>) . fst) ms+		unless (List.null bs) $+			let err =+				"\n\n  Constraints violated:\n"+				 <> List.unlines (fmap (("  - " <>) . snd) bs) in+			error $ "constraint_check: " <> err++-- ** Type 'Log_Constraint'++data Log_Constraint+ =   forall c. (Show c, Buildable c) => Log_Constraint_Pop  c+ |   forall c. (Show c, Buildable c) => Log_Constraint_Push c+deriving instance Show Log_Constraint+instance Buildable Log_Constraint where+	build x =+		case x of+		 Log_Constraint_Pop  c -> "constraint_pop : " <> build c+		 Log_Constraint_Push c -> "constraint_push: " <> build c
+ Language/LOL/Typing/Solver/Greedy.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}++-- | The point at which point inconsistency is detected.+-- depends on the ordering of the 'Constraint's+-- and on the 'Solver's used.+--+-- Because choosing an ordering for the 'Constraint's+-- closely relates to the order in which types are unified (with 'mgu_with_synonyms'),+-- a /greedy 'Constraint' solver/, beeing highly sensitive+-- to the order in which it solves 'Constraint_Monotype_Unification's,+-- will report different 'Constraint's for different orders.+module Language.LOL.Typing.Solver.Greedy where++import Control.Monad (Monad)+import qualified Control.Monad.Classes as MC+import Data.Bool (Bool(..))+import Data.Sequence (Seq)+import Data.Text.Buildable (Buildable(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Solver.Common+import Language.LOL.Typing.Solver.Constraint+import Language.LOL.Typing.Solver.Monotype+import Language.LOL.Typing.Solver.Polytype+import Language.LOL.Typing.Solver.Class+import Language.LOL.Typing.Solver.Monad+import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.StateInstance as MC++-- * Type 'Solver_Greedy_Finite'++type Solver_Greedy_Finite info m+   = Solver info m Substitution_Finite++solver_greedy_finite ::+ ( sol ~ Solver_Greedy_Finite info m+ , res ~ Solver_Result (Info sol) (Error sol)+ , Monad m+ , Solvable constraint sol+ , MC.CansMonadStateInstance State (MC.EffState ()) m ~ '[ 'False ]+ , Buildable info+ , Infoable Info_Monotype info+ , Infoable Info_Polytype info+ , Infoable (Info_Class info) info+ ) => Solver_Config -> Seq constraint -> sol res+solver_greedy_finite = solver++-- * Type 'Solver_Greedy_Fixpoint'++type Solver_Greedy_Fixpoint info m+ =   Solver info m Substitution_Fixpoint++solver_greedy_fixpoint ::+ ( sol ~ Solver_Greedy_Fixpoint info m+ , res ~ Solver_Result (Info sol) (Error sol)+ , Monad m+ , Solvable constraint sol+ , MC.CansMonadStateInstance State (MC.EffState ()) m ~ '[ 'False ]+ , Buildable info+ , Infoable Info_Monotype info+ , Infoable Info_Polytype info+ , Infoable (Info_Class info) info+ ) => Solver_Config -> Seq constraint -> sol res+solver_greedy_fixpoint = solver
+ Language/LOL/Typing/Solver/Monad.hs view
@@ -0,0 +1,304 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Solver.Monad where++import Control.Applicative (Applicative(..))+import Control.Monad (Monad(..))+import qualified Control.Monad.Classes as MC+import qualified Control.Monad.Classes.Run as MC+import qualified Control.Monad.Trans.State.Lazy as SL+import Data.Bool+import Data.Eq (Eq(..))+import Data.Function (($), (.))+import Data.Functor ((<$>))+import qualified Data.List as List+import Data.Map.Strict (Map)+import Data.Monoid (Monoid(..), (<>))+import Data.Ord (Ord(..), max)+import Data.Sequence (Seq)+import Data.Text.Buildable (Buildable(..))+import Prelude (Num(..))+import Text.Show (Show(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Solver.Common+import Language.LOL.Typing.Solver.Constraint+import Language.LOL.Typing.Solver.Monotype+import Language.LOL.Typing.Solver.Polytype+import Language.LOL.Typing.Solver.Class+import Language.LOL.Typing.Lib.Data.Empty (Empty(..))+import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC+import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix as MC+import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.StateInstance as MC+import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build++-- * Type 'Solver'++-- | A 'Monad' stack gathering all the @Solver_*@.+--+-- * @m@ is a base 'Monad'+--   (for instance within which 'Solver_Log's+--   can be handled during the solving).+-- * @info@ is a polymorphic type to hold informations+--   about the origin of the 'Constraint's.+-- * @monotype_substitution@ is a for accumulating known 'Monotype's+--   (for example it can be: 'Substitution_Finite' or 'Substitution_Fixpoint').+type Solver info m monotype_substitution =+	MC.StateLazyFixT State_Constraint+	(SL.StateT (State_Monotype monotype_substitution)+	(SL.StateT (State_Polytype info)+	(SL.StateT (State_Class info)+	(WriterT Solver_Log+	m))))++-- * Type 'Solver_Log'++data Solver_Log+ =   Solver_Log_States [MC.Instance State]+     -- ^ Logs summarizing the 'State's.+ |   Solver_Log_Constraint Log_Constraint+     -- ^ Log of 'Constraint' handling.+ |   Solver_Log_Class Log_Class+     -- ^ Log of 'Class' handling.+ |   Solver_Log_Polytype Log_Polytype+     -- ^ Log of 'Polytype' handling.++instance Monad m+ => Solver_Logable Log_Constraint (Solver info m sub) where+	log = MC.tell . Solver_Log_Constraint+instance Monad m+ => Solver_Logable Log_Class (Solver info m sub) where+	log = MC.tell . Solver_Log_Class+instance Monad m+ => Solver_Logable Log_Polytype (Solver info m sub) where+	log = MC.tell . Solver_Log_Polytype++log_states+ :: forall m.+ ( MC.MonadWriter Solver_Log m+ , MC.MonadStateInstance State m+ , Solver_Constraint m+ ) => m ()+log_states = do+	(states::[MC.Instance State]) <- MC.getInstance+	MC.tell $ Solver_Log_States states++-- | Type synonym to 'MC.CustomWriterT',+-- /eta-reduced/ to fit in 'Solver'.+type WriterT w m = MC.CustomWriterT' w m m++-- * Type 'Solver_Info'++data Solver_Info info+ =   Solver_Info_Class    (Info_Class info)+ |   Solver_Info_Monotype Info_Monotype+ |   Solver_Info_Polytype Info_Polytype+ deriving (Eq, Show)+instance Buildable info => Buildable (Solver_Info info) where+	build x =+		case x of+		 Solver_Info_Class    i -> build i+		 Solver_Info_Monotype i -> build i+		 Solver_Info_Polytype i -> build i+instance Buildable info => Buildable [Solver_Info info] where+	build = Build.list++instance+ ( Monad m+ , Buildable info+ ) =>  Information (Solver info m sub) where+	type Info        (Solver info m sub) = info++data instance Error (Solver info m sub)+ = Solver_Error_Class    Error_Class+ | Solver_Error_Monotype Error_Monotype+ | Solver_Error_Polytype Error_Polytype+ deriving (Eq, Show)++instance+ ( Monad m+ , Buildable info+ ) => Solver_Constraint (Solver info m sub)+instance+ ( Monad m+ , Buildable info+ , Solver_Monotype_Substitution sub+ , Infoable Info_Monotype info+ ) =>  Solver_Monotype     (Solver info m sub) where+	type Solver_Monotype_Sub (Solver info m sub) = sub+	error_monotype = Solver_Error_Monotype+instance+ ( Monad m+ , Buildable info+ , info ~ Info (Solver info m sub)+ , Infoable Info_Polytype info+ ) => Solver_Polytype (Solver info m sub) where+	error_polytype = Solver_Error_Polytype+instance+ ( Monad m+ , Buildable info+ , info ~ Info (Solver info m sub)+ , Infoable Info_Monotype info+ , Infoable Info_Polytype info+ , Infoable (Info_Class info) info+ , Solver_Monotype_Substitution sub+ ) => Solver_Class (Solver info m sub) where+	error_class = Solver_Error_Class++-- | Return within base 'Monad' @m@.+-- the 'Solver_Result' produced+-- by evaluating the given 'Solver',+-- while using the given 'Solver_Log' handler.+solve ::+ ( sol ~ Solver info m sub+ , res ~ Solver_Result (Info sol) (Error sol)+ , Monad m+ , Empty sub+ ) => (Solver_Log -> m ())+ -> sol res -> m res+solve writer_log =+	MC.evalWriterWith writer_log .+	MC.evalStateLazy    empty .+	MC.evalStateLazy    empty .+	MC.evalStateLazy    empty .+	MC.evalStateLazyFix empty++-- | Return the 'Solver' produced+-- by the given 'Solver_Config' and 'Contraint's.+solver ::+ ( sol ~ Solver info m sub+ , res ~ Solver_Result (Info sol) (Error sol)+ , Monad m+ , Solver_Monotype_Substitution sub+ , Solvable constraint sol+ , MC.CansMonadStateInstance State (MC.EffState ()) m ~ '[ 'False ]+   -- NOTE: require that the inner 'Monad' does not have 'State' instances.+ , Buildable info+ , Infoable Info_Monotype info+ , Infoable Info_Polytype info+ , Infoable (Info_Class info) info+ ) => Solver_Config -> Seq constraint -> sol res+solver cfg cs = do+	solver_init cs cfg+	solver_run cs+	solver_result++-- | Run the solvers of a 'Monad' over the given 'Constraint's.+solver_run ::+ ( Solvable constraint m+ , Solver_Constraint m+ , Solver_Monotype m+ , Solver_Polytype m+ , Solver_Class m+ , MC.MonadWriter Solver_Log m+ , MC.MonadStateInstance State m+ ) => Seq constraint -> m ()+solver_run cs = do+	constraint_push_many $ constraints cs+	log_states+	constraint_solve+	monotype_substitution_consistentify+	polytype_rigids_check+	class_ambiguities+	log_states++-- ** Type 'Solver_Config'++data Solver_Config+ =   Solver_Config+ {   solver_config_class_env :: Class_Env+ ,   solver_config_freshvar  :: Freshvar+ ,   solver_config_synotypes :: Synotype_Substitution+ ,   solver_config_check     :: Bool+ ,   solver_config_stop      :: Bool+ }++-- | Return a 'Solver_Config'.+solver_config :: Solver_Config+solver_config =+	Solver_Config+	 { solver_config_class_env = class_env_default+	 , solver_config_freshvar  = -1+	 , solver_config_synotypes = empty+	 , solver_config_check     = option_current $ state_constraint_option_check empty+	 , solver_config_stop      = option_current $ state_constraint_option_stop  empty+	 }++-- | Initialize a solver 'Monad' with given 'Solver_Config'.+solver_init ::+ forall m constraints.+ ( Substitutable constraints+ , Solver_Constraint m+ , Solver_Polytype m+ , Solver_Class m+ ) => constraints -> Solver_Config -> m ()+solver_init cs cfg = do+	polytype_freshvar_set freshvar+	synotype_substitution_set $+		solver_config_synotypes cfg+	class_env_set $+		solver_config_class_env cfg+	MC.modifyFix $ \(s::State_Constraint m) ->+		s{ state_constraint_option_check =+			(state_constraint_option_check s)+			 { option_current = solver_config_check cfg }+		 , state_constraint_option_stop =+			(state_constraint_option_stop s)+			 { option_current = solver_config_stop cfg }+		 }+	where+	freshvar+	 | solver_config_freshvar cfg < 0 = 1 + List.maximum (-1 : subvars cs)+	 | otherwise                      = solver_config_freshvar cfg++-- ** Type 'Solver_Result'++data Solver_Result info err+ =   Solver_Result+ {   solver_result_freshvar    :: Freshvar+ ,   solver_result_monotypes   :: Substitution_Fixpoint+ ,   solver_result_polytypes   :: Polysub+ ,   solver_result_quantifiers :: Map Monovar [Quantifier]+ ,   solver_result_qualifiers  :: [Class_Qualifier]+     -- ^ 'Class_Qualifier's assumed to hold.+ ,   solver_result_errors      :: [(info, err)]+ }++instance Empty (Solver_Result info err) where+	empty = mempty+instance Monoid (Solver_Result info err) where+	mempty = Solver_Result 0 mempty mempty mempty mempty mempty+	mappend+	 (Solver_Result fr1 ms1 ps1 qts1 qls1 es1)+	 (Solver_Result fr2 ms2 ps2 qts2 qls2 es2) =+		Solver_Result+		 (fr1 `max` fr2)+		 (ms1 <> ms2)+		 (ps1 <> ps2)+		 (qts1 <> qts2)+		 (qls1 <> qls2)+		 (es1 <> es2)++-- | Return a 'Solver_Result' from a solver 'Monad'.+solver_result ::+ ( Solver_Constraint m+ , Solver_Monotype m+ , Solver_Polytype m+ , Solver_Class m+ ) => m (Solver_Result (Info m) (Error m))+solver_result =+	Solver_Result+	 <$> polytype_freshvar+	 <*> monotype_substitution+	 <*> polytype_substitution+	 <*> polytype_quantifiers+	 <*> class_qualifiers_reduced+	 <*> constraint_errors
+ Language/LOL/Typing/Solver/Monotype.hs view
@@ -0,0 +1,265 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+-- | Type inference for /monomorphic types/.+module Language.LOL.Typing.Solver.Monotype where++import Control.Monad (Monad(..), mapM)+import qualified Control.Monad.Classes as MC+import Data.Bool+import Data.Either (Either(..))+import Data.Eq (Eq(..))+import Data.Function (($), (.), id)+import Data.Int (Int)+import qualified Data.List as List+import qualified Data.Map.Strict as Map+import Data.Maybe (Maybe(..), fromMaybe)+import Data.Monoid (Monoid(..), (<>))+import Data.Text (Text)+import Data.Text.Buildable (Buildable(..))+import Data.Tuple (uncurry)+import Prelude (error)+import Text.Show (Show(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Solver.Common+import Language.LOL.Typing.Solver.Constraint+import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC+import Language.LOL.Typing.Lib.Data.Empty (Empty(..))+import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build++-- * Type 'State_Monotype'++data State_Monotype sub+ =   State_Monotype+ {   state_monotype_substitution :: sub+     -- ^ Known 'Monovar's.+ ,   state_monotype_synotypes :: Synotype_Substitution+     -- ^ Known 'Synotype's.+ } deriving (Show)++-- | Make 'State_Monotype' collectable as a 'State' instance+-- out of a 'Monad' stack.+type instance MC.Class State (State_Monotype sub) = 'True++instance Buildable sub => Buildable (State_Monotype sub) where+	build State_Monotype+	 { state_monotype_substitution = sub+	 , state_monotype_synotypes    = synotys+	 } =+		Build.unlines+		 [ "monotypes: "+		 , Build.indent "  " sub+		 , "synotypes: " <> build synotys+		 ]+instance Buildable sub => State (State_Monotype sub) where+	state_name _ = "State_Monotype"+	state_show = Build.text+instance Empty sub => Empty (State_Monotype sub) where+	empty = State_Monotype+		 { state_monotype_substitution = empty+		 , state_monotype_synotypes    = empty+		 }++-- * Class 'Solver_Monotype'++-- | A type class for 'Monad's containing a 'Substitution',+-- that may be in an inconsistent state.+class+ ( Solver_Constraint m+ , Monad m+ , MC.MonadState (State_Monotype (Solver_Monotype_Sub m)) m+ , Solver_Monotype_Substitution (Solver_Monotype_Sub m)+ , Infoable Info_Monotype (Info m)+ ) => Solver_Monotype (m :: * -> *) where+	error_monotype :: Error_Monotype -> Error m+	type Solver_Monotype_Sub m+	+	monotype_substitution :: m Substitution_Fixpoint+	monotype_substitution = MC.gets $+	 \(s::State_Monotype (Solver_Monotype_Sub m)) ->+		monotype_substitution_fixpoint $+		state_monotype_substitution s+	+	-- | Lookup the value of a 'Monotype_Var' in the substitution.+	monotype_lookup :: Monovar -> m Monotype+	monotype_lookup v = MC.gets $+	 \(s::State_Monotype (Solver_Monotype_Sub m)) ->+		fromMaybe (Monotype_Var v) $+		substitution_lookup v $+		state_monotype_substitution s+	+	-- | Apply the 'Substitution' to any instance of 'Substitutable'.+	monotype_substitute :: Substitutable a => a -> m a+	monotype_substitute a = do+		let subvars_a = subvars a+		monotys <- monotype_lookup `mapM` subvars_a+		let sub = substitution_finite (List.zip subvars_a monotys)+		return (sub `substitute` a)+	+	-- | Unify two 'Monotype's.+	--+	-- NOTE: In the end, the two 'Monotype's should be equivalent+	-- under 'monotype_substitution'. However, unifying two 'Monotype's+	-- may bring the substitution into an /inconsistent state/.+	monotype_unify :: Info m -> Monotype -> Monotype -> m ()+	monotype_unify info ty1 ty2 = do+		synotys <- synotype_substitution+		subty1 <- monotype_substitute ty1+		subty2 <- monotype_substitute ty2+		case monotype_substitution_unify+		 synotys (ty1, subty1) (ty2, subty2) of+		 Left err ->+			constraint_error_insert+			 (error_monotype $ Error_Monotype_Unification err)+			 info+		 Right (_log, uni) -> -- do+			-- constraint_log "monotype_unify" log+			MC.modify $ \(s::State_Monotype (Solver_Monotype_Sub m)) ->+				s{state_monotype_substitution =+					uni $ state_monotype_substitution s }+	-- | Make 'state_monotype_substitution' consistent.+	--+	-- NOTE: Only relevant for 'Substitution' states+	-- that can be inconsistent+	-- (eg. the /type graph/ substitution state).+	monotype_substitution_consistentify :: m ()+	monotype_substitution_consistentify = return ()+	+	synotype_substitution :: m Synotype_Substitution+	synotype_substitution = MC.gets $+	 \(s::State_Monotype (Solver_Monotype_Sub m)) ->+		state_monotype_synotypes s+	synotype_substitution_set :: Synotype_Substitution -> m ()+	synotype_substitution_set state_monotype_synotypes =+		MC.modify $ \(s::State_Monotype (Solver_Monotype_Sub m)) ->+			s{ state_monotype_synotypes }++-- ** Class 'Solver_Monotype_Substitution'++class+ ( Buildable sub+ , Show sub+ , Monoid sub+ , Substitution sub+ ) => Solver_Monotype_Substitution sub where+	monotype_substitution_fixpoint :: sub -> Substitution_Fixpoint+	monotype_substitution_unify+	 :: Synotype_Substitution+	 -> (Monotype, Monotype)+	 -> (Monotype, Monotype)+	 -> Either Unification_Error (Text, sub -> sub)++instance Solver_Monotype_Substitution Substitution_Finite where+	monotype_substitution_fixpoint = Substitution_Fixpoint+	monotype_substitution_unify synotys (_origty1, ty1) (_origty2, ty2) =+		case mgu_with_synotypes synotys ty1 ty2 of+		 Left err -> Left err+		 Right (_, uni) -> Right $ (Build.text uni,) $ substitution_finite_union uni+instance Solver_Monotype_Substitution Substitution_Fixpoint where+	monotype_substitution_fixpoint = id+	monotype_substitution_unify synotys (origty1, ty1) (origty2, ty2) =+		case mgu_with_synotypes synotys ty1 ty2 of+		 Left err -> Left err+		 Right (was_synexpanded, uni) ->+			Right $ (Build.text uni,) $+				(if was_synexpanded then subexpand else id) .+				subunion uni+			where+			subunion x (Substitution_Fixpoint y) =+				Substitution_Fixpoint $+				(`Map.union` y) $+				Map.fromList+				 [ (v, fromMaybe (Monotype_Var v) $ substitution_lookup v x)+				 | v <- substitution_domain x+				 ]+			subexpand =+				substitution_fixpoint_synexpand synotys origty2 unity .+				substitution_fixpoint_synexpand synotys origty1 unity+			unity =+				fromMaybe (error "monotype_substitution_unify: types not unifiable") $+				mgt_with_synotypes synotys+				 (uni `substitute` ty1)+				 (uni `substitute` ty2)++-- TODO: understand and test this code better…++-- NOTE: Top: The key idea is as follows:+-- try to minimize the number of expansions by 'Synotype's.+-- If a type is expanded, then this should be recorded in the substitution.+-- Invariant of this function should be that "atp" (the first type) can be+-- made equal to "utp" (the second type) with a number of 'Synotype' expansions+substitution_fixpoint_synexpand+ :: Synotype_Substitution+ -> Monotype+ -> Monotype+ -> Substitution_Fixpoint+ -> Substitution_Fixpoint+substitution_fixpoint_synexpand syns =+	go+	where+	go :: Monotype -> Monotype -> Substitution_Fixpoint -> Substitution_Fixpoint+	go atp utp original =+		case (app_spine_left atp, app_spine_left utp) of+		 (App_Spine (Monotype_Var i) [], _) -> writeIntType i utp original+		 (  App_Spine (Monotype_Const s) as+		  , App_Spine (Monotype_Const t) bs+		  ) | s == t && not (is_panthom_synotype syns s) ->+			List.foldr (uncurry go) original (List.zip as bs)+		 (App_Spine (Monotype_Const _) _, _) ->+			case synexpand_top_step (synotypes syns) atp of+			 Just atp' -> go atp' utp original+			 Nothing -> error $ "substitution_fixpoint_synexpand: inconsistent types(1)" <> show (atp, utp)+		 _ -> error $ "substitution_fixpoint_synexpand: inconsistent types(2)" <> show (atp, utp)+	+	writeIntType :: Int -> Monotype -> Substitution_Fixpoint -> Substitution_Fixpoint+	writeIntType i utp original@(Substitution_Fixpoint fm) =+		case Map.lookup i fm of+		 Nothing ->+			case utp of+			 Monotype_Var j | i == j -> original+			 _ -> Substitution_Fixpoint (Map.insert i utp fm)+		 Just atp ->+			case (app_spine_left atp, app_spine_left utp) of+			 (App_Spine (Monotype_Var j) [], _) -> writeIntType j utp original+			 (  App_Spine (Monotype_Const s) as+			  , App_Spine (Monotype_Const t) bs+			  ) | s == t ->+				List.foldr (uncurry go) original (List.zip as bs)+			 (App_Spine (Monotype_Const _) _, _) ->+				case synexpand_top_step (synotypes syns) atp of+				 Just atp' -> writeIntType i utp (Substitution_Fixpoint (Map.insert i atp' fm))+				 Nothing ->+					-- NOTE: Top: FIX!!!   HERSCHRIJVEN!+					-- de volgende situatie trad op:+					--    utp=Categorie, atp = [Char]+					--  met type Categorie = String+					case synexpand_top_step (synotypes syns) utp of+					 Just utp' -> writeIntType i atp (Substitution_Fixpoint (Map.insert i utp' fm))+					 Nothing -> error $ "substitution_fixpoint_synexpand: inconsistent types(1)" <> show (i, utp, atp)+			 _ -> error "substitution_fixpoint_synexpand: inconsistent types(2)"++-- ** Class 'Info_Monotype'++data Info_Monotype+ =   Info_Monotype_Unification Monotype Monotype+ deriving (Eq, Show)++instance Buildable Info_Monotype where+	build x =+		case x of+		 Info_Monotype_Unification m1 m2 ->+			"Info_Monotype_Unification " <> Build.tuple [m1, m2]++-- ** Type 'Error_Monotype'++data Error_Monotype+ =   Error_Monotype_Unification Unification_Error+ deriving (Eq, Show)
+ Language/LOL/Typing/Solver/Polytype.hs view
@@ -0,0 +1,352 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+-- | Type inference for /parametric polymorphism/.+module Language.LOL.Typing.Solver.Polytype where++import Control.Monad (Monad(..), mapM, forM_, foldM, sequence)+import qualified Control.Monad.Classes as MC+import Data.Bool+import Data.Eq (Eq(..))+import Data.Function (($), flip)+import Data.Functor ((<$>))+import qualified Data.List as List+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Data.Maybe (Maybe(..))+import Data.Monoid (Monoid(..), (<>))+import Data.Text.Buildable (Buildable(..))+import Data.Tuple (snd)+import Prelude (Num(..), error)+import Text.Show (Show(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Solver.Common+import Language.LOL.Typing.Solver.Constraint+import Language.LOL.Typing.Solver.Monotype+import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC+import Language.LOL.Typing.Lib.Data.Default (Default(..))+import Language.LOL.Typing.Lib.Data.Empty (Empty(..))+import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build++-- * Type 'State_Polytype'++data State_Polytype info+ =   State_Polytype+ {   state_polytype_freshvar :: Freshvar+     -- ^ An incrementing counter+     -- for fresh 'Monovar's, fresh 'Rigvar's, or 'Polyvar's.+ ,   state_polytype_substitution :: Polysub+     -- ^ Known 'Polytype's.+ ,   state_polytype_rigids :: [Infoed info ([Rigvar], [Rigtype])]+     -- ^ The 'Rigvar's introduced as 'Freshvar's by 'polytype_rigvarify'+     -- with the 'Rigtype's from the /typing context/+     -- (used by 'polytype_rigids_check').+ , state_polytype_quantifiers :: Map Monovar [Quantifier]+     -- ^ Map every 'Monovar' unified with an instance of a 'Polytype'+     -- to the 'Freshvar's allocated to instantiate+     -- the 'quantifiers' of this 'Polytype'.+ } deriving (Show)++-- | Make 'State_Polytype' collectable as a 'State' instance+-- out of a 'Monad' stack.+type instance MC.Class State (State_Polytype info) = 'True++instance Buildable info => Buildable (State_Polytype info) where+	build State_Polytype+	 { state_polytype_freshvar     = freshvar+	 , state_polytype_substitution = polytys+	 , state_polytype_rigids       = rigids+	 , state_polytype_quantifiers    = instances+	 } =+		Build.unlines $+		 [ "freshvar: " <> build freshvar+		 , "rigids: " ] <>+			(("  " <>) <$>+			List.foldr (\(Infoed info (rigvas, monotys)) ->+				((Build.tuple+				 [ Build.list rigvas+				 , Build.list monotys+				 ] <> " {- " <> build info <> " -}") :)+			 ) [] rigids) <>+		 [ "polytypes: " ] <>+			Map.foldrWithKey (\v ty ->+				(("  p" <> build v <> " == " <>+				build (def::Quantification_Build_Options, ty)) :)+			 ) [] polytys <>+		 [ "instances: " ] <>+			Map.foldrWithKey (\v vs ->+				(("  " <> build (Monotype_Var v) <> " -> " <>+				Build.list (Monotype_Var <$> vs)) :)+			 ) [] instances+instance Buildable info => State (State_Polytype info) where+	state_name _ = "State_Polytype"+	state_show = Build.text+instance Empty (State_Polytype m) where+	empty =+		State_Polytype+		 { state_polytype_freshvar     = 0+		 , state_polytype_substitution = mempty+		 , state_polytype_rigids       = mempty+		 , state_polytype_quantifiers    = mempty+		 }++-- * Class 'Solver_Polytype'++class+ ( Solver_Constraint m+ , MC.MonadState (State_Polytype (Info m)) m+ , Infoable Info_Polytype (Info m)+ , Solver_Logable Log_Polytype m+ ) => Solver_Polytype m where+	error_polytype :: Error_Polytype -> Error m+	+	polytype_freshvar :: m Freshvar+	polytype_freshvar =+		MC.gets $ \(s::State_Polytype (Info m)) ->+			state_polytype_freshvar s+	polytype_freshvar_set :: Freshvar -> m ()+	polytype_freshvar_set state_polytype_freshvar =+		MC.modify $ \(s::State_Polytype (Info m)) ->+			s{ state_polytype_freshvar }+	+	polytype_substitution :: m Polysub+	polytype_substitution =+		MC.gets $ \(s::State_Polytype (Info m)) ->+			state_polytype_substitution s+	polytype_insert :: Polyvar -> Polytype -> m ()+	polytype_insert var polyty = do+		log $ Log_Polytype_Insert var polyty+		MC.modify $ \(s::State_Polytype (Info m)) ->+			s{ state_polytype_substitution =+				Map.insert var polyty $+				state_polytype_substitution s+			 }+	polytype_lookup+	 :: Polytyref -> m Polytype+	polytype_lookup polyref =+		case polyref of+		 Polytyref polyty -> return polyty+		 Polytyref_Var v ->+			Map.findWithDefault+			 (error "polytype_lookup: Polytyref_Var not found in polytype_substitution")+			 v <$> polytype_substitution+	+	-- | 'Rigvar' variables+	--+	-- NOTE: used by 'polytype_rigids_check'.+	polytype_rigids :: m [Infoed (Info m) ([Rigvar], [Rigtype])]+	polytype_rigids =+		MC.gets $ \(s::State_Polytype (Info m)) ->+			state_polytype_rigids s+	polytype_rigids_set :: [Infoed (Info m) ([Rigvar], [Rigtype])] -> m ()+	polytype_rigids_set state_polytype_rigids =+		MC.modify $ \(s::State_Polytype (Info m)) ->+			s{ state_polytype_rigids }+	polytype_rigids_push+	 :: Infoed (Info m) ([Rigvar], [Rigtype]) -> m ()+	polytype_rigids_push rig{-@(Infoed info (vs, ms))-} = do+		--constraint_log "polytype_rigids_push"+		-- (Infoed info (Build.tuple [Build.list vs, Build.list ms]))+		rigs <- polytype_rigids+		polytype_rigids_set (rig:rigs)+	+	-- | Return the 'quantified' of the given 'Forall'+	-- with the 'quantifiers' 'substitute'd with 'Freshvar's.+	-- Also, if the given 'Monotype' is a 'Monotype_Var',+	-- and at least one 'Freshvar' has been allocated,+	-- record them in the 'State_Polytype'.+	polytype_instantiate+	 :: Substitutable a => Monotype -> Forall a -> m a+	polytype_instantiate monoty quant = do+		freshvar <- polytype_freshvar+		let Unquantification freshvar' a = unquantify_forall freshvar quant+		polytype_freshvar_set freshvar'+		case monoty of+		 Monotype_Var monovar ->+			case [freshvar..freshvar'-1] of+			 [] -> return ()+			 fs ->+				MC.modify $ \(s::State_Polytype (Info m)) ->+					s{ state_polytype_quantifiers =+						Map.insert monovar fs $+						state_polytype_quantifiers s+					 }+		 _ -> return ()+		return a+	polytype_quantifiers :: m (Map Monovar [Quantifier])+	polytype_quantifiers =+		MC.gets $ \(s::State_Polytype (Info m)) ->+			state_polytype_quantifiers s+	+	-- | Like 'rigvarify', but 'unquantify'+	-- by using fresh 'Monovar's ('Freshvar') instead of fresh 'Const's ('Rigvar's).+	--+	-- NOTE: useful for the 'quantifiers' of a 'Polytype',+	-- maintaining a list of 'Rigvar's in 'state_polytype_rigids'.+	polytype_rigvarify+	 :: Substitutable a+	 => Info m -> [Rigtype] -> Forall a -> m a+	polytype_rigvarify info rigtys forall_a = do+		freshvar <- polytype_freshvar+		let Unquantification freshvar' a =+			unquantify_forall freshvar forall_a+		polytype_freshvar_set freshvar'+		polytype_rigids_push $+			Infoed info ([freshvar .. freshvar'-1], rigtys)+		return a++polytype_rigids_check+ :: forall m.+ ( Solver_Constraint m+ , Solver_Monotype m+ , Solver_Polytype m+ ) => m ()+polytype_rigids_check =+	polytype_rigids >>=+		rigvars_substitution >>=+		check_rigvars_are_mapped_to_vars >>=+		check_rigvars_are_mapped_to_different_vars >>=+		check_monotys_have_no_rigvar >>=+		rigvars_substituted >>=+		polytype_rigids_set+		 -- NOTE: restore the 'Rigvar's+		 -- which are consistent with the current 'monotype_substitution'.+	where+		-- | Return the 'Monotype's toward which 'monotype_substitution'+		-- maps the given 'Rigvar's.+		rigvars_substitution+		 ::   [Infoed (Info m) ([Rigvar]            , [Rigtype])]+		 -> m [Infoed (Info m) ([(Rigvar, Monotype)], [Rigtype])]+		rigvars_substitution =+			mapM $ \(Infoed info (rigvas, rigtys)) -> do+				subtys <- monotype_lookup `mapM` rigvas+				return $ Infoed info+				 ( List.zip rigvas subtys+				 , rigtys )+		-- | Return the 'Monovar's of the given 'Monotype's which are 'Monotype_Var's.+		check_rigvars_are_mapped_to_vars+		 ::   [Infoed (Info m) ([(Rigvar, Monotype)], [Rigtype])]+		 -> m [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])]+		check_rigvars_are_mapped_to_vars tochecks = do+			let (goods, bads) =+				List.foldr+				 (\i@(Infoed info (rigvars_monotys, rigtys)) (gs, bs) ->+					let (rigvars_subvars::Maybe [(Rigvar, Monovar)]) =+						sequence $ (\(rig, ty) ->+							case ty of+							 Monotype_Var v -> Just (rig, v)+							 _ -> Nothing+						 ) <$> rigvars_monotys in+					case rigvars_subvars of+					 Just x  -> (Infoed info (x, rigtys):gs, bs)+					 Nothing -> (gs, i:bs)+				 )+				 ([], [])+				 tochecks+			forM_ bads $ \(Infoed info (rigvars_monotys, _monotys)) ->+				constraint_error_insert+				 (error_polytype $ Error_Polytype_Rigid_type_mismatch rigvars_monotys)+				 info+			return goods+		-- | Return the 'Rigvar's which are injectively mapped to the given 'Monovar's.+		check_rigvars_are_mapped_to_different_vars+		 ::   [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])]+		 -> m [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])]+		check_rigvars_are_mapped_to_different_vars tochecks = do+			let (subvars_rigvars::Map Monovar [Rigvar]) =+				Map.fromListWith (flip (<>))+				 [ (subvar, [rigvar])+				 | Infoed _ (rigvars_subvars, _) <- tochecks+				 , (rigvar, subvar) <- rigvars_subvars+				 ]+			let subvars_colliding_rigvars =+				Map.filter+				 (\l -> case l of { [] -> False; [_] -> False; _ -> True })+				 subvars_rigvars+			let (goods, bads) =+				List.partition+				 (\(Infoed _ (rigvars_subvars, _)) ->+					List.null $ (subvars_colliding `List.intersect`) $+					snd <$> rigvars_subvars)+				 tochecks+				where subvars_colliding = Map.keys subvars_colliding_rigvars+			forM_ bads $ \(Infoed info (rigvars_subvars, _)) ->+				constraint_error_insert+				 (error_polytype $ Error_Polytype_Rigid_injectivity_lost $+					Map.fromList+					 [ (subvar, rigvas)+					 | (_rigvar, subvar) <- rigvars_subvars+					 , Just rigvas <- [Map.lookup subvar subvars_colliding_rigvars]+					 ])+				 info+			return goods+		check_monotys_have_no_rigvar+		 ::   [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])]+		 -> m [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])]+		check_monotys_have_no_rigvar =+			foldM (\goods this@(Infoed info (rigvars_subvars, rigtys)) -> do+				rigtys' <- monotype_substitute rigtys+				case subvars rigtys' `List.intersect` (snd <$> rigvars_subvars) of+				 []  -> return (this:goods)+				 rigvars_escaping -> do+					constraint_error_insert+					 (error_polytype $ Error_Polytype_Rigid_escaping rigvars_escaping)+					 info+					return goods+			 ) []+		rigvars_substituted+		 ::   [Infoed (Info m) ([(Rigvar, Monovar)], [Rigtype])]+		 -> m [Infoed (Info m) ([Rigvar], [Rigtype])]+		rigvars_substituted checkeds =+			return+			 [ Infoed info (snd <$> rigvars_subvars, rigtys)+			 | Infoed info (        rigvars_subvars, rigtys) <- checkeds+			 ]++-- * Class 'Info_Polytype'++data Info_Polytype+ =   Info_Polytype_Instantiated Polytype+ |   Info_Polytype_Rigidified [Rigtype] Polytype+ deriving (Eq, Show)++instance Buildable Info_Polytype where+	build x =+		case x of+		 Info_Polytype_Instantiated p ->+			"Info_Polytype_Instantiated " <> build p+		 Info_Polytype_Rigidified rs p ->+			"Info_Polytype_Rigidified " <> Build.list rs <> " " <> build p++-- * Type 'Error_Polytype'++data Error_Polytype+ =   Error_Polytype_Rigid_type_mismatch [(Rigvar, Monotype)]+     -- ^ A 'Rigvar' is mapped by the current 'monotype_substitution'+     -- to a 'Monotype' which is not a 'Monotype_Var'.+ |   Error_Polytype_Rigid_injectivity_lost (Map Monovar [Rigvar])+     -- ^ 'Map' of 'Monovar's reached by at least two distincts 'Rigvar's.+ |   Error_Polytype_Rigid_escaping [Rigvar]+     -- ^ Some 'Rigvar's escape via a 'Rigtype'.+ deriving (Eq, Show)++-- ** Type 'Log_Polytype'++data Log_Polytype+ =   Log_Polytype_Insert Polyvar Polytype+ deriving (Show)+instance Buildable Log_Polytype where+	build x =+		case x of+		 Log_Polytype_Insert var polyty ->+			"polytype_insert : " <>+			build (Polytyref_Var var) <> " == " <> build polyty
+ Language/LOL/Typing/Solver/Test.hs view
@@ -0,0 +1,510 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Solver.Test where++import Control.Arrow (second)+import Control.Monad (Monad(..))+import Data.Bool+import Data.Either (Either(..))+import Data.Function (($), (.))+import Data.Functor ((<$>))+-- import Data.Functor.Identity (Identity(..))+import Data.Int (Int)+import qualified Data.List as List+import qualified Data.Map.Strict as Map+import Data.Maybe ({-Maybe(..),-} fromMaybe)+import Data.Monoid ((<>))+import Data.Sequence (Seq)+import Data.String (IsString(..))+-- import Data.Text (Text)+import qualified Data.Text as Text+import Data.Text.Buildable (Buildable(..))+-- import qualified Data.Text.IO as Text+import qualified Data.Text.Lazy.Builder as Build+import qualified Data.Text.Lazy.IO as TL+-- import Data.Tuple (fst)+import Prelude (Num(..), error)+import System.IO (IO)+-- import Test.HUnit hiding (test)+import Test.Tasty+import Test.Tasty.HUnit+import Text.Show (Show(..))++import Language.LOL.Typing.Type+import Language.LOL.Typing.Expr+import Language.LOL.Typing.Solver+import Language.LOL.Typing.Collect.Constraint+-- import Language.LOL.Typing.Collect.Grammar+import qualified Language.LOL.Typing.Collect.Grammar as Collect+import Language.LOL.Typing.Lib.Data.Default (Default(..))+import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC+import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build++-- Convenient instances+instance IsString Polytype where+	fromString = polytype . Monotype_Const . fromString+instance Num Monotype where+	(+) = Monotype_App+	(*) = Monotype_App+	abs x = x+	signum _ = 0+	negate x = x+	fromInteger = Monotype_Var . fromInteger++type Test_Solver+ =   Solver_Greedy_Finite Collect_Infos IO++{-+polytype_of_expr+ :: Expr+ -> Either (Collect_Error (Info  Test_Solver)+                          (Error Test_Solver))+           Text+polytype_of_expr ex = do+	-- Text.putStrLn (Text.pack $ show ex)+	let Syn_Expr+		 { constraints_Syn_Expr = cs+		 , freshvar_Syn_Expr    = freshvar+		 , monoty_Syn_Expr      = monotype+		 , errors_Syn_Expr      = errors+		 } = wrap_Expr (sem_Expr ex) Inh_Expr+		 { polytys_Inh_Expr  = -- Map.fromList+			 [ ("eq", polytyref+				(Quantification [1] [(1, "a")] $+				[Class_Qualifier "Eq" 1]+				 .=>. (1.->.1.->."Bool")+				 :: Polytype))+			 ]+		 , freshvar_Inh_Expr = 0+		 }+	case errors of+	 (_:_) -> Left $ Collect_Error_Grammar errors+	 [] ->+		let cs' = {-hussel-} cs in+		let cfg = solver_config+			 { solver_config_freshvar = freshvar+			 , solver_config_check    = True+			 } in+		let (result :: Solver_Result (Info Test_Solver) (Error Test_Solver)) =+			runIdentity $+			solve (\_ -> return ()) $+			solver_greedy_finite cfg cs' in+		case solver_result_errors result of+		 [] -> Right $ Build.text $+			(def::Quantification_Build_Options,) $+			for_all $ solver_result_monotypes result `substitute` monotype+		 errs -> Left $ Collect_Error_Solver errs++-- | Like 'polytype_of_expr', but more verbose;+-- mainly for debugging.+debug_expr :: Expr -> IO Text+debug_expr ex = do+	Text.putStrLn (Text.pack $ Build.string ex)+	let Syn_Expr+		 { constraints_Syn_Expr = cs+		 , freshvar_Syn_Expr    = freshvar+		 , monoty_Syn_Expr      = monotype+		 , errors_Syn_Expr      = errors+		 } = wrap_Expr (sem_Expr ex) Inh_Expr+		 { polytys_Inh_Expr  = mempty+		 , freshvar_Inh_Expr = 0+		 }+	case errors of+	 (_:_) -> return $ Build.text $+		show (Collect_Error_Grammar errors::Collect_Error Collect_Info (Error Test_Solver))+	 [] -> do+		let cs' = {-hussel-} cs+		let cfg = solver_config+			 { solver_config_freshvar = freshvar+			 , solver_config_check    = True+			 }+		(result :: Solver_Result (Info  (Solver_Greedy_Finite Collect_Infos IO))+		                         (Error (Solver_Greedy_Finite Collect_Infos IO))) <-+			solve write_log $+			solver_greedy_finite cfg cs'+			 -- (\_ -> return ())+		return $+			case solver_result_errors result of+			 [] -> Build.text $+				(def::Quantification_Build_Options,) $+				for_all $ solver_result_monotypes result `substitute` monotype+			 errs -> Build.text $ show $ Collect_Error_Solver errs+-}++write_log :: Solver_Log -> IO ()+write_log l =+	case l of+	 Solver_Log_Constraint x ->+		TL.putStrLn $ Build.toLazyText $ "- " <> build x+	 Solver_Log_Class x ->+		TL.putStrLn $ Build.toLazyText $ "- " <> build x+	 Solver_Log_Polytype x ->+		TL.putStrLn $ Build.toLazyText $ "- " <> build x+	 Solver_Log_States states ->+		TL.putStrLn $ Build.toLazyText $+		Build.unlines $+			[ hline ] <>+			List.zipWith+			 (\i (MC.Instance s) ->+				build i <> ". " <> build (state_name s) <> "\n" <>+				Build.indent "    " (Build.unlines $+				 (build <$> state_options s) <>+				 [build $ state_show s]))+			 [1::Int ..]+			 states <>+			[ hline ]+	where+		hline :: Build.Builder = build $ Text.replicate 80 "-"++polytys_env :: [(Name, Polytype)]+polytys_env =+	[ ("equal", polytype+		(Quantification [1] [(1, "a")] $+		[Class_Qualifier "Eq" 1]+		 .=>. (1.->.1.->."Bool")+		 :: Polytype))+	, ("compare", polytype+		(Quantification [1] [(1, "a")] $+		[Class_Qualifier "Ord" 1]+		 .=>. (1.->.1.->."Ordering")+		 :: Polytype))+	, ("True", polytype+		(Quantification [] [] $+		[] .=>. "Bool"+		 :: Polytype))+	, ("one", polytype+		(Quantification [] [] $+		[] .=>. "Int"+		 :: Polytype))+	, ("pair", polytype+		(Quantification [1,2] [] $+		[] .=>. (1.->.2.->.type_Tuple [1,2])+		 :: Polytype))+	]+++class Collect_Constraints a where+	collect_constraints+	 :: a -> Either (Collect_Error (Info Test_Solver) (Error Test_Solver))+	                (Freshvar, Seq Collect_Constraint)+instance Collect_Constraints Expr where+	collect_constraints expr =+		let Collect.Syn_Expr+			 { Collect.freshvar_Syn_Expr    = freshvar+			 , Collect.constraints_Syn_Expr = constrs+			 , Collect.errors_Syn_Expr      = errors+			 } = Collect.wrap_Expr (Collect.sem_Expr expr)+			 Collect.Inh_Expr+			 { Collect.polytys_Inh_Expr  = (polytyref `second`) <$> polytys_env+			 , Collect.freshvar_Inh_Expr = 0+			 } in+		case errors of+		 errs@(_:_) -> Left $ Collect_Error_Grammar errs+		 [] -> Right (freshvar, constrs)+instance Collect_Constraints Decl where+	collect_constraints decl =+		let Collect.Syn_Decl+			 { Collect.freshvar_Syn_Decl    = freshvar+			 , Collect.constraints_Syn_Decl = constrs+			 , Collect.errors_Syn_Decl      = errors+			 } = Collect.wrap_Decl (Collect.sem_Decl decl)+			 Collect.Inh_Decl+			 { Collect.polytys_Inh_Decl  = (polytyref `second`) <$> polytys_env+			 , Collect.freshvar_Inh_Decl = 0+			 } in+		case errors of+		 errs@(_:_) -> Left $ Collect_Error_Grammar errs+		 [] -> Right (freshvar, constrs)++infer :: Collect_Constraints a+ => Bool -> a+ -> IO (Either (Collect_Error (Info Test_Solver) (Error Test_Solver))+               (Solver_Result (Info Test_Solver) (Error Test_Solver)))+infer logging x =+	case collect_constraints x of+	 Left err -> return $ Left err+	 Right (solver_config_freshvar, constrs) -> do+		let cfg = solver_config+			 { solver_config_freshvar+			 , solver_config_check = True+			 }+		let wlog = if logging then write_log else (\_ -> return ())+		res <- solve wlog $ solver_greedy_finite cfg constrs+		return $+			case solver_result_errors res of+			 [] -> Right res+			 errs -> Left $ Collect_Error_Solver errs++class Collect_Constraints a => Infer_Polytype a where+	infer_polytype+	 :: Bool -> a+	 -> IO (Either (Collect_Error (Info Test_Solver) (Error Test_Solver))+	               Polytype)+instance Infer_Polytype Expr where+	infer_polytype logging ex = do+		res <- infer logging ex+		case res of+		 Left err -> return $ Left err+		 Right Solver_Result+			 { solver_result_monotypes  = monosub+			 , solver_result_qualifiers = quals+			 } -> return $ Right $+				for_all $ (quals .=>.) $+				(monosub `substitute`) $+				Monotype_Var 0+instance Infer_Polytype Decl where+	infer_polytype logging ex = do+		res <- infer logging ex+		case res of+		 Left err -> return $ Left err+		 Right Solver_Result+			 { solver_result_monotypes = monosub+			 , solver_result_polytypes = polysub+			 } -> return $ Right $+				(monosub `substitute`) $+				fromMaybe (error $ "Oops, Polytype missing" <> show polysub) $+				Map.lookup 0 polysub+++tests :: TestTree+tests = testGroup "Solver"+ [ testGroup "Expr" $+		let test logging input expected = do+			p <- infer_polytype logging input+			let got = (Build.text . (def::Quantification_Build_Options,)) <$> p+			got @?= expected in+		let (==>) = test False in+		-- let (==>>) = test True in+	 [ testGroup "SKI" $+			-- DOC: https://en.wikipedia.org/wiki/SKI_combinator_calculus+			-- DOC: https://en.wikipedia.org/wiki/B,_C,_K,_W_system+			let i = "x".-> "x" in+			let k = "x".-> "y".-> "x" in+			let s = "x".-> "y".-> "z".-> ("x"!"z") ! ("y"!"z") in+			let c = "f".-> "x".-> "y".-> "f"!"y"!"x" in+			let b = "f".-> "g".-> "x".-> "f"!("g"!"x") in+			let w = "x".-> "y".-> "x"!"y"!"y" in+			let t = k in -- True+			let f = s ! k in -- False+			let no = f ! t in -- not+		 [ testCase "I" $ i+			 ==> Right "forall a. a -> a"+		 , testCase "K" $ k+			 ==> Right "forall a b. a -> b -> a"+		 , testCase "S" $ s+			 ==> Right "forall a b c. (a -> b -> c) -> (a -> b) -> a -> c"+		 , testCase "B" $ b+			 ==> Right "forall a b c. (a -> b) -> (c -> a) -> c -> b"+		 , testCase "B = S (K S) K" $+			 (s ! (k!s) ! k)+			 ==> Right "forall a b c. (a -> b) -> (c -> a) -> c -> b"+		 , testCase "C" $ c+			 ==> Right "forall a b c. (a -> b -> c) -> b -> a -> c"+		 , testCase "C = S (B B S) (K K)" $+			 (s ! (b!b!s) ! (k!k))+			 ==> Right "forall a b c. (a -> b -> c) -> b -> a -> c"+		 , testCase "W" $ w+			 ==> Right "forall a b. (a -> a -> b) -> a -> b"+		 , testCase "W = S S (S K)" $+			 (s ! s ! (s!k))+			 ==> Right "forall a b. (a -> a -> b) -> a -> b"+		 , testCase "W /= S I I" $+			 (s!i!i)+			 ==> Left (Collect_Error_Solver+				 [( Collect_Infos+					 [ Collect_Info_Solver (Solver_Info_Monotype $ Info_Monotype_Unification 1 (18 .->. 0))+					 , Collect_Info_Grammar (Collect_Info_Grammar_Expr "App") ]+				 , Solver_Error_Monotype $+					Error_Monotype_Unification $+					Unification_Error_Infinite_type 12+				 )])+		 , testCase "W W /= W W" $+			 (w ! w)+			 ==> Left (Collect_Error_Solver+				 [( Collect_Infos+					 [ Collect_Info_Solver (Solver_Info_Monotype $ Info_Monotype_Unification 1 (10 .->. 0))+					 , Collect_Info_Grammar (Collect_Info_Grammar_Expr "App") ]+				 , Solver_Error_Monotype $+					Error_Monotype_Unification $+					Unification_Error_Infinite_type 13+				 )])+		 , testCase "S = B (B W) (B B C)" $+			 (b ! (b!w) ! (b!b!c))+			 ==> Right "forall a b c. (a -> b -> c) -> (a -> b) -> a -> c"+		 , testCase "I = S K K" $+			 (s!k!k)+			 ==> Right "forall a. a -> a"+		 , testCase "I = W K" $+			 (w ! k)+			 ==> Right "forall a. a -> a"+		 , testCase "not" $ no+			 ==> Right "forall a. a -> a"+		 ]+	 , testGroup "Abst" $+			let o = "f".-> "g".-> "x".-> "f"!("g"!"x") in+		 [ testCase "(x:Int) -> x" $+			 (("x", "Int"::Monotype)..-> "x")+			 ==> Right "Int -> Int"+		 , testCase "(x:Int) -> (x:Bool)" $+			 (("x", "Int"::Monotype)..-> ("x".:("Bool"::Monotype)))+			 ==> Left (Collect_Error_Solver+				 [ ( Collect_Infos+					 [ Collect_Info_Solver (Solver_Info_Monotype (Info_Monotype_Unification 2 "Bool"))+					 , Collect_Info_Solver (Solver_Info_Polytype (Info_Polytype_Rigidified [1] "Bool"))+					 , Collect_Info_Grammar (Collect_Info_Grammar_Expr "Annot Bool") ]+				 , Solver_Error_Monotype (Error_Monotype_Unification (Unification_Error_Constant_clash "Int" "Bool")))+				 ])+		 , testCase "(x:Int -> Int) -> x" $+			 (("x", "Int".->."Int")..-> "x")+			 ==> Right "(Int -> Int) -> Int -> Int"+		 , testCase "x -> y" $+			 ("x".-> "y")+			 ==> Left (Collect_Error_Grammar [Collect_Error_Grammar_Variable_not_in_scope "y"])+		 , testCase "compose" $ o+			 ==> Right "forall a b c. (a -> b) -> (c -> a) -> c -> b"+		 , testCase "twice" $+			 ("f".-> "x".-> "f"!("f"!"x"))+			 ==> Right "forall a. (a -> a) -> a -> a"+		 , testCase "twice = \\f -> f . f" $+			 ("f".-> "c" .= o $ "c"!"f"!"f")+			 ==> Right "forall a. (a -> a) -> a -> a"+		 , testCase "(x y) z" $+			 ("x".-> "y".-> "z".-> "x"!"y"!"z")+			 ==> Right "forall a b c. (a -> b -> c) -> a -> b -> c"+		 , testCase "x (y z)" $+			 ("x".-> "y".-> "z".-> "x"!("y"!"z"))+			 ==> Right "forall a b c. (a -> b) -> (c -> a) -> c -> b"+		 , testCase "x u v t" $+			 ("x".-> "y".-> "z".-> "t".->+				"y" ! ("u".-> ("t" ! (("z"!"u") ! ("v".-> "x"!"u"!"v"!"t")))))+			 ==> Right "forall a b c d e f. (a -> b -> (c -> d) -> e) -> ((a -> d) -> f) -> (a -> (b -> e) -> c) -> (c -> d) -> f"+		 , testCase "x -> x x" $+			 ("x".-> "x"!"x")+			 ==> Left (Collect_Error_Solver+				 [( Collect_Infos+					 [ Collect_Info_Solver (Solver_Info_Monotype $ Info_Monotype_Unification 3 (4 .->. 2))+					 , Collect_Info_Grammar (Collect_Info_Grammar_Expr "App") ]+				 , Solver_Error_Monotype $+					Error_Monotype_Unification $+					Unification_Error_Infinite_type 1+				 )])+		 , testCase "y -> (x -> x) y y" $+			 ("y".-> ("x".-> "x")!"y"!"y")+			 ==> Left (Collect_Error_Solver+				 [( Collect_Infos+					 [ Collect_Info_Solver (Solver_Info_Monotype $ Info_Monotype_Unification 3 (8 .->. 2))+					 , Collect_Info_Grammar (Collect_Info_Grammar_Expr "App") ]+				 , Solver_Error_Monotype $+					Error_Monotype_Unification $+					Unification_Error_Infinite_type 1+				 )])+		 , testCase "x -> (a b c -> a c) (x -> x) (f -> f x x)" $+			 ("x".-> ("a".-> "b".-> "c".-> "a"!"c") ! ("x".-> "x") ! ("f".-> "f"!"x"!"x"))+			 ==> Right "forall a b. a -> b -> b"+		 ]+	 , testGroup "Let"+		 [ testCase "top_example_4_7" $+			 ("x".->+					"f".= ("g".= "x" $ "a".-> "g") $+						"h".= "f" $ "h"!"x")+			 ==> Right "forall a. a -> a"+		 , testCase "(i:Int) -> let (f:Int) = i in f" $+			 (("i", "Int"::Monotype)..->+				(("f", "Int"::Monotype)..= "i") "f")+			 ==> Right "Int -> Int"+		 , testCase "i -> let (f:forall a. a -> a) = i in f" $+			 ("i".-> (("f", for_all ([] .=>. (1 .->. 1)))..= "i") "f")+			 ==> Left (Collect_Error_Solver+				 [( Collect_Infos [ Collect_Info_Grammar (Collect_Info_Grammar_Expr "Let(sig) forall a. a -> a") ]+				 , Solver_Error_Polytype (Error_Polytype_Rigid_escaping [6])+				 )])+		 , testCase "(i:Int) -> let (f:Bool) = i in f" $+			 (("i", "Int"::Monotype)..->+				(("f", "Bool"::Monotype)..= "i") "f")+			 ==> Left (Collect_Error_Solver+				 [( Collect_Infos+					 [ Collect_Info_Solver (Solver_Info_Monotype (Info_Monotype_Unification 4 (Monotype_Const "Bool")))+					 , Collect_Info_Solver (Solver_Info_Polytype (Info_Polytype_Rigidified [1] "Bool"))+					 , Collect_Info_Grammar (Collect_Info_Grammar_Expr "Let(sig) Bool") ]+				 , Solver_Error_Monotype $+					Error_Monotype_Unification $+					Unification_Error_Constant_clash "Int" "Bool"+				 )])+		 , testCase "a -> b -> a" $+			 ("x".-> "f".= ("y".->"x") $ "f")+			 ==> Right "forall a b. a -> b -> a"+		 ]+	 , testGroup "Annot" $+			let id = "x".-> "x" in+		 [ testCase "id : a -> a" $+			 (id .: for_all ([] .=>. (1 .->. 1)))+			 ==> Right "forall a. a -> a"+		 , testCase "id : Int -> Int" $+			 (id .: for_all ([] .=>. ("Int" .->. "Int")))+			 ==> Right "Int -> Int"+		 , testCase "id /: a -> Int" $+			 (id .: for_all ([] .=>. (1 .->. "Int")))+			 ==> Left (Collect_Error_Solver+				 [( Collect_Infos [ Collect_Info_Grammar (Collect_Info_Grammar_Expr "Annot forall a. a -> Int") ]+				 , Solver_Error_Polytype $+					Error_Polytype_Rigid_type_mismatch+					[(3, Monotype_Const "Int")] )+				 ])+		 , testCase "id /: a -> b" $+			 (id .: for_all ([] .=>. (1 .->. 2)))+			 ==> Left (Collect_Error_Solver+				 [( Collect_Infos [ Collect_Info_Grammar (Collect_Info_Grammar_Expr "Annot forall a b. a -> b") ]+				 , Solver_Error_Polytype $+					Error_Polytype_Rigid_injectivity_lost $+					Map.fromList [(3, [3, 4])] )+				 ])+		 ]+	 {-+	 , testGroup "Class" $+		let (==>) input (expected::Text) = do+			got <- ((Build.text . (def::Quantification_Build_Options,)) <$>)+				 <$> polytype_of_expr input+			-- Text.putStrLn ("exp: " <> Build.text term)+			got @?= Right expected in+		 [ testCase "Eq a => a -> Bool" $+			("x".-> "=="!"x"!"x")+			-- ("f".= ("x".-> "=="!"x"!"x") "f")+			 ==> "forall a. Eq a => a -> Bool"+		 ]+	 , testGroup "Class" $+		let test logging input (expected::Text) = do+			p <- polytype_of_decl logging input+			let got = (Build.text . (def::Quantification_Build_Options,)) <$> p+			got @?= Right expected in+		let (==>) = test False in+		let (==>>) = test True in+		 [ testCase "Eq a => a -> a -> Bool" $+			Decl_Let Nothing "f" "=="+			 ==> "forall a. Eq a => a -> a -> Bool"+		 , testCase "Eq a => a -> Bool" $+			Decl_Let Nothing "f"+			 ("x".-> "=="!"x"!"x")+			 ==> "forall a. Eq a => a -> Bool"+		 , testCase "Eq a => a -> Bool" $+			Decl_Let Nothing "f"+			 ("x".-> "=="!("=="!"x"!"x")!("=="!"x"!"x"))+			 ==> "forall a. Eq a => a -> Bool"+		 , testCase "Ord a => a -> Bool" $+			Decl_Let Nothing "f" ("x".->+				"=="+				 !("=="!"x"!"x")+				 !("=="+					 !("compare"!"x"!"x")+					 !("compare"!"x"!"x")))+			 ==> "forall a. Ord a => a -> Bool"+		 , testCase "a -> b -> a" $+			 Decl_Let Nothing "f"+			 ("x".-> "g".= ("y".->"x") $ "g")+			 ==>> "forall a b. a -> b -> a"+		 ]+	-} ]+ ]
+ Language/LOL/Typing/Test.hs view
@@ -0,0 +1,24 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Test where++import Data.Function (($))+import System.IO (IO)+import Test.Tasty++import qualified Type.Test+-- import qualified Collect.Test+import qualified Solver.Test+import qualified Expr.Test++main :: IO ()+main =+	defaultMain $ testGroup "Tests"+	 [ Type.Test.tests+	 -- , Collect.Test.tests+	 , Solver.Test.tests+	 , Expr.Test.tests+	 ]
+ Language/LOL/Typing/Type.hs view
@@ -0,0 +1,22 @@+-- | All submodules, in a topological order.+module Language.LOL.Typing.Type+ ( module Language.LOL.Typing.Type.Monotype+ , module Language.LOL.Typing.Type.Substitution+ , module Language.LOL.Typing.Type.Synotype+ , module Language.LOL.Typing.Type.Unification+ , module Language.LOL.Typing.Type.Quantification+ , module Language.LOL.Typing.Type.Qualification+ , module Language.LOL.Typing.Type.Class+ , module Language.LOL.Typing.Type.Polytype+ , module Language.LOL.Typing.Type.Kind+ ) where++import Language.LOL.Typing.Type.Monotype+import Language.LOL.Typing.Type.Substitution+import Language.LOL.Typing.Type.Synotype+import Language.LOL.Typing.Type.Unification+import Language.LOL.Typing.Type.Quantification+import Language.LOL.Typing.Type.Qualification+import Language.LOL.Typing.Type.Class+import Language.LOL.Typing.Type.Polytype+import Language.LOL.Typing.Type.Kind
+ Language/LOL/Typing/Type/Class.hs view
@@ -0,0 +1,402 @@+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TupleSections #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+-- | /type class/.+--+-- __Ressources:__+--+-- * /Type classes: exploring the design space/,+--   Simon Peyton Jones, Mark Jones, Erik Meijer, 1997,+--   http://research.microsoft.com/en-us/um/people/simonpj/Papers/type-class-design-space/multi.ps.gz+--+-- * /Implementing, and Understanding Type Classes/,+--   Oleg Kiselyov, 2014,+--   http://okmij.org/ftp/Computation/typeclass.html+module Language.LOL.Typing.Type.Class where++import Control.Arrow (first)+import Control.Monad (mapM)+import Data.Bool+import Data.Either (Either(..))+import Data.Eq (Eq(..))+import qualified Data.Foldable as Foldable+import Data.Function (($), (.), flip)+import Data.Functor ((<$>))+import qualified Data.List as List+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Maybe (Maybe(..), maybe)+import Data.Monoid ((<>))+import Data.Text (Text)+import Data.Text.Buildable (Buildable(..))+import Text.Show (Show(..))++import Language.LOL.Typing.Type.Monotype+import Language.LOL.Typing.Type.Substitution (Substitutable(..))+import Language.LOL.Typing.Type.Synotype+import Language.LOL.Typing.Type.Unification+import Language.LOL.Typing.Type.Qualification++-- * Type 'Class'++data Class+ =   Class+ {   class_supers    :: [Class_Name] -- ^ /adjacent super classes/+ ,   class_instances :: [Class_Instance] -- ^ /class instances/+ } deriving (Eq, Show)++-- ** Type 'Class_Instance'++data Class_Instance+ =   Class_Instance+ {   class_instance_head    :: Class_Qualifier+ ,   class_instance_context :: [Class_Qualifier]+ } deriving (Eq, Show)++-- ** Type 'Class_Qualifier'++data Class_Qualifier+ =   Class_Qualifier+ {   class_qualifier_name :: Class_Name+ ,   class_qualifier_type :: Monotype+ } deriving (Eq, Show)++-- | Right associative alias for 'Qualification'.+(.=>.) :: [Class_Qualifier] -> a -> Qualification [Class_Qualifier] a+(.=>.) = Qualification+infixr 2 .=>.++instance Buildable Class_Qualifier where+	build (Class_Qualifier q ty) =+		build q <> " "  <> build ty+instance Substitutable Class_Qualifier where+	subvars = subvars . class_qualifier_type+	sub `substitute` p = p{class_qualifier_type =+		sub `substitute` class_qualifier_type p}+instance Has_Monoconsts Class_Qualifier where+	monoconsts p = monoconsts (class_qualifier_type p)+instance Has_Monotypes Class_Qualifier where+	monotypes q = [class_qualifier_type q]+	monotypes_map f q = q{class_qualifier_type = f (class_qualifier_type q)}++-- | Return the 'Unification' (when it exists)+-- of two given 'Class_Qualifier's,+-- using given 'Synotype_Substitution'.+class_qualifier_unification+ :: Synotype_Substitution+ -> Class_Qualifier+ -> Class_Qualifier+ -> Maybe Unification+class_qualifier_unification syns+ (Class_Qualifier na1 ty1)+ (Class_Qualifier na2 ty2)+ | na1 == na2 =+	case mgu_with_synotypes syns (constify ty1) ty2 of+	 Left _ -> Nothing+	 Right (_, uni) -> Just (unconstify <$> uni)+ | otherwise = Nothing++-- ** Type 'Class_Env'++type Class_Env  = Map Class_Name Class+type Class_Name = Text+type Class_Path = [Class_Name]++class_env_empty :: Class_Env+class_env_empty = Map.empty++class_env_default :: Class_Env+class_env_default = Map.fromList+	[ ("Num",)+		Class+		 { class_supers    = ["Eq", "Show"]+		 , class_instances =+			 [ Class_Instance (Class_Qualifier "Num" ty) []+			 | ty <- [type_Int, type_Float]+			 ]+		 }+	, ("Enum",)+		Class+		 { class_supers    = []+		 , class_instances =+			 [ Class_Instance (Class_Qualifier "Enum" ty) []+			 | ty <- [type_Unit, type_Int, type_Float, type_Bool, type_Char]+			 ]+		 }+	, ("Eq",)+		Class+		 { class_supers    = []+		 , class_instances =+			Class_Instance+			 { class_instance_head = Class_Qualifier "Eq" "Ordering"+			 , class_instance_context  = []+			 } :+			instances_Eq_Ord_Show "Eq"+		 }+	, ("Ord",)+		Class+		 { class_supers    = ["Eq"]+		 , class_instances = instances_Eq_Ord_Show "Ord"+		 }+	, ("Show",)+		Class+		 { class_supers    = []+		 , class_instances = instances_Eq_Ord_Show "Show"+		 }+	]+	where+	instances_Eq_Ord_Show name =+		Class_Instance -- NOTE: List instance+		 { class_instance_head = Class_Qualifier name (type_List (Monotype_Var 0))+		 , class_instance_context  = [Class_Qualifier name (Monotype_Var 0)]+		 } :+		[ Class_Instance+			 { class_instance_head = Class_Qualifier name ty+			 , class_instance_context  = []+			 }+		| ty <- [type_Bool, type_Char, type_Float, type_Int]+		] <>+		(inst_tuples <$> (0 : [2..10]))+		where+		inst_tuples i =+			Class_Instance+			 { class_instance_head =+				Class_Qualifier name (type_Tuple [ Monotype_Var n | n <- [1..i] ])+			 , class_instance_context =+				[ Class_Qualifier name (Monotype_Var n)+				| n <- [1..i]+				]+			 }++-- | Return given 'Class_Env'+-- with given 'Class_Name'+-- mapping to a 'Class'+-- with given 'Class_Instance'.+class_env_insert_instance+ :: Class_Name+ -> Class_Instance+ -> Class_Env -> Class_Env+class_env_insert_instance name inst =+	Map.insertWith+	 (\_new old -> old{class_instances = inst : class_instances old})+	 name Class+	 { class_supers    = []+	 , class_instances = [inst]+	 }++-- | Return whether given 'Class_Env'+-- has a 'Class' with given 'Class_Name'.+class_env_has :: Class_Env -> Class_Name -> Bool+class_env_has = flip Map.member++-- | Return the 'class_supers'+-- associated to the given 'Class_Name',+-- in given 'Class_Env'.+--+-- Example: @'class_env_supers' 'class_env_default' \"Ord\" '==' [\"Eq\"]@+class_env_supers :: Class_Env -> Class_Name -> [Class_Name]+class_env_supers env name = maybe [] class_supers $ Map.lookup name env++-- | Return the 'Class_Path's+-- between given 'Class_Name's+-- in given 'Class_Env'.+class_env_super_path+ :: Class_Env+ -> Class_Name -> Class_Name+ -> [Class_Path]+class_env_super_path env from to+ | from == to = [[to]]+ | otherwise =+	[ from : path+	| super <- class_env_supers env from+	, path <- class_env_super_path env super to+	]++-- | Return the 'Class_Instance's+-- of given 'Class_Name' within given 'Class_Env'.+class_env_instances+ :: Class_Env -> Class_Name -> [Class_Instance]+class_env_instances env name =+	maybe [] class_instances $+	Map.lookup name env++-- | Return all the 'Class_Qualifier's+-- of all the 'class_supers'+-- of the given 'Class_Qualifier',+-- within given 'Class_Env'.+class_env_supers_all+ :: Class_Env+ -> Class_Qualifier+ -> [Class_Qualifier]+class_env_supers_all env p@(Class_Qualifier name ty) =+	p : List.concat+	 [ class_env_supers_all env (Class_Qualifier supers ty)+	 | supers <- class_env_supers env name+	 ]++-- | Return the 'class_instance_context'+-- 'substitute'd by the 'class_qualifier_unification'+-- of the first 'class_instance_head'+-- unifying with given 'Class_Qualifier',+-- within given 'Class_Env',+-- and using given 'Synotype_Substitution'.+class_env_instance_context+ :: Synotype_Substitution+ -> Class_Env+ -> Class_Qualifier+ -> Maybe [Class_Qualifier]+class_env_instance_context syns env qual@(Class_Qualifier qname _) =+	Foldable.msum+	 [ context inst+	 | inst <- class_env_instances env qname+	 ]+	where+	context :: Class_Instance -> Maybe [Class_Qualifier]+	context Class_Instance{class_instance_head, class_instance_context} = do+		uni <- class_qualifier_unification syns qual class_instance_head+		Just (uni `substitute` class_instance_context)++-- ** Normalization++class_qualifier_normalize+ :: Synotype_Substitution+ -> Class_Env+ -> Class_Qualifier+ -> Maybe [Class_Qualifier]+class_qualifier_normalize syns env p+ | is_class_qualifier_normalized p = Just [p]+ | otherwise = do+	ctx <- class_env_instance_context syns env p+	class_context_normalize syns env ctx++is_class_qualifier_normalized :: Class_Qualifier -> Bool+is_class_qualifier_normalized (Class_Qualifier _ ty) = go ty+	where+	go (Monotype_Var _)   = True+	go (Monotype_Const _) = False+	go (Monotype_App t _) = go t++class_context_normalize+ :: Synotype_Substitution+ -> Class_Env+ -> [Class_Qualifier]+ -> Maybe [Class_Qualifier]+class_context_normalize syns env ps =+	List.concat <$>+	mapM (class_qualifier_normalize syns env) ps++-- ** Entailment++class_entails+ :: Synotype_Substitution+ -> Class_Env+ -> [Class_Qualifier]+ -> Class_Qualifier+ -> Bool+class_entails syns env quals qual =+	class_entails_super_class env quals qual ||+	case class_env_instance_context syns env qual of+	 Nothing -> False+	 Just insts -> Foldable.all (class_entails syns env quals) insts++-- | Return whether a given 'Class'+-- implies another as a 'class_supers'.+class_entails_super_class+ :: Class_Env+ -> [Class_Qualifier]+ -> Class_Qualifier+ -> Bool+class_entails_super_class env ps p =+	Foldable.any+	 (p `List.elem`)+	 (class_env_supers_all env <$> ps)++class_entails_all+ :: Synotype_Substitution+ -> Class_Env+ -> [Class_Qualifier]+ -> [Class_Qualifier]+ -> Bool+class_entails_all syns env ps =+	Foldable.all (class_entails syns env ps)++-- ** Type 'Class_Reduction_Error'++newtype Class_Reduction_Error a+ =      Class_Reduction_Error a+ deriving (Show)++-- | Reduce a 'Class' context by performing:+--+-- 1. Simplification using 'Class_Instance's.+--+--      Example: @Eq (a, b)@ is simplified to @Eq a@ and @Eq b@.+--+--      Example: @Eq Int@ is removed.+--+--      Example: @Num Bool@ (whose 'Class_Instance' does not exist)+--               gives a 'Class_Reduction_Error'.+--+-- 2. Removal of 'Class'es entailed by 'class_supers'.+--+--      Example: Because @Eq@ is the superclass of @Ord@, @Ord a@ 'class_entails' @Eq a@,+--               which therefore can safely be removed when @Ord a@ is present.+--+-- 3. Removal of duplicate 'Class'es.+class_context_reduction+ :: Synotype_Substitution+ -> Class_Env+ -> [Class_Qualifier]+ -> ( [Class_Qualifier]+    , [Class_Reduction_Error Class_Qualifier]+    )+class_context_reduction syns env =+	first (go []) . List.foldr fold ([], [])+	where+	fold qual (quals, errs) =+		case class_qualifier_normalize syns env qual of+		 Just qs -> (qs <> quals, errs)+		 Nothing -> (quals, Class_Reduction_Error qual : errs)+	go rs [] = rs+	go rs (q:qs)+	 | entailed  = go    rs  qs+	 | otherwise = go (q:rs) qs+		where entailed = class_entails_super_class env (rs <> qs) q++{-+context_reduction_associated+ :: Synotype_Substitution+ -> Class_Env+ -> [(Class_Qualifier, a)]+ -> ( [(Class_Qualifier, a)]+    , [Class_Reduction_Error (Class_Qualifier, a)]+    )+context_reduction_associated syns env =+	first (go []) . List.foldr fold ([], [])+	where+	fold (qual, a) (reduced, es) =+		case class_qualifier_normalize syns env qual of+		 Just qs -> ([(p, a) | p <- qs] <> reduced, es)+		 Nothing -> (reduced, Class_Reduction_Error (qual, a) : es)+	go rs [] = rs+	go rs (q:qs)+	 | entailed  = go    rs  qs+	 | otherwise = go (q:rs) qs+		where+		entailed = class_entails_super_class env+			 (fst <$> (rs <> qs)) (fst q)+-}++-- * Type 'Class_Directive'++data Class_Directive info+ =   Class_Directive_Never    Class_Qualifier info+ |   Class_Directive_Close    Class_Name            info+ |   Class_Directive_Disjoint [Class_Name]          info+ |   Class_Directive_Default  Class_Name [Monotype] info+ deriving (Eq, Show)++instance Buildable info => Buildable (Class_Directive info) where+	build _ = "Class_Directive"+	 -- FIXME: write it.
+ Language/LOL/Typing/Type/Kind.hs view
@@ -0,0 +1,57 @@+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Type.Kind where++import Data.Function (($))+import Data.Int (Int)+import Data.List ((++))+import qualified Data.List as List+import Data.String (String)+import qualified Data.Text as Text+import Text.Show (Show(..))++import Language.LOL.Typing.Type.Monotype+import Language.LOL.Typing.Type.Polytype+import Language.LOL.Typing.Type.Substitution+import Language.LOL.Typing.Type.Quantification++-- * Type 'Monokind'++type Monokind = Monotype+type Polykind = Polytype++-- | The kind of all 'Type's.+star :: Monokind+star = Monotype_Const "*"++-- | In traditional /kind inference systems/,+-- a kind cannot contain /kind variables/.+-- At some point in the inference process+-- the /kind variables/ are defaulted to 'star'.+monokind_vars_to_star :: Monokind -> Monokind+monokind_vars_to_star ki = sub `substitute` ki+	where+	sub = substitution_finite+	 [ (v, star)+	 | v <- subvars ki+	 ]++-- | A function to show kinds.+show_Monokind :: Monokind -> String+show_Monokind ki = show (sub `substitute` ki)+	where+	sub = substitution_finite+	 [ (v, Monotype_Const (Text.pack ('k':show v)))+	 | v <- subvars ki+	 ]++show_Polykind :: Polykind -> String+show_Polykind polyki = show (sub `substitute` quantified polyki)+	where+	sub = substitution_finite $+	 [ (v1, Monotype_Const (Text.pack ('k':show v2)))+	 | (v1, v2) <- List.zip (quantifiers polyki) [1 :: Int ..]+	 ] +++	 [ (v, Monotype_Const (Text.pack ("_k"++show v)))+	 | v <- subvars polyki+	 ]
+ Language/LOL/Typing/Type/Monotype.hs view
@@ -0,0 +1,373 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Type.Monotype where++import Data.Bool+import Data.Either (Either(..), either)+import Data.Eq (Eq(..))+import Data.Function (($), (.), id)+import Data.Functor (Functor(..), (<$>))+import Data.Int (Int)+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Data.Maybe (Maybe(..), maybe, isNothing)+import Data.Monoid (Monoid(..), (<>))+import Data.Ord (Ord(..))+import Data.String (IsString(..))+import Data.Text (Text)+import Data.Text.Buildable (Buildable(..))+import Prelude (Num(..))+import Text.Read (read)+import Text.Show (Show(..))+import qualified Data.Char as Char+import qualified Data.Foldable as Foldable+import qualified Data.List as List+import qualified Data.Text as Text++import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build++-- * Type 'Monotype'++-- | A /monomorphic type/ (aka. /monotype/).+--+-- NOTE: all 'Monotype's that can be constructed are NOT necessarily well-formed.+--+-- NOTE: however, a useful typing of this type language+-- is added by separating 'Monotype', 'Polytype' and 'Polytyref'+-- in order to indicate where to expect a 'Polyvar' or a 'Polytyref_Var'.+data Monotype+ =   Monotype_App   Monotype Monotype -- ^ /binary type application/+ |   Monotype_Const Monoconst         -- ^ /type constant/+ |   Monotype_Var   Monovar           -- ^ /type variable/+ deriving (Eq, Ord, Show)++instance Buildable Monotype where+	build = build . (precedence_Toplevel,)+instance Buildable (Precedence, Monotype) where+	build (prec, typ)+	 | prec >= precedence typ = Build.parens (go typ)+	 | otherwise              = go typ+		where+		go ty =+			case app_spine_left ty of+			 Monotype_Var v `App_Spine` [] -> "m" <> build v+			 Monotype_Const c `App_Spine` [] -> build c+			 Monotype_Const "->" `App_Spine` [t1, t2] ->+				build (precedence_Fun, t1) <>+				" -> " <>+				build (precedence_previous precedence_Fun, t2)+			 Monotype_Const "[]" `App_Spine` [t1] ->+				"[" <> build t1 <> "]"+			 Monotype_Const (is_Tuple -> True) `App_Spine` tys ->+				Build.tuple (build <$> tys)+			 t `App_Spine` tys ->+				mconcat $ List.intersperse " " $+				(build . (precedence_App,)) <$> (t : tys)+instance IsString Monotype where+	fromString = Monotype_Const . fromString++-- * Type 'Precedence'++-- | A /binding precedence/ for an operator.+newtype Precedence+ =      Precedence Int+ deriving (Eq, Ord, Show)++-- ** Class 'Has_Precedence'++class Has_Precedence a where+	precedence :: a -> Precedence+instance Has_Precedence Monotype where+	precedence ty =+		case app_spine_left ty of+		 Monotype_Const "->" `App_Spine` [_, _] -> precedence_Fun+		 Monotype_Const "[]" `App_Spine` [_] -> precedence_Atomic+		 Monotype_Const (is_Tuple -> True) `App_Spine` _ -> precedence_Atomic+		 _ `App_Spine` [] -> precedence_Atomic+		 _ -> precedence_App++precedence_previous :: Precedence -> Precedence+precedence_previous (Precedence p) = Precedence (p - 1)++-- ** Convenient 'Precedence's+precedence_Toplevel :: Precedence+precedence_Toplevel =  Precedence 0+precedence_Fun :: Precedence+precedence_Fun =  Precedence 1+precedence_App :: Precedence+precedence_App =  Precedence 2+precedence_Atomic :: Precedence+precedence_Atomic =  Precedence 3++-- ** Type 'Monoconst'++-- | A /type constant/.+type Monoconst = Text++-- ** Type 'Monoconsts'++-- | A context of 'Monoconst's, without duplicates.+type Monoconsts = Map Monoconst ()++-- *** Class 'Has_Monoconsts'++-- | Return the 'Monoconst's of a 'Monotype', without duplicates.+class Has_Monoconsts a where+	monoconsts :: a -> Monoconsts++instance Has_Monoconsts Monotype where+	monoconsts ty =+		case ty of+		 Monotype_Var _ -> Map.empty+		 Monotype_Const c -> Map.singleton c ()+		 Monotype_App t1 t2 -> monoconsts t1 `Map.union` monoconsts t2++{-+-- | Return the 'Monoconst's of a 'Has_Monotypes' instance, without duplicates.+monoconsts_from :: Has_Monotypes a => a -> [Monoconst]+monoconsts_from =+	List.nub . List.concatMap go . monotypes+	where+	go (Monotype_Var _) = []+	go (Monotype_Const c) = [c]+	go (Monotype_App t1 t2) = go t1 `List.union` go t2+-}++-- | Infinite list of unique 'Monoconst's:+-- @a, b, .., z, a1, b1 .., z1, a2, ..@+const_pool :: [Monoconst]+const_pool =+	[ Text.singleton n+	| n <- ['a'..'z']+	] <>+	[ Text.pack (n:show i)+	| n <- ['a'..'z']+	, i <- [1 :: Int ..]+	]++-- | Return given 'Monoconst' renamed a bit to avoid+-- conflicting with any given 'Monoconst's.+const_freshify+ :: Monoconsts+ -> Monoconst+ -> (Monoconsts, Monoconst)+const_freshify consts_used const =+	let ints = [1..] :: [Int] in+	let fresh_const =+		List.head+		 [ x+		 | extra <- "" : (show <$> ints)+		 , x <- [const <> Text.pack extra]+		 , isNothing (Map.lookup x consts_used)+		 ] in+	( Map.insert fresh_const () consts_used+	, fresh_const )++-- | Return given 'Monotype'+-- with all its 'Monotype_Var's+-- turned into 'Monotype_Const's.+--+-- NOTE: each 'Monovar' being mapped to a 'Monoconst'+-- prefixing by an underscore ('_')+-- the 'show'ed 'Int' of the 'Monovar'.+constify :: Monotype -> Monotype+constify ty =+	case ty of+	 Monotype_Var v   -> Monotype_Const $ Text.pack ('_':show v)+	 Monotype_Const s -> Monotype_Const s+	 Monotype_App l r -> Monotype_App (constify l) (constify r)++-- | Return given 'Monotype'+-- with all previously 'constify'ed 'Monovar's+-- turned back into 'Monotype_Var's.+unconstify :: Monotype -> Monotype+unconstify ty =+	case ty of+	 Monotype_Var v -> Monotype_Var v+	 Monotype_Const (Text.uncons -> Just ('_', c))+	  | not (Text.null c)+	  && Text.all Char.isDigit c ->+		Monotype_Var (read $ Text.unpack c)+	 Monotype_Const c -> Monotype_Const c+	 Monotype_App l r -> Monotype_App+		 (unconstify l)+		 (unconstify r)++-- *** Useful 'Monoconst's++type_Bool   :: Monotype+type_Bool    = Monotype_Const "Bool"+type_Char   :: Monotype+type_Char    = Monotype_Const "Char"+type_Float  :: Monotype+type_Float   = Monotype_Const "Float"+type_Int    :: Monotype+type_Int     = Monotype_Const "Int"+type_String :: Monotype+type_String  = Monotype_Const "String"++-- | Constructs a function 'Monotype' from one 'Monotype' to another.+type_Fun :: Monotype -> Monotype -> Monotype+type_Fun t1 = Monotype_App (Monotype_App (Monotype_Const "->") t1)++-- | Right associative alias for 'type_Fun'.+(.->.) :: Monotype -> Monotype -> Monotype+(.->.) = type_Fun+infixr 0 .->.++-- | For instance, @(type_List type_Int)@ represents @[Int]@+type_List :: Monotype -> Monotype+type_List = Monotype_App (Monotype_Const "[]")++-- | For instance, @(type_IO type_Bool)@ represents @(IO Bool)@+type_IO :: Monotype -> Monotype+type_IO = Monotype_App (Monotype_Const "IO")++-- | A carthesian product of zero or more 'Monotype'.+-- For instance @(type_Tuple [])@ represents @()@,+-- and @(type_Tuple [type_Char, type_String])@ represents @(Char, String)@.+type_Tuple :: [Monotype] -> Monotype+type_Tuple tys = List.foldl Monotype_App (Monotype_Const name) tys+	where+	name | Foldable.null tys  = "()"+	     | otherwise = Text.pack $ "("<>List.replicate (List.length tys - 1) ','<>")"++-- | The unit type. A special instance of 'type_Tuple'.+type_Unit :: Monotype+type_Unit = type_Tuple []++-- ** Type 'Monovar'++-- | A /monomorphic type variable/:+-- a place-holder for a 'Monotype' that is not yet known,+-- but that become available at some time during 'Constraint' solving.+type Monovar = Int++-- | Return the list of 'Monovar's of a 'Monotype', without duplicates.+monovars :: Monotype -> [Monovar]+monovars ty =+	case ty of+	 Monotype_Var v -> [v]+	 Monotype_Const _ -> []+	 Monotype_App t1 t2 -> monovars t1 `List.union` monovars t2++-- * Type 'App'++-- | A /binary 'Monotype' application/.+type App = Monotype -> Monotype -> Monotype++-- | Left associative alias for 'Monotype_App'.+(.!.) :: Monotype -> Monotype -> Monotype+(.!.) = Monotype_App+infixl 5 .!.++-- | 'Monotype_App'ly given 'Monotype's to given 'Monotype'.+monoapp :: Monotype -> [Monotype] -> Monotype+monoapp = List.foldl Monotype_App++-- ** Type 'App_Spine'++-- | A /application spine/ of a 'Monotype'.+data App_Spine+ =   App_Spine+ {   app_spine_end :: Monotype+ ,   app_spine     :: [Monotype]+ }++-- | Return the /left 'App_Spine'/ of a 'Monotype_App'.+--+-- EXAMPLE: if type @t@ is @Either Bool [Int]@,+-- then @app_spine_left t@ is @(Either, [Bool, [Int]])@.+app_spine_left :: Monotype -> App_Spine+app_spine_left = go []+	where+	go tys (Monotype_App t1 t2) = go (t2:tys) t1+	go tys ty = App_Spine ty tys++-- | Return the /right 'App_Spine'/ of a 'Monotype'.+--+-- EXAMPLE: if type @t@ is @Int -> (Bool -> String)@,+-- then @app_spine_right t@ is @([Int, Bool], String)@.+app_spine_right :: Monotype -> App_Spine+app_spine_right = go []+	where+	go tys (Monotype_App (Monotype_App (Monotype_Const "->") t1) t2) = go (t1:tys) t2+	go tys ty = App_Spine ty (List.reverse tys)++-- | Return the /right 'App_Spine'/ of a 'Monotype' upto a maximal length.+app_spine_right_upto :: Int -> Monotype -> App_Spine+app_spine_right_upto maxlen ty =+	let a `App_Spine` as = app_spine_right ty in+	let (bs, cs) = List.splitAt maxlen as in+	List.foldr (.->.) a cs `App_Spine` bs++-- ** Type 'Arity'++-- | The /arity of a 'Monotype'/,+-- i.e. the total number of expected arguments of a 'Monotype'.+type Arity = Int++-- | Return the 'Arity' of a 'Monotype'.+type_arity :: Monotype -> Arity+type_arity = List.length . app_spine . app_spine_right++-- * 'Monotype' predicates+is_Var :: Monotype -> Bool+is_Var (Monotype_Var _) = True+is_Var _ = False++is_Const :: Monotype -> Bool+is_Const (Monotype_Const _) = True+is_Const _ = False++is_App :: Monotype -> Bool+is_App (Monotype_App _ _) = True+is_App _ = False++is_Fun :: Monotype -> Bool+is_Fun (Monotype_App (Monotype_App (Monotype_Const "->") _) _) = True+is_Fun _ = False++is_Tuple :: Monoconst -> Bool+is_Tuple (Text.uncons -> Just ('(', t))+ | Text.null t = False+ | otherwise   = Text.all (',' ==) (Text.init t) && Text.last t == ')'+is_Tuple _ = False++is_IO :: Monotype -> Bool+is_IO (Monotype_App (Monotype_Const "IO") _) = True+is_IO _ = False++-- * Class 'Has_Monotypes'++class Has_Monotypes a where+	monotypes :: a -> [Monotype]+	monotypes_map :: (Monotype -> Monotype) -> a -> a++instance Has_Monotypes Monotype where+	monotypes ty = [ty]+	monotypes_map = ($)+instance Has_Monotypes a => Has_Monotypes [a] where+	monotypes = List.concatMap monotypes+	monotypes_map f = (monotypes_map f <$>)+instance Has_Monotypes a => Has_Monotypes (Maybe a) where+	monotypes = maybe [] monotypes+	monotypes_map = fmap . monotypes_map+instance (Has_Monotypes a, Has_Monotypes b) => Has_Monotypes (Either a b) where+	monotypes  = either monotypes monotypes+	monotypes_map f = either (Left . monotypes_map f) (Right . monotypes_map f)++-- ** Class 'Monotypeable'++-- | A type class to convert something into a 'Monotype'+class Monotypeable a where+	monotype :: a -> Monotype+instance Monotypeable Monotype where+	monotype = id+instance Monotypeable Monovar where+	monotype = Monotype_Var+instance Monotypeable Monoconst where+	monotype = Monotype_Const
+ Language/LOL/Typing/Type/Polytype.hs view
@@ -0,0 +1,122 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Language.LOL.Typing.Type.Polytype where++import Data.Bool+import qualified Data.Foldable as Foldable+import Data.Functor ((<$>))+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Data.Function ((.), id)+import qualified Data.List as List+import Data.Monoid ((<>))+import Data.Text.Buildable (Buildable(..))+import Text.Show (Show(..))++import Language.LOL.Typing.Type.Monotype+import Language.LOL.Typing.Type.Substitution+import Language.LOL.Typing.Type.Quantification+import Language.LOL.Typing.Type.Qualification+import Language.LOL.Typing.Type.Class+import Language.LOL.Typing.Lib.Data.Default (Default(..))++-- * Type 'Polytype'++-- | A /rank-1 polymorphic type/ (aka. /polytype/), with qualifiers.+type Polytype+ = Forall (Qualification [Class_Qualifier] Monotype)+instance Buildable Polytype where+	build x = build (def::Quantification_Build_Options, x)+instance Has_Monoconsts Polytype where+	monoconsts Quantification{quantified = Qualification quals monoty} =+		Map.unions (monoconsts monoty : (monoconsts <$> quals))++-- | Return a 'Polytype' /generalizing/ the given 'Monotype':+--+-- * quantifying all its 'Monovar's (which thus become /polymorphic/)+--   except the given 'Monovar's (which thus remain /monomorphic/),+-- * and qualifying them by the given 'Class_Qualifier's+--   which use at least one of them.+polytype_but+ :: [Monovar] -> [Class_Qualifier]+ -> Monotype -> Polytype+polytype_but vars_mono quals monoty =+	forall_in vars_poly Qualification+	 { qualifiers = List.filter is_quantified quals+	 , qualified  = monoty+	 }+	where+	vars_poly = subvars monoty List.\\ vars_mono+	is_quantified = Foldable.any (`List.elem` vars_poly) . subvars++-- | A /type with qualifiers/, constructed from a 'Monotype'+-- and some 'Class_Qualifier's (aka. /class context/).+--+-- These 'Class_Qualifier's put restrictions on certain 'Monovar's.+type Qualified_Type+ =   Qualification [Class_Qualifier] Monotype++-- ** Class 'Polytypeable'++-- | A type class to convert something into a 'Polytype'+class Polytypeable a where+	polytype :: a -> Polytype+instance Polytypeable Monotype where+	polytype = quantification . ([] .=>.)+instance Polytypeable (Qualification [Class_Qualifier] Monotype) where+	polytype = quantification+instance Polytypeable Polytype where+	polytype = id++-- | Return the 'Arity' of a 'Polytype'.+polytype_arity :: Polytype -> Arity+polytype_arity = type_arity . qualified . quantified++-- | Return whether the given 'Polytype' contains 'Class_Qualifier's.+is_polytype_qualified :: Polytype -> Bool+is_polytype_qualified = not . Foldable.null . qualifiers . quantified++-- * Type 'Polysub'++-- | A /polymorphic type substitution/.+type Polysub = Map Polyvar Polytype++-- | A /polymorphic type variable/:+-- a place-holder for a 'Polytype' that is not yet known,+-- but that become available at some time during 'Constraint' solving.+--+-- NOTE: is to 'Polytype', what a 'Monovar' is to a 'Monotype'.+type Polyvar = Quantifier++-- * Type 'Polytyref'++data Polytyref+ =   Polytyref     Polytype+ |   Polytyref_Var Polyvar+ deriving (Show)++instance Buildable Polytyref where+	build r =+		case r of+		 Polytyref polyty -> build (def::Quantification_Build_Options, polyty)+		 Polytyref_Var v  -> "p" <> build v+instance Substitutable Polytyref where+	subvars (Polytyref polyty) = subvars polyty+	subvars (Polytyref_Var _)  = []+	+	_   `substitute` r@(Polytyref_Var _) = r+	sub `substitute` (Polytyref s)       = Polytyref (sub `substitute` s)++-- ** Class 'Polytyrefable'++class Polytyrefable a where+	polytyref :: a -> Polytyref++instance Polytyrefable Monotype       where polytyref = Polytyref . polytype+instance Polytyrefable Polytype       where polytyref = Polytyref . polytype+instance Polytyrefable Polytyref      where polytyref = id+instance Polytyrefable Polyvar        where polytyref = Polytyref_Var+instance Polytyrefable Qualified_Type where polytyref = Polytyref . polytype
+ Language/LOL/Typing/Type/Qualification.hs view
@@ -0,0 +1,84 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Type.Qualification where++import Data.Eq (Eq)+import qualified Data.Foldable as Foldable+import Data.Function (($), (.))+import Data.Functor (Functor(..), (<$>))+import qualified Data.List as List+import Data.Monoid (Monoid(..), (<>))+import Text.Show (Show(..))+import Data.Text.Buildable (Buildable(..))++import Language.LOL.Typing.Type.Monotype+import Language.LOL.Typing.Type.Substitution+import Language.LOL.Typing.Type.Quantification++-- * Type 'Qualification'++-- | A 'Qualification' introduces constraints on 'Monotype_Var's.+--+-- Example: the qualified 'Polytype': @forall a. Eq a => [a] -> [a]@+--          restricts @a@ to the members of the 'Class' @Eq@.+--+-- Example: @forall a b. (a ~ b) => a -> b@+-- could be an alternative formulation for the 'Polytype'+-- of the /identity function/.+data Qualification qs a+ =   Qualification+ {   qualifiers :: qs+ ,   qualified  :: a+ } deriving (Eq, Show)++-- | Qualify the 'subvars' of given 'a' (except those in given @context@)+-- with given @[qualifier]@.+qualify_but ::+ ( Substitutable qualifier+ , Substitutable a+ ) => [Monovar] -> [qualifier] -> a+ -> Qualification [qualifier] a+qualify_but vars_mono quals qualified =+	Qualification+	 { qualifiers = List.filter is_quantified quals+	 , qualified+	 }+	where+		vars_poly = subvars qualified List.\\ vars_mono+		is_quantified = Foldable.any (`List.elem` vars_poly) . subvars++instance Functor (Qualification qt) where+	fmap f q = q{qualified = f (qualified q)}+instance Buildable q => Buildable+ ( Quantification_Build_Options+ , Qualification [q] Monotype+ ) where+	build (_opts, q) = build q++instance+ ( Substitutable q+ , Substitutable a+ ) => Substitutable (Qualification q a) where+	subvars q = subvars (qualifiers q) `List.union` subvars (qualified q)+	sub `substitute` q = Qualification+	 { qualifiers = sub `substitute` qualifiers q+	 , qualified  = sub `substitute` qualified  q+	 }+instance (Has_Monotypes q, Has_Monotypes a) => Has_Monotypes (Qualification q a) where+	monotypes = monotypes . qualifiers+	monotypes_map f q = Qualification+	 { qualifiers = monotypes_map f $ qualifiers q+	 , qualified  = monotypes_map f $ qualified  q+	 }+instance (Buildable q, Buildable a)+ => Buildable (Qualification [q] a) where+	build Qualification{qualifiers, qualified} =+		(case qualifiers of+		 []  -> ""+		 [q] -> build q <> " => "+		 _   -> "(" <> mconcat (List.intersperse ", " $ build <$> qualifiers) <> ") => "+		) <>+		build qualified
+ Language/LOL/Typing/Type/Quantification.hs view
@@ -0,0 +1,464 @@+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Type.Quantification where++import Data.Bool+import Data.Eq (Eq)+import qualified Data.Foldable as Foldable+import Data.Function (($), (.))+import Data.Functor (Functor(..), (<$>))+import Data.Int (Int)+import qualified Data.List as List+import qualified Data.Map.Strict as Map+import Data.Maybe (Maybe(..), fromMaybe, maybeToList, isNothing)+import Data.Monoid (Monoid(..), (<>))+import Data.Proxy (Proxy(..))+import Data.Text (Text)+import qualified Data.Text as Text+import Data.Text.Buildable (Buildable(..))+import Data.Tuple (fst)+import Prelude (Num(..))+import Text.Read (read)+import Text.Show (Show(..))++import Language.LOL.Typing.Type.Monotype+import Language.LOL.Typing.Type.Substitution+import Language.LOL.Typing.Lib.Data.Default (Default(..))++-- * Type 'Quantification'++-- | 'Universal' and 'Existential' /quantification of 'Monotype's/.+--+-- A 'Quantification' is an abstract interpretation+-- of an expression that can be inlined in many places.+data Quantification quantification_type a+ =   Quantification+ { quantifiers :: [Quantifier]+   -- ^ /quantifying type variables/+ , quantifier_hintnames :: [Quantifier_Hinted]+   -- ^ original names used for some 'quantifiers'+   -- (likely to carry some meaning for a human)+ , quantified :: a+   -- ^ value upon which the 'Quantification' applies+ } deriving (Eq, Show)++-- | A type synonym indicating a /quantifying type variable/:+-- a /type variable/ bound by a 'Quantification'.+type Quantifier = Monovar++quantification :: a -> Quantification quantification_type a+quantification = Quantification mempty mempty++quantify+ :: Substitutable a+ => [Monovar] -> a+ -> Quantification qt a+quantify quantifiers quantified =+	Quantification+	 { quantifiers+	 , quantifier_hintnames = []+	 , quantified+	 }++quantify_rigvars+ :: Rigvarifiable a+ => [Rigvar] -> a+ -> Quantification qt a+quantify_rigvars quantifiers a =+	Quantification+	 { quantifiers+	 , quantifier_hintnames = []+	 , quantified = [ (v, Monotype_Var v) | v <- quantifiers ] `rigidvars_substitute` a+	 }++instance Functor (Quantification quantification_type) where+	fmap f q = q{quantified = f (quantified q)}+instance Substitutable a => Substitutable (Quantification quantification_type a) where+	-- | NOTE: the 'subvars' of a 'Quantification'+	-- do not include the 'quantifiers'.+	subvars q = subvars (quantified q) List.\\ quantifiers q+	sub `substitute` q = q{ quantified =+		substitution_domain_remove (quantifiers q) sub+		 `substitute` quantified q }+instance Has_Monotypes a => Has_Monotypes (Quantification quantification_type a) where+	monotypes = monotypes . quantified+	monotypes_map f q = q{ quantified = monotypes_map f $ quantified q }+{-+instance+ ( Buildable (Quantification_Build_Options, a)+ , Substitutable a+ ) => Buildable (Quantification q a) where+	build q = build ((def::Quantification_Build_Options), q)+-}++-- ** Type 'Quantifier_Freshname'++-- | A 'Quantifier_Name' for a 'Quantifier',+-- which is unique with respect to some 'Monoconst's.+type Quantifier_Freshname = (Quantifier, Quantifier_Name)+type Quantifier_Name = Monoconst+-- | A 'Quantifier_Name' for a 'Quantifier',+-- to be used as a hint to determine a 'Quantifier_Freshname'.+type Quantifier_Hinted = (Quantifier, Quantifier_Name)+-- | A 'Quantifier' without any hint+-- to determine a 'Quantifier_Freshname'.+type Quantifier_Hintless = Quantifier++-- | Return 'Quantifier_Freshname's+-- for given 'Quantifier's,+-- without using any of given 'Monoconst's.+quantifiers_freshify+ :: Monoconsts -- ^ 'Monoconst's already used.+ -> [Quantifier_Hinted] -- ^ Hints to use.+ -> [Quantifier] -- ^ 'Quantifier's to freshify.+ -> (Monoconsts, [Quantifier_Freshname]) -- ^ Fresh 'Quantifier_Name's, and 'Monoconst's now used.+quantifiers_freshify consts_used hints quants =+	quantifiers_hint_freshify consts_used $+	quantifiers_hint_partition hints quants++-- | Partition between 'Quantifier_Hinted' and 'Quantifier_Hintless'.+quantifiers_hint_partition+ :: [Quantifier_Hinted] -- ^ Hints to use.+ -> [Quantifier] -- ^ 'Quantifier's to partition.+ -> ([Quantifier_Hinted], [Quantifier_Hintless])+quantifiers_hint_partition hints =+	List.foldr (\q (yes, no) ->+		case List.lookup q hints of+		 Nothing -> (yes, q:no)+		 Just n -> ((q, n):yes, no))+	 mempty++-- | Return 'Quantifier_Freshname's+-- for given hinted and hintless 'Quantifier's,+-- without using any of given 'Monoconst's.+quantifiers_hint_freshify+ :: Monoconsts -- ^ 'Monoconst's already used.+ -> ([Quantifier_Hinted], [Quantifier_Hintless]) -- ^ 'Quantifier's to freshify.+ -> (Monoconsts, [Quantifier_Freshname]) -- ^ 'Monoconst's now used, and Fresh 'Quantifier_Name's.+quantifiers_hint_freshify consts_used (quants_hinted, quants_hintless) =+	let (consts_used', quants_hinted_fresh) =+		quantifiers_freshify_hinted consts_used quants_hinted in+	let (consts_used'', quants_hintless_fresh) =+		quantifiers_freshify_hintless consts_used' quants_hintless in+	let quants_fresh = quants_hinted_fresh <> quants_hintless_fresh in+	(consts_used'', quants_fresh)++-- | Rename a bit any hinted 'Quantifier_Name'+-- in order to avoid capturing given 'Monoconst's:+-- by appending an increasing integer suffix+-- to any given 'Quantifier_Hinted' colliding.+quantifiers_freshify_hinted+ :: Monoconsts -- ^ 'Monoconst's already used.+ -> [Quantifier_Hinted] -- ^ 'Quantifier's to freshify.+ -> (Monoconsts, [Quantifier_Freshname]) -- ^ 'Monoconst's now used, and Fresh 'Quantifier_Name's.+quantifiers_freshify_hinted monoconsts_used =+	List.foldr freshify (monoconsts_used, [])+	where+	freshify+	 :: (Quantifier, Quantifier_Name)+	 -> (Monoconsts, [Quantifier_Hinted])+	 -> (Monoconsts, [Quantifier_Freshname])+	freshify (q, name) (consts_used, qnames) =+		let ints = [1..] :: [Int] in+		let fresh_name =+			List.head+			 [ x+			 | extra <- "" : (show <$> ints)+			 , x <- [name <> Text.pack extra]+			 , isNothing (Map.lookup x consts_used)+			 ] in+		( Map.insert fresh_name () consts_used+		, (q, fresh_name):qnames )++quantifiers_freshify_hintless+ :: Monoconsts -- ^ 'Monoconst's already used.+ -> [Quantifier_Hintless] -- ^ 'Quantifier's to freshify.+ -> (Monoconsts, [Quantifier_Freshname]) -- ^ 'Monoconst's now used, and Fresh 'Quantifier_Name's.+quantifiers_freshify_hintless consts_used quants =+	let fresh_qnames = List.zip quants (const_pool List.\\ Map.keys consts_used) in+	let fresh_consts = Map.fromList $ (\(_, x) -> (x, ())) <$> fresh_qnames in+	( Map.union fresh_consts consts_used+	, fresh_qnames )++-- ** Type 'Quantification_Build_Options'++data Quantification_Build_Options+ =   Quantification_Build_Options+	 { quantification_build_option_consts_used :: Monoconsts+	   -- ^ The context of 'Monoconst's not to be captured+	   -- by the 'quantifiers' to output.+	 , quantification_build_option_force_var_names :: Bool+	   -- ^ Output 'quantifiers' like other 'subvars'+	   -- instead of using 'quantifier_hintnames' and 'const_pool'.+	 , quantification_build_option_show_toplevel_quantifiers :: Bool+	   -- ^ Output a declaration for the 'quantifiers',+	   --+	   -- Example: @forall a b.@+	   --+	   -- Example: @exists a b.@+	 , quantification_build_option_use_hints :: Bool+	   -- ^ Whether to use 'quantifier_hintnames'+	   -- to output the 'quantifiers'.+	 , quantification_build_option_var_prefix :: Text+	   -- ^ A prefix for 'subvars' which are not 'quantifiers'.+	 }++instance Default Quantification_Build_Options where+	def =+		Quantification_Build_Options+		 { quantification_build_option_consts_used               = mempty+		 , quantification_build_option_force_var_names           = False+		 , quantification_build_option_show_toplevel_quantifiers = True+		 , quantification_build_option_use_hints                 = True+		 , quantification_build_option_var_prefix                = "m"+		 }+instance Buildable (Quantification_Build_Options, Monotype) where+	build (_opts, ty) = build ty+instance+ ( Buildable (Quantification_Build_Options, a)+ , Buildable (Proxy qt)+ , Substitutable a+ ) => Buildable (Quantification_Build_Options, Quantification qt a) where+	build+	 ( opts@Quantification_Build_Options+		 { quantification_build_option_consts_used+		 , quantification_build_option_force_var_names+		 , quantification_build_option_show_toplevel_quantifiers+		 , quantification_build_option_use_hints+		 , quantification_build_option_var_prefix+		 }+	 , Quantification+		 { quantifiers+		 , quantifier_hintnames+		 , quantified+		 } ) =+		let subvas = subvars quantified in+		let quants = quantifiers `List.intersect` subvas in+		 -- NOTE: hide unused 'quantifiers'.+		let (consts_used, freshnames_quanted) =+			if quantification_build_option_force_var_names+			then (quantification_build_option_consts_used, [])+			else+				quantifiers_hint_freshify+				 quantification_build_option_consts_used $+					if quantification_build_option_use_hints+					then quantifiers_hint_partition quantifier_hintnames quants+					else ([], quants) in+		let freshnames_quantless =+			(\v -> -- NOTE: find a name for the non-quantifying substitutable 'Monovar's.+				(v, quantification_build_option_var_prefix <> Text.pack (show v))+			 ) <$> (subvas List.\\ (fst <$> freshnames_quanted)) in+		let freshsub = substitution_finite $+			(Monotype_Const <$>) <$> (freshnames_quanted <> freshnames_quantless) in+		(if quantification_build_option_show_toplevel_quantifiers+		&& not (Foldable.null quants)+		then build_declaration $ (freshsub `substitute`) . Monotype_Var <$> quants+		else "") <>+		build+		 ( opts+			 { quantification_build_option_consts_used = consts_used+			 , quantification_build_option_show_toplevel_quantifiers = True+			 }+		 , freshsub `substitute` quantified+		 )+		where+		build_declaration quants =+			build (Proxy::Proxy qt) <> " " <>+			mconcat (List.intersperse " " $ build <$> quants) <> ". "++-- ** Type 'Unquantification'++data Unquantification a+ =   Unquantification+ {   unquantification_freshvar :: Freshvar+     -- ^ The given 'Freshvar'+     -- usable for the next fresh 'Monovar' (or 'Rigvar'),+     -- incremented by one for each fresh 'Monovar' (or 'Rigvar's)+     -- as needed by 'unquantify'.+ ,   unquantified :: a+     -- ^ The given 'quantified' value with the 'quantifiers'+     -- replaced by fresh 'Monovar's (or 'Rigvar's).+ }++-- | Type synonym to signify that a 'Monovar' is used as a counter.+type Freshvar = Monovar++-- | Perform a /type variable unabstraction/ (aka. /type variable instantiation/).+--+-- Return the 'quantified' value of the given 'Quantification'+-- with its 'quantifiers' 'substitute'd+-- by 'Monovar's counting from given 'Monovar'+-- and applied to given 'Monotype' injection,+-- along with the 'Freshvar' incremented as needed.+unquantify+ :: Substitutable a+ => (Freshvar -> Monotype)+ -> Freshvar+ -> Quantification qt a+ -> Unquantification a+unquantify monoty freshvar+ Quantification{quantifiers, quantified} =+	Unquantification+	 { unquantification_freshvar = freshvar + List.length quantifiers+	 , unquantified              = sub `substitute` quantified+	 }+	where+	sub = substitution_finite $+		List.zip quantifiers (monoty <$> [freshvar..])++-- ** Type 'Universal'++data Universal+type Forall = Quantification Universal++instance Show (Proxy Universal) where+	show _ = "Universal"+instance Buildable (Proxy Universal) where+	build _ = "forall"++-- | /Generalize/ a 'Monotype' to a 'Polytype',+-- 'quantify'ing all its 'subvars'.+for_all :: Substitutable a => a -> Forall a+for_all a = quantify (subvars a) a++-- | /Generalize/ a 'Monotype' to a 'Polytype',+-- 'quantify'ing its 'subvars' which are within given 'Monovar's.+forall_in :: Substitutable a => [Monovar] -> a -> Forall a+forall_in quants a = quantify (quants `List.intersect` subvars a) a++-- | /Generalize/ a 'Monotype' to a 'Polytype'+-- 'quantify'ing all its 'subvars'+-- except those within given 'Monovar's.+forall_but+ :: Substitutable a+ => [Monovar] -> a -> Forall a+forall_but vars_mono a = forall_in (subvars a List.\\ vars_mono) a++-- | 'unquantify' a 'Forall' with fresh 'Monovar's.+unquantify_forall+ :: Substitutable a+ => Freshvar -> Forall a+ -> Unquantification a+unquantify_forall = unquantify Monotype_Var++-- ** Type 'Existential'++data Existential+type Exists = Quantification Existential++instance Show (Proxy Existential) where+	show _ = "Existential"+instance Buildable (Proxy Existential) where+	build _ = "exists"++exists :: Rigvarifiable a => a -> Exists a+exists a = quantify_rigvars (rigidvars a) a++unquantify_exists+ :: Substitutable a+ => Rigvar -> Exists a+ -> Unquantification a+unquantify_exists = unquantify (Monotype_Const . monoconst_from_rigvar)++reveal+ :: Substitutable a+ => Freshvar -> Exists a+ -> Unquantification a+reveal = unquantify Monotype_Var++unreveal :: Substitutable a => [Monovar] -> a -> Exists a+unreveal vars a = quantify (vars `List.intersect` subvars a) a++-- * Type 'Rigvar'++-- | A /rigid type variable/ (aka. /skolem constant/, named after Thoralf Skolem)+-- is a 'Monovar' bound by a 'Quantification'+-- outside the current /typing context/+-- (therefore a 'Rigvar' cannot be unified with an other 'Monovar').+--+-- Intuitionally, a 'Rigvar' represents a /fixed unknown 'Monotype'/.+type Rigvar = Monovar++-- | 'Monotype' which must remain monomorphic,+-- used to form the current /typing context/.+type Rigtype = Monotype++-- | A /rigvarification/ is a special form of 'unquantify'cation+-- in which the 'quantifiers' are replaced by fresh 'Rigvar's:+-- these are 'Monoconst's that do not appear elsewhere.+--+-- NOTE: 'rigconstify'ing a 'Forall' 'Quantification'+-- is an implementation technique+-- used to ensure that no assumption can be made+-- about certain 'Monovar's.+rigconstify+ :: Substitutable a+ => Freshvar -> Forall a+ -> Unquantification a+rigconstify  = unquantify (Monotype_Const . monoconst_from_rigvar)++unrigconstify :: Rigvarifiable a => a -> Forall a+unrigconstify a = quantify_rigvars (rigidvars a) a++-- | A prefix to single out 'Rigvar's from other 'Monoconst's.+rigvar_prefix :: Text+rigvar_prefix = "_"++monoconst_from_rigvar :: Rigvar -> Monoconst+monoconst_from_rigvar = (rigvar_prefix <>) . Text.pack . show++rigvar_from_monoconst :: Monoconst -> Maybe Rigvar+rigvar_from_monoconst c+ | rigvar_prefix `Text.isPrefixOf` c =+	Just $ read $ Text.unpack $+	Text.drop (Text.length rigvar_prefix) c+ | otherwise = Nothing++-- | Return the given 'Substitutable' value+-- with its 'subvars' mapped to 'Monotype_Const'.+constify_subvars :: Substitutable a => a -> a+constify_subvars a = sub `substitute` a+	where+	sub =+		substitution_finite+		 [ (v, Monotype_Const $ monoconst_from_rigvar v)+		 | v <- subvars a+		 ]++-- ** Type 'Rigvar_Substitution'++type Rigvar_Substitution = [(Rigvar, Monotype)]++-- ** Class 'Rigvarifiable'++-- | Like 'Substitutable', but acting on 'Rigvar's.+class Rigvarifiable a where+	rigidvars :: a -> [Rigvar]+	rigidvars_substitute :: Rigvar_Substitution -> a -> a++instance Rigvarifiable Monotype where+	rigidvars monoty =+		case monoty of+		 Monotype_Var _   -> []+		 Monotype_Const c -> maybeToList $ rigvar_from_monoconst c+		 Monotype_App l r -> rigidvars l `List.union` rigidvars r+	+	rigidvars_substitute rsub monoty =+		case monoty of+		 Monotype_Var _ -> monoty+		 Monotype_Const c ->+			fromMaybe monoty $ do+				rig <- rigvar_from_monoconst c+				rig `List.lookup` rsub+		 Monotype_App l r ->+			Monotype_App+			 (rsub `rigidvars_substitute` l)+			 (rsub `rigidvars_substitute` r)+instance Rigvarifiable a => Rigvarifiable [a] where+	rigidvars = List.foldr (List.union . rigidvars) []+	rigidvars_substitute rsub = ((rsub `rigidvars_substitute`) <$>)
+ Language/LOL/Typing/Type/Substitution.hs view
@@ -0,0 +1,203 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Type.Substitution where++import Data.Bool+import Data.Either (Either(..), either)+import Data.Eq (Eq(..))+import Data.Function (($), (.))+import Data.Functor ((<$>))+import qualified Data.List as List+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Maybe (Maybe(..), fromMaybe, maybe)+import Data.Monoid (Monoid(..), (<>))+import Data.Sequence (Seq)+import qualified Data.Set as Set+import Data.Text.Buildable (Buildable(..))+import Prelude (Num(..), error)+import Text.Show (Show(..))++import Language.LOL.Typing.Type.Monotype+import Language.LOL.Typing.Lib.Data.Empty (Empty(..))++-- * Class 'Substitution'++-- | A /monomorphic type substitution/.+--+-- TODO: maybe rename to Monosub?+class Substitution s where+	substitution_codomain        :: s -> [Monotype]+	substitution_domain          :: s -> [Monovar]+	substitution_domain_remove   :: [Monovar] -> s -> s+	substitution_domain_restrict :: [Monovar] -> s -> s+	substitution_lookup          :: Monovar -> s -> Maybe Monotype++-- ** Type 'Substitution_Finite'++-- | A 'Substitution' represented by a finite map.+type Substitution_Finite = Map Monovar Monotype++instance Empty Substitution_Finite where+	empty = mempty+instance Buildable Substitution_Finite where+	build =+		mconcat . List.intersperse "\n" .+		Map.foldrWithKey (\var ty ->+			((build (Monotype_Var var) <> " == " <> build ty) :)+		 ) []+instance Substitution Substitution_Finite where+	substitution_codomain = Map.elems+	substitution_domain   = Map.keys+	substitution_domain_remove vars s =+		List.foldr Map.delete s vars+	substitution_domain_restrict vars =+		Map.filterWithKey (\v _ -> Set.member v vars_kept)+		where vars_kept = Set.fromList vars+	substitution_lookup = Map.lookup++substitution_finite_singleton :: Monovar -> Monotype -> Substitution_Finite+substitution_finite_singleton = Map.singleton++substitution_finite :: [(Monovar, Monotype)] -> Substitution_Finite+substitution_finite = Map.fromList++-- | Safely unify two 'Substitution_Finite's.+--+-- NOTE: the union is left-biased:+-- it prefers the first 'Substitution_Finite'+-- when duplicate keys are encountered.+substitution_finite_union :: Substitution_Finite -> Substitution_Finite -> Substitution_Finite+substitution_finite_union x y = x `Map.union` ((x `substitute`) <$> y)++-- | Unsafely unify two 'Substitution_Finite's.+substitution_finite_union_unsafe :: Substitution_Finite -> Substitution_Finite -> Substitution_Finite+substitution_finite_union_unsafe = Map.union++-- ** Type 'Substitution_Fixpoint'++-- | A fixpoint is computed when looking up+-- the target of a 'Monovar' in this 'Substitution'.+-- 'mappend'ing two 'Substitution's is cheap,+-- whereas a 'substitution_lookup' is more expensive+-- than with 'Substitution_Finite'.+newtype Substitution_Fixpoint+ =      Substitution_Fixpoint (Map Monovar Monotype)+ deriving (Show)++instance Empty Substitution_Fixpoint where+	empty = Substitution_Fixpoint Map.empty+instance Buildable Substitution_Fixpoint where+	build (Substitution_Fixpoint sub) = build sub+-- | WARNING: only disjoint 'Substitution_Fixpoint's can be 'mappend'ed.+instance Monoid Substitution_Fixpoint where+	mempty  = empty+	mappend = substitution_fixpoint_union+instance Substitution Substitution_Fixpoint where+	substitution_codomain (Substitution_Fixpoint s) = Map.elems s+	substitution_domain   (Substitution_Fixpoint s) = Map.keys  s+	substitution_domain_remove vars (Substitution_Fixpoint s) =+		Substitution_Fixpoint $+		Map.filterWithKey (\v _ -> v `List.notElem` vars) s+	substitution_domain_restrict vars (Substitution_Fixpoint s) =+		Substitution_Fixpoint $+		Map.filterWithKey (\v _ -> Set.member v vars_kept) s+		where vars_kept = Set.fromList vars+		-- Map.filterWithKey (\v _ -> v `List.notElem` vars_removed) s+		-- where vars_removed = Map.keys s List.\\ vars+	substitution_lookup v sub@(Substitution_Fixpoint s) =+		case Map.lookup v s of+		 Nothing -> Nothing+		 Just ty | ty == Monotype_Var v -> Nothing+		         | otherwise -> Just $ sub `substitute` ty++substitution_fixpoint :: [(Monovar, Monotype)] -> Substitution_Fixpoint+substitution_fixpoint = Substitution_Fixpoint . Map.fromList++-- | WARNING: only valid with disjoint 'Substitution_Fixpoint's+substitution_fixpoint_union+ :: Substitution_Fixpoint+ -> Substitution_Fixpoint+ -> Substitution_Fixpoint+substitution_fixpoint_union+ (Substitution_Fixpoint x)+ (Substitution_Fixpoint y) =+	Substitution_Fixpoint $+	Map.unionWith err x y+	where err = error "substitution_fixpoint_union: the two substitutions are not disjoint"++-- ** Type 'Substitution_Instance'++data Substitution_Instance+ = forall s. Substitution s+ => Substitution_Instance+	 { substitution_instance_substitution :: s+	 , substitution_instance_codomain     :: s -> [Monotype]+	 , substitution_instance_domain       :: s -> [Monovar]+	 , substitution_instance_remove       :: [Monovar] -> s -> s+	 , substitution_instance_restrict     :: [Monovar] -> s -> s+	 , substitution_instance_lookup       :: Monovar -> s -> Maybe Monotype+	 }++substitution_instance :: Substitution s => s -> Substitution_Instance+substitution_instance s =+	Substitution_Instance s+	 substitution_codomain+	 substitution_domain+	 substitution_domain_remove+	 substitution_domain_restrict+	 substitution_lookup++instance Substitution Substitution_Instance where+	substitution_codomain           (Substitution_Instance s f _ _ _ _) = f s+	substitution_domain             (Substitution_Instance s _ f _ _ _) = f s+	substitution_domain_remove   vs (Substitution_Instance s _ _ f _ _) = substitution_instance (f vs s)+	substitution_domain_restrict vs (Substitution_Instance s _ _ _ f _) = substitution_instance (f vs s)+	substitution_lookup          v  (Substitution_Instance s _ _ _ _ f) = f v s++-- * Class 'Substitutable'++class Substitutable a where+	-- | /substitutable type variables/ (aka. /free type variables/).+	subvars :: a -> [Monovar]+	-- | /idempotent substitution application/.+	substitute :: Substitution s => s -> a -> a++instance Substitutable Monotype where+	subvars ty =+		case ty of+		 Monotype_Var v -> [v]+		 Monotype_Const _ -> []+		 Monotype_App t1 t2 -> subvars t1 `List.union` subvars t2+	sub `substitute` ty =+		case ty of+		 Monotype_Var v -> fromMaybe (Monotype_Var v) $ substitution_lookup v sub+		 Monotype_Const _ -> ty+		 Monotype_App t1 t2 -> Monotype_App (sub `substitute` t1) (sub `substitute` t2)+instance Substitutable a => Substitutable [a] where+	subvars = List.foldr (List.union . subvars) []+	substitute sub = ((sub `substitute`) <$>)+instance Substitutable a => Substitutable (Seq a) where+	subvars        = List.foldr (List.union . subvars) mempty+	substitute sub = ((sub `substitute`) <$>)+instance Substitutable a => Substitutable (Maybe a) where+	subvars = maybe [] subvars+	sub `substitute` m  = (sub `substitute`) <$> m+instance (Substitutable a, Substitutable b) => Substitutable (Either a b) where+	subvars = either subvars subvars+	sub `substitute` e = either (Left . (sub `substitute`)) (Right . (sub `substitute`)) e++-- | Return the next 'Monovar'+-- that is not in the 'subvars'+-- of the given 'Substitutable' value.+--+-- NOTE: return @0@ when 'subvars' is empty+subvar_next :: Substitutable a => a -> Monovar+subvar_next a =+	case subvars a of+	 [] -> 0+	 vs -> 1 + List.maximum vs
+ Language/LOL/Typing/Type/Synotype.hs view
@@ -0,0 +1,238 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Type.Synotype where++import Control.Monad (forM)+import Data.Bool+import Data.Eq (Eq(..))+import qualified Data.Foldable as Foldable+import Data.Function (($), (.), id)+import Data.Functor ((<$>))+import qualified Data.Graph as Graph (scc, buildG)+import Data.Int (Int)+import qualified Data.List as List+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Maybe (Maybe(..), fromMaybe, maybe)+import Data.Monoid (Monoid(..), (<>))+import Data.Ord (Ord(..))+import qualified Data.Text as Text+import Data.Text.Buildable (Buildable(..))+import qualified Data.Tree as Tree (flatten)+import Data.Tuple (uncurry)+import Prelude (Num(..), error)+import Text.Show (Show(..), showChar, showParen, showString)++import Language.LOL.Typing.Type.Monotype+import Language.LOL.Typing.Type.Substitution+import Language.LOL.Typing.Lib.Data.Empty (Empty(..))++-- * Type 'Synotype'++-- | An (unordered) collection of /type synonyms/.+data Synotype+ = Synotype+ { synotype_arity    :: Arity+ , synotype_monotype :: [Monotype] -> Monotype+ }+type Synotypes+ = Map Synoname Synotype++type Synoname = Monoconst++-- | An ordering of 'Synotypes'.+type Synotype_Ordering+ = Map Synoname Synotype_Position++-- | A position in a 'Synotype_Ordering'.+type Synotype_Position = Int++-- | 'Synotypes' with a 'Synotype_Ordering'.+data Synotype_Substitution+ =   Synotype_Substitution+ {   synotypes_ordering :: Synotype_Ordering+ ,   synotypes          :: Synotypes+ }+instance Show Synotype_Substitution where+	showsPrec d Synotype_Substitution{synotypes_ordering} =+		showParen (d > 10) $+		showString "Synotype_Substitution" .+		showChar ' ' .+		showChar '[' .+		showString+		 (mconcat $ List.intersperse ", " $+			Text.unpack <$> Map.keys synotypes_ordering) .+		showChar ']'+instance Buildable Synotype_Substitution where+	build Synotype_Substitution{synotypes_ordering} =+		"[" <>+		mconcat (+			List.intersperse ", " $+			build <$> Map.keys+			synotypes_ordering) <>+		"]"++instance Empty Synotype_Substitution where+	empty = Synotype_Substitution+	 { synotypes_ordering = mempty+	 , synotypes          = mempty+	 }++-- | A 'type_String' is a 'type_List' of 'type_Char's+synotype_String :: Synotype_Substitution+synotype_String =+	Synotype_Substitution+	 (Map.singleton "String" 0)+	 (Map.singleton "String" $ Synotype 0 $ \_ -> type_List type_Char)++-- | Return the 'Synotype_Ordering' of given 'Synotypes'+-- along with the mutually recursive 'Synotypes' that are detected.+synorder+ :: Synotypes+ -> (Synotype_Ordering, [[Synoname]])+synorder sys =+	let keys = Map.keys sys in+	let names = Map.fromList $ List.zip keys [0..] in+	let positions = Map.fromList $ List.zip [0..] keys in+	+	let err = error "synorder: error in lookup table" in+	let name_lookup n = fromMaybe err (Map.lookup n names) in+	let pos_lookup  p = fromMaybe err (Map.lookup p positions) in+	+	let edges = Map.foldrWithKey go [] sys+		where+		go s1 (Synotype ari monoty) es =+			Map.foldrWithKey add es $+			monoconsts $ monoty (Monotype_Var <$> [0 .. ari - 1])+			where+			add s2 _ =+				case Map.lookup s2 names of+				 Just i2 -> (:) (i2, i1)+				 Nothing -> id+				where+				i1 = name_lookup s1+	 in+	+	let graph = Graph.buildG (0, Map.size sys - 1) edges in+	let list  = Tree.flatten <$> Graph.scc graph in+	+	let (ordering, recursive, _) =+		List.foldr go (Map.empty, [], 0) list+		where+		go ps (os, rs, counter) =+			case ps of+			 [p] | (p, p) `List.notElem` edges -> -- NOTE: correct type synotype+				( Map.insert (pos_lookup p) counter os+				, rs+				, counter + 1+				)+			 _ ->+				( os+				, (pos_lookup <$> ps) : rs+				, counter+				)+	 in+	(ordering, recursive)++-- | Return whether given 'Synoname'+-- +is_panthom_synotype :: Synotype_Substitution -> Synoname -> Bool+is_panthom_synotype Synotype_Substitution{synotypes} name =+	case Map.lookup name synotypes of+	 Nothing -> False+	 Just (Synotype ari monoty) ->+		let args = List.take ari [0..] in+		let subvars_ty = subvars $ monoty (Monotype_Var <$> args) in+		Foldable.any (`List.notElem` subvars_ty) args++-- | Fully expand a type in a recursive way.+synexpand :: Synotypes -> Monotype -> Monotype+synexpand sys ty =+	top_expanded `monoapp` (synexpand sys <$> tail)+	where top_expanded `App_Spine` tail =+		app_spine_left $ synexpand_tops sys ty++-- | Fully expand the top-level 'Monotype_Const's.+synexpand_tops :: Synotypes -> Monotype -> Monotype+synexpand_tops sys ty =+	maybe ty (synexpand_tops sys) $+	synexpand_top_step sys ty++{-+-- | Fully expand the top-level 'Monotype_Const'.+synexpand_top :: Synotype_Substitution -> Monotype -> Maybe Monotype+synexpand_top Synotype_Substitution{synotypes} =+	(synexpand_tops synotypes <$>) .+	synexpand_top_step synotypes+-}++-- | Try to expand the top-level 'Monotype_Const' one step.+synexpand_top_step :: Synotypes -> Monotype -> Maybe Monotype+synexpand_top_step sys ty =+	case app_spine_left ty of+	 Monotype_Const c `App_Spine` args ->+		case Map.lookup c sys of+		 Just (Synotype ari monoty)+		  | ari == List.length args -> Just (monoty args)+		  | otherwise -> err "synotype arity mismatch"+		 Nothing -> Nothing+	 _ -> Nothing+	where+		err s = error $ "synexpand_top_step: " <> s++-- | Try to expand the top-level 'Monotype_Const'+-- of one of the two paired 'Monotype's.+--+-- If both top-level 'Monotype_Const' can be expanded one step,+-- then the 'Synotype' which appears first+-- in the 'Synotype_Ordering' is expanded.+synexpand_top_step_ordered+ :: Synotype_Substitution+ -> (Monotype, Monotype)+ -> Maybe (Monotype, Monotype)+synexpand_top_step_ordered+ Synotype_Substitution{synotypes_ordering, synotypes}+ (ty1, ty2) =+	case (position ty1, position ty2) of+	 (Just p1, Just p2) | p1 <= p2  -> Just (expand_top_step ty1, ty2)+	                    | otherwise -> Just (ty1, expand_top_step ty2)+	 (Just _ , Nothing) -> Just (expand_top_step ty1, ty2)+	 (Nothing, Just _ ) -> Just (ty1, expand_top_step ty2)+	 _ -> Nothing+	where+	position ty =+		case app_spine_left ty of+		 Monotype_Const c `App_Spine` _ -> Map.lookup c synotypes_ordering+		 _ -> Nothing+	expand_top_step ty =+		fromMaybe+		 (error "synexpand_top_step_ordered: Synotype_Substitution is invalid")+		 (synexpand_top_step synotypes ty)++-- | Return the /most general type/+-- (i.e. with the least number of expansions).+-- of two 'Monotype's which must be equal+-- under given 'Synotype_Substitution'.+mgt_with_synotypes+ :: Synotype_Substitution+ -> Monotype -> Monotype+ -> Maybe Monotype+mgt_with_synotypes syns t1 t2 =+	case (app_spine_left t1, app_spine_left t2) of+	 (  Monotype_Var v `App_Spine` []+	  , Monotype_Var _ `App_Spine` [] )+	  -> Just $ Monotype_Var v+	 (  Monotype_Const c1 `App_Spine` tail1+	  , Monotype_Const c2 `App_Spine` tail2 )+	  | c1 == c2 && not (is_panthom_synotype syns c1)+	  -> do+		mgts <-+			forM (List.zip tail1 tail2) $ uncurry $+			mgt_with_synotypes syns+		Just (Monotype_Const c1 `monoapp` mgts)+	  | otherwise -> do+		(t1', t2') <- synexpand_top_step_ordered syns (t1, t2)+		mgt_with_synotypes syns t1' t2'+	 _ -> Nothing
+ Language/LOL/Typing/Type/Test.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE OverloadedStrings #-}+module Type.Test where++import Data.Function (($))+import Data.Text.Buildable (Buildable(..))+import Test.Tasty+import Test.Tasty.HUnit+-- import Test.HUnit hiding (test)++import Language.LOL.Typing.Type+import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build++tests :: TestTree+tests = testGroup "Type"+ [ tests_Monotype+ ]++tests_Monotype :: TestTree+tests_Monotype = testGroup "Monotype"+ [ testGroup "Build" $+		let (==>) x expected = testCase (Build.string expected) $ build x @?= expected in+	 [ ("a"::Monotype) ==> "a"+	 , ("a".->."b") ==> "a -> b"+	 , ("a".->."b".->."c") ==> "a -> b -> c"+	 , ("a".->."b".->."c".->."d") ==> "a -> b -> c -> d"+	 , ("a".->."b".->.("c".->."d")) ==> "a -> b -> c -> d"+	 , (("a".->."b").->."c".->."d") ==> "(a -> b) -> c -> d"+	 , (("a".->."b").->.("c".->."d")) ==> "(a -> b) -> c -> d"+	 , ("a".->.("b".->."c").->."d") ==> "a -> (b -> c) -> d"+	 , ((("a".->."b").->.("c".->."d")).->.(("e".->."f").->.("g".->."h")))+		 ==> "((a -> b) -> c -> d) -> (e -> f) -> g -> h"+	 , ("T".!."a".!."b") ==> "T a b"+	 , ("T".!."a".!."b".!.("U".!."c".!."d")) ==> "T a b (U c d)"+	 , ("T".!."a".!."b".->."U".!."c".!."d") ==> "T a b -> U c d"+	 , ("T".!."a".!."b".->."U".!."c".!."d".->."V".!."e".!."f") ==> "T a b -> U c d -> V e f"+	 , ("T".!."x".!.(("a".->."b").->.("c".->."d")).!."y") ==> "T x ((a -> b) -> c -> d) y"+	 ]+ ]
+ Language/LOL/Typing/Type/Unification.hs view
@@ -0,0 +1,127 @@+{-# LANGUAGE NamedFieldPuns #-}+{-# OPTIONS_GHC -fno-warn-tabs #-}+module Language.LOL.Typing.Type.Unification where++import Data.Bool+import Data.Either (Either(..))+import Data.Eq (Eq(..))+import Data.Function (($))+import Data.Functor ((<$>))+import qualified Data.List as List+import qualified Data.Map as Map+import Data.Maybe (Maybe(..), fromMaybe)+import Data.Monoid (Monoid(..), (<>))+import Data.Tuple (snd)+import Prelude (error)+import Text.Show (Show(..))++import Language.LOL.Typing.Type.Monotype+import Language.LOL.Typing.Type.Substitution+import Language.LOL.Typing.Type.Synotype+import Language.LOL.Typing.Lib.Data.Empty (Empty(..))++-- * Type 'Unification'++type Unification+ =   Substitution_Finite++-- | Like 'mgu_with_synotypes', but with an empty 'Synotype_Substitution'.+mgu :: Monotype -> Monotype -> Either Unification_Error Unification+mgu t1 t2 = snd <$> mgu_with_synotypes empty t1 t2++-- | The /most general unification/ ('Substitution') of two 'Monotype's,+--   expanding 'Synotypes' as lazy as possible.+--+-- Example:+--+-- @+--   if String => [Char]+--   then   v11 -> [v11]  `mgu`  String -> [[v14]]+--   should be:+--      [ v11 := [Char] , v14 := Char ]+-- @+--+-- NOTE: the boolean indicates whether expansions were necessary.+mgu_with_synotypes+ :: Synotype_Substitution+ -> Monotype -> Monotype+ -> Either Unification_Error (Bool, Unification)+mgu_with_synotypes syns = go mempty+	where+	err s = error $ "mgu_with_synotypes: " <> s+	go sub t1 t2 =+		case (app_spine_left t1, app_spine_left t2) of+		 (App_Spine (Monotype_Var v) [], _) -> go_Var sub v t2+		 (_, App_Spine (Monotype_Var v) []) -> go_Var sub v t1+		 (  App_Spine (Monotype_Const c1) s1+		  , App_Spine (Monotype_Const c2) s2 )+		  | c1 == c2 && not (is_panthom_synotype syns c1) ->+			go_List sub s1 s2+		  | otherwise ->+			case synexpand_top_step_ordered syns (t1, t2) of+			 Nothing -> Left $ Unification_Error_Constant_clash c1 c2+			 Just (t1', t2') ->+				case go sub t1' t2' of+				 Left e -> Left e+				 Right (_, sub') -> Right (True, sub')+		 _ -> case (t1, t2) of+			 (Monotype_App l1 r1, Monotype_App l2 r2) ->+				go_List sub [l1, r1] [l2, r2]+			 _ ->  err "illegal type"+	go_Var sub v ty =+		case Map.lookup v sub of+		 Just t2 ->+			case go sub ty t2 of+			 Right (True, sub') ->+				let mgt =+					fromMaybe (err "illegal types") $+					mgt_with_synotypes syns+					 (sub' `substitute` ty)+					 (sub' `substitute` t2) in+				Right+				 ( True+				 , substitution_finite_union+					 (substitution_finite_singleton v mgt)+					 (substitution_domain_remove [v] sub')+				 )+			 e -> e+		 Nothing ->+			case sub `substitute` ty of+			 Monotype_Var v' | v == v' -> Right (False, sub)+			 ty' | v `List.elem` subvars ty' -> Left (Unification_Error_Infinite_type v)+			     | otherwise -> Right (False, substitution_finite_singleton v ty' `substitution_finite_union` sub)+	go_List sub [] [] = Right (False, sub)+	go_List sub (s:ss) (t:tt) =+		case go sub s t of+		 Left e -> Left e+		 Right (b,sub') ->+			case go_List sub' ss tt of+			 Left e -> Left e+			 Right (b', sub'') -> Right (b || b', sub'')+	go_List _ _ _ = err "kinds do not match"++-- | Given a set of 'Synotype_Substitution', can two types be unified?+unifiable :: Synotype_Substitution -> Monotype -> Monotype -> Bool+unifiable syns t1 t2 =+	case mgu_with_synotypes syns t1 t2 of+	 Left  _ -> False+	 Right _ -> True++-- | Same as unifiable, but takes as input a list of 'Monotype's+unifiables :: Synotype_Substitution -> [Monotype] -> Bool+unifiables syns (t1:t2:ts) =+	case mgu_with_synotypes syns t1 t2 of+	 Left _         -> False+	 Right (_, sub) -> unifiables syns (sub `substitute` (t2:ts))+unifiables _ _ = True++-- ** Type 'Unification_Error'++-- | Reasons why two 'Monotype's cannot be unified.+data Unification_Error+ =   Unification_Error_Constant_clash Monoconst Monoconst+     -- ^ Two different 'Monoconst's clash (they should be the same).+ |   Unification_Error_Infinite_type Monovar+     -- ^ A 'Monotype_Var' is unified with a composed 'Monotype'+     --   which contains this same 'Monotype_Var'.+ deriving (Eq, Show)
+ Setup.hs view
@@ -0,0 +1,5 @@+import Distribution.Simple (defaultMainWithHooks)+import Distribution.Simple.UUAGC (uuagcLibUserHook)+import UU.UUAGC (uuagc)++main = defaultMainWithHooks (uuagcLibUserHook uuagc)
+ lol-typing.cabal view
@@ -0,0 +1,204 @@+author: Julien Moutinho <julm+lol@autogeree.net>+-- bug-reports: http://bug.autogeree.net/lol+build-type: Custom+cabal-version: >= 1.24+category: Language+-- data-dir: .+-- data-files:+description:+ WARNING: this is a research program+ written as I learn and explore /type inferencing/:+ please understand well by yourself whatever you may take from it;+ any question or contribution being welcome :-)+ .+ This package implements /type inferencing/+ by manipulating /type constraints/+ through 3 successive phases:+ 1. the 'Collect' phase collects them from some expression,+ 2. the 'Order' phase modifies the order in which they will be solved,+ 3. the 'Solver' phase solves them according to the logic+    of some /type inference rules/.+ .+ So far, the principles within these phases+ are mainly a rewrite of Bastiaan Heeren's+ <https://hackage.haskell.org/package/Top Top>,+ using my own code conventions and ideals of simplicity.+ The most notable change being the use of Roman Cheplyaka's+ <https://hackage.haskell.org/package/monad-classes monad-classes>+ (a little bit augmented):+ to handle the 'Monad' stack building a 'Solver'+ (instead of a homegrown machinery I could not understand well).+ At this point, only a /bottom-up/ 'Collect', a no-op 'Order'+ and a 'Greedy' 'Solver' are implemented, supporting:+ /monomorphic types/ ('Monotype'),+ /parametric polymorphism/ ('Polytype'),+ /type class polymorphism/ ('Class'),+ and /type synonyms/ ('Synotype').+ The quite understandable thesis of Bastiaan Heeren+ explains a lot of this in details:+ <http://www.open.ou.nl/bhr/TopQuality.pdf Top Quality Type Error Messages>.+ .+ The <https://hackage.haskell.org/package/uuagc Attribute Grammar System of Universiteit Utrecht>+ is used to demonstrate how to collect /type constraints/ from an expression ('Expr'),+ and then how to transform this /implicitely typed/ expression into an /explicitely typed/+ <https://hackage.haskell.org/package/lol-calculus lol-calculus> expression+ .+ See also: the <https://hackage.haskell.org/package/helium helium> compiler.+extra-source-files:+  stack.yaml,+  uuagc_options,+  Language/LOL/Typing/Collect/Grammar.ag,+  Language/LOL/Typing/Expr/Calculus.ag,+  Language/LOL/Typing/Expr/Grammar.ag+extra-tmp-files:+homepage: http://pad.autogeree.net/informatique/lol/+license: GPL-3+license-file: COPYING+maintainer: Julien Moutinho <julm+lol@autogeree.net>+name: lol-typing+stability: experimental+synopsis: Type inferencer for LOL (λω language)+tested-with: GHC==7.10.3+version: 1.20160822++source-repository head+  location: git://git.autogeree.net/lol+  type:     git++Flag dev+  Default:     False+  Description: Turn on development settings.+  Manual:      True++Flag dump+  Default:     False+  Description: Dump some intermediate files.+  Manual:      True++Flag exe+  Default:     False+  Description: Turn on executables.+  Manual:      True++Flag prof+  Default:     False+  Description: Turn on profiling settings.+  Manual:      True++Flag threaded+  Default:     True+  Description: Enable threads.+  Manual:      True++Custom-Setup+  setup-depends:+    base >= 4.6 && < 5+    , Cabal >= 1.24+    , uuagc >= 0.9+    , uuagc-cabal >= 1.0.6.0++Library+  default-extensions: NoImplicitPrelude+  default-language: Haskell2010+  ghc-options: -Wall -fno-warn-tabs+  if flag(dev)+    cpp-options: -DDEVELOPMENT+    ghc-options:+  if flag(dump)+    ghc-options: -ddump-simpl -ddump-stg -ddump-to-file+  if flag(prof)+    cpp-options: -DPROFILING+    ghc-options: -fprof-auto+  exposed-modules:+    Language.LOL.Typing+    Language.LOL.Typing.Collect+    Language.LOL.Typing.Collect.Constraint+    Language.LOL.Typing.Collect.Grammar+    Language.LOL.Typing.Constraint+    Language.LOL.Typing.Constraint.Either+    Language.LOL.Typing.Constraint.Extra+    Language.LOL.Typing.Constraint.Monotype+    Language.LOL.Typing.Constraint.Polytype+    Language.LOL.Typing.Expr+    Language.LOL.Typing.Expr.Calculus+    Language.LOL.Typing.Expr.Common+    Language.LOL.Typing.Expr.Grammar+    Language.LOL.Typing.Expr.Utils+    Language.LOL.Typing.Expr.Write+    Language.LOL.Typing.Lib.Control.Monad.Classes.EffectsFix+    Language.LOL.Typing.Lib.Control.Monad.Classes.Instance+    Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix+    Language.LOL.Typing.Lib.Control.Monad.Classes.StateInstance+    Language.LOL.Typing.Lib.Data.Default+    Language.LOL.Typing.Lib.Data.Empty+    Language.LOL.Typing.Lib.Data.Text.Buildable+    Language.LOL.Typing.Solver+    Language.LOL.Typing.Solver.Class+    Language.LOL.Typing.Solver.Common+    Language.LOL.Typing.Solver.Constraint+    Language.LOL.Typing.Solver.Greedy+    Language.LOL.Typing.Solver.Monad+    Language.LOL.Typing.Solver.Monotype+    Language.LOL.Typing.Solver.Polytype+    Language.LOL.Typing.Type+    Language.LOL.Typing.Type.Class+    Language.LOL.Typing.Type.Kind+    Language.LOL.Typing.Type.Monotype+    Language.LOL.Typing.Type.Polytype+    Language.LOL.Typing.Type.Qualification+    Language.LOL.Typing.Type.Quantification+    Language.LOL.Typing.Type.Substitution+    Language.LOL.Typing.Type.Synotype+    Language.LOL.Typing.Type.Unification+  build-depends:+    base >= 4.6 && < 5+    , containers >= 0.5 && < 0.6+    , ghc-prim+    , lol-calculus+    , monad-classes >= 0.3.1.1+    -- , monad-control+    , parsec >= 3.1.2 && < 4+    -- , peano+    -- , reflection+    , text+    , text-format+    , transformers >= 0.4 && < 0.5+    -- , transformers-base+    , uuagc >= 0.9+    , uuagc-cabal >= 1.0.6.0+++test-suite lol-typing-test+  type: exitcode-stdio-1.0+  default-extensions: NoImplicitPrelude+  default-language: Haskell2010+  ghc-options: -Wall -fno-warn-tabs+               -main-is Test+  hs-source-dirs: Language/LOL/Typing+  main-is: Test.hs+  other-modules:+    Expr.Test+    Solver.Test+    Type.Test+  if flag(threaded)+    ghc-options: -threaded -rtsopts -with-rtsopts=-N+  if flag(dev)+    cpp-options: -DDEVELOPMENT+    ghc-options:+  if flag(prof)+    cpp-options: -DPROFILING+    ghc-options: -fprof-auto+  build-depends:+    base >= 4.6 && < 5+    , containers >= 0.5 && < 0.6+    , directory+    , filepath+    , ghc-prim+    , lol-calculus+    , lol-typing+    , monad-classes >= 0.3.1.1+    , tasty >= 0.11+    , tasty-hunit+    , text+    , text-format+    , transformers >= 0.4 && < 0.5
+ stack.yaml view
@@ -0,0 +1,15 @@+flags: {}+extra-package-dbs: []+packages:+- '.'+- ../calculus+extra-deps:+- Cabal-1.24.0.0+- monad-classes-0.3.1.1+- peano-0.1.0.1+- uuagc-0.9.52.1+- uuagc-cabal-1.0.6.0+- uulib-0.9.22+explicit-setup-deps:+  '*': true+resolver: lts-6.12
+ uuagc_options view
@@ -0,0 +1,8 @@+file : "Language/LOL/Typing/Expr/Grammar.ag"+options : data, haskellsyntax, rename++file : "Language/LOL/Typing/Expr/Calculus.ag"+options : catas, haskellsyntax, pretty, rename, semfuns, signatures, wrappers++file : "Language/LOL/Typing/Collect/Grammar.ag"+options : catas, haskellsyntax, pretty, rename, semfuns, signatures, wrappers