diff --git a/CREDITS.txt b/CREDITS.txt new file mode 100644 --- /dev/null +++ b/CREDITS.txt @@ -0,0 +1,14 @@ +AUTHORS + +Bastiaan Heeren, Jurriaan Hage + +CREDITS + +The following people have contributed to the development and testing of the +Helium compiler and its components: + +Arjan van IJzendoorn, Daan Leijen, Rijk-Jan van Haaften, Arie Middelkoop, +Arjan Oosting, Jurri‘n Stutterheim, Jeroen Fokker, Andres Lšh, +Arthur Baars, Remco Burema, Atze Dijkstra, Maarten van Gompel, +Doaitse Swierstra, Martijn Lammerts, Martijn Schrage and +Stefan Holdermans. diff --git a/LICENSE.txt b/LICENSE.txt new file mode 100644 --- /dev/null +++ b/LICENSE.txt @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The GNU General Public License is a free, copyleft license for +software and other kinds of works. + + The licenses for most software and other practical works are designed +to take away your freedom to share and change the works. By contrast, +the GNU General Public License is intended to guarantee your freedom to +share and change all versions of a program--to make sure it remains free +software for all its users. We, the Free Software Foundation, use the +GNU General Public License for most of our software; it applies also to +any other work released this way by its authors. You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +them if you wish), that you receive source code or can get it if you +want it, that you can change the software or use pieces of it in new +free programs, and that you know you can do these things. + + To protect your rights, we need to prevent others from denying you +these rights or asking you to surrender the rights. Therefore, you have +certain responsibilities if you distribute copies of the software, or if +you modify it: responsibilities to respect the freedom of others. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must pass on to the recipients the same +freedoms that you received. You must make sure that they, too, receive +or can get the source code. And you must show them these terms so they +know their rights. + + Developers that use the GNU GPL protect your rights with two steps: +(1) assert copyright on the software, and (2) offer you this License +giving you legal permission to copy, distribute and/or modify it. + + For the developers' and authors' protection, the GPL clearly explains +that there is no warranty for this free software. For both users' and +authors' sake, the GPL requires that modified versions be marked as +changed, so that their problems will not be attributed erroneously to +authors of previous versions. + + Some devices are designed to deny users access to install or run +modified versions of the software inside them, although the manufacturer +can do so. This is fundamentally incompatible with the aim of +protecting users' freedom to change the software. The systematic +pattern of such abuse occurs in the area of products for individuals to +use, which is precisely where it is most unacceptable. Therefore, we +have designed this version of the GPL to prohibit the practice for those +products. If such problems arise substantially in other domains, we +stand ready to extend this provision to those domains in future versions +of the GPL, as needed to protect the freedom of users. + + Finally, every program is threatened constantly by software patents. +States should not allow patents to restrict development and use of +software on general-purpose computers, but in those that do, we wish to +avoid the special danger that patents applied to a free program could +make it effectively proprietary. To prevent this, the GPL assures that +patents cannot be used to render the program non-free. + + The precise terms and conditions for copying, distribution and +modification follow. + + TERMS AND CONDITIONS + + 0. Definitions. + + "This License" refers to version 3 of the GNU General Public License. + + "Copyright" also means copyright-like laws that apply to other kinds of +works, such as semiconductor masks. + + "The Program" refers to any copyrightable work licensed under this +License. Each licensee is addressed as "you". "Licensees" and +"recipients" may be individuals or organizations. + + To "modify" a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of an +exact copy. The resulting work is called a "modified version" of the +earlier work or a work "based on" the earlier work. + + A "covered work" means either the unmodified Program or a work based +on the Program. + + To "propagate" a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + + To "convey" a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user through +a computer network, with no transfer of a copy, is not conveying. + + An interactive user interface displays "Appropriate Legal Notices" +to the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + + 1. Source Code. + + The "source code" for a work means the preferred form of the work +for making modifications to it. "Object code" means any non-source +form of a work. + + A "Standard Interface" means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + + The "System Libraries" of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +"Major Component", in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + + The "Corresponding Source" for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. + + The Corresponding Source need not include anything that users +can regenerate automatically from other parts of the Corresponding +Source. + + The Corresponding Source for a work in source code form is that +same work. + + 2. Basic Permissions. + + All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + + You may make, run and propagate covered works that you do not +convey, without conditions so long as your license otherwise remains +in force. You may convey covered works to others for the sole purpose +of having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + + Conveying under any other circumstances is permitted solely under +the conditions stated below. Sublicensing is not allowed; section 10 +makes it unnecessary. + + 3. Protecting Users' Legal Rights From Anti-Circumvention Law. + + No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + + When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such circumvention +is effected by exercising rights under this License with respect to +the covered work, and you disclaim any intention to limit operation or +modification of the work as a means of enforcing, against the work's +users, your or third parties' legal rights to forbid circumvention of +technological measures. + + 4. Conveying Verbatim Copies. + + You may convey verbatim copies of the Program's source code as you +receive it, in any medium, provided that you conspicuously and +appropriately publish on each copy an appropriate copyright notice; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + + You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + + 5. Conveying Modified Source Versions. + + You may convey a work based on the Program, or the modifications to +produce it from the Program, in the form of source code under the +terms of section 4, provided that you also meet all of these conditions: + + a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + + b) The work must carry prominent notices stating that it is + released under this License and any conditions added under section + 7. This requirement modifies the requirement in section 4 to + "keep intact all notices". + + c) You must license the entire work, as a whole, under this + License to anyone who comes into possession of a copy. This + License will therefore apply, along with any applicable section 7 + additional terms, to the whole of the work, and all its parts, + regardless of how they are packaged. This License gives no + permission to license the work in any other way, but it does not + invalidate such permission if you have separately received it. + + d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your + work need not make them do so. + + A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +"aggregate" if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + + 6. Conveying Non-Source Forms. + + You may convey a covered work in object code form under the terms +of sections 4 and 5, provided that you also convey the +machine-readable Corresponding Source under the terms of this License, +in one of these ways: + + a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium + customarily used for software interchange. + + b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a + written offer, valid for at least three years and valid for as + long as you offer spare parts or customer support for that product + model, to give anyone who possesses the object code either (1) a + copy of the Corresponding Source for all the software in the + product that is covered by this License, on a durable physical + medium customarily used for software interchange, for a price no + more than your reasonable cost of physically performing this + conveying of source, or (2) access to copy the + Corresponding Source from a network server at no charge. + + c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This + alternative is allowed only occasionally and noncommercially, and + only if you received the object code with such an offer, in accord + with subsection 6b. + + d) Convey the object code by offering access from a designated + place (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) + that supports equivalent copying facilities, provided you maintain + clear directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + + e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + + A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + + A "User Product" is either (1) a "consumer product", which means any +tangible personal property which is normally used for personal, family, +or household purposes, or (2) anything designed or sold for incorporation +into a dwelling. In determining whether a product is a consumer product, +doubtful cases shall be resolved in favor of coverage. For a particular +product received by a particular user, "normally used" refers to a +typical or common use of that class of product, regardless of the status +of the particular user or of the way in which the particular user +actually uses, or expects or is expected to use, the product. A product +is a consumer product regardless of whether the product has substantial +commercial, industrial or non-consumer uses, unless such uses represent +the only significant mode of use of the product. + + "Installation Information" for a User Product means any methods, +procedures, authorization keys, or other information required to install +and execute modified versions of a covered work in that User Product from +a modified version of its Corresponding Source. The information must +suffice to ensure that the continued functioning of the modified object +code is in no case prevented or interfered with solely because +modification has been made. + + If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + + The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or updates +for a work that has been modified or installed by the recipient, or for +the User Product in which it has been modified or installed. Access to a +network may be denied when the modification itself materially and +adversely affects the operation of the network or violates the rules and +protocols for communication across the network. + + Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + 7. Additional Terms. + + "Additional permissions" are terms that supplement the terms of this +License by making exceptions from one or more of its conditions. +Additional permissions that are applicable to the entire Program shall +be treated as though they were included in this License, to the extent +that they are valid under applicable law. If additional permissions +apply only to part of the Program, that part may be used separately +under those permissions, but the entire Program remains governed by +this License without regard to the additional permissions. + + When you convey a copy of a covered work, you may at your option +remove any additional permissions from that copy, or from any part of +it. (Additional permissions may be written to require their own +removal in certain cases when you modify the work.) You may place +additional permissions on material, added by you to a covered work, +for which you have or can give appropriate copyright permission. + + Notwithstanding any other provision of this License, for material you +add to a covered work, you may (if authorized by the copyright holders of +that material) supplement the terms of this License with terms: + + a) Disclaiming warranty or limiting liability differently from the + terms of sections 15 and 16 of this License; or + + b) Requiring preservation of specified reasonable legal notices or + author attributions in that material or in the Appropriate Legal + Notices displayed by works containing it; or + + c) Prohibiting misrepresentation of the origin of that material, or + requiring that modified versions of such material be marked in + reasonable ways as different from the original version; or + + d) Limiting the use for publicity purposes of names of licensors or + authors of the material; or + + e) Declining to grant rights under trademark law for use of some + trade names, trademarks, or service marks; or + + f) Requiring indemnification of licensors and authors of that + material by anyone who conveys the material (or modified versions of + it) with contractual assumptions of liability to the recipient, for + any liability that these contractual assumptions directly impose on + those licensors and authors. + + All other non-permissive additional terms are considered "further +restrictions" within the meaning of section 10. If the Program as you +received it, or any part of it, contains a notice stating that it is +governed by this License along with a term that is a further +restriction, you may remove that term. If a license document contains +a further restriction but permits relicensing or conveying under this +License, you may add to a covered work material governed by the terms +of that license document, provided that the further restriction does +not survive such relicensing or conveying. + + If you add terms to a covered work in accord with this section, you +must place, in the relevant source files, a statement of the +additional terms that apply to those files, or a notice indicating +where to find the applicable terms. + + Additional terms, permissive or non-permissive, may be stated in the +form of a separately written license, or stated as exceptions; +the above requirements apply either way. + + 8. Termination. + + You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + + However, if you cease all violation of this License, then your +license from a particular copyright holder is reinstated (a) +provisionally, unless and until the copyright holder explicitly and +finally terminates your license, and (b) permanently, if the copyright +holder fails to notify you of the violation by some reasonable means +prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + + Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + + 9. Acceptance Not Required for Having Copies. + + You are not required to accept this License in order to receive or +run a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + + 10. Automatic Licensing of Downstream Recipients. + + Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + + An "entity transaction" is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + + You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + + 11. Patents. + + A "contributor" is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's "contributor version". + + A contributor's "essential patent claims" are all patent claims +owned or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, "control" includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + + Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + + In the following three paragraphs, a "patent license" is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To "grant" such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + + If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. "Knowingly relying" means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + + If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + + A patent license is "discriminatory" if it does not include within +the scope of its coverage, prohibits the exercise of, or is +conditioned on the non-exercise of one or more of the rights that are +specifically granted under this License. You may not convey a covered +work if you are a party to an arrangement with a third party that is +in the business of distributing software, under which you make payment +to the third party based on the extent of your activity of conveying +the work, and under which the third party grants, to any of the +parties who would receive the covered work from you, a discriminatory +patent license (a) in connection with copies of the covered work +conveyed by you (or copies made from those copies), or (b) primarily +for and in connection with specific products or compilations that +contain the covered work, unless you entered into that arrangement, +or that patent license was granted, prior to 28 March 2007. + + Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + + 12. No Surrender of Others' Freedom. + + If conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot convey a +covered work so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you may +not convey it at all. For example, if you agree to terms that obligate you +to collect a royalty for further conveying from those to whom you convey +the Program, the only way you could satisfy both those terms and this +License would be to refrain entirely from conveying the Program. + + 13. Use with the GNU Affero General Public License. + + Notwithstanding any other provision of this License, you have +permission to link or combine any covered work with a work licensed +under version 3 of the GNU Affero General Public License into a single +combined work, and to convey the resulting work. The terms of this +License will continue to apply to the part which is the covered work, +but the special requirements of the GNU Affero General Public License, +section 13, concerning interaction through a network will apply to the +combination as such. + + 14. Revised Versions of this License. + + The Free Software Foundation may publish revised and/or new versions of +the GNU General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + + Each version is given a distinguishing version number. If the +Program specifies that a certain numbered version of the GNU General +Public License "or any later version" applies to it, you have the +option of following the terms and conditions either of that numbered +version or of any later version published by the Free Software +Foundation. If the Program does not specify a version number of the +GNU General Public License, you may choose any version ever published +by the Free Software Foundation. + + If the Program specifies that a proxy can decide which future +versions of the GNU General Public License can be used, that proxy's +public statement of acceptance of a version permanently authorizes you +to choose that version for the Program. + + Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + + 15. Disclaimer of Warranty. + + THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY +APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT +HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY +OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM +IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF +ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. Limitation of Liability. + + IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS +THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY +GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE +USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF +DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD +PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), +EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF +SUCH DAMAGES. + + 17. Interpretation of Sections 15 and 16. + + If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +state the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + + Copyright (C) + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see . + +Also add information on how to contact you by electronic and paper mail. + + If the program does terminal interaction, make it output a short +notice like this when it starts in an interactive mode: + + Copyright (C) + This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the appropriate +parts of the General Public License. Of course, your program's commands +might be different; for a GUI interface, you would use an "about box". + + You should also get your employer (if you work as a programmer) or school, +if any, to sign a "copyright disclaimer" for the program, if necessary. +For more information on this, and how to apply and follow the GNU GPL, see +. + + The GNU General Public License does not permit incorporating your program +into proprietary programs. If your program is a subroutine library, you +may consider it more useful to permit linking proprietary applications with +the library. If this is what you want to do, use the GNU Lesser General +Public License instead of this License. But first, please read +. diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain diff --git a/Top.cabal b/Top.cabal new file mode 100644 --- /dev/null +++ b/Top.cabal @@ -0,0 +1,95 @@ +name: Top +version: 1.7 +synopsis: Constraint solving framework employed by the Helium Compiler. +homepage: http://www.cs.uu.nl/wiki/bin/view/Helium/WebHome +description: + + At its most general, Top is a framework for constructing abstract interpretations + which focuses on giving good feedback on why an abstract interpretation does not give + any useful information. In a mathematical notation this is usually made explicit by + returning the top element of a (complete) lattice. This is also one of the reasons + for the name of the project. + +category: Constraints +copyright: (c) 2012 +license: GPL +license-file: LICENSE.txt +author: Bastiaan Heeren, Jurriaan Hage +maintainer: helium@cs.uu.nl +stability: provisional +extra-source-files: CREDITS.txt +build-type: Simple +cabal-version: >= 1.10.1.0 +tested-with: GHC == 7.0.2, GHC == 7.0.3, GHC == 7.4.1 + +source-repository head + type: svn + location: https://subversion.cs.uu.nl/repos/staff.jur.Top/trunk + +-------------------------------------------------------------------------------- + +Executable topsolver + Build-Depends: base >= 3 && < 5, containers, mtl, parsec + ghc-options: -Wall + default-language: Haskell98 + hs-source-dirs: src + Main-is: TopSolver.hs + +Library + Build-Depends: base >= 3 && < 5, containers, mtl + ghc-options: -Wall + default-language: Haskell98 + hs-source-dirs: src + Exposed-modules: + Top.Constraint + Top.Constraint.Equality + Top.Constraint.Information + Top.Constraint.Polymorphism + Top.Constraint.Qualifier + Top.Implementation.Basic + Top.Implementation.FastSubstitution + Top.Implementation.General + Top.Implementation.Overloading + Top.Implementation.SimpleSubstitution + Top.Implementation.TypeGraph.ApplyHeuristics + Top.Implementation.TypeGraph.Basics + Top.Implementation.TypeGraph.Class + Top.Implementation.TypeGraph.ClassMonadic + Top.Implementation.TypeGraph.DefaultHeuristics + Top.Implementation.TypeGraph.EquivalenceGroup + Top.Implementation.TypeGraph.Heuristic + Top.Implementation.TypeGraph.Path + Top.Implementation.TypeGraph.Standard + Top.Implementation.TypeGraphSubstitution + Top.Implementation.TypeInference + Top.Interface.Basic + Top.Interface.Qualification + Top.Interface.Substitution + Top.Interface.TypeInference + Top.Monad.Select + Top.Monad.StateFix + Top.Ordering.Tree + Top.Ordering.TreeWalk + Top.Solver + Top.Solver.Greedy + Top.Solver.PartitionCombinator + Top.Solver.SwitchCombinator + Top.Solver.TypeGraph + Top.Types + Top.Types.Classes + Top.Types.Kinds + Top.Types.Primitive + Top.Types.Qualification + Top.Types.Quantification + Top.Types.Schemes + Top.Types.Substitution + Top.Types.Synonym + Top.Types.Unification + Top.Util.Embedding + Top.Util.Empty + Top.Util.Option + Other-modules: + Utils + +-------------------------------------------------------------------------------- + diff --git a/src/Top/Constraint.hs b/src/Top/Constraint.hs new file mode 100644 --- /dev/null +++ b/src/Top/Constraint.hs @@ -0,0 +1,97 @@ +{-# LANGUAGE UndecidableInstances, ExistentialQuantification, + MultiParamTypeClasses, FlexibleInstances, RankNTypes #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +-- +-- A data type to represent constraints in general, and a type class for +-- constraints that are solvable. +-- +----------------------------------------------------------------------------- + +module Top.Constraint where + +import Top.Types (Substitutable(..)) + +type Constraints m = [Constraint m] +data Constraint m = + forall c . (Show c, Substitutable c) => Constraint c (c -> m ()) (c -> m Bool) + +-- |A constraint is solvable if it knows how it can be solved in a certain +-- state (a monadic operation), if it can check afterwards whether the final +-- state satisfies it, and when it can be shown. +class (Show c, Substitutable c, Monad m) => Solvable c m where + solveConstraint :: c -> m () + checkCondition :: c -> m Bool + + -- default definition + checkCondition _ = return True + +instance Show (Constraint m) where + show (Constraint c _ _) = show c + +instance Substitutable (Constraint m) where + ftv (Constraint c _ _) = ftv c + sub |-> (Constraint c f g) = Constraint (sub |-> c) f g + +instance Monad m => Solvable (Constraint m) m where + solveConstraint (Constraint c f _) = f c + checkCondition (Constraint c _ g) = g c + +-- |Lifting a constraint to the Constraint data type. Every instance of +-- the Solvable type class can be lifted. +liftConstraint :: Solvable c m => c -> Constraint m +liftConstraint c = Constraint c solveConstraint checkCondition + +liftConstraints :: Solvable c m => [c] -> Constraints m +liftConstraints = map liftConstraint + +mapConstraint :: (forall a . m1 a -> m2 a) -> Constraint m1 -> Constraint m2 +mapConstraint t (Constraint c f g) = Constraint c (t . f) (t . g) + +newtype Operation m = Op_ String + +operation :: Monad m => String -> m () -> Constraint m +operation s m = Constraint (Op_ s) (const m) (const (return True)) + +instance Show (Operation m) where + show (Op_ s) = "<" ++ s ++ ">" + +instance Substitutable (Operation m) where + ftv _ = [] + _ |-> op = op + +-- |If both constraints of type 'a' and 'b' can be solved in a Monad 'm', then +-- 'Either a b' constraints can also be solved in this monad. +instance (Solvable a m, Solvable b m) => Solvable (Either a b) m where + solveConstraint = either solveConstraint solveConstraint + checkCondition = either checkCondition checkCondition + +-- |The data type ConstraintSum is similar to the (standard) Either data type. +-- However, its Show instance is slightly different as the name of the constructor +-- is not shown. +data ConstraintSum f g info + = SumLeft (f info) + | SumRight (g info) + +instance (Show (f info), Show (g info)) => Show (ConstraintSum f g info) where + show = constraintSum show show + +instance (Functor f, Functor g) => Functor (ConstraintSum f g) where + fmap f = constraintSum (SumLeft . fmap f) (SumRight . fmap f) + +instance (Substitutable (f info), Substitutable (g info)) => Substitutable (ConstraintSum f g info) where + (|->) sub = constraintSum (SumLeft . (sub |->)) (SumRight . (sub |->)) + ftv = constraintSum ftv ftv + +instance (Solvable (f info) m, Solvable (g info) m) => Solvable (ConstraintSum f g info) m where + solveConstraint = constraintSum solveConstraint solveConstraint + checkCondition = constraintSum checkCondition checkCondition + +-- |Similar to the 'either' function. +constraintSum :: (f info -> c) -> (g info -> c) -> ConstraintSum f g info -> c +constraintSum f _ (SumLeft a) = f a +constraintSum _ f (SumRight b) = f b diff --git a/src/Top/Constraint/Equality.hs b/src/Top/Constraint/Equality.hs new file mode 100644 --- /dev/null +++ b/src/Top/Constraint/Equality.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Constraint.Equality where + +import Top.Types +import Top.Constraint +import Top.Constraint.Information +import Top.Interface.Substitution +import Top.Interface.TypeInference +import Data.List (union) + +data EqualityConstraint info + = Equality Tp Tp info + +-- |The constructor of an equality constraint. +(.==.) :: Tp -> Tp -> info -> EqualityConstraint info +(.==.) = Equality + +instance Show info => Show (EqualityConstraint info) where + show (Equality t1 t2 info) = + let showInfo = " : {" ++ show info ++ "}" + in show t1 ++ " == " ++ show t2 ++ showInfo + +instance Functor EqualityConstraint where + fmap f (Equality t1 t2 info) = + Equality t1 t2 (f info) + +instance Substitutable (EqualityConstraint info) where + sub |-> (Equality t1 t2 info) = Equality (sub |-> t1) (sub |-> t2) info + ftv (Equality t1 t2 _) = ftv t1 `union` ftv t2 + +instance ( TypeConstraintInfo info + , HasSubst m info + , HasTI m info + ) => + Solvable (EqualityConstraint info) m + where + solveConstraint (Equality t1 t2 info) = + unifyTerms (equalityTypePair (t1, t2) info) t1 t2 + + checkCondition (Equality t1 t2 _) = + do t1' <- applySubst t1 + t2' <- applySubst t2 + (_ ,syns) <- getTypeSynonyms + return (expandType syns t1' == expandType syns t2') diff --git a/src/Top/Constraint/Information.hs b/src/Top/Constraint/Information.hs new file mode 100644 --- /dev/null +++ b/src/Top/Constraint/Information.hs @@ -0,0 +1,48 @@ +{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Constraint.Information where + +import Top.Types + +instance TypeConstraintInfo () +instance PolyTypeConstraintInfo () + +instance TypeConstraintInfo String +instance PolyTypeConstraintInfo String + +class Show info => TypeConstraintInfo info where + equalityTypePair :: (Tp, Tp) -> info -> info + ambiguousPredicate :: Predicate -> info -> info + unresolvedPredicate :: Predicate -> info -> info + predicateArisingFrom :: (Predicate, info) -> info -> info + parentPredicate :: Predicate -> info -> info + escapedSkolems :: [Int] -> info -> info + neverDirective :: (Predicate, info) -> info -> info + closeDirective :: (String, info) -> info -> info + disjointDirective :: (String, info) -> (String, info) -> info -> info + + -- default definitions + equalityTypePair _ = id + ambiguousPredicate _ = id + unresolvedPredicate _ = id + predicateArisingFrom _ = id + parentPredicate _ = id + escapedSkolems _ = id + neverDirective _ = id + closeDirective _ = id + disjointDirective _ _ = id + +class TypeConstraintInfo info => PolyTypeConstraintInfo info where + instantiatedTypeScheme :: Forall (Qualification Predicates Tp) -> info -> info + skolemizedTypeScheme :: (Tps, Forall (Qualification Predicates Tp)) -> info -> info + + -- default definition + instantiatedTypeScheme _ = id + skolemizedTypeScheme _ = id diff --git a/src/Top/Constraint/Polymorphism.hs b/src/Top/Constraint/Polymorphism.hs new file mode 100644 --- /dev/null +++ b/src/Top/Constraint/Polymorphism.hs @@ -0,0 +1,113 @@ +{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Constraint.Polymorphism where + +import Top.Types hiding (contextReduction) +import Top.Constraint +import Top.Constraint.Equality ( (.==.) ) +import Top.Interface.Basic +import Top.Interface.TypeInference +import Top.Interface.Substitution +import Top.Interface.Qualification +import Top.Constraint.Information +import Data.List (union, intercalate) + +data PolymorphismConstraint info + = Generalize Int (Tps, Tp) info + | Instantiate Tp (Sigma Predicates) info -- or: explicit instance constraint + | Skolemize Tp (Tps, Sigma Predicates) info + | Implicit Tp (Tps, Tp) info + +-- |The constructor of an instantiate (explicit instance) constraint. +(.::.) :: Tp -> Scheme Predicates -> info -> PolymorphismConstraint info +tp .::. s = Instantiate tp (SigmaScheme s) + +instance Show info => Show (PolymorphismConstraint info) where + show constraint = + case constraint of + Generalize sv (monos, tp) info -> + "s" ++ show sv ++ " := Generalize" ++ commaList [show (map TVar (ftv monos)), show tp] ++ showInfo info + Instantiate tp sigma info -> + show tp ++ " := Instantiate" ++ commaList [showQuantors sigma] ++ showInfo info + Skolemize tp (monos, sigma) info -> + show tp ++ " := Skolemize" ++ commaList [show (map TVar (ftv monos)), showQuantors sigma] ++ showInfo info + Implicit t1 (monos, t2) info -> + show t1 ++ " := Implicit" ++ commaList [show (map TVar (ftv monos)), show t2] ++ showInfo info + + where showInfo info = " : {" ++ show info ++ "}" + commaList = par . intercalate ", " + par s = "(" ++ s ++ ")" + +instance Functor PolymorphismConstraint where + fmap f constraint = + case constraint of + Generalize sv pair info -> Generalize sv pair (f info) + Instantiate tp sigma info -> Instantiate tp sigma (f info) + Skolemize tp pair info -> Skolemize tp pair (f info) + Implicit t1 (monos, t2) info -> Implicit t1 (monos, t2) (f info) + +instance Substitutable (PolymorphismConstraint info) where + sub |-> typeConstraint = + case typeConstraint of + Generalize sv (monos, tp) info -> Generalize sv (sub |-> monos, sub |-> tp) info + Instantiate tp sigma info -> Instantiate (sub |-> tp) (sub |-> sigma) info + Skolemize tp pair info -> Skolemize (sub |-> tp) (sub |-> pair) info + Implicit t1 (monos, t2) info -> Implicit (sub |-> t1) (sub |-> monos, sub |-> t2) info + + ftv typeConstraint = + case typeConstraint of + Generalize _ (monos, tp) _ -> ftv monos `union` ftv tp + Instantiate tp sigma _ -> ftv tp `union` ftv sigma + Skolemize tp pair _ -> ftv tp `union` ftv pair + Implicit t1 (monos, t2) _ -> ftv t1 `union` ftv monos `union` ftv t2 + +instance ( HasBasic m info + , HasTI m info + , HasSubst m info + , HasQual m info + , PolyTypeConstraintInfo info + ) => + Solvable (PolymorphismConstraint info) m where + solveConstraint constraint = + case constraint of + + Generalize var (m, tp) _ -> + do -- makeConsistent -- done by contextReduction + contextReduction + m' <- applySubst m + tp' <- applySubst tp + changeQualifiers applySubst + scheme <- generalizeWithQualifiers m' tp' + storeTypeScheme var scheme + + Instantiate tp sigma info -> + do scheme <- findScheme sigma + let newInfo = instantiatedTypeScheme scheme info + qtp <- instantiateM scheme + let (ps, itp) = split qtp + proveQualifiers (equalityTypePair (itp, tp) newInfo) ps + pushConstraint $ liftConstraint + (itp .==. tp $ newInfo) + + Skolemize tp (monos, sigma) info -> + do scheme <- findScheme sigma + let newInfo = skolemizedTypeScheme (monos, scheme) info + qtp <- skolemizeFaked (equalityTypePair (tp, tp) newInfo) monos scheme + let (ps, stp) = split qtp + assumeQualifiers (equalityTypePair (tp, tp) newInfo) ps + pushConstraint $ liftConstraint + (tp .==. stp $ newInfo) + + Implicit t1 (monos, t2) info -> + do sv <- getUnique + pushConstraints $ liftConstraints + [ Generalize sv (monos, t2) info + , Instantiate t1 (SigmaVar sv) info + ] diff --git a/src/Top/Constraint/Qualifier.hs b/src/Top/Constraint/Qualifier.hs new file mode 100644 --- /dev/null +++ b/src/Top/Constraint/Qualifier.hs @@ -0,0 +1,64 @@ +{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +-- +-- Constraints for overloading +-- +----------------------------------------------------------------------------- + + +module Top.Constraint.Qualifier where + +import Top.Types +import Top.Constraint +import Top.Constraint.Information +import Top.Interface.Qualification +import Data.List + +data ExtraConstraint info + = Prove Predicate info + | Assume Predicate info + +instance Show info => Show (ExtraConstraint info) where + show typeConstraint = + case typeConstraint of + Prove p info -> + "Prove (" ++ intercalate ", " (showQualifiers p) ++ ")" ++ showInfo info + Assume p info -> + "Assume (" ++ intercalate ", " (showQualifiers p) ++ ")" ++ showInfo info + + where showInfo info = " : {" ++ show info ++ "}" + +instance Functor ExtraConstraint where + fmap f typeConstraint = + case typeConstraint of + Prove p info -> Prove p (f info) + Assume p info -> Assume p (f info) + +instance Substitutable (ExtraConstraint info) where + sub |-> typeConstraint = + case typeConstraint of + Prove p info -> Prove (sub |-> p) info + Assume p info -> Assume (sub |-> p) info + + ftv typeConstraint = + case typeConstraint of + Prove p _ -> ftv p + Assume p _ -> ftv p + +instance ( HasQual m info + , PolyTypeConstraintInfo info + ) => + Solvable (ExtraConstraint info) m + where + solveConstraint typeConstraint = + case typeConstraint of + Prove p info -> + proveQualifier info p + + Assume p info -> + assumeQualifier info p diff --git a/src/Top/Implementation/Basic.hs b/src/Top/Implementation/Basic.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/Basic.hs @@ -0,0 +1,125 @@ +{-# LANGUAGE UndecidableInstances, OverlappingInstances, + FlexibleInstances, MultiParamTypeClasses#-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +-- +-- An interface for a monad that constains the most basic operations to +-- solve constraints. Can be reused for all kinds of constraint-based +-- analyses. +-- +----------------------------------------------------------------------------- + + +module Top.Implementation.Basic where + +import Control.Arrow +import Top.Constraint +import Top.Util.Option +import Top.Implementation.General +import Top.Interface.Basic +import Top.Monad.Select +-- import Control.Monad.State +import Top.Util.Embedding +import Top.Util.Empty + +------------------------------------------------------------------------ +-- (I) Algebraic data type + +-- |A BasicState is parameterized over the monad in which the constraints can +-- be solved, and over the information that is stored with each constraint. +data BasicState info m = BasicState + { constraints :: Constraints m -- ^ A stack of constraints that is to be solved + , errors :: [(info, ErrorLabel)] -- ^ The detected errors + , conditions :: [(m Bool, String)] -- ^ Conditions to check (for the solved constraints) + , optionStop :: Option Bool -- ^ Discard all remaining constraints after the first error + , optionCheck :: Option Bool + } + +------------------------------------------------------------------------ +-- (II) Instance of SolveState (Empty, Show) + +instance SolveState (BasicState info m) where + stateName _ = "Basic State" + stateOptions s = [show (optionStop s), show (optionCheck s)] + +-- |An empty BasicState. +instance Empty (BasicState info m) where + empty = BasicState + { constraints = [] + , errors = [] + , conditions = [] + , optionStop = stopOption + , optionCheck = checkOption + } + +instance Show (BasicState info m) where + show s + | null (constraints s) = overview + | otherwise = + unlines $ + ["Constraints", "-----------"] ++ + map ((" "++) . show) (constraints s) ++ + [overview] + where + overview = "("++show (length (constraints s))++" constraints, "++ + show (length (errors s))++" errors, "++ + show (length (conditions s))++" checks)" + +------------------------------------------------------------------------ +-- (III) Embeddings + +instance Embedded ClassBasic (BasicState info m) (BasicState info m) where embedding = idE +instance Embedded ClassBasic (Fix (BasicState info) x m) (BasicState info m) where embedding = fromFstFixE embedding + +------------------------------------------------------------------------ +-- (IV) Instance declaration + +instance ( MonadState s m + , Embedded ClassBasic s (BasicState info m) + ) => + HasBasic (SelectFix (BasicState info) m) info where + + -- constraints + pushConstraints xs = + modify (\s -> s { constraints = map (mapConstraint deselectFix) xs ++ constraints s }) + + popConstraint = + do cs <- gets constraints + case cs of + [] -> return Nothing + (x:xs) -> do modify (\s -> s { constraints = xs }) + return (Just (mapConstraint selectFix x)) + + discardConstraints = + modify (\s -> s { constraints = [] }) + + -- errors + addLabeledError label info = + do modify (\s -> s { errors = (info, label) : errors s }) + stop <- getOption stopAfterFirstError + when stop discardConstraints + + getLabeledErrors = + gets errors + + updateErrorInfo f = + do errs <- getLabeledErrors + newErrs <- let g (info, label) = + do newInfo <- f info + return (newInfo, label) + in mapM g errs + modify (\s -> s { errors = newErrs }) + + -- conditions + addCheck text check = + modify (\s -> s { conditions = (deselectFix check, text) : conditions s}) + + getChecks = + gets (map (first selectFix) . conditions) + + stopAfterFirstError = useOption optionStop (\x s -> s { optionStop = x }) + checkConditions = useOption optionCheck (\x s -> s { optionCheck = x }) diff --git a/src/Top/Implementation/FastSubstitution.hs b/src/Top/Implementation/FastSubstitution.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/FastSubstitution.hs @@ -0,0 +1,128 @@ +{-# LANGUAGE UndecidableInstances, OverlappingInstances, + FlexibleInstances, MultiParamTypeClasses #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Implementation.FastSubstitution where + +import Top.Types +import Top.Implementation.General +import Top.Util.Embedding +import Top.Monad.Select +import Top.Interface.TypeInference +import Top.Interface.Basic +import Top.Interface.Substitution +import qualified Data.Map as M +import Data.Maybe +import Utils (internalError) + +------------------------------------------------------------------------ +-- (I) Algebraic data type + +newtype GreedyState info = GreedyState { unGS :: FixpointSubstitution } + +------------------------------------------------------------------------ +-- (II) Instance of SolveState (Empty, Show) + +instance SolveState (GreedyState info) where + stateName _ = "Greedy Substitution State" + +instance Show (GreedyState info) where + show gs = let FixpointSubstitution hs = unGS gs in show hs -- _ = "" + +instance Empty (GreedyState info) where + empty = GreedyState (FixpointSubstitution M.empty) + +------------------------------------------------------------------------ +-- (III) Embeddings + +instance Embedded ClassSubst (GreedyState info) (GreedyState info) where embedding = idE +instance Embedded ClassSubst (Simple (GreedyState info) m b) (GreedyState info) where embedding = fromFstSimpleE embedding + +------------------------------------------------------------------------ +-- (IV) Instance declaration + +instance ( MonadState s m + , HasBasic m info + , HasTI m info + , Embedded ClassSubst s (GreedyState info) + ) => + HasSubst (Select (GreedyState info) m) info where + + makeSubstConsistent = return () + findSubstForVar i = gets (lookupInt i . unGS) + fixpointSubst = gets unGS + + unifyTerms info t1 t2 = + do t1' <- applySubst t1 + t2' <- applySubst t2 + synonyms <- select getTypeSynonyms + + case mguWithTypeSynonyms synonyms t1' t2' of + Left _ -> select (addLabeledError unificationErrorLabel info) + Right (used,sub) -> + let mutp = equalUnderTypeSynonyms synonyms (sub |-> t1') (sub |-> t2') + utp = fromMaybe err mutp + err = internalError "Top.Solvers.GreedySubst" "greedyState" "types not unifiable" + f (FixpointSubstitution fm) = + FixpointSubstitution (M.fromList [ (i, lookupInt i sub) | i <- dom sub ] `M.union` fm) + g = writeExpandedType synonyms t2 utp + . writeExpandedType synonyms t1 utp + h = if used then g . f else f + in modify (GreedyState . h . unGS) + +-- The key idea is as follows: +-- try to minimize the number of expansions by type synonyms. +-- 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 type synonym expansions +writeExpandedType :: OrderedTypeSynonyms -> Tp -> Tp -> FixpointSubstitution -> FixpointSubstitution +writeExpandedType synonyms = writeTypeType where + + writeTypeType :: Tp -> Tp -> FixpointSubstitution -> FixpointSubstitution + writeTypeType atp utp original = + case (leftSpine atp,leftSpine utp) of + ((TVar i,[]),_) -> + writeIntType i utp original + + ((TCon s,as),(TCon t,bs)) + | s == t && not (isPhantomTypeSynonym synonyms s) -> + foldr (uncurry writeTypeType) original (zip as bs) + + ((TCon _, _),_) -> + case expandTypeConstructorOneStep (snd synonyms) atp of + Just atp' -> writeTypeType atp' utp original + Nothing -> internalError "Top.Solvers.GreedySubst" "writeTypeType" ("inconsistent types(1)" ++ show (atp, utp)) + + _ -> internalError "Top.Solvers.GreedySubst" "writeTypeType" ("inconsistent types(2)" ++ show (atp, utp)) + + writeIntType :: Int -> Tp -> FixpointSubstitution -> FixpointSubstitution + writeIntType i utp original@(FixpointSubstitution fm) = + case M.lookup i fm of + + Nothing -> + case utp of + TVar j | i == j -> original + _ -> FixpointSubstitution (M.insert i utp fm) + + Just atp -> + case (leftSpine atp,leftSpine utp) of + ((TVar j,[]),_) -> writeIntType j utp original + ((TCon s,as),(TCon t,bs)) | s == t -> foldr (uncurry writeTypeType) original (zip as bs) + ((TCon _, _), _) -> case expandTypeConstructorOneStep (snd synonyms) atp of + Just atp' -> writeIntType i utp (FixpointSubstitution (M.insert i atp' fm)) + Nothing -> -- FIX!!! HERSCHRIJVEN! + -- de volgende situatie trad op: + -- utp=Categorie, atp = [Char] + -- met type Categorie = String + case expandTypeConstructorOneStep (snd synonyms) utp of + Just utp' -> + writeIntType i atp (FixpointSubstitution (M.insert i utp' fm)) + Nothing -> + internalError "Top.Solvers.GreedySubst" "writeIntType" ("inconsistent types(1)" ++ show (i, utp, atp)) + _ -> internalError "Top.Solvers.GreedySubst" "writeIntType" "inconsistent types(2)" diff --git a/src/Top/Implementation/General.hs b/src/Top/Implementation/General.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/General.hs @@ -0,0 +1,107 @@ +{-# LANGUAGE UndecidableInstances, FlexibleInstances, KindSignatures, + MultiParamTypeClasses, OverlappingInstances #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Implementation.General + ( module Top.Implementation.General + , module Top.Util.Empty + ) where + +import Top.Util.Embedding +import Top.Util.Empty +import Top.Monad.Select + +class (Show s, Empty s) => SolveState s where + showState :: s -> String + stateName :: s -> String + stateOptions :: s -> [String] + collectStates :: s -> [(String, String)] + + showState = show + stateOptions _ = [] + collectStates s = [(stateName s, showState s)] + +instance SolveState () where + stateName _ = "EmptyState" + collectStates _ = [] + +allStates :: (MonadState s m, SolveState s) => m [(String, String)] +allStates = gets collectStates + +allOptions :: (MonadState s m, SolveState s) => m [String] +allOptions = gets stateOptions + +---------------------- +-- New + +-- ToDo: replace And by infix type constructor (:^:) +-- ToDo: kind annotations for And, Simple, Fix +-- infixr 7 :^: + +data And f g x (m :: * -> *) = Compose (f (g x m) m) +data Simple a x (m :: * -> *) = Simple a x +data Fix g x (m :: * -> *) = Fix (g m) x + +--- Empty +instance Empty (f (g x m) m) => Empty (And f g x m) where + empty = Compose empty + +instance (Empty a, Empty x) => Empty (Simple a x m) where + empty = Simple empty empty + +instance (Empty (g m), Empty x) => Empty (Fix g x m) where + empty = Fix empty empty + +-- Show +instance Show (f (g x m) m) => Show (And f g x m) where + show (Compose a) = show a + +instance (Show a, Show x) => Show (Simple a x m) where + show (Simple a x) = show (a, x) + +instance (Show (f m), Show x) => Show (Fix f x m) where + show (Fix a x) = show (a, x) + +-- SolveState +instance SolveState (f (g x m) m) => SolveState (And f g x m) where + showState (Compose a) = showState a + stateName (Compose a) = stateName a + stateOptions (Compose a) = stateOptions a + collectStates (Compose a) = collectStates a + +instance (SolveState a, SolveState x) => SolveState (Simple a x m) where + showState (Simple a x) = show (a, x) + stateName (Simple a x) = concat ["(", stateName a, ",", stateName x, ")"] + stateOptions (Simple a x) = stateOptions a ++ stateOptions x + collectStates (Simple a x) = collectStates a ++ collectStates x + +instance (SolveState (f m), SolveState x) => SolveState (Fix f x m) where + showState (Fix a x) = show (a, x) + stateName (Fix a x) = concat ["(", stateName a, ",", stateName x, ")"] + stateOptions (Fix a x) = stateOptions a ++ stateOptions x + collectStates (Fix a x) = collectStates a ++ collectStates x + +-- Embedded +instance Embedded c (f (g x m) m) s => Embedded c (And f g x m) s where + embedding = composeE Embedding { getE = \(Compose a) -> a, changeE = \f (Compose a) -> Compose (f a) } embedding + +instance Embedded c x s => Embedded c (Simple a x m) s where + embedding = composeE Embedding { getE = \(Simple _ b) -> b, changeE = \f (Simple a b) -> Simple a (f b) } embedding + +instance Embedded c x s => Embedded c (Fix a x m) s where + embedding = composeE Embedding { getE = \(Fix _ b) -> b, changeE = \f (Fix a b) -> Fix a (f b) } embedding + +fromFstFixE :: Embedding (g m) c -> Embedding (Fix g x m) c +fromFstFixE = composeE Embedding { getE = \(Fix a _) -> a, changeE = \f (Fix a b) -> Fix (f a) b } + +fromFstSimpleE :: Embedding a c -> Embedding (Simple a x m) c +fromFstSimpleE = composeE fstSimpleE + +fstSimpleE :: Embedding (Simple a x m) a +fstSimpleE = Embedding { getE = \(Simple a _) -> a, changeE = \f (Simple a b) -> Simple (f a) b } diff --git a/src/Top/Implementation/Overloading.hs b/src/Top/Implementation/Overloading.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/Overloading.hs @@ -0,0 +1,290 @@ +{-# LANGUAGE UndecidableInstances, FlexibleInstances, + MultiParamTypeClasses, FlexibleContexts #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Implementation.Overloading where + +import Top.Types hiding (contextReduction) +import qualified Top.Types (contextReduction) +import Top.Constraint.Information +import Top.Implementation.General +import Top.Interface.TypeInference (getTypeSynonyms, HasTI, getSkolems) +import Top.Interface.Basic +import Top.Interface.Substitution +import Top.Interface.Qualification +import Top.Monad.Select +import Top.Util.Embedding +import qualified Data.Map as M +import Data.Maybe +import Data.List (intercalate, (\\), partition) + +------------------------------------------------------------------------ +-- (I) Algebraic data type + +data OverloadingState info = OverloadingState + { classEnvironment :: ClassEnvironment -- ^ All known type classes and instances + , predicateMap :: PredicateMap info -- ^ Type class assertions + , typeClassDirectives :: TypeClassDirectives info -- ^ Directives for type class assertions + } + +------------------------------------------------------------------------ +-- (II) Instance of SolveState (Empty, Show) + +instance Empty (OverloadingState info) where + empty = OverloadingState + { classEnvironment = emptyClassEnvironment + , predicateMap = empty + , typeClassDirectives = [] + } + +instance Show (OverloadingState info) where + show s = unlines [ "class environment: " ++ intercalate "," (M.keys (classEnvironment s)) + , "directives: " ++ show (typeClassDirectives s) + , "predicates: " ++ show (predicateMap s) + ] + +instance Show info => SolveState (OverloadingState info) where + stateName _ = "OverloadingState State" + +------------------------------------------------------------------------ +-- (III) Embeddings + +instance Embedded ClassQual (OverloadingState info) (OverloadingState info) where embedding = idE +instance Embedded ClassQual (Simple (OverloadingState info) x m) (OverloadingState info) where embedding = fromFstSimpleE embedding + +------------------------------------------------------------------------ +-- (IV) Instance declaration + +instance ( MonadState s m + , HasBasic m info + , HasTI m info + , TypeConstraintInfo info + , Embedded ClassQual s (OverloadingState info) + ) => + HasQual (Select (OverloadingState info) m) info where + + setClassEnvironment env = + modify (\s -> s { classEnvironment = env }) + + getClassEnvironment = + gets classEnvironment + + proveQualifier info p = + modifyPredicateMap (\qm -> qm { globalQualifiers = (p, info) : globalQualifiers qm }) + + assumeQualifier info p = + modifyPredicateMap (\qm -> qm { globalAssumptions = (p, info) : globalAssumptions qm }) + + changeQualifiers f = + do let g = mapM (\(p, info) -> f p >>= \new -> return (new, info) ) + as <- gets (globalQualifiers . predicateMap) >>= g + bs <- gets (globalGeneralizedQs . predicateMap) >>= g + cs <- gets (globalAssumptions . predicateMap) >>= g + modifyPredicateMap (\qm -> qm { globalQualifiers = as + , globalGeneralizedQs = bs + , globalAssumptions = cs }) + + allQualifiers = + do syns <- select getTypeSynonyms + classEnv <- getClassEnvironment + qmap <- gets predicateMap + let ps = globalQualifiers qmap ++ globalGeneralizedQs qmap ++ globalAssumptions qmap + return (fst (Top.Types.contextReduction syns classEnv (map fst ps))) + + generalizeWithQualifiers monos tp = + do preds1 <- proveQsSubst + preds2 <- generalizedQsSubst + let is = ftv tp \\ ftv monos + p = any (`elem` is) . ftv . fst + (as, bs) = partition p preds1 + cs = filter p preds2 + modifyPredicateMap (\qm -> qm { globalQualifiers = bs, globalGeneralizedQs = as ++ globalGeneralizedQs qm }) + return (generalize monos (map fst (as ++ cs) .=>. tp)) + + + -- improveQualifiersFinal -- use Default directives + + simplifyQualifiers = + do preds <- proveQsSubst + assumptions <- assumeQsSubst + syns <- select getTypeSynonyms + classEnv <- getClassEnvironment + directives <- gets typeClassDirectives + new <- select (simplify syns classEnv directives preds) + let final = filter (not . entail syns classEnv (map fst assumptions) . fst) new + modifyPredicateMap (\qm -> qm { globalQualifiers = final }) + + ambiguousQualifiers = + do ps <- proveQsSubst + select (ambiguous ps) + +------------------------------------------------------------------------ +-- (IV) Helper-functions + +simplify :: (HasTI m info, TypeConstraintInfo info, HasBasic m info) + => OrderedTypeSynonyms -> ClassEnvironment -> TypeClassDirectives info -> [(Predicate, info)] -> m [(Predicate, info)] +simplify syns classEnv directives psNew = + do let loopIn t@(p@(Predicate className _), info) + | inHeadNormalForm p = return [t] + | otherwise = + case byInstance syns classEnv p of + Just ps -> + loopInList [ (q, parentPredicate p info) | q <- ps ] + Nothing -> + let nevers = [ (q, i) | NeverDirective q i <- directives, isJust (matchPredicates syns p q) ] + newInfo = + case nevers of + tuple:_ -> neverDirective tuple info + [] -> case [ i | CloseDirective s i <- directives, s == className ] of + [i] -> closeDirective (className, i) info + _ -> unresolvedPredicate p info + in addLabeledError unresolvedLabel newInfo >> return [] + + loopInList ts = + do psList <- mapM loopIn ts + return (concat psList) + + loopSc rs [] = rs + loopSc rs (x:xs) + | scEntail classEnv (map fst (rs++xs)) (fst x) + = loopSc rs xs + | otherwise + = loopSc (x:rs) xs + + testDisjoints [] = return [] + testDisjoints (t@(Predicate className tp, info):ts) = + let f t'@(Predicate className' tp', info') = + case [ i | tp == tp', DisjointDirective ss i <- directives, className `elem` ss, className' `elem` ss ] of + [] -> return ([t'], True) + infodir : _ -> + do addLabeledError disjointLabel (disjointDirective (className, info) (className', info') infodir) + return ([], False) + + in do result <- mapM f ts + let (list, bs) = unzip result + rest <- testDisjoints (concat list) + return $ if and bs then t : rest else rest + + hnf <- loopInList psNew + testDisjoints (loopSc [] hnf) + +ambiguous :: (HasBasic m info, HasTI m info, TypeConstraintInfo info) + => [(Predicate, info)] -> m () +ambiguous listStart = + do skolems <- getSkolems + let skolemPairs = [ (is, info) | (is, info, _) <- skolems ] + + reportAmbiguous (p, info) = + addLabeledError ambiguousLabel (ambiguousPredicate p info) + + reportMissing pair info2 = + addLabeledError missingInSignatureLabel (predicateArisingFrom pair info2) + + f pair@(Predicate _ (TVar i), _) = + case [ info2 | (is, info2) <- skolemPairs, i `elem` is ] of + info2:_ -> reportMissing pair info2 + _ -> reportAmbiguous pair + f pair = reportAmbiguous pair + + mapM_ f listStart + +{- + -- try to use a defaulting directive before reporting an error message + tryToDefault (i, ts) = + do candidates <- + let f (Predicate cn _) = + case [ (tps, info) | DefaultDirective s tps info <- directives, s == cn ] of + [(tps, info)] -> + let op result tp = + do let sub = singleSubstitution i tp + let b = entailList syns classEnv [] [ sub |-> x | (x, _) <- ts ] + return $ if b then (tp, info) : result else result + in foldM op [] (reverse tps) + _ -> return [] + in mapM (f . fst) ts + + case [ x | x:_ <- candidates ] of + (tp, info) : rest | all (tp ==) (map fst rest) -> + do solveConstraint ( TVar i .==. tp $ info ) + makeSubstConsistent -- ?? + return [] + + _ -> return ts -} + +modifyPredicateMap :: MonadState (OverloadingState info) m => (PredicateMap info -> PredicateMap info) -> m () +modifyPredicateMap f = + modify (\s -> s { predicateMap = f (predicateMap s) }) + +proveQsSubst, assumeQsSubst, generalizedQsSubst :: + (MonadState s m, Embedded ClassQual s (OverloadingState info) {-, MonadState s m, HasSubst m info -}) + => Select (OverloadingState info) m [(Predicate, info)] + +proveQsSubst = gets (globalQualifiers . predicateMap) -- >>= select . mapM substPredicate +assumeQsSubst = gets (globalAssumptions . predicateMap) -- >>= select . mapM substPredicate +generalizedQsSubst = gets (globalGeneralizedQs . predicateMap) -- >>= select . mapM substPredicate + +substPredicate :: HasSubst m info => (Predicate, info) -> m (Predicate, info) +substPredicate (p, info) = + do new <- applySubst p + return (new, info) + +-- Type class directives +type TypeClassDirectives info = [TypeClassDirective info] + +data TypeClassDirective info + = NeverDirective Predicate info + | CloseDirective String info + | DisjointDirective [String] info + | DefaultDirective String Tps info + +instance Show (TypeClassDirective info) where + show _ = "<>" + +-- Predicate map +data PredicateMap info = + PredicateMap + { globalQualifiers :: [(Predicate, info)] + , globalGeneralizedQs :: [(Predicate, info)] + , globalAssumptions :: [(Predicate, info)] + } + +instance Show (PredicateMap info) where + show qm = + let f (s, sf) + | null ps = [] + | otherwise = [" " ++ s ++ ": " ++ intercalate "," (map (show . fst) ps)] + where ps = sf qm + in unlines $ concatMap f + [ ("qualifiers" , globalQualifiers) + , ("generalized qualifiers", globalGeneralizedQs) + , ("assumptions" , globalAssumptions) + ] + +instance Empty (PredicateMap info) where + empty = PredicateMap { globalQualifiers = [], globalGeneralizedQs = [], globalAssumptions = [] } + +instance Substitutable (PredicateMap info) where + sub |-> (PredicateMap as bs cs) = + let as' = [ (sub |-> a, info) | (a, info) <- as ] + bs' = [ (sub |-> b, info) | (b, info) <- bs ] + cs' = [ (sub |-> c, info) | (c, info) <- cs ] + in PredicateMap as' bs' cs' + ftv (PredicateMap as bs cs) = ftv (map fst $ as ++ bs ++ cs) + +unresolvedLabel :: ErrorLabel +unresolvedLabel = ErrorLabel "unresolved predicate" + +disjointLabel :: ErrorLabel +disjointLabel = ErrorLabel "disjoint predicates" + +ambiguousLabel :: ErrorLabel +ambiguousLabel = ErrorLabel "ambiguous predicate" + +missingInSignatureLabel :: ErrorLabel +missingInSignatureLabel = ErrorLabel "predicate missing in signature" diff --git a/src/Top/Implementation/SimpleSubstitution.hs b/src/Top/Implementation/SimpleSubstitution.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/SimpleSubstitution.hs @@ -0,0 +1,70 @@ +{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Implementation.SimpleSubstitution where + +import Top.Types +import Top.Implementation.General +import Top.Interface.Substitution +import Top.Interface.TypeInference +import Top.Interface.Basic +import Top.Monad.Select +import Top.Util.Embedding +import Top.Util.Empty + +------------------------------------------------------------------------ +-- (I) Algebraic data type + +newtype SimpleState info = SimpleState { unSS :: MapSubstitution } + +------------------------------------------------------------------------ +-- (II) Instance of SolveState (Empty, Show) + +instance SolveState (SimpleState info) where + stateName _ = "Simple Substitution State" + +instance Show (SimpleState info) where + show _ = "" + +instance Empty (SimpleState info) where + empty = SimpleState emptySubst + +------------------------------------------------------------------------ +-- (III) Embeddings + +instance Embedded ClassSubst (SimpleState info) (SimpleState info) where embedding = idE +instance Embedded ClassSubst (Simple (SimpleState info) x m) (SimpleState info) where embedding = fromFstSimpleE embedding + +------------------------------------------------------------------------ +-- (IV) Instance declaration + +instance ( MonadState s m + , HasBasic m info + , HasTI m info + , Embedded ClassSubst s (SimpleState info) + ) => + HasSubst (Select (SimpleState info) m) info where + + makeSubstConsistent = + return () + + unifyTerms info t1 t2 = + do synonyms <- select getTypeSynonyms + t1' <- applySubst t1 + t2' <- applySubst t2 + case mguWithTypeSynonyms synonyms t1' t2' of + Right (_, sub) -> + modify (SimpleState . (sub @@) . unSS) + Left _ -> select (addLabeledError unificationErrorLabel info) + + findSubstForVar i = + gets (lookupInt i . unSS) + + fixpointSubst = + gets (FixpointSubstitution . unSS) diff --git a/src/Top/Implementation/TypeGraph/ApplyHeuristics.hs b/src/Top/Implementation/TypeGraph/ApplyHeuristics.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/TypeGraph/ApplyHeuristics.hs @@ -0,0 +1,390 @@ +{-# LANGUAGE FlexibleContexts, FlexibleInstances #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Implementation.TypeGraph.ApplyHeuristics (applyHeuristics, predicatePath, expandPath) where + +import Data.Graph (buildG, scc) +import Data.List +import Data.Function +import Data.Tree (flatten) +import qualified Data.Map as M +import qualified Data.Set as S +import Top.Implementation.TypeGraph.Basics +import Top.Implementation.TypeGraph.ClassMonadic +import Top.Implementation.TypeGraph.Heuristic +import Top.Implementation.TypeGraph.Path +import Top.Interface.Qualification hiding (contextReduction) +import Top.Interface.TypeInference +import Top.Solver +import Top.Types +import Utils (internalError) + +type ErrorInfo info = ([EdgeId], info) + +applyHeuristics :: HasTypeGraph m info => (Path (EdgeId, info) -> [Heuristic info]) -> m [ErrorInfo info] +applyHeuristics heuristics = + let rec thePath = + case simplifyPath thePath of + Empty -> internalError "Top.TypeGraph.ApplyHeuristics" "applyHeuristics" "unexpected empty path" + Fail -> return [] + path -> + do err <- evalHeuristics path (heuristics path) + let restPath = changeStep (\t@(a,_) -> if a `elem` fst err then Fail else Step t) path + errs <- rec restPath + return (err : errs) + in + do errorPath <- allErrorPaths + rec (removeSomeDuplicates info2ToEdgeNr errorPath) + +-- These functions are used to describe for a change due to a heuristic how it affected the error path +-- showing whether the set of constraints shrunk and if so, whether it has now become a singleton. +tag :: String -> String +tag s = "~" ++ s ++ "~" + +shrunkAndFinalMsg :: [a] -> [a] -> String +shrunkAndFinalMsg old new = + if length new < length old then + if length new == 1 then + tag "shrunk" ++ " " ++ tag "final" + else + tag "shrunk" + else + tag "unmodified" + + +evalHeuristics :: HasTypeGraph m info => Path (EdgeId, info) -> [Heuristic info] -> m (ErrorInfo info) +evalHeuristics path = rec edgesBegin + where + edgesBegin = nubBy eqInfo2 (steps path) + + rec edges [] = + case edges of + (edgeId@(EdgeId _ _ cnr), info) : _ -> + do logMsg ("\n*** The selected constraint: " ++ show cnr ++ " ***\n") + return ([edgeId], info) + _ -> internalError "Top.TypeGraph.ApplyHeuristics" "evalHeuristics" "empty list" + + rec edges (Heuristic heuristic:rest) = + case heuristic of + + Filter name f -> + do edges' <- f edges + logMsg (name ++ " (filter) " ++ shrunkAndFinalMsg edges edges') + logMsg (" " ++ showSet [ i | (EdgeId _ _ i, _) <- edges' ]) + rec edges' rest + + Voting selectors -> + do logMsg ("Voting with "++show (length selectors) ++ " heuristics") + results <- mapM (evalSelector edges) selectors + let successList = [ (getSelectorName s, x) | (s, xs) <- zip selectors results, x <- xs ] + (thePrio, listWithBest) = foldr op (minBound, []) successList + op (selname, (prio, es, info)) best@(i, list) = + case compare prio i of + LT -> best + EQ -> (i, (selname, (head es, info)):list) + GT -> (prio, [(selname, (head es, info))]) + heuristicNames = map fst listWithBest + remainingEdges = map snd listWithBest + case listWithBest of + [] -> do logMsg "Unfortunately, none of the heuristics could be applied" + rec edges rest + _ -> do logMsg ("Selected heuristics are " ++ unwords heuristicNames ++ ". " + ++ shrunkAndFinalMsg edges remainingEdges) + logMsg (" selected with priority "++show thePrio++": "++showSet (map fst remainingEdges)++"\n") + rec remainingEdges rest + +evalSelector :: (MonadWriter LogEntries m, HasTypeGraph m info) => [(EdgeId, info)] -> Selector m info -> m [(Int, [EdgeId], info)] +evalSelector edges selector = + case selector of + + Selector (name, f) -> + do logMsg ("- "++name++" (selector)") + let op list edge = + do x <- f edge + case x of + Nothing -> return list + Just (prio, string, es, info) -> + do logMsg (" "++string++" (prio="++show prio++") => "++showSet es) + return ((prio, es, info) : list) + foldM op [] edges + + SelectorList (name, f) -> + do result <- f edges + logMsg ("- "++name++" (list selector)") + case result of + Nothing -> return [] + Just (i,_,es,info) -> return [(i,es,info)] + +showSet :: Show a => [a] -> String +showSet as = "{" ++ f (map show as) ++ "}" + where f [] = "" + f xs = foldr1 (\x y -> x++","++y) (map show xs) + +allErrorPaths :: HasTypeGraph m info => m (Path (EdgeId, info)) +allErrorPaths = + do is <- getMarkedPossibleErrors + cGraph <- childrenGraph is + let toCheck = nub $ concat (is : [ [a,b] | ((a,b),_) <- cGraph ]) + paths1 <- constantClashPaths toCheck + paths2 <- infiniteTypePaths cGraph + let errorPath = reduceNumberOfPaths (simplifyPath (altList (paths1 ++ paths2))) + expandPath errorPath + +---------------------------- + +-- not simplified: can also contain implied edges +constantClashPaths :: HasTypeGraph m info => [VertexId] -> m [TypeGraphPath info] +constantClashPaths [] = return [] +constantClashPaths (first:rest) = + do vertices <- verticesInGroupOf first + let vs = map fst vertices + rest' = filter (`notElem` vs) rest + pathInGroup vertices <++> constantClashPaths rest' + + where + pathInGroup :: HasTypeGraph m info => [(VertexId, VertexInfo)] -> m [TypeGraphPath info] + pathInGroup = errorPath . groupTheConstants . getConstants + + getConstants :: [(VertexId, VertexInfo)] -> [(VertexId, String)] + getConstants vertices = + [ (i, s ) | (i, (VCon s , _)) <- vertices ] ++ + [ (i, "@") | (i, (VApp _ _, _)) <- vertices ] + + -- lists of vertex numbers with the same type constant + -- (all vertices are in the same equivalence group) + groupTheConstants :: [(VertexId, String)] -> [[VertexId]] + groupTheConstants = + sortBy (compare `on` length) + . map (map fst) + . groupBy ((==) `on` snd) + . sortBy (compare `on` snd) + + errorPath :: HasTypeGraph m info => [[VertexId]] -> m [TypeGraphPath info] + errorPath [] = return [] + errorPath [_] = return [] + errorPath (is:iss) = + let f i = allPathsList i (concat iss) + in mapM f is <++> errorPath iss + +---------------------------- + +-- not simplified: can also contain implied edges +infiniteTypePaths :: HasTypeGraph m info => ChildGraph -> m [TypeGraphPath info] +infiniteTypePaths cGraph = + do pss <- mapM (makePathForInfiniteGroup . inThisGroup) allGroups + return (concat pss) + -- error (unlines $ map (show . inThisGroup) allGroups) + + where + allGroups :: [[VertexId]] + allGroups = infiniteGroups (map fst cGraph) + + -- puts the eqgroup with the least childedges to another group in front of the list + inThisGroup :: [VertexId] -> ChildGraph + inThisGroup infGroup = + let p ((x, y), _) = (x `elem` infGroup) && (y `elem` infGroup) + f (_, xs) (_, ys) = length xs `compare` length ys + in sortBy f (filter p cGraph) + + makePathForInfiniteGroup :: HasTypeGraph m info => ChildGraph -> m [TypeGraphPath info] + makePathForInfiniteGroup groupGraph = + case groupGraph of + [] -> return [] + (_, childEdges) : rest -> + let g (x, y) = allSubPathsList (concatMap snd rest) y [x] + in mapM g childEdges <++> infiniteTypePaths rest + +type ChildGraph = [((VertexId, VertexId), [(VertexId, VertexId)])] + +childrenGraph :: HasTypeGraph m info => [VertexId] -> m ChildGraph +childrenGraph = rec [] + where + rec as [] = return as + rec as (i:is) = + do vertices <- verticesInGroupOf i + ri <- representativeInGroupOf i + if ri `elem` map (fst . fst) as + then rec as is + else do let cs = concat [ [(n, l), (n, r)] | (n, (VApp l r, _)) <- vertices ] + cs' <- let f t = do r <- representativeInGroupOf (snd t) + return (r, t) + in mapM f cs + let children = map (\((a,b):xs) -> (a,b:map snd xs)) + . groupBy ((==) `on` fst) + . sortBy (compare `on` fst) + $ cs' + rec ([ ((ri, rc), xs) | (rc, xs) <- children ] ++ as) (map fst children ++ is) + +infiniteGroups :: [(VertexId, VertexId)] -> [[VertexId]] +infiniteGroups xs = + let representatives = nub (map fst xs ++ map snd xs) + map1 = M.fromList (zip representatives [0..]) + f1 i = M.findWithDefault (internalError "Top.TypeGraph.ApplyHeuristics" "infiniteGroups" "error in lookup1 of makeMap") i map1 + map2 = M.fromList (zip [0..] representatives) + f2 i = M.findWithDefault (internalError "Top.TypeGraph.ApplyHeuristics" "infiniteGroups" "error in lookup2 of makeMap") i map2 + edgeList = [ (f1 i, f1 c) | (i, c) <- xs ] + graph = buildG (0, length representatives - 1) edgeList + groups = map flatten (scc graph) + selfRecursive = [ f1 i | (i, j) <- xs, i == j ] + recursive = let p [i] = i `elem` selfRecursive + p is = length is > 1 + in map (map f2) (filter p groups) + in recursive + +allSubPathsList :: HasTypeGraph m info => [(VertexId, VertexId)] -> VertexId -> [VertexId] -> m (TypeGraphPath info) +allSubPathsList childList vertex targets = rec S.empty vertex + where + rec :: HasTypeGraph m info => S.Set VertexId -> VertexId -> m (TypeGraphPath info) + rec without start = + do vs <- verticesInGroupOf start + if any (`elem` map fst vs) targets + then sameGroup + else otherGroup vs + where + -- targets are in the same group as the source + sameGroup = do + directPath <- allPathsListWithout without start targets + return (simplifyPath directPath) + + -- go down to another equivalence group + otherGroup vs = do + extendedPaths <- mapM (recDown vs) (targetPairs vs) + return (altList extendedPaths) + + recDown vs (newStart, childTargets) = do + let newWithout = without `S.union` S.fromList (map fst vs){- don't return to this equivalence group -} + f ct = let set = S.fromList [ t | t <- childTargets, t /= ct ] + in rec (set `S.union` newWithout) ct + path <- allPathsListWithout without start [newStart] + newPaths <- mapM f childTargets + return (path :+: altList newPaths) + + targetPairs :: [(VertexId, (VertexKind, Maybe Tp))] -> [(VertexId, [VertexId])] + targetPairs vs = + let p (i, j) = i `elem` map fst vs + && not (i `S.member` without || j `S.member` without) + in map (\((i,j):rest) -> (i, j:map snd rest)) + . groupBy ((==) `on` fst) + . sortBy (compare `on` fst) + $ filter p childList + +expandPath :: HasTypeGraph m info => TypeGraphPath info -> m (Path (EdgeId, info)) +expandPath Fail = return Fail +expandPath p = + do expandTable <- + let impliedEdges = nub [ intPair (v1, v2) | (_, Implied _ (VertexId v1) (VertexId v2)) <- steps p ] + in impliedEdgeTable impliedEdges + + let convert history path = + case path of + Empty -> Empty + Fail -> Fail + p1 :+: p2 -> convert history p1 :+: convert history p2 + p1 :|: p2 -> convert history p1 :|: convert history p2 + Step (edge, edgeInfo) -> + case edgeInfo of + Initial info -> Step (edge, info) + Child _ -> Empty + Implied _ (VertexId v1) (VertexId v2) + | pair `S.member` history -> Empty + | otherwise -> + convert (S.insert pair history) (lookupPair expandTable pair) + where + pair = intPair (v1, v2) + + return (convert S.empty p) + +impliedEdgeTable :: HasTypeGraph m info => [IntPair] -> m (PathMap info) +impliedEdgeTable = insertPairs M.empty + where + insertPairs fm [] = return fm + insertPairs fm (pair:rest) + | pair `M.member` fm = insertPairs fm rest + | otherwise = + do path <- let (i1, i2) = tupleFromIntPair pair + in allPaths (VertexId i1) (VertexId i2) + let new = nub [ intPair (v1, v2) | (_, Implied _ (VertexId v1) (VertexId v2)) <- steps path ] + insertPairs (M.insert pair path fm) (rest `union` new) + +------------------------------- +-- + +newtype IntPair = HiddenIP { tupleFromIntPair :: (Int, Int) } + +intPair :: (Int, Int) -> IntPair +intPair (x, y) + | x <= y = HiddenIP (x, y) + | otherwise = HiddenIP (y, x) + +instance Show IntPair where + show (HiddenIP pair) = show pair + +instance Eq IntPair where + HiddenIP pair1 == HiddenIP pair2 = + pair1 == pair2 + +instance Ord IntPair where + HiddenIP pair1 `compare` HiddenIP pair2 = + pair1 `compare` pair2 + +type PathMap info = M.Map IntPair (Path (EdgeId, PathStep info)) + +lookupPair :: PathMap info -> IntPair -> Path (EdgeId, PathStep info) +lookupPair fm pair = + let err = internalError "Top.TypeGraph.ApplyHeuristics" "lookupPair" "could not find implied edge while expanding" + in M.findWithDefault err pair fm + +-- move to another module +predicatePath :: (HasQual m info, HasTypeGraph m info) => m (Path (EdgeId, PathStep info)) +predicatePath = + do ps <- allQualifiers + simples <- simplePredicates ps + makeList S.empty Empty simples + + where + simplePredicates ps = + do classEnv <- getClassEnvironment + syns <- getTypeSynonyms + let reduced = fst (contextReduction syns classEnv ps) + return [ (s, VertexId i) | Predicate s (TVar i) <- reduced ] + + makeList history path pairs = + do xs <- mapM (make history path) pairs + return (altList xs) + + make history path (pClass, i) + | i `S.member` history = return Fail + | otherwise = + do classEnv <- getClassEnvironment + syns <- getTypeSynonyms + vertices <- verticesInGroupOf i + + -- vertices to inspect + let constants = [ (vid, TCon s) | (vid, (VCon s, _)) <- vertices ] + applys <- let f i' = do tp <- typeFromTermGraph i' + return (i', tp) + in mapM f [ i' | (i', (VApp _ _, _)) <- vertices ] + + let f (vid, tp) + | null errs = -- everything is okay: recursive call + do let -- don't visit these vertices + donts = S.fromList [ VertexId j | j <- ftv (map snd applys), j `notElem` ftv tp ] + path' <- allPathsListWithout history i [vid] + simples <- simplePredicates reduced + makeList (donts `S.union` newHistory) (path :+: path') simples + + | otherwise = -- this is an error path + do path' <- allPathsListWithout history i [vid] + return (path :+: path') + + where (reduced, errs) = contextReduction syns classEnv [Predicate pClass tp] + newHistory = S.fromList (map fst vertices) `S.union` history + + xs <- mapM f (constants ++ applys) + return (altList xs) diff --git a/src/Top/Implementation/TypeGraph/Basics.hs b/src/Top/Implementation/TypeGraph/Basics.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/TypeGraph/Basics.hs @@ -0,0 +1,147 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +----------------------------------------------------------------------------- + +module Top.Implementation.TypeGraph.Basics where + +import Top.Implementation.TypeGraph.Path +import Top.Types +import Utils (internalError) +-- import Data.Maybe +import Data.List (sort, partition, intercalate) + +----------------------------------------------------------------------------------------- + +newtype VertexId = VertexId Int deriving (Eq, Ord) +type VertexInfo = (VertexKind, Maybe Tp) +data VertexKind = VVar | VCon String | VApp VertexId VertexId + deriving (Show, Eq, Ord) + +instance Show VertexId where + show (VertexId i) = show i + +vertexIdToTp :: VertexId -> Tp +vertexIdToTp (VertexId i) = TVar i + +data EdgeId = EdgeId VertexId VertexId EdgeNr +newtype EdgeNr = EdgeNrX Int deriving (Eq, Ord) +data ChildSide = LeftChild | RightChild + deriving (Eq, Ord) + +makeEdgeNr :: Int -> EdgeNr +makeEdgeNr = EdgeNrX + +impliedEdgeNr :: EdgeNr +impliedEdgeNr = makeEdgeNr (-1) + +instance Show EdgeNr where + show (EdgeNrX i) = '#':show i + +instance Show ChildSide where + show LeftChild = "(l)" + show RightChild = "(r)" + +data ParentChild = ParentChild { parent :: VertexId, child :: VertexId, childSide :: ChildSide } + deriving Eq + +instance Show ParentChild where + show pc = show (child pc) ++ " <- " ++ show (parent pc) ++ show (childSide pc) + +instance Ord ParentChild where + compare pc1 pc2 = compare (child pc1, parent pc1) (child pc2, parent pc2) + +type TypeGraphPath info = Path (EdgeId, PathStep info) +data PathStep info + = Initial info + | Implied ChildSide VertexId VertexId + | Child ChildSide + +instance Show (PathStep info) where + show (Initial _) = "Initial" + show (Implied cs x y) = "(" ++ show cs ++ " : " ++ show (x, y) ++ ")" + show (Child i) = "(" ++ show i ++ ")" + +instance Show EdgeId where + show (EdgeId a b _) = "("++show a'++"-"++show b'++")" + where (a',b') = if a <= b then (a,b) else (b,a) + +instance Eq EdgeId where -- why not compare the edge numbers here? + EdgeId a b _ == EdgeId c d _ = (a == c && b == d) || (a == d && b == c) + +instance Ord EdgeId where + EdgeId a b _ <= EdgeId c d _ = order (a,b) <= order (c,d) + where order (i,j) = if i <= j then (i,j) else (j,i) + +-- A clique is a set of vertices that are equivalent because their parents are equal +-- Invariant: a clique cannot be empty +newtype Clique = CliqueX [ParentChild] +type CliqueList = [Clique] + +instance Show Clique where + show (CliqueX xs) = "{" ++ intercalate ", " (map show xs) ++ "}" + +instance Eq Clique where + CliqueX xs == CliqueX ys = + xs == ys + +instance Ord Clique where + compare (CliqueX xs) (CliqueX ys) = compare xs ys + +isSubsetClique :: Clique -> Clique -> Bool +isSubsetClique (CliqueX as) (CliqueX bs) = rec as bs + where + rec [] _ = True + rec _ [] = False + rec a@(x:xs) (y:ys) + | x == y = rec xs ys + | x > y = rec a ys + | otherwise = False + +isDisjointClique :: Clique -> Clique -> Bool +isDisjointClique (CliqueX as) (CliqueX bs) = rec as bs + where + rec [] _ = True + rec _ [] = True + rec a@(x:xs) b@(y:ys) + | x == y = False + | x > y = rec a ys + | otherwise = rec xs b + +cliqueRepresentative :: Clique -> VertexId +cliqueRepresentative (CliqueX xs) = + case xs of + [] -> internalError "Top.TypeGraph.Basics" "cliqueRepresentative" "A clique cannot be empty" + x:_ -> child x + +triplesInClique :: Clique -> [ParentChild] +triplesInClique (CliqueX xs) = xs + +childrenInClique :: Clique -> [VertexId] +childrenInClique = map child . triplesInClique + +mergeCliques :: CliqueList -> Clique +mergeCliques list = CliqueX (foldr op [] [ xs | CliqueX xs <- list ]) + where + op xs [] = xs + op [] ys = ys + op a@(x:xs) b@(y:ys) + | x < y = x : op xs b + | x == y = x : op xs ys + | otherwise = y : op a ys + +makeClique :: [ParentChild] -> Clique +makeClique list + | length set < 2 = internalError "Top.TypeGraph.Basics" "makeClique" "incorrect clique" + | otherwise = CliqueX set + where + set = sort list + +combineCliqueList :: CliqueList -> CliqueList -> CliqueList +combineCliqueList [] ys = ys +combineCliqueList (x:xs) ys = + let (ys1, ys2) = partition (isDisjointClique x) ys + in mergeCliques (x:ys2) : combineCliqueList xs ys1 diff --git a/src/Top/Implementation/TypeGraph/Class.hs b/src/Top/Implementation/TypeGraph/Class.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/TypeGraph/Class.hs @@ -0,0 +1,88 @@ +{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Implementation.TypeGraph.Class where + +import Top.Types +import Top.Implementation.TypeGraph.Basics +import Data.Maybe +import qualified Data.Set as S +import Data.List (nub) +import Utils (internalError) + +class TypeGraph graph info | graph -> info where + + -- construct a type graph + addTermGraph :: OrderedTypeSynonyms -> Int -> Tp -> graph -> (Int, VertexId, graph) + addVertex :: VertexId -> VertexInfo -> graph -> graph + addEdge :: EdgeId -> info -> graph -> graph + addNewEdge :: (VertexId, VertexId) -> info -> graph -> graph + + -- deconstruct a type graph + deleteEdge :: EdgeId -> graph -> graph + + -- inspect an equivalence group in a type graph + verticesInGroupOf :: VertexId -> graph -> [(VertexId, VertexInfo)] + childrenInGroupOf :: VertexId -> graph -> ([ParentChild], [ParentChild]) + constantsInGroupOf :: VertexId -> graph -> [String] + representativeInGroupOf :: VertexId -> graph -> VertexId + edgesFrom :: VertexId -> graph -> [(EdgeId, info)] + + -- query a path in an equivalence group + allPaths :: VertexId -> VertexId -> graph -> TypeGraphPath info + allPathsList :: VertexId -> [VertexId] -> graph -> TypeGraphPath info + allPathsListWithout :: S.Set VertexId -> VertexId -> [VertexId] -> graph -> TypeGraphPath info + + -- substitution and term graph + substituteVariable :: OrderedTypeSynonyms -> Int -> graph -> Tp + substituteType :: OrderedTypeSynonyms -> Tp -> graph -> Tp + substituteTypeSafe :: OrderedTypeSynonyms -> Tp -> graph -> Maybe Tp + makeSubstitution :: OrderedTypeSynonyms -> graph -> [(VertexId, Tp)] + typeFromTermGraph :: VertexId -> graph -> Tp + + -- Extra administration + markAsPossibleError :: VertexId -> graph -> graph + getMarkedPossibleErrors :: graph -> [VertexId] + unmarkPossibleErrors :: graph -> graph + + ------------------------------------------- + -- default definitions + + allPaths i1 i2 = + allPathsList i1 [i2] + + allPathsList = + allPathsListWithout S.empty + + childrenInGroupOf i graph = + unzip [ ( ParentChild { parent=p, child = t1, childSide=LeftChild } + , ParentChild { parent=p, child = t2, childSide=RightChild } + ) + | (p, (VApp t1 t2, _)) <- verticesInGroupOf i graph + ] + + constantsInGroupOf i graph = + nub [ s | (_, (VCon s, _)) <- verticesInGroupOf i graph ] + + representativeInGroupOf i graph = + case verticesInGroupOf i graph of + (vid, _):_ -> vid + _ -> internalError "Top.TypeGraph.TypeGraphState" "representativeInGroupOf" "unexpected empty equivalence group" + + substituteVariable syns = + substituteType syns . TVar + + substituteType syns tp graph = + let err = internalError "Top.TypeGraph.TypeGraphState" "substituteType" "inconsistent state" + in fromMaybe err (substituteTypeSafe syns tp graph) + + -- Extra administration + markAsPossibleError _ = id + getMarkedPossibleErrors _ = [] + unmarkPossibleErrors = id diff --git a/src/Top/Implementation/TypeGraph/ClassMonadic.hs b/src/Top/Implementation/TypeGraph/ClassMonadic.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/TypeGraph/ClassMonadic.hs @@ -0,0 +1,137 @@ +{-# LANGUAGE UndecidableInstances, FunctionalDependencies, RankNTypes, + MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Implementation.TypeGraph.ClassMonadic where + +import Top.Interface.Basic +import Top.Interface.TypeInference +import Top.Interface.Qualification +import qualified Top.Implementation.TypeGraph.Class as TG +import Top.Implementation.TypeGraph.Basics +import Top.Types +import Top.Solver +import qualified Data.Map as M +import qualified Data.Set as S + +class (HasBasic m info, HasTI m info, HasQual m info, HasTG m info, MonadWriter LogEntries m, Show info) => HasTypeGraph m info | m -> info + +instance (HasBasic m info, HasTI m info, HasQual m info, HasTG m info, MonadWriter LogEntries m, Show info) => HasTypeGraph m info + +class Monad m => HasTG m info | m -> info where + withTypeGraph :: (forall graph . TG.TypeGraph graph info => graph -> (a, graph)) -> m a + +useTypeGraph :: HasTG m info => (forall graph . TG.TypeGraph graph info => graph -> a) -> m a +useTypeGraph f = withTypeGraph (\g -> (f g, g)) + +changeTypeGraph :: HasTG m info => (forall graph . TG.TypeGraph graph info => graph -> graph ) -> m () +changeTypeGraph f = withTypeGraph (\g -> ((), f g)) + +-- construct a type graph + +addTermGraph :: HasTypeGraph m info => Tp -> m VertexId +addTermGraph tp = + do unique <- getUnique + synonyms <- getTypeSynonyms + (newUnique, vid) <- withTypeGraph + (\graph -> let (u, v, g) = TG.addTermGraph synonyms unique tp graph + in ((u, v), g)) + setUnique newUnique + return vid + +addVertex :: HasTypeGraph m info => VertexId -> VertexInfo -> m () +addVertex vid info = changeTypeGraph (TG.addVertex vid info) + +addEdge :: HasTypeGraph m info => EdgeId -> info -> m () +addEdge edgeId info = changeTypeGraph (TG.addEdge edgeId info) + +addNewEdge :: HasTypeGraph m info => (VertexId, VertexId) -> info -> m () +addNewEdge pair info = changeTypeGraph (TG.addNewEdge pair info) + +-- deconstruct a type graph + +deleteEdge :: HasTypeGraph m info => EdgeId -> m () +deleteEdge edgeId = changeTypeGraph (TG.deleteEdge edgeId) + +-- inspect an equivalence group in a type graph + +verticesInGroupOf :: HasTypeGraph m info => VertexId -> m [(VertexId, VertexInfo)] +verticesInGroupOf vid = useTypeGraph (TG.verticesInGroupOf vid) + +childrenInGroupOf :: HasTypeGraph m info => VertexId -> m ([ParentChild], [ParentChild]) +childrenInGroupOf vid = useTypeGraph (TG.childrenInGroupOf vid) + +constantsInGroupOf :: HasTypeGraph m info => VertexId -> m [String] +constantsInGroupOf vid = useTypeGraph (TG.constantsInGroupOf vid) + +representativeInGroupOf :: HasTypeGraph m info => VertexId -> m VertexId +representativeInGroupOf vid = useTypeGraph (TG.representativeInGroupOf vid) + +edgesFrom :: HasTypeGraph m info => VertexId -> m [(EdgeId, info)] +edgesFrom vid = useTypeGraph (TG.edgesFrom vid) + +-- query a path in an equivalence group +allPaths :: HasTypeGraph m info => VertexId -> VertexId -> m (TypeGraphPath info) +allPaths v1 v2 = useTypeGraph (TG.allPaths v1 v2) + +allPathsList :: HasTypeGraph m info => VertexId -> [VertexId] -> m (TypeGraphPath info) +allPathsList v1 vs = useTypeGraph (TG.allPathsList v1 vs) + +allPathsListWithout :: HasTypeGraph m info => S.Set VertexId -> VertexId -> [VertexId] -> m (TypeGraphPath info) +allPathsListWithout set v1 vs = useTypeGraph (TG.allPathsListWithout set v1 vs) + +-- substitution and term graph +substituteVariable :: HasTypeGraph m info => Int -> m Tp +substituteVariable i = + do synonyms <- getTypeSynonyms + useTypeGraph (TG.substituteVariable synonyms i) + +substituteType :: HasTypeGraph m info => Tp -> m Tp +substituteType tp = + do synonyms <- getTypeSynonyms + useTypeGraph (TG.substituteType synonyms tp) + +substituteTypeSafe :: HasTypeGraph m info => Tp -> m (Maybe Tp) +substituteTypeSafe tp = + do synonyms <- getTypeSynonyms + useTypeGraph (TG.substituteTypeSafe synonyms tp) + +makeSubstitution :: HasTypeGraph m info => m [(VertexId, Tp)] +makeSubstitution = + do synonyms <- getTypeSynonyms + useTypeGraph (TG.makeSubstitution synonyms) + +typeFromTermGraph :: HasTypeGraph m info => VertexId -> m Tp +typeFromTermGraph vid = useTypeGraph (TG.typeFromTermGraph vid) + +-- Extra administration +markAsPossibleError :: HasTypeGraph m info => VertexId -> m () +markAsPossibleError vid = changeTypeGraph (TG.markAsPossibleError vid) + +getMarkedPossibleErrors :: HasTypeGraph m info => m [VertexId] +getMarkedPossibleErrors = useTypeGraph TG.getMarkedPossibleErrors + +unmarkPossibleErrors :: HasTypeGraph m info => m () +unmarkPossibleErrors = changeTypeGraph TG.unmarkPossibleErrors + +--------------------- +------ EXTRA + +theUnifyTerms :: HasTypeGraph m info => info -> Tp -> Tp -> m () +theUnifyTerms info t1 t2 = + do v1 <- addTermGraph t1 + v2 <- addTermGraph t2 + addNewEdge (v1, v2) info + +makeFixpointSubst :: HasTypeGraph m info => m FixpointSubstitution +makeFixpointSubst = + do xs <- makeSubstitution + let list = [ (i, tp) | (VertexId i, tp) <- xs ] + return (FixpointSubstitution (M.fromList list)) + diff --git a/src/Top/Implementation/TypeGraph/DefaultHeuristics.hs b/src/Top/Implementation/TypeGraph/DefaultHeuristics.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/TypeGraph/DefaultHeuristics.hs @@ -0,0 +1,94 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +----------------------------------------------------------------------------- + +module Top.Implementation.TypeGraph.DefaultHeuristics where + +import Top.Implementation.TypeGraph.ApplyHeuristics (predicatePath, expandPath) +import Top.Implementation.TypeGraph.Basics +import Top.Implementation.TypeGraph.Heuristic +import Top.Implementation.TypeGraph.Path +import Data.List +import qualified Data.Map as M +import Top.Solver + +----------------------------------------------------------------------------- + +defaultHeuristics :: Show info => Path (EdgeId, info) -> [Heuristic info] +defaultHeuristics path = + [ highParticipation 1.00 path, firstComeFirstBlamed ] + +----------------------------------------------------------------------------- + +-- |Compute the smallest 'minimal' sets. This computation is very(!) costly +-- (might take a long time for complex inconsistencies) +inMininalSet :: Path (EdgeId, info) -> Heuristic info +inMininalSet path = + Heuristic ( + let sets = minimalSets eqInfo2 path + candidates = nubBy eqInfo2 (concat sets) + f e = return (any (eqInfo2 e) candidates) + in edgeFilter "In a smallest minimal set" f) + +-- |Although not as precise as the minimal set analysis, this calculates the participation of +-- each edge in all error paths. +-- Default ratio = 1.0 (100 percent) +-- (the ratio determines which scores compared to the best are accepted) +highParticipation :: Show info => Double -> Path (EdgeId, info) -> Heuristic info +highParticipation ratio path = + Heuristic (Filter ("Participation ratio [ratio="++show ratio++"]") selectTheBest) + where + selectTheBest es = + let (nrOfPaths, fm) = participationMap (mapPath (\(EdgeId _ _ cnr,_) -> cnr) path) + participationList = M.filterWithKey p fm + p cnr _ = cnr `elem` activeCNrs + activeCNrs = [ cnr | (EdgeId _ _ cnr, _) <- es ] + maxInList = maximum (M.elems participationList) + limit -- test if one edge can solve it completely + | maxInList == nrOfPaths = maxInList + | otherwise = round (fromIntegral maxInList * ratio) `max` 1 + goodCNrs = M.keys (M.filter (>= limit) participationList) + bestEdges = filter (\(EdgeId _ _ cnr,_) -> cnr `elem` goodCNrs) es + + -- prints a nice report + mymsg = unlines ("" : title : replicate 50 '-' : map f es) + title = "cnr edge ratio info" + f (edgeID@(EdgeId _ _ cnr),info) = + take 5 (show cnr++(if cnr `elem` goodCNrs then "*" else "")++repeat ' ') ++ + take 14 (show edgeID++repeat ' ') ++ + take 8 (show (M.findWithDefault 0 cnr fm * 100 `div` nrOfPaths)++"%"++repeat ' ') ++ + "{"++show info++"}" + in do logMsg mymsg + return bestEdges + +-- |Select the "latest" constraint +firstComeFirstBlamed :: Heuristic info +firstComeFirstBlamed = + Heuristic ( + let f (EdgeId _ _ cnr, _) = return cnr + in maximalEdgeFilter "First come, first blamed" f) + +-- |Select only specific constraint numbers +selectConstraintNumbers :: [EdgeNr] -> Heuristic info +selectConstraintNumbers is = + Heuristic ( + let f (EdgeId _ _ cnr, _) = return (cnr `elem` is) + in edgeFilter ("select constraint numbers " ++ show is) f) + +-- |Select only the constraints for which there is evidence in the predicates +-- of the current state that the constraint at hand is incorrect. +inPredicatePath :: Heuristic info +inPredicatePath = + Heuristic (Filter "in a predicate path" f) where + + f xs = + do pp <- predicatePath + path <- expandPath (simplifyPath pp) + let cnrs = nub [ c | (EdgeId _ _ c, _) <- steps path ] + p (EdgeId _ _ cnr, _) = cnr `elem` cnrs + ys = filter p xs + return (if null ys then xs else ys) diff --git a/src/Top/Implementation/TypeGraph/EquivalenceGroup.hs b/src/Top/Implementation/TypeGraph/EquivalenceGroup.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/TypeGraph/EquivalenceGroup.hs @@ -0,0 +1,224 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +-- +-- An equivalence group is a graph-like structure containing type variables and +-- type constants that should all be equivalent. The edges explain why they should +-- be equal. +-- +----------------------------------------------------------------------------- + +module Top.Implementation.TypeGraph.EquivalenceGroup + ( EquivalenceGroup + , emptyGroup, insertVertex, insertEdge, insertClique, combineGroups + , vertices, constants, edges, equalPaths + , removeEdge, removeClique, splitGroup + , typeOfGroup, consistent, checkGroup + ) where + +import Top.Implementation.TypeGraph.Path +import Top.Implementation.TypeGraph.Basics +import Top.Types +import Data.List +import Data.Maybe +import qualified Data.Set as S + +----------------------------------------------------------------------- +-- * Representation of an equivalence group + +data EquivalenceGroup info = + EQGroup { vertices :: [(VertexId, VertexInfo)] -- ^ vertices in this equivalence group + , edges :: [(EdgeId, info)] -- ^ (initial) edges in this equivalence group + , cliques :: [Clique] -- ^ (implied) cliques in this equivalence group + } + +-- first sort the items of an equivalence group +instance Show (EquivalenceGroup info) where + show eqgroup = + unlines $ + [ "[Vertices]:" + , " " ++ concatMap show (sort (vertices eqgroup)) + , "[Edges]:" + , " " ++ concatMap show (sort [ a | (a, _) <- edges eqgroup ]) + , "[Cliques ]:" + ] ++ + map ((" "++) . show) (sort (cliques eqgroup)) + +----------------------------------------------------------------------- +-- * Constructing an equivalence group + +emptyGroup :: EquivalenceGroup info +emptyGroup = + EQGroup { vertices = [], edges = [], cliques = [] } + +insertVertex :: VertexId -> VertexInfo -> EquivalenceGroup info -> EquivalenceGroup info +insertVertex i info eqgroup = + eqgroup { vertices = (i, info) : vertices eqgroup } + +insertEdge :: EdgeId -> info -> EquivalenceGroup info -> EquivalenceGroup info +insertEdge edge info eqgroup = + eqgroup { edges = (edge, info) : edges eqgroup } + +insertClique :: Clique -> EquivalenceGroup info -> EquivalenceGroup info +insertClique clique eqgroup = + eqgroup { cliques = newCliques } + + where + newCliques = mergeCliques (clique : cs2) : cs1 + (cs1, cs2) = partition (isDisjointClique clique) (cliques eqgroup) + + {- msg = unlines [ "------------------insert clique -------------------------" + , show eqgroup + , "---- new cliques ----" + , show newCliques + ] -} + +combineGroups :: EquivalenceGroup info -> EquivalenceGroup info -> EquivalenceGroup info +combineGroups eqgroup1 eqgroup2 = + EQGroup { vertices = vertices eqgroup1 ++ vertices eqgroup2 + , edges = edges eqgroup1 ++ edges eqgroup2 + , cliques = cliques eqgroup1 `combineCliqueList` cliques eqgroup2 + } + +---------------------------------------------------------------------- +-- * Removing parts from an equivalence group + +removeEdge :: EdgeId -> EquivalenceGroup info -> EquivalenceGroup info +removeEdge edge eqgroup = + let p (e, _) = edge /= e + in eqgroup { edges = filter p (edges eqgroup) } + +removeClique :: Clique -> EquivalenceGroup info -> EquivalenceGroup info +removeClique clique eqgroup = + eqgroup { cliques = filter (not . (`isSubsetClique` clique)) (cliques eqgroup) } + +splitGroup :: EquivalenceGroup info -> [EquivalenceGroup info] +splitGroup eqgroup = + let (vs, es, cs) = (vertices eqgroup, edges eqgroup, cliques eqgroup) + eqcs = map (\(a, b) -> insertVertex a b emptyGroup) vs + + addClique clique groups = + let is = childrenInClique clique + (gs1, gs2) = partition (any ((`elem` is) . fst) . vertices) groups + in insertClique clique (foldr combineGroups emptyGroup gs1) : gs2 + + addEdge (edge@(EdgeId v1 v2 _), info) groups = + let is = [v1, v2] + (gs1, gs2) = partition (any ((`elem` is) . fst) . vertices) groups + in insertEdge edge info (foldr combineGroups emptyGroup gs1) : gs2 + + in foldr addEdge (foldr addClique eqcs cs) es + +---------------------------------------------------------------------- +-- * Interrogating an equivalence group + +constants :: EquivalenceGroup info -> [String] +constants eqgroup = + nub [ s | (_, (VCon s, _)) <- vertices eqgroup ] + +consistent :: EquivalenceGroup info -> Bool +consistent eqgroup = + case constants eqgroup of + [] -> True + [_] -> null [ () | (_, (VApp _ _, _)) <- vertices eqgroup ] + _ -> False + +equalPaths :: S.Set VertexId -> VertexId -> [VertexId] -> EquivalenceGroup info -> TypeGraphPath info +equalPaths without start targets eqgroup = + reduceNumberOfPaths $ + tailSharingBy (\(e1, _) (e2, _) -> e1 `compare` e2) $ + rec start (edgeList, cliqueList) + where + -- msg = "Path from "++show start++" to "++show targets++" without "++show (S.elems without) + edgeList = let p (EdgeId v1 v2 _, _) = + not (v1 `S.member` without) && not (v2 `S.member` without) + in filter p (edges eqgroup) + cliqueList = let f = filter (not . (`S.member` without) . child) . triplesInClique + in map f (cliques eqgroup) + targetSet = S.fromList targets + + -- Allow a second visit of a clique in a path? + secondCliqueVisit = False + + rec :: VertexId -> ([(EdgeId, info)], [[ParentChild]]) -> TypeGraphPath info + rec v1 (es, cs) + | v1 `S.member` targetSet = Empty + | otherwise = + let (edges1,es' ) = partition (\(EdgeId a _ _, _) -> v1 == a) es + (edges2,es'') = partition (\(EdgeId _ a _, _) -> v1 == a) es' + (neighbourCliques, otherCliques) = + partition ((v1 `elem`) . map child) cs + rest@(_, restCliques) + | secondCliqueVisit = (es'', removeFromClique v1 neighbourCliques ++ otherCliques) + | otherwise = (es'', otherCliques) + in + altList $ + map (\(EdgeId _ neighbour edgeNr, info) -> + Step (EdgeId v1 neighbour edgeNr, Initial info) + :+: rec neighbour rest) edges1 + ++ map (\(EdgeId neighbour _ edgeNr, info) -> + Step (EdgeId v1 neighbour edgeNr, Initial info) + :+: rec neighbour rest) edges2 + ++ concatMap (\list -> + let (sources, others) = partition ((v1==) . child) list + sourceParents = map parent sources + neighbours = nub (map child others) + f neighbour = altList + [ beginPath :+: restPath + | pc <- others + , child pc == neighbour + , let beginPath = altList1 (map g sourceParents) + restPath + | secondCliqueVisit = rec neighbour (es'', map (filter (/= pc)) restCliques) + | otherwise = rec neighbour rest + g sp = Step ( EdgeId v1 neighbour impliedEdgeNr + , Implied (childSide pc) sp (parent pc) + ) + ] + in if null sources + then [] + else map f neighbours) neighbourCliques + + removeFromClique :: VertexId -> [[ParentChild]] -> [[ParentChild]] + removeFromClique vid = + let p = (> 1) . length + f = filter ((/=vid) . child) + in filter p . map f + +typeOfGroup :: OrderedTypeSynonyms -> EquivalenceGroup info -> Maybe Tp +typeOfGroup synonyms eqgroup + + | length allConstants > 1 = Nothing + | not (null allConstants) && not (null allApplies) = Nothing + + | not (null allOriginals) = Just (theBestType synonyms allOriginals) + | not (null allConstants) = Just (TCon (head allConstants)) + | not (null allApplies) = Just $ let (VertexId l, VertexId r) = head allApplies + in (TApp (TVar l) (TVar r)) + | otherwise = Just (TVar (head allVariables)) + + where + allVariables = [ i | (VertexId i, _) <- vertices eqgroup ] + allConstants = nub [ s | (_, (VCon s, _)) <- vertices eqgroup ] + allApplies = [ (l, r) | (_, (VApp l r, _)) <- vertices eqgroup ] + allOriginals = [ tp | (_, (_, Just tp)) <- vertices eqgroup ] + +-- If I cannot select a best type at this point, an arbitary type is returned. +-- This is because I cannot see "inside" the types +-- Todo: improve +theBestType :: OrderedTypeSynonyms -> Tps -> Tp +theBestType synonyms tps = + let f t1 t2 = fromMaybe t1 (equalUnderTypeSynonyms synonyms t1 t2) + in foldr1 f tps + +-- Check for some invariants: identity if everything is okay, otherwise an internal error +checkGroup :: EquivalenceGroup info -> EquivalenceGroup info +checkGroup = test c2 . test c1 where + test p eqGroup = if p eqGroup then error "Check failed for equivalence group" else eqGroup + c1 eqGroup = hasDouble (concatMap triplesInClique $ cliques eqGroup) + c2 eqGroup = any ((<2) . length . triplesInClique) (cliques eqGroup) + hasDouble [] = False + hasDouble (x:xs) = x `elem` xs || hasDouble xs diff --git a/src/Top/Implementation/TypeGraph/Heuristic.hs b/src/Top/Implementation/TypeGraph/Heuristic.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/TypeGraph/Heuristic.hs @@ -0,0 +1,97 @@ +{-# LANGUAGE RankNTypes, FlexibleContexts #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Implementation.TypeGraph.Heuristic where + +import Top.Implementation.TypeGraph.ClassMonadic +import Top.Implementation.TypeGraph.Basics +import Top.Implementation.TypeGraph.Path +import Top.Types +import Top.Solver +import Utils (internalError) + +----------------------------------------------------------------------------- + +type PathHeuristics info = Path (EdgeId, info) -> [Heuristic info] + +newtype Heuristic info = Heuristic (forall m . HasTypeGraph m info => HComponent m info) +data Selector m info + = Selector (String, (EdgeId, info) -> m (Maybe (Int, String, [EdgeId], info))) + | SelectorList (String, [(EdgeId, info)] -> m (Maybe (Int, String, [EdgeId], info))) + +data HComponent m info + = Filter String ([(EdgeId, info)] -> m [(EdgeId, info)]) + | Voting [Selector m info] + +getSelectorName :: (MonadWriter LogEntries m, HasTypeGraph m info) => Selector m info -> String +getSelectorName (Selector (name,_)) = name +getSelectorName (SelectorList (name,_)) = name + +resultsEdgeFilter :: (Eq a, Monad m) => ([a] -> a) -> String -> ((EdgeId,info) -> m a) -> HComponent m info +resultsEdgeFilter selector description function = + Filter description $ \es -> + do tupledList <- let f tuple = + do result <- function tuple + return (result, tuple) + in mapM f es + let maximumResult + | null tupledList = internalError "Top.TypeGraph.Heuristics" "resultsEdgeFilter" "unexpected empty list" + | otherwise = selector (map fst tupledList) + return (map snd (filter ((maximumResult ==) . fst) tupledList)) + +maximalEdgeFilter :: (Ord a, Monad m) => String -> ((EdgeId,info) -> m a) -> HComponent m info +maximalEdgeFilter = resultsEdgeFilter maximum + +minimalEdgeFilter :: (Ord a, Monad m) => String -> ((EdgeId,info) -> m a) -> HComponent m info +minimalEdgeFilter = resultsEdgeFilter minimum + +edgeFilter :: Monad m => String -> ((EdgeId, info) -> m Bool) -> HComponent m info +edgeFilter description function = + Filter description $ \es -> + do xs <- filterM function es + return (if null xs then es else xs) + + +----------------------------------------------------------------------------- + +doWithoutEdges :: HasTypeGraph m info => [(EdgeId, info)] -> m result -> m result +doWithoutEdges xs computation = + case xs of + [] -> computation + [e] -> doWithoutEdge e computation + e:es -> doWithoutEdge e (doWithoutEdges es computation) + +doWithoutEdge :: HasTypeGraph m info => (EdgeId, info) -> m result -> m result +doWithoutEdge (edge, info) computation = + do -- copy1 <- mapM showGroupOf [0..100] + deleteEdge edge + result <- computation + addEdge edge info + -- copy2 <- mapM showGroupOf [0..100] + -- if copy1 /= copy2 then + -- error ("SAFETY check failed\n\n" ++ head [ x1++x2 | (x1, x2) <- zip copy1 copy2, x1 /= x2]) else + return result + +eqInfo2 :: (EdgeId, info) -> (EdgeId, info) -> Bool +eqInfo2 (EdgeId _ _ b1, _) (EdgeId _ _ b2, _) = b1 == b2 + +info2ToEdgeNr :: (EdgeId, info) -> EdgeNr +info2ToEdgeNr (EdgeId _ _ i, _) = i + +----------------------------------------------------------------------------- + +class HasTwoTypes a where + getTwoTypes :: a -> (Tp, Tp) + +getSubstitutedTypes :: (HasTypeGraph m info, HasTwoTypes info) => info -> m (Maybe Tp, Maybe Tp) +getSubstitutedTypes info = + do let (t1,t2) = getTwoTypes info + mt1 <- substituteTypeSafe t1 + mt2 <- substituteTypeSafe t2 + return (mt1, mt2) diff --git a/src/Top/Implementation/TypeGraph/Path.hs b/src/Top/Implementation/TypeGraph/Path.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/TypeGraph/Path.hs @@ -0,0 +1,290 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +----------------------------------------------------------------------------- + +module Top.Implementation.TypeGraph.Path where + +import Data.Function +import Data.List +import Data.Maybe +import qualified Data.Map as M +import Utils (internalError) + +---------------------- + +data Path a = Path a :|: Path a -- alternative + | Path a :+: Path a -- sequence + | Step a + | Fail + | Empty + +seqList, seqList1 :: [Path a] -> Path a +seqList = foldr (:+:) Empty +seqList1 = foldr1 (:+:) + +altList, altList1 :: [Path a] -> Path a +altList = foldr (:|:) Fail +altList1 = foldr1 (:|:) + +instance Show a => Show (Path a) where + show path = + case path of + x :|: y -> show x ++ "|" ++ show y + x :+: y -> parIf (pathPrio x < 1) (show x) ++ "+" ++ parIf (pathPrio y < 1) (show y) + Step a -> show a + Fail -> "Fail" + Empty -> "Empty" + + where pathPrio :: Path a -> Int + pathPrio (_ :|: _) = 0 + pathPrio (_ :+: _) = 1 + pathPrio _ = 2 + + parIf b s = if b then "("++s++")" else s + +-- |Combine two monadic computations +mCombine :: Monad m => (a -> b -> c) -> m a -> m b -> m c +mCombine op mp1 mp2 = + do p1 <- mp1 + p2 <- mp2 + return (p1 `op` p2) + +(<+>), (<|>) :: Monad m => m (Path a) -> m (Path a) -> m (Path a) +(<+>) = mCombine (:+:) +(<|>) = mCombine (:|:) + +(<++>) :: Monad m => m [Path a] -> m [Path a] -> m [Path a] +(<++>) = mCombine (++) + +steps :: Path a -> [a] +steps = ($ []) . rec where + rec path = + case path of + x :|: y -> rec x . rec y + x :+: y -> rec x . rec y + Step a -> (a:) + Fail -> id + Empty -> id + +mapPath :: (a -> b) -> Path a -> Path b +mapPath f = changeStep (Step . f) + +changeStep :: (a -> Path b) -> Path a -> Path b +changeStep f = rec + where + rec path = + case path of + Step a -> f a + x :|: y -> rec x :|: rec y + x :+: y -> rec x :+: rec y + Fail -> Fail + Empty -> Empty + +changeStepM :: Monad m => (a -> m (Path b)) -> Path a -> m (Path b) +changeStepM f path = + case path of + Step a -> f a + x :|: y -> do x' <- changeStepM f x; y' <- changeStepM f y; return (x' :|: y') + x :+: y -> do x' <- changeStepM f x; y' <- changeStepM f y; return (x' :+: y') + Fail -> return Fail + Empty -> return Empty + +minCompleteInPath :: (a -> a -> Ordering) -> Path a -> Maybe a +minCompleteInPath f = rec . simplifyPath + where + rec path = + case path of + x :|: y -> do v1 <- rec x; v2 <- rec y; return (minimumBy f [v1, v2]) + x :+: y -> do v1 <- rec x; v2 <- rec y; return (maximumBy f [v1, v2]) + Step a -> Just a + Fail -> Nothing + Empty -> Nothing + +simplifyPath :: Path a -> Path a +simplifyPath path = + case path of + x :|: y -> + case (simplifyPath x, simplifyPath y) of + (Empty, _ ) -> Empty + (_ , Empty) -> Empty + (Fail , p2 ) -> p2 + (p1 , Fail ) -> p1 + (p1 , p2 ) -> p1 :|: p2 + x :+: y -> + case (simplifyPath x, simplifyPath y) of + (Fail , _ ) -> Fail + (_ , Fail ) -> Fail + (Empty, p1 ) -> p1 + (p2 , Empty) -> p2 + (p1 , p2 ) -> p1 :+: p2 + _ -> path + +tailSharingBy :: (a -> a -> Ordering) -> Path a -> Path a +tailSharingBy compf thePath = + case simplifyPath thePath of + Empty -> Empty + Fail -> Fail + p -> rec p + + where + eqf x y = compf x y == EQ + eqfM x y = compfM x y == EQ + compfM Nothing Nothing = EQ + compfM (Just x) (Just y) = compf x y + compfM m1 _ = if isJust m1 then GT else LT + + -- invariant: rec does not have Empty's or Fail's + rec (Step a) = Step a + rec (p1 :+: p2) = p1 :+: rec p2 + rec path = + let sharedTail = map (\((p, tl):rest) -> combine (p:map fst rest) tl) + . groupBy (eqfM `on` snd) + . sortBy (compfM `on` snd) + $ [ (p, lastStep p) | p <- altPath path ] + + combine paths Nothing = altList1 paths + combine paths (Just tl) = + case tailSharingBy compf (altList1 (map removeTail paths)) of + Fail -> Fail + Empty -> Step tl + p -> p :+: Step tl + + in altList1 sharedTail + + altPath :: Path a -> [Path a] + altPath (p1 :|: p2) = altPath p1 ++ altPath p2 + altPath path = [path] + + lastStep (Step a) = Just a + lastStep (_ :+: p2) = lastStep p2 + lastStep (p1 :|: p2) = do a <- lastStep p1 + b <- lastStep p2 + if a `eqf` b + then Just a + else Nothing + lastStep _ = internalError "Top.TypeGraph.Paths" "lastStep" "unexpected path" + + + removeTail (Step _) = Empty + removeTail (p1 :+: p2) = p1 :+: removeTail p2 + removeTail (p1 :|: p2) = removeTail p1 :|: removeTail p2 + removeTail _ = internalError "Top.TypeGraph.Paths" "removeTail" "unexpected path" + +flattenPath :: Path a -> [[a]] +flattenPath path = + case path of + Empty -> [[]] + Fail -> [] + Step a -> [[a]] + p1 :+: p2 -> [ as ++ bs | as <- flattenPath p1, bs <- flattenPath p2] + p1 :|: p2 -> flattenPath p1 ++ flattenPath p2 + +-- returns a list with 'smallest minimal sets' +minimalSets :: (a -> a -> Bool) -> Path a -> [[a]] +minimalSets eqF = rec where + + -- invariant: rec returns lists with the same length + rec path = + case simplifyPath path of + Empty -> [] + Fail -> [[]] + p -> + let a = head (steps p) + sol1 = rec (changeStep (\b -> if a `eqF` b then Empty else Step b) p) + sol2 = [ a : set + | set <- rec (changeStep (\b -> if a `eqF` b then Fail else Step b) p) + ] + in case (sol1, sol2) of + (x:_, y:_) -> + case length x `compare` length y of + LT -> sol1 + EQ -> sol1 ++ sol2 + GT -> sol2 + _ -> sol1 ++ sol2 + +removeSomeDuplicates :: Ord b => (a -> b) -> Path a -> Path a +removeSomeDuplicates toOrd = simplifyPath . rec M.empty where + rec fm path = + case path of + + left :+: right -> + case left of + Step a -> let int = toOrd a + fm' = M.insert int Empty fm + in case M.lookup int fm of + Just left' -> left' :+: rec fm right + Nothing -> left :+: rec fm' right + p1 :+: p2 -> rec fm (p1 :+: (p2 :+: right)) + _ -> rec fm left :+: rec fm right + + left :|: right -> + case left of + Step a -> let int = toOrd a + fm' = M.insert int Fail fm + in case M.lookup int fm of + Just left' -> left' :|: rec fm right + Nothing -> left :|: rec fm' right + p1 :|: p2 -> rec fm (p1 :|: (p2 :|: right)) + _ -> rec fm left :|: rec fm right + + Step a -> + M.findWithDefault path (toOrd a) fm + + _ -> path + +participationMap :: Ord a => Path a -> (Integer, M.Map a Integer) +participationMap path = + case path of + Empty -> (1, M.empty) + Fail -> (0, M.empty) + Step a -> (1, M.singleton a 1) + p1 :+: p2 -> let (i1, fm1) = participationMap p1 + (i2, fm2) = participationMap p2 + fm1' = M.map (*i2) fm1 + fm2' = M.map (*i1) fm2 + in (i1 * i2, M.unionWith (\j1 j2 -> j1 + j2 - ((j1*j2) `div` (i1*i2))) fm1' fm2') + p1 :|: p2 -> let (i1, fm1) = participationMap p1 + (i2, fm2) = participationMap p2 + in (i1 + i2, M.unionWith (+) fm1 fm2) + +pathSize :: Path a -> Int +pathSize (p1 :|: p2) = pathSize p1 + pathSize p2 +pathSize (p1 :+: p2) = pathSize p1 * pathSize p2 +pathSize (Step _) = 1 +pathSize _ = 0 + +-- |The maximal number of equality paths that is returned by equalPaths +-- (although this number can be exceeded...it is more or less used as approximation) +-- Nothing indicates that there is no limit +maxNumberOfEqualPaths :: Maybe Int +maxNumberOfEqualPaths = Just 50 + +reduceNumberOfPaths :: Path a -> Path a +reduceNumberOfPaths = maybe id limitNumberOfPaths maxNumberOfEqualPaths + +limitNumberOfPaths :: Int -> Path a -> Path a +limitNumberOfPaths size = fst . rec size + where + fromInt :: Num a => Int -> a + fromInt = fromInteger . toInteger + + rec sz path = + case path of + Empty -> (path, 1) + Fail -> (path, 0) + Step _ -> (path, 1) + p1 :+: p2 -> let (p1', n1) = rec sz p1 + newSize + | n1 == 0 = sz + | otherwise = ceiling ((fromInt sz / fromInt n1) :: Double) + (p2', n2) = rec newSize p2 + in (p1' :+: p2', n1*n2) + p1 :|: p2 -> let both@(p1' , n1) = rec sz p1 + (p2', n2) = rec (sz - n1) p2 + in if n1 >= sz + then both + else (p1' :|: p2', n1 + n2) diff --git a/src/Top/Implementation/TypeGraph/Standard.hs b/src/Top/Implementation/TypeGraph/Standard.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/TypeGraph/Standard.hs @@ -0,0 +1,261 @@ +{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Implementation.TypeGraph.Standard where + +import Top.Implementation.TypeGraph.Basics +import Top.Implementation.TypeGraph.EquivalenceGroup +import Top.Implementation.TypeGraph.Class +import Top.Implementation.General +import Top.Types +import qualified Data.Map as M +import Data.List (nub) +import Data.Maybe +import Utils (internalError) + +data StandardTypeGraph info = STG + { referenceMap :: M.Map VertexId Int{- group number -} + , equivalenceGroupMap :: M.Map Int (EquivalenceGroup info) + , equivalenceGroupCounter :: Int + , possibleErrors :: [VertexId] + , constraintNumber :: Int + } + +instance Show info => Empty (StandardTypeGraph info) where + empty = STG + { referenceMap = M.empty + , equivalenceGroupMap = M.empty + , equivalenceGroupCounter = 0 + , possibleErrors = [] + , constraintNumber = 0 + } + +instance Show (StandardTypeGraph info) where + show stg = + "(Type graph consists of " ++ show (M.size (equivalenceGroupMap stg)) ++ " equivalence groups)" + +instance TypeGraph (StandardTypeGraph info) info where + + addTermGraph synonyms = rec + where + rec unique tp stg = + let (newtp, original) = + case expandToplevelTC synonyms tp of + Nothing -> (tp, Nothing) + Just x -> (x, Just tp) + in case newtp of + TVar i -> + let vid = VertexId i + in (unique, vid, if vertexExists vid stg then stg else addVertex vid (VVar, original) stg) + TCon s -> + let vid = VertexId unique + in (unique+1, vid, addVertex vid (VCon s, original) stg) + TApp t1 t2 -> + let (u1, v1, g1) = rec unique t1 stg + (u2, v2, g2) = rec u1 t2 g1 + vid = VertexId u2 + in (u2+1, vid, addVertex vid (VApp v1 v2, original) g2) + + addVertex v info = + createGroup (insertVertex v info emptyGroup) + + addEdge edge@(EdgeId v1 v2 _) info = + propagateEquality v1 . updateGroupOf v1 (insertEdge edge info) . combineClasses [v1, v2] + + addNewEdge (v1, v2) info stg = + let cnr = makeEdgeNr (constraintNumber stg) + in addEdge (EdgeId v1 v2 cnr) info (stg { constraintNumber = constraintNumber stg + 1}) + + deleteEdge edge@(EdgeId v1 _ _) = + propagateRemoval v1 . updateGroupOf v1 (removeEdge edge) + + verticesInGroupOf i = + vertices . getGroupOf i + + substituteTypeSafe synonyms = + let rec history (TVar i) stg + | i `elem` history = Nothing + | otherwise = + case maybeGetGroupOf (VertexId i) stg of + Nothing -> + Just (TVar i) + Just _ -> + do newtp <- typeOfGroup synonyms (getGroupOf (VertexId i) stg) + case newtp of + TVar j -> Just (TVar j) + _ -> rec (i:history) newtp stg + + rec _ tp@(TCon _) _ = Just tp + + rec history (TApp l r) stg = + do l' <- rec history l stg + r' <- rec history r stg + Just (TApp l' r') + in rec [] + + edgesFrom i = + let p (EdgeId v1 v2 _, _) = v1 == i || v2 == i + in filter p . edges . getGroupOf i + + allPathsListWithout without v1 vs = + equalPaths without v1 vs . getGroupOf v1 + + makeSubstitution syns stg = + let f eqgroup = + case typeOfGroup syns eqgroup of + Just tp -> [ (vid, tp) | (vid@(VertexId i), _) <- vertices eqgroup, notId i tp ] + Nothing -> internalError "Top.TypeGraph.Implementation" "makeSubstitution" "inconsistent equivalence group" + notId i (TVar j) = i /= j + notId _ _ = True + in concatMap f (getAllGroups stg) + + typeFromTermGraph vid stg = + case [ tp | (x, (tp, _)) <- verticesInGroupOf vid stg, vid == x ] of + [VCon s] -> TCon s + [VApp a b] -> TApp (typeFromTermGraph a stg) (typeFromTermGraph b stg) + _ -> vertexIdToTp vid + + markAsPossibleError = + addPossibleInconsistentGroup + + getMarkedPossibleErrors = + getPossibleInconsistentGroups + + unmarkPossibleErrors = + setPossibleInconsistentGroups [] + +-- Helper functions +combineClasses :: [VertexId] -> StandardTypeGraph info -> StandardTypeGraph info +combineClasses is stg = + case nub (map (`representativeInGroupOf` stg) is) of + list@(i:_:_) -> + let eqgroups = map (`getGroupOf` stg) list + newGroup = foldr combineGroups emptyGroup eqgroups + in addPossibleInconsistentGroup i . createGroup newGroup . foldr removeGroup stg $ eqgroups + _ -> stg + +propagateEquality :: VertexId -> StandardTypeGraph info -> StandardTypeGraph info +propagateEquality vid stg = + let (listLeft, listRight) = childrenInGroupOf vid stg + left = map (flip representativeInGroupOf stg . child) listLeft + right = map (flip representativeInGroupOf stg . child) listRight + in (if length (nub right) > 1 + then propagateEquality (head right) + else id) + . (if length (nub left) > 1 + then propagateEquality (head left) + else id) + . (if length listLeft > 1 + then addClique (makeClique listRight) . addClique (makeClique listLeft) + else id) + $ stg + +addClique :: Clique -> StandardTypeGraph info -> StandardTypeGraph info +addClique clique = + updateGroupOf (cliqueRepresentative clique) (insertClique clique) . combineClasses (childrenInClique clique) + +propagateRemoval :: VertexId -> StandardTypeGraph info -> StandardTypeGraph info +propagateRemoval i stg = + let (is, new) = splitClass i stg + ts = map (`childrenInGroupOf` new) is + + (leftList, rightList) = unzip ts + cliqueLeft = makeClique (concat leftList) + cliqueRight = makeClique (concat rightList) + newCliques = [ makeClique list | list <- leftList ++ rightList, length list > 1 ] + children = [ child pc | pc:_ <- leftList ++ rightList ] + in + if length (filter (not . null) leftList) > 1 + then flip (foldr propagateRemoval) children + . flip (foldr addClique) newCliques + . deleteClique cliqueRight + . deleteClique cliqueLeft + $ new + else new + +splitClass :: VertexId -> StandardTypeGraph info -> ([VertexId], StandardTypeGraph info) +splitClass vid stg = + let eqgroup = getGroupOf vid stg + newGroups = splitGroup eqgroup + results = [ vid2 | (vid2, _):_ <- map vertices newGroups ] + newGraph + | length newGroups > 1 = foldr createGroup (removeGroup eqgroup stg) newGroups + | otherwise = stg + in (results, newGraph) + +deleteClique :: Clique -> StandardTypeGraph info -> StandardTypeGraph info +deleteClique clique = + updateGroupOf (cliqueRepresentative clique) (removeClique clique) + +----------------------------------------------------------------- + +createGroup :: EquivalenceGroup info -> StandardTypeGraph info -> StandardTypeGraph info +createGroup eqgroup stg = + let newGroupNumber = equivalenceGroupCounter stg + list = [(i, newGroupNumber) | (i, _) <- vertices eqgroup ] + in if null list + then internalError "Top.TypeGraph.TypeGraphMonad" "createNewGroup" "cannot create an empty equivalence group" + else stg { referenceMap = referenceMap stg `M.union` M.fromList list + , equivalenceGroupMap = M.insert newGroupNumber eqgroup (equivalenceGroupMap stg) + , equivalenceGroupCounter = newGroupNumber + 1 + } + +removeGroup :: EquivalenceGroup info -> StandardTypeGraph info -> StandardTypeGraph info +removeGroup eqgroup stg = + let vertexIds = map fst (vertices eqgroup) + oldGroupNr = maybeToList (M.lookup (head vertexIds) (referenceMap stg)) + in stg { referenceMap = foldr M.delete (referenceMap stg) vertexIds + , equivalenceGroupMap = foldr M.delete (equivalenceGroupMap stg) oldGroupNr + } + +updateGroupOf :: VertexId -> (EquivalenceGroup info -> EquivalenceGroup info) -> StandardTypeGraph info -> StandardTypeGraph info +updateGroupOf vid f stg = + let eqgrp = getGroupOf vid stg + err = internalError "Top.TypeGraph.TypeGraphMonad" "updateEquivalenceGroupOf" ("error in lookup map: "++show vid) + eqnr = M.findWithDefault err vid (referenceMap stg) + in stg { equivalenceGroupMap = M.insert eqnr (f eqgrp) (equivalenceGroupMap stg) } + +maybeGetGroupOf :: VertexId -> StandardTypeGraph info -> Maybe (EquivalenceGroup info) +maybeGetGroupOf vid stg = + do eqnr <- M.lookup vid (referenceMap stg) + let err = internalError "Top.TypeGraph.TypeGraphMonad" "equivalenceGroupOf" "error in lookup map" + return (M.findWithDefault err eqnr (equivalenceGroupMap stg)) + +getGroupOf :: VertexId -> StandardTypeGraph info -> EquivalenceGroup info +getGroupOf vid = + let err = internalError "Top.TypeGraph.Standard" "getGroupOf" "the function getGroupOf does no longer create an empty group if the vertexId doesn't exist" + in fromMaybe err . maybeGetGroupOf vid + +getAllGroups :: StandardTypeGraph info -> [EquivalenceGroup info] +getAllGroups = M.elems . equivalenceGroupMap + +vertexExists :: VertexId -> StandardTypeGraph info -> Bool +vertexExists vid = isJust . M.lookup vid . referenceMap + +----------------------------------------------------------------------------------- + +getPossibleInconsistentGroups :: StandardTypeGraph info -> [VertexId] +getPossibleInconsistentGroups = possibleErrors + +setPossibleInconsistentGroups :: [VertexId] -> StandardTypeGraph info -> StandardTypeGraph info +setPossibleInconsistentGroups vids stg = stg { possibleErrors = vids } + +addPossibleInconsistentGroup :: VertexId -> StandardTypeGraph info -> StandardTypeGraph info +addPossibleInconsistentGroup vid stg = stg { possibleErrors = vid : possibleErrors stg } + +-------------------------------------------------------------------------------- +{- +setHeuristics :: [Heuristic info] -> StandardTypeGraph info -> StandardTypeGraph info +setHeuristics = setPathHeuristics . const + +setPathHeuristics :: (Path (EdgeId, info) -> [Heuristic info]) -> StandardTypeGraph info -> StandardTypeGraph info +setPathHeuristics f stg = stg {typegraphHeuristics = f} + +getPathHeuristics :: StandardTypeGraph info -> Path (EdgeId, info) -> [Heuristic info] +getPathHeuristics = typegraphHeuristics -} diff --git a/src/Top/Implementation/TypeGraphSubstitution.hs b/src/Top/Implementation/TypeGraphSubstitution.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/TypeGraphSubstitution.hs @@ -0,0 +1,103 @@ +{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Implementation.TypeGraphSubstitution where + +import Top.Implementation.TypeGraph.ClassMonadic +import Top.Implementation.TypeGraph.Standard +import Top.Implementation.TypeGraph.Heuristic +import Top.Interface.Substitution +import Top.Interface.Basic +import Top.Interface.TypeInference +import Top.Interface.Qualification +import Top.Implementation.TypeGraph.DefaultHeuristics +import Top.Implementation.TypeGraph.ApplyHeuristics +import Top.Monad.Select +import Top.Monad.StateFix +import Top.Solver +import Top.Implementation.General +import Top.Util.Embedding + +------------------------------------------------------------------------ +-- (I) Algebraic data type + +data TypeGraphState info = TypeGraphState + { typegraph :: StandardTypeGraph info + , heuristics :: PathHeuristics info + } + +------------------------------------------------------------------------ +-- (II) Instance of SolveState (Empty, Show) + +instance Show info => SolveState (TypeGraphState info) where + stateName _ = "Typegraph substitution state" + +instance Show info => Show (TypeGraphState info) where + show = show . typegraph + +instance Show info => Empty (TypeGraphState info) where + empty = TypeGraphState empty defaultHeuristics + +------------------------------------------------------------------------ +-- (III) Embeddings + +instance Embedded ClassSubst (TypeGraphState info) (TypeGraphState info) where embedding = idE +instance Embedded ClassSubst (Simple (TypeGraphState info) x m) (TypeGraphState info) where embedding = fromFstSimpleE embedding + +------------------------------------------------------------------------ +-- (IV) Instance declaration + +instance ( Monad m + , Embedded ClassSubst (s (StateFixT s m)) t + , HasTG (Select t (StateFixT s m)) info + ) => + HasTG (StateFixT s m) info where + + withTypeGraph f = deSubst (withTypeGraph f) + +instance ( MonadState s m + , Embedded ClassSubst s (TypeGraphState info) + ) => + HasTG (Select (TypeGraphState info) m) info where + + withTypeGraph f = + do (a, new) <- gets (f . typegraph) + modify (\tgs -> tgs { typegraph = new }) + return a + +instance ( HasBasic m info + , HasTI m info + , HasQual m info + , HasTG m info + , MonadWriter LogEntries m + , Show info + , MonadState s m + , Embedded ClassSubst s (TypeGraphState info) + ) => + HasSubst (Select (TypeGraphState info) m) info where + + makeSubstConsistent = + do hs <- gets heuristics + select (removeInconsistencies hs) + + unifyTerms a b c = select (theUnifyTerms a b c) + findSubstForVar a = select (substituteVariable a) + fixpointSubst = select makeFixpointSubst + +removeInconsistencies :: HasTypeGraph m info => PathHeuristics info -> m () +removeInconsistencies hs = + do errs <- applyHeuristics hs + mapM_ deleteEdge (concatMap fst errs) + mapM_ (addLabeledError unificationErrorLabel . snd) errs + if null errs + then -- everything is okay: no errors were found. + unmarkPossibleErrors + else -- Bug patch 3 february 2004 + -- safety first: check whether *everything* is really removed. + removeInconsistencies hs diff --git a/src/Top/Implementation/TypeInference.hs b/src/Top/Implementation/TypeInference.hs new file mode 100644 --- /dev/null +++ b/src/Top/Implementation/TypeInference.hs @@ -0,0 +1,90 @@ +{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +-- +-- Additional state information that should be stored in order to perform +-- type inference. +-- +----------------------------------------------------------------------------- + +module Top.Implementation.TypeInference where + +import Top.Types +import Top.Implementation.General +import Top.Interface.TypeInference +-- import Data.List +import qualified Data.Map as M +import Top.Util.Empty +import Top.Monad.Select +-- import Control.Monad.State +import Utils (internalError) + +------------------------------------------------------------------------ +-- (I) Algebraic data type + +data TIState info = TIState + { counter :: Int -- ^ A counter for fresh type variables + , synonyms :: OrderedTypeSynonyms -- ^ All known type synonyms + , skolems :: [([Int], info, Tps)] -- ^ List of skolem constants + , schemeMap :: M.Map Int (Scheme Predicates) -- ^ Type scheme map + } + +------------------------------------------------------------------------ +-- (II) Instance of SolveState (Empty, Show) + +instance Show info => SolveState (TIState info) where + stateName _ = "Type Inference State" + +-- |An empty type inference state. +instance Show info => Empty (TIState info) where + empty = TIState + { counter = 0 + , synonyms = noOrderedTypeSynonyms + , skolems = [] + , schemeMap = M.empty + } + +instance Show info => Show (TIState info) where + show s = unlines [ "counter: " ++ show (counter s) + , "skolem constants: " ++ show (skolems s) + , "synonyms: " ++ concat [ t++"; " | t <- M.keys (fst (synonyms s)) ] + , let f (i, x) = " s"++show i++" = "++show x + in unlines $ map f (M.toList $ schemeMap s) + ] + +------------------------------------------------------------------------ +-- (III) Embeddings + +instance Embedded ClassTI (Simple (TIState info) x m) (TIState info) where embedding = fstSimpleE + +------------------------------------------------------------------------ +-- (IV) Instance declaration + +instance ( MonadState s m + , Embedded ClassTI s (TIState info) + ) => + HasTI (Select (TIState info) m) info where + + getUnique = gets counter + setUnique i = modify (\x -> x { counter = i }) + + getTypeSynonyms = gets synonyms + setTypeSynonyms xs = modify (\x -> x { synonyms = xs }) + + getSkolems = gets skolems + setSkolems sk = modify (\x -> x { skolems = sk }) + + allTypeSchemes = + gets schemeMap + + getTypeScheme i = + let err = internalError "Top.States.QualifierState" "getTypeScheme" "sigma var not found in map" + in gets (M.findWithDefault err i . schemeMap) + + storeTypeScheme sv scheme = + let f s = s { schemeMap = M.insert sv scheme (schemeMap s) } + in modify f diff --git a/src/Top/Interface/Basic.hs b/src/Top/Interface/Basic.hs new file mode 100644 --- /dev/null +++ b/src/Top/Interface/Basic.hs @@ -0,0 +1,123 @@ +{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances, + FunctionalDependencies, FlexibleInstances, FlexibleContexts #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Interface.Basic where + +import Top.Constraint +import Top.Util.Option +import Top.Monad.Select +import Top.Monad.StateFix +import Utils (internalError) + +------------------------------------------------------------------------ +-- (I) Class name and (dedicated) deselect function + +data ClassBasic = ClassBasic + +deBasic :: (Embedded ClassBasic (s (StateFixT s m)) (t (StateFixT s m)), Monad m) => SelectFix t (StateFixT s m) a -> StateFixT s m a +deBasic = deselectFixFor ClassBasic + +------------------------------------------------------------------------ +-- (II) Type class declaration + +class Monad m => HasBasic m info | m -> info where + + -- constraints + pushConstraint :: Constraint m -> m () + pushConstraints :: Constraints m -> m () + popConstraint :: m (Maybe (Constraint m)) + discardConstraints :: m () + -- errors + addLabeledError :: ErrorLabel -> info -> m () + getLabeledErrors :: m [(info, ErrorLabel)] + updateErrorInfo :: (info -> m info) -> m () + -- conditions + addCheck :: String -> m Bool -> m () + getChecks :: m [(m Bool, String)] + -- options + stopAfterFirstError :: OptionAccess m Bool + checkConditions :: OptionAccess m Bool + + -- defaults + pushConstraint c = pushConstraints [c] + pushConstraints = mapM_ pushConstraint + stopAfterFirstError = ignoreOption stopOption + checkConditions = ignoreOption checkOption + +------------------------------------------------------------------------ +-- (III) Instance for solver monad + +instance ( Monad m + , Embedded ClassBasic (s (StateFixT s m)) (t (StateFixT s m)) + , HasBasic (SelectFix t (StateFixT s m)) info + ) => + HasBasic (StateFixT s m) info where + + -- constraints + pushConstraint = deBasic . pushConstraint . mapConstraint selectFix + pushConstraints = deBasic . pushConstraints . map (mapConstraint selectFix) + popConstraint = deBasic $ liftM (fmap (mapConstraint deBasic)) popConstraint + discardConstraints = deBasic discardConstraints + -- errors + addLabeledError label = deBasic . addLabeledError label + getLabeledErrors = deBasic getLabeledErrors + updateErrorInfo = deBasic . selectFix . updateErrorInfo + -- conditions + addCheck s = deBasic . addCheck s . selectFix + getChecks = deBasic (selectFix getChecks) + -- options + stopAfterFirstError = optionAccessTrans deBasic stopAfterFirstError + checkConditions = optionAccessTrans deBasic checkConditions + +------------------------------------------------------------------------ +-- (IV) Additional functions + +pushOperation :: HasBasic m info => m () -> m () +pushOperation = pushNamedOperation "operation" + +pushNamedOperation :: HasBasic m info => String -> m () -> m () +pushNamedOperation s = pushConstraint . operation s + +addError :: HasBasic m info => info -> m () +addError = addLabeledError NoErrorLabel + +getErrors :: HasBasic m info => m [info] +getErrors = liftM (map fst) getLabeledErrors + +doChecks :: HasBasic m info => m () +doChecks = + do ms <- getChecks + bs <- filterM (liftM not . fst) ms + unless (null bs) $ + let err = "\n\n The following constraints were violated:\n" + ++ unlines (map ((" - "++) . snd) bs) + in internalError "Top.States.BasicState" "doChecks" err + +startSolving :: HasBasic m info => m () +startSolving = + do mc <- popConstraint + case mc of + Nothing -> + do check <- getOption checkConditions + errs <- getErrors + when (check && null errs) doChecks + Just c -> + do solveConstraint c + addCheck (show c) (checkCondition c) + startSolving + +-- |A datatype to label the errors that are detected. +data ErrorLabel = ErrorLabel String + | NoErrorLabel + deriving (Eq, Ord, Show) + +stopOption, checkOption :: Option Bool +stopOption = option False "Stop solving constraints after the first error" +checkOption = option False "Check constraint satisfaction afterwards" diff --git a/src/Top/Interface/Qualification.hs b/src/Top/Interface/Qualification.hs new file mode 100644 --- /dev/null +++ b/src/Top/Interface/Qualification.hs @@ -0,0 +1,124 @@ +{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses, + FunctionalDependencies, FlexibleInstances, FlexibleContexts #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Interface.Qualification where + +import Top.Monad.Select +import Top.Monad.StateFix +import Top.Types hiding (contextReduction) +import Top.Interface.Substitution + +------------------------------------------------------------------------ +-- (I) Class name and (dedicated) deselect function + +data ClassQual = ClassQual + +deQual :: (Embedded ClassQual (s (StateFixT s m)) t, Monad m) => Select t (StateFixT s m) a -> StateFixT s m a +deQual = deselectFor ClassQual + +------------------------------------------------------------------------ +-- (II) Type class declaration + + +class Monad m => HasQual m info | m -> info where + + -- general + proveQualifier :: info -> Predicate -> m () + assumeQualifier :: info -> Predicate -> m () + changeQualifiers :: (Predicate -> m Predicate) -> m () + + allQualifiers :: m [Predicate] + generalizeWithQualifiers :: Tps -> Tp -> m (Scheme [Predicate]) + + improveQualifiers :: Bool -> m [(info, Tp, Tp)] + improveQualifiersNormal :: m [(info, Tp, Tp)] + improveQualifiersFinal :: m [(info, Tp, Tp)] + simplifyQualifiers :: m () + ambiguousQualifiers :: m () + + -- class environment + setClassEnvironment :: ClassEnvironment -> m () + getClassEnvironment :: m ClassEnvironment + + -- default definitions + generalizeWithQualifiers monos = + return . generalize monos . ([] .=>.) + + improveQualifiers normal = + if normal then improveQualifiersNormal else improveQualifiersFinal + + improveQualifiersNormal = + return [] + + improveQualifiersFinal = + return [] + + simplifyQualifiers = + return () + + ambiguousQualifiers = + return () + +------------------------------------------------------------------------ +-- (III) Instance for solver monad + +instance ( Monad m + , Embedded ClassQual (s (StateFixT s m)) t + , HasQual (Select t (StateFixT s m)) info + ) => + HasQual (StateFixT s m) info where + + proveQualifier info p = deQual (proveQualifier info p) + assumeQualifier info p = deQual (assumeQualifier info p) + changeQualifiers f = deQual (changeQualifiers (select . f)) + + allQualifiers = deQual allQualifiers + generalizeWithQualifiers monos tp = + deQual (generalizeWithQualifiers monos tp) + + improveQualifiers = deQual . improveQualifiers + improveQualifiersNormal = deQual improveQualifiersNormal + improveQualifiersFinal = deQual improveQualifiersFinal + simplifyQualifiers = deQual simplifyQualifiers + ambiguousQualifiers = deQual ambiguousQualifiers + + setClassEnvironment = deQual . setClassEnvironment + getClassEnvironment = deQual getClassEnvironment + +------------------------------------------------------------------------ +-- (IV) Additional functions + +proveQualifiers :: HasQual m info => info -> Predicates -> m () +proveQualifiers info = mapM_ (proveQualifier info) + +assumeQualifiers :: HasQual m info => info -> Predicates -> m () +assumeQualifiers info = mapM_ (assumeQualifier info) + +contextReduction :: (HasSubst m info, HasQual m info) => m () +contextReduction = + do makeSubstConsistent + changeQualifiers applySubst + improveQualifiersFix True + simplifyQualifiers + +ambiguities :: (HasSubst m info, HasQual m info) => m () +ambiguities = + do contextReduction + improveQualifiersFix False + ambiguousQualifiers + +improveQualifiersFix :: (HasSubst m info, HasQual m info) => Bool -> m () +improveQualifiersFix normal = + do improvements <- improveQualifiers normal + case improvements of + [] -> return () + _ -> do mapM_ (\(info, t1, t2) -> unifyTerms info t1 t2) improvements + makeSubstConsistent + improveQualifiersFix normal diff --git a/src/Top/Interface/Substitution.hs b/src/Top/Interface/Substitution.hs new file mode 100644 --- /dev/null +++ b/src/Top/Interface/Substitution.hs @@ -0,0 +1,71 @@ +{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses, + FunctionalDependencies, FlexibleInstances, FlexibleContexts #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Interface.Substitution where + +import Top.Types +import Top.Monad.Select +import Top.Monad.StateFix +import Top.Interface.Basic (ErrorLabel(..)) + +------------------------------------------------------------------------ +-- (I) Class name and (dedicated) deselect function + +data ClassSubst = ClassSubst + +deSubst :: (Embedded ClassSubst (s (StateFixT s m)) t, Monad m) => Select t (StateFixT s m) a -> StateFixT s m a +deSubst = deselectFor ClassSubst + +------------------------------------------------------------------------ +-- (II) Type class declaration + +class Monad m => HasSubst m info | m -> info where + + -- |Make the state consistent. Only relevant for substitution states that + -- can be inconsistent (for instance, the type graph substitution state). + makeSubstConsistent :: m () + + -- |Unify two terms. Supply additional information for this unification. + unifyTerms :: info -> Tp -> Tp -> m () + + -- |Lookup the value of a type variable in the substitution + findSubstForVar :: Int -> m Tp + + -- |Return a fixpoint substitution. + fixpointSubst :: m FixpointSubstitution + +------------------------------------------------------------------------ +-- (III) Instance for solver monad + +instance ( Monad m + , Embedded ClassSubst (s (StateFixT s m)) t + , HasSubst (Select t (StateFixT s m)) info + ) => + HasSubst (StateFixT s m) info where + + makeSubstConsistent = deSubst makeSubstConsistent + unifyTerms info t1 t2 = deSubst (unifyTerms info t1 t2) + findSubstForVar = deSubst . findSubstForVar + fixpointSubst = deSubst fixpointSubst + +------------------------------------------------------------------------ +-- (IV) Additional functions + +unificationErrorLabel :: ErrorLabel +unificationErrorLabel = ErrorLabel "unification" + +-- |Apply the substitution to a value that contains type variables (a +-- member of the Substitutable type class). +applySubst :: (Substitutable a, HasSubst m info) => a -> m a +applySubst a = + do let var = ftv a + tps <- mapM findSubstForVar var + let sub = listToSubstitution (zip var tps) + return (sub |-> a) diff --git a/src/Top/Interface/TypeInference.hs b/src/Top/Interface/TypeInference.hs new file mode 100644 --- /dev/null +++ b/src/Top/Interface/TypeInference.hs @@ -0,0 +1,271 @@ +{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses, + FunctionalDependencies, FlexibleInstances, FlexibleContexts #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Interface.TypeInference where + +import Top.Types +import Top.Monad.Select +import Top.Monad.StateFix +import Top.Interface.Basic +import Top.Interface.Substitution +import Top.Constraint.Information +import Data.Function +import Data.List (intersect, sortBy, partition, groupBy) +import qualified Data.Map as M + +------------------------------------------------------------------------ +-- (I) Class name and (dedicated) deselect function + +data ClassTI = ClassTI + +deTI :: (Embedded ClassTI (s (StateFixT s m)) t, Monad m) => Select t (StateFixT s m) a -> StateFixT s m a +deTI = deselectFor ClassTI + +------------------------------------------------------------------------ +-- (II) Type class declaration + +class Monad m => HasTI m info | m -> info where + + -- unique counter + getUnique :: m Int + setUnique :: Int -> m () + -- type synonyms + setTypeSynonyms :: OrderedTypeSynonyms -> m () + getTypeSynonyms :: m OrderedTypeSynonyms + -- skolem variables + getSkolems :: m [([Int], info, Tps)] + setSkolems :: [([Int], info, Tps)] -> m () + -- type scheme map + allTypeSchemes :: m (M.Map Int (Scheme Predicates)) + getTypeScheme :: Int -> m (Scheme Predicates) + storeTypeScheme :: Int -> Scheme Predicates -> m () + +------------------------------------------------------------------------ +-- (III) Instance for solver monad + +instance ( Monad m + , Embedded ClassTI (s (StateFixT s m)) t + , HasTI (Select t (StateFixT s m)) info + ) => + HasTI (StateFixT s m) info where + + getUnique = deTI getUnique + setUnique = deTI . setUnique + -- type synonym + setTypeSynonyms = deTI . setTypeSynonyms + getTypeSynonyms = deTI getTypeSynonyms + -- skolem variables + getSkolems = deTI getSkolems + setSkolems = deTI . setSkolems + -- type scheme map + allTypeSchemes = deTI allTypeSchemes + getTypeScheme = deTI . getTypeScheme + storeTypeScheme i = deTI . storeTypeScheme i + +------------------------------------------------------------------------ +-- (IV) Additional functions + +nextUnique :: HasTI m info => m Int +nextUnique = + do i <- getUnique + setUnique (i+1) + return i + +zipWithUniques :: HasTI m info => (Int -> a -> b) -> [a] -> m [b] +zipWithUniques f as = + do i <- getUnique + setUnique (i+length as) + return (zipWith f [i..] as) +{- +addToProve :: HasTI m info => Predicate -> info -> m () +addToProve p info = + do qm <- getQM + putQM (qm { globalQualifiers = (p, info) : globalQualifiers qm }) + +addToAssume :: HasTI m info => Predicate -> info -> m () +addToAssume p info = + do qm <- getQM + putQM (qm { globalAssumptions = (p, info) : globalAssumptions qm }) + +generalizeWithPreds :: HasTI m info => Tps -> Tp -> m (Scheme Predicates) +generalizeWithPreds monos tp = + do qm <- getQM + let as = ftv tp \\ ftv monos + ps = [ p | (p, _) <- globalQualifiers qm, any (`elem` as) (ftv p) ] + return (generalize monos (ps .=>. tp)) + +type NeverDirective info = (Predicate, info) +type CloseDirective info = (String, info) +type DisjointDirective info = ([String], info) +type DefaultDirective info = (String, (Tps, info)) + +data TypeClassDirectives info = TypeClassDirectives + { neverDirectives :: [NeverDirective info] + , closeDirectives :: [CloseDirective info] + , disjointDirectives :: [DisjointDirective info] + , defaultDirectives :: [DefaultDirective info] + } + +instance Show info => Show (TypeClassDirectives info) where + show tcd = + let f title pf xs + | null xs = "" + | otherwise = "\n "++title++": "++concat (intersperse "; " (map pf xs)) + p1 (x, _) = show x + p2 (x, _) = x + p3 (x, _) = concat (intersperse "," x) + p4 (cn, (tps, _)) = cn ++ " ("++concat (intersperse "," (map show tps)) ++ ")" + in f "never" p1 (neverDirectives tcd) ++ + f "close" p2 (closeDirectives tcd) ++ + f "disjoint" p3 (disjointDirectives tcd) ++ + f "default" p4 (defaultDirectives tcd) + +instance Empty (TypeClassDirectives info) where + empty = TypeClassDirectives { neverDirectives = [], closeDirectives = [], disjointDirectives = [], defaultDirectives = [] } + +addNeverDirective :: HasTI m info => NeverDirective info -> m () +addNeverDirective x = + changeTCD (\s -> s { neverDirectives = x : neverDirectives s }) + +addCloseDirective :: HasTI m info => CloseDirective info -> m () +addCloseDirective x = + changeTCD (\s -> s { closeDirectives = x : closeDirectives s }) + +addDisjointDirective :: HasTI m info => DisjointDirective info -> m () +addDisjointDirective x = + changeTCD (\s -> s { disjointDirectives = x : disjointDirectives s }) + +addDefaultDirective :: HasTI m info => DefaultDirective info -> m () +addDefaultDirective x = + changeTCD (\s -> s { defaultDirectives = x : defaultDirectives s }) -} + +-- * Instantiation and skolemization + +addSkolem :: HasTI m info => ([Int], info, Tps) -> m () +addSkolem x = + do xs <- getSkolems + setSkolems (x:xs) + +instantiateM :: (HasTI m info, Substitutable a) => Forall a -> m a +instantiateM fa = + do unique <- getUnique + let (newUnique, a) = instantiate unique fa + setUnique newUnique + return a + +skolemizeTruly :: (HasTI m info, Substitutable a) => Forall a -> m a +skolemizeTruly fa = + do unique <- getUnique + let (newUnique, a) = skolemize unique fa + setUnique newUnique + return a + +skolemizeFaked :: (HasTI m info, Substitutable a) => info -> Tps -> Forall a -> m a +skolemizeFaked info monos fa = + do unique <- getUnique + let (newUnique, a) = instantiate unique fa + new = ([ unique .. newUnique-1 ], info, monos) + addSkolem new + setUnique newUnique + return a + +getSkolemSubstitution :: HasTI m info => m MapSubstitution +getSkolemSubstitution = + do skcs <- getSkolems + return $ listToSubstitution [ (i, makeSkolemConstant i) | (is, _, _) <- skcs, i <- is ] + +-- |First, make the substitution consistent. Then check the skolem constants(?) +makeConsistent :: (HasTI m info, HasBasic m info, HasSubst m info) => m () +makeConsistent = makeSubstConsistent -- >> checkSkolems + +checkSkolems :: (HasTI m info, HasSubst m info, HasBasic m info, TypeConstraintInfo info) => m () +checkSkolems = + do xs <- getSkolems + list1 <- let f (is, info, monos) = + do tps <- mapM findSubstForVar is + return (zip is tps, (info, monos)) + in mapM f xs + + -- skolem constant versus type constant + let (list2, errs) = partition (all (isTVar . snd) . fst) list1 + mapM_ (addLabeledError skolemVersusConstantLabel . fst . snd) errs + + -- skolem constant versus a different skolem constant + let problems = filter ((>1) . length) + . groupBy ((==) `on` fst) + . sortBy (compare `on` fst) + $ [ (i, info) | (pairs, (info, _)) <- list2, (_, TVar i) <- pairs ] + list3 = let is = concatMap (map fst) problems + p (pairs, _) = null (ftv (map snd pairs) `intersect` is) + in filter p list2 + mapM_ (addLabeledError skolemVersusSkolemLabel . snd . head) problems + + -- escaping skolem constants + list4 <- let op rest this@(pairs, (info, monos)) = + do monos' <- applySubst monos + case ftv monos' `intersect` ftv (map snd pairs) of + [] -> return (this:rest) + esc -> do addLabeledError escapingSkolemLabel (escapedSkolems esc info) + return rest + in foldM op [] list3 + + -- store the remaining skolem constants (that are consistent with the current substitution). + let new = [ (concatMap (ftv . snd) pairs, info, monos) | (pairs, (info, monos)) <- list4 ] + setSkolems new + +skolemVersusConstantLabel :: ErrorLabel +skolemVersusConstantLabel = ErrorLabel "skolem versus constant" + +skolemVersusSkolemLabel :: ErrorLabel +skolemVersusSkolemLabel = ErrorLabel "skolem versus skolem" + +escapingSkolemLabel :: ErrorLabel +escapingSkolemLabel = ErrorLabel "escaping skolem" + +replaceSchemeVar :: HasTI m info => Sigma Predicates -> m (Scheme Predicates) +replaceSchemeVar (SigmaVar i) = getTypeScheme i +replaceSchemeVar (SigmaScheme s) = return s + +findScheme :: HasTI m info => Sigma Predicates -> m (Scheme Predicates) +findScheme = replaceSchemeVar + +--------------------------------------------------------------------- +-- Global qualifier map +{- +data GlobalQM q info = + GlobalQM + { globalQualifiers :: [(q, info)] + , globalGeneralizedQs :: [(q, info)] + , globalAssumptions :: [(q, info)] + } + +instance (Show qs, Show info) => Show (GlobalQM qs info) where + show qm = + let f (s, sf) + | null ps = [] + | otherwise = [" " ++ s ++ ": " ++ foldr1 (\x y -> x++", "++y) (map g ps)] + where ps = sf qm + g (p, info) = show p ++ "{" ++ show info ++ "}" + in unlines $ concatMap f + [ ("qualifiers" , globalQualifiers) + , ("generalized qualifiers", globalGeneralizedQs) + , ("assumptions" , globalAssumptions) + ] + +instance Empty (GlobalQM qs info) where + empty = GlobalQM { globalQualifiers = [], globalGeneralizedQs = [], globalAssumptions = [] } + +instance Substitutable qs => Substitutable (GlobalQM qs info) where + sub |-> (GlobalQM as bs cs) = + let as' = [ (sub |-> a, info) | (a, info) <- as ] + bs' = [ (sub |-> b, info) | (b, info) <- bs ] + cs' = [ (sub |-> c, info) | (c, info) <- cs ] + in GlobalQM as' bs' cs' + ftv (GlobalQM as bs cs) = ftv (map fst $ as ++ bs ++ cs) -} diff --git a/src/Top/Monad/Select.hs b/src/Top/Monad/Select.hs new file mode 100644 --- /dev/null +++ b/src/Top/Monad/Select.hs @@ -0,0 +1,86 @@ +{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses, KindSignatures, + FunctionalDependencies, FlexibleInstances #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Monad.Select + ( module Top.Monad.Select + , module Control.Monad.State + ) where + +import Top.Util.Embedding +import Control.Monad.State + +-------------------------------------------------------- +-- Select Monad + +newtype Select t m a = Select (m a) + +instance Monad m => Monad (Select t m) where + return a = Select (return a) + Select f >>= g = Select (do x <- f + let Select h = g x + h) + +instance (MonadState s m, Embedded label s t) => MonadState t (Select t m) where + get = Select (gets (getE embedding )) + put i = Select (modify (setE embedding i)) + +instance MonadTrans (Select t) where + lift = select + +select :: m a -> Select t m a +select = Select + +-------------------------------------------------------- +-- SelectFix Monad + +data SelectFix (t :: (* -> *) -> *) (m :: * -> *) a = SelectFix (m a) + +instance Monad m => Monad (SelectFix t m) where + return a = SelectFix (return a) + SelectFix f >>= g = SelectFix (do x <- f + let SelectFix h = g x + h) + +instance (MonadState s m, Embedded label s (t m)) => MonadState (t m) (SelectFix t m) where + get = SelectFix (gets (getE embedding )) + put i = SelectFix (modify (setE embedding i)) + +instance MonadTrans (SelectFix t) where + lift = selectFix + +selectFix :: m a -> SelectFix t m a +selectFix = SelectFix + +-------------------------------------------------------- +-- Class Embedded + +class Embedded label s t | label s -> t, t -> label where + embedding :: Embedding s t + +instance Embedded c s2 t => Embedded c (s1, s2) t where + embedding = composeE sndE embedding + +-------------------------------------------------------- +-- deselect functions for Select Monad + +deselect :: Select t m a -> m a +deselect (Select m) = m + +deselectFor :: (Embedded label s t, MonadState s m) => label -> Select t m a -> m a +deselectFor _ = deselect + +-------------------------------------------------------- +-- deselect functions for SelectFix Monad + +deselectFix :: SelectFix t m a -> m a +deselectFix (SelectFix m) = m + +deselectFixFor :: (Embedded label s (t m), MonadState s m) => label -> SelectFix t m a -> m a +deselectFixFor _ = deselectFix diff --git a/src/Top/Monad/StateFix.hs b/src/Top/Monad/StateFix.hs new file mode 100644 --- /dev/null +++ b/src/Top/Monad/StateFix.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Monad.StateFix + ( module Top.Monad.StateFix + , module Control.Monad.State + ) where + +import Control.Monad.State +import Control.Monad.Identity +import Control.Monad.Writer + +type StateFix s = StateFixT s Identity + +data StateFixT s m a = Fix { unFix :: StateT (s (StateFixT s m)) m a } + +instance Monad m => Monad (StateFixT s m) where + return = Fix . return + m >>= f = Fix (unFix m >>= unFix . f) + +instance Monad m => MonadState (s (StateFixT s m)) (StateFixT s m) where + get = Fix get + put = Fix . put + +instance MonadTrans (StateFixT s) where + lift = Fix . lift + +instance MonadWriter w m => MonadWriter w (StateFixT s m) where + tell = lift . tell + listen = Fix . listen . unFix + pass = Fix . pass . unFix + +-- + +runStateFixT :: StateFixT s m a -> s (StateFixT s m) -> m (a, s (StateFixT s m)) +runStateFixT = runStateT . unFix + +evalStateFixT :: Monad m => StateFixT s m a -> s (StateFixT s m) -> m a +evalStateFixT = evalStateT . unFix + +execStateFixT :: Monad m => StateFixT s m a -> s (StateFixT s m) -> m (s (StateFixT s m)) +execStateFixT = execStateT . unFix + +-- + +runStateFix :: StateFix s a -> s (StateFix s) -> (a, s (StateFix s)) +runStateFix m = runIdentity . runStateFixT m + +evalStateFix :: StateFix s a -> s (StateFix s) -> a +evalStateFix m = runIdentity . evalStateFixT m + +execStateFix :: StateFix s a -> s (StateFix s) -> s (StateFix s) +execStateFix m = runIdentity . execStateFixT m diff --git a/src/Top/Ordering/Tree.hs b/src/Top/Ordering/Tree.hs new file mode 100644 --- /dev/null +++ b/src/Top/Ordering/Tree.hs @@ -0,0 +1,222 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +----------------------------------------------------------------------------- + +module Top.Ordering.Tree where + +import Top.Ordering.TreeWalk +import Data.List (partition, intersperse) +import qualified Data.Map as M +import qualified Data.Set as S + +type Trees a = [Tree a] +data Tree a = Node (Trees a) + | AddList Direction [a] (Tree a) + | StrictOrder (Tree a) (Tree a) + | Spread Direction [a] (Tree a) + | Receive Int + | Phase Int [a] + | Chunk Int (Tree a) + deriving Show + +emptyTree :: Tree a +unitTree :: a -> Tree a +listTree :: [a] -> Tree a +binTree :: Tree a -> Tree a -> Tree a + +emptyTree = Node [] +unitTree c = listTree [c] +listTree cs = cs .>. emptyTree +binTree a b = Node [a, b] + +infixr 8 .>. , .>>. , .<. , .<<. + +(.>.), (.>>.), (.<.), (.<<.) :: [a] -> Tree a -> Tree a +(.>.) = makeTreeHelper AddList Down +(.>>.) = makeTreeHelper Spread Down +(.<.) = makeTreeHelper AddList Up +(.<<.) = makeTreeHelper Spread Up + +-- prevents adding an empty list +makeTreeHelper constructor direction xs tree + | null xs = tree + | otherwise = constructor direction xs tree + +------------------------------------------------------------------------ + +data Direction = Up | Down deriving (Eq, Show) +type Spreaded a = M.Map Int [a] +type Phased a = M.Map Int (List a) + +flattenTree :: TreeWalk -> Tree a -> [a] +flattenTree (TreeWalk treewalk) theTree = + strictRec theTree [] + + where + rec :: List a -> -- downward constraints + Tree a -> -- the tree to flatten + ( List a -- the result + , List a -- upward constraints + ) + rec down tree = + case tree of + + Node trees -> + let tuples = map (rec id) trees + in (treewalk down tuples, id) + + Chunk _ t -> + rec down t + + AddList Up as t -> + let (result, up) = rec down t + in (result, (as++) . up) + + AddList Down as t -> + rec ((as++) . down) t + + StrictOrder left right -> + let left_result = strictRec left + right_result = strictRec right + in (treewalk down [(left_result . right_result, id)], id) + + Spread direction as t -> + rec down (AddList direction as t) + + Receive _ -> + rec down emptyTree + + Phase _ as -> + rec down (listTree as) + + strictRec :: Tree a -> -- the tree to flatten + List a -- the result + strictRec tree = + let (result, up) = rec id tree + in treewalk id [(result, up)] + +spreadTree :: (a -> Maybe Int) -> Tree a -> Tree a +spreadTree spreadFunction = fst . rec M.empty + where + rec fm tree = + case tree of + + Node trees -> + let (trees', sets) = unzip (map (rec fm) trees) + in (Node trees', S.unions sets) + + Chunk cnr t -> + let (tree', set) = rec fm t + in (Chunk cnr tree', set) + + AddList direction as t -> + let (tree', set) = rec fm t + in (AddList direction as tree', set) + + StrictOrder left right -> + let (left' , set1) = rec fm left + (right', set2) = rec fm right + in (StrictOrder left' right', set1 `S.union` set2) + + Spread direction as t -> + let (tree', set) = rec fmNew t + fmNew = M.unionWith (++) fm (M.fromList [ (i, [x]) | x <- doSpread, let Just i = spreadFunction x ]) + (doSpread, noSpread) = + partition (maybe False (`S.member` set) . spreadFunction) as + in (Spread direction noSpread tree', set) + + Receive i -> + let t = maybe emptyTree listTree (M.lookup i fm) + in (t, S.singleton i) + + Phase _ _ -> + (tree, S.empty) + +phaseTree :: a -> Tree a -> Tree a +phaseTree a = strictRec + + where + rec tree = + case tree of + + Node trees -> + let (trees', phasesList) = unzip (map rec trees) + phases = foldr (M.unionWith (.)) M.empty phasesList + in (Node trees', phases) + + Chunk cnr t -> + let (tree', phases) = rec t + in (Chunk cnr tree', phases) + + AddList dir as t -> + let (tree', phases) = rec t + in (AddList dir as tree', phases) + + StrictOrder left right -> + let left' = strictRec left + right' = strictRec right + in (StrictOrder left' right', M.empty) + + Spread dir as t -> + let (tree', phases) = rec t + in (Spread dir as tree', phases) + + Receive _ -> + (tree, M.empty) + + Phase i as -> + (emptyTree, M.singleton i (as++)) + + strictRec tree = + let (tree', phases) = rec tree + f list = listTree (list []) + in foldr1 StrictOrder (intersperse (unitTree a) (M.elems (M.insertWith binTree 5 tree' (M.map f phases)))) + +chunkTree :: Tree a -> [(Int, Tree a)] +chunkTree theTree = + let (ts, chunks) = rec theTree + in (-1, ts) : chunks + + where + rec tree = + case tree of + + Node trees -> + let (ts, chunks) = unzip (map rec trees) + in (Node ts, concat chunks) + + -- This chunk should be solved later then the inner chunks. + -- Therefore, the new chunk is appended + Chunk cnr t -> + let (ts, chunks) = rec t + in (emptyTree, chunks ++ [(cnr, ts)]) + + AddList direction as t -> + let (ts, chunks) = rec t + in (AddList direction as ts, chunks) + + StrictOrder left right -> + let (ts1, chunks1) = rec left + (ts2, chunks2) = rec right + in (StrictOrder ts1 ts2, chunks1 ++ chunks2) + + Spread direction as t -> + let (ts, chunks) = rec t + in (Spread direction as ts, chunks) + + _ -> (tree, []) + +instance Functor Tree where + fmap f tree = + case tree of + Node ts -> Node (map (fmap f) ts) + AddList d as t -> AddList d (map f as) (fmap f t) + StrictOrder t1 t2 -> StrictOrder (fmap f t1) (fmap f t2) + Spread d as t -> Spread d (map f as) (fmap f t) + Receive i -> Receive i + Phase i as -> Phase i (map f as) + Chunk i t -> Chunk i (fmap f t) diff --git a/src/Top/Ordering/TreeWalk.hs b/src/Top/Ordering/TreeWalk.hs new file mode 100644 --- /dev/null +++ b/src/Top/Ordering/TreeWalk.hs @@ -0,0 +1,46 @@ +{-# LANGUAGE RankNTypes #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Ordering.TreeWalk where + +newtype TreeWalk = TreeWalk (forall a . List a -> [(List a, List a)] -> List a) + +topDownTreeWalk :: TreeWalk +topDownTreeWalk = TreeWalk (\top cs -> top . children (unzip cs)) + where children (fs,gs) = concatList gs . concatList fs + +bottomUpTreeWalk :: TreeWalk +bottomUpTreeWalk = TreeWalk (\top cs -> children (unzip cs) . top) + where children (fs,gs) = concatList fs . concatList gs + +inorderTopFirstPreTreeWalk :: TreeWalk +inorderTopFirstPreTreeWalk = TreeWalk (\top cs -> top . children cs) + where children = concatList . map (\(f,g) -> g . f) + +inorderTopLastPreTreeWalk :: TreeWalk +inorderTopLastPreTreeWalk = TreeWalk (\top cs -> children cs . top) + where children = concatList . map (\(f,g) -> g . f) + +inorderTopFirstPostTreeWalk :: TreeWalk +inorderTopFirstPostTreeWalk = TreeWalk (\top cs -> top . children cs) + where children = concatList . map (uncurry (.)) + +inorderTopLastPostTreeWalk :: TreeWalk +inorderTopLastPostTreeWalk = TreeWalk (\top cs -> children cs . top) + where children = concatList . map (uncurry (.)) + +reverseTreeWalk :: TreeWalk -> TreeWalk +reverseTreeWalk (TreeWalk f) = TreeWalk (\top cs -> f top (reverse cs)) + +------------------------------------------------------------------- + +type List a = [a] -> [a] + +concatList :: [List a] -> List a +concatList = foldr (.) id diff --git a/src/Top/Solver.hs b/src/Top/Solver.hs new file mode 100644 --- /dev/null +++ b/src/Top/Solver.hs @@ -0,0 +1,198 @@ +{-# LANGUAGE FlexibleContexts #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Solver + ( module Top.Solver + , module Control.Monad.Writer + ) where + +import Top.Types +import Top.Interface.Basic +import Top.Interface.TypeInference +import Top.Interface.Substitution +import Top.Interface.Qualification +import Top.Implementation.General +import Top.Util.Option +import Top.Monad.StateFix +import Top.Constraint +import qualified Data.Map as M +import Top.Constraint.Information +import Control.Monad.Writer + +data ConstraintSolver constraint info = ConstraintSolver (SolveOptions -> [constraint] -> (SolveResult info, LogEntries)) + +makeConstraintSolver :: (Empty (f () (BasicMonad f))) => + (SolveOptions -> [constraint] -> BasicMonad f (SolveResult info)) + -> ConstraintSolver constraint info +makeConstraintSolver f = ConstraintSolver (\options -> evalBasicMonad . f options) + +solve :: SolveOptions -> [constraint] -> ConstraintSolver constraint info -> (SolveResult info, LogEntries) +solve options constraints (ConstraintSolver f) = f options constraints + +--- + +onlySolveConstraints :: + ( HasTI m info + , HasBasic m info + , HasSubst m info + , HasQual m info + , TypeConstraintInfo info + , Solvable constraint m + , MonadState s m + , SolveState s + , MonadWriter LogEntries m + ) => + [constraint] -> m () + +onlySolveConstraints cs = + do pushConstraints (liftConstraints cs) + logState + startSolving + makeConsistent + checkSkolems + ambiguities + logState + +solveConstraints :: + ( HasTI m info + , HasBasic m info + , HasSubst m info + , HasQual m info + , TypeConstraintInfo info + , Solvable constraint m + , MonadState s m + , SolveState s + , MonadWriter LogEntries m + ) => + SolveOptions -> + [constraint] -> + m (SolveResult info) + +solveConstraints options cs = + do initialize cs options + onlySolveConstraints cs + solveResult + +solveResult :: + ( HasBasic m info + , HasTI m info + , HasSubst m info + , HasQual m info + , TypeConstraintInfo info + ) => + m (SolveResult info) +solveResult = + do uniqueAtEnd <- getUnique + errs <- getLabeledErrors + qs <- allQualifiers + sub <- fixpointSubst + ts <- allTypeSchemes + return (SolveResult uniqueAtEnd sub ts qs errs) + +---------------------------------------------------------------------- +-- Solve type constraints + +data SolveResult info = + SolveResult { uniqueFromResult :: Int + , substitutionFromResult :: FixpointSubstitution + , typeschemesFromResult :: M.Map Int (Scheme Predicates) + , qualifiersFromResult :: Predicates + , errorsFromResult :: [(info, ErrorLabel)] + } + +instance Empty (SolveResult info) where + empty = emptyResult 0 + +emptyResult :: Int -> SolveResult info +emptyResult unique = SolveResult unique emptyFPS M.empty empty [] + +combineResults :: SolveResult info -> SolveResult info -> SolveResult info +combineResults (SolveResult _ s1 ts1 qs1 er1) (SolveResult unique s2 ts2 qs2 er2) = + SolveResult unique (disjointFPS s1 s2) (ts1 `M.union` ts2) (qs1 ++ qs2) (er1++er2) + +-------------------------------------------------------------------------------- + +data SolveOptions = SolveOptions_ + { + -- initial values + uniqueCounter :: Int + , typeSynonyms :: OrderedTypeSynonyms + , classEnvironment :: ClassEnvironment + + -- optional settings + , setStopAfterFirstError :: Bool -- see Basic + , setCheckConditions :: Bool -- see Basic + } + +solveOptions :: SolveOptions +solveOptions = SolveOptions_ + { uniqueCounter = -1 + , typeSynonyms = noOrderedTypeSynonyms + , classEnvironment = standardClasses + , setStopAfterFirstError = currentValue stopOption + , setCheckConditions = currentValue checkOption + } + +initialize :: (HasBasic m info, HasQual m info, HasTI m info, Substitutable a) => a -> SolveOptions -> m () +initialize cs options = + do setUnique unique + setTypeSynonyms (typeSynonyms options) + setClassEnvironment (classEnvironment options) + setOption stopAfterFirstError (setStopAfterFirstError options) + setOption checkConditions (setCheckConditions options) + where + unique + | uniqueCounter options < 0 = 1 + maximum (-1 : ftv cs) + | otherwise = uniqueCounter options + +---------------------- +-- Basic Monad + +type BasicMonad f = StateFixT (f ()) (Writer LogEntries) + +newtype LogEntries = LogEntries ([LogEntry] -> [LogEntry]) +data LogEntry = LogEntry { priority :: Int, msg :: String } + +noLogEntries :: LogEntries +noLogEntries = LogEntries id + +singleEntry :: Int -> String -> LogEntries +singleEntry i s = LogEntries (LogEntry i s:) + +evalBasicMonad :: Empty (f () (BasicMonad f)) => BasicMonad f a -> (a, LogEntries) +evalBasicMonad = runWriter . flip evalStateFixT empty + +instance Monoid LogEntries where + mempty = LogEntries id + mappend (LogEntries f) (LogEntries g) = LogEntries (f . g) + +instance Show LogEntry where + show = msg + +instance Show LogEntries where + show (LogEntries f) = unlines (map show (f [])) + +logMsg :: MonadWriter LogEntries m => String -> m () +logMsg = logMsgPrio 5 + +logMsgPrio :: MonadWriter LogEntries m => Int -> String -> m () +logMsgPrio i s = + let entry = LogEntry { priority = i, msg = s } + in tell (LogEntries (entry:)) + +-- |Print the current state and add this as a debug message. +logState :: (MonadState s m, SolveState s, MonadWriter LogEntries m) => m () +logState = + do xs <- allStates + ys <- allOptions + let hline = replicate 80 '-' + options = "Solver options:\n" ++ indent (unlines ys) + f i (name,s) = show i ++ ". " ++ name ++ "\n" ++ indent s + indent = unlines . map (" "++) . lines + logMsg (unlines $ hline : options : zipWith f [1::Int ..] xs ++ [hline]) diff --git a/src/Top/Solver/Greedy.hs b/src/Top/Solver/Greedy.hs new file mode 100644 --- /dev/null +++ b/src/Top/Solver/Greedy.hs @@ -0,0 +1,70 @@ +{-# LANGUAGE OverlappingInstances, FlexibleContexts, FlexibleInstances #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Solver.Greedy where + +import Top.Implementation.General +import Top.Implementation.Basic +import Top.Implementation.TypeInference +import Top.Implementation.FastSubstitution +import Top.Implementation.SimpleSubstitution +import Top.Implementation.Overloading +import Top.Solver +import Top.Constraint +import Top.Constraint.Information +-- for testing only +-- import Top.Types +-- import Top.Constraint.Equality + +type Greedy info = BasicMonad (GreedyS info) +type GreedyS info = And ( Fix (BasicState info) ) + ( And ( Simple (TIState info) ) + ( And ( Simple (GreedyState info) ) + ( Simple (OverloadingState info) ) + ) + ) + +solveGreedy :: (Solvable constraint (Greedy info), TypeConstraintInfo info) => + SolveOptions -> [constraint] -> Greedy info (SolveResult info) +solveGreedy = solveConstraints + +greedyConstraintSolver :: (TypeConstraintInfo info, Solvable constraint (Greedy info)) => ConstraintSolver constraint info +greedyConstraintSolver = makeConstraintSolver solveGreedy + +-------------------------------- + +type GreedySimple info = BasicMonad (GreedySimpleS info) +type GreedySimpleS info = And ( Fix (BasicState info) ) + ( And ( Simple (TIState info) ) + ( And ( Simple (SimpleState info) ) + ( Simple (OverloadingState info) ) + ) + ) + +solveSimple :: (Solvable constraint (GreedySimple info), TypeConstraintInfo info) => + SolveOptions -> [constraint] -> GreedySimple info (SolveResult info) +solveSimple = solveConstraints + +greedySimpleConstraintSolver :: (TypeConstraintInfo info, Solvable constraint (GreedySimple info)) => ConstraintSolver constraint info +greedySimpleConstraintSolver = makeConstraintSolver solveSimple + +-------------------------------- +{- +cs :: [EqualityConstraint String] +cs = [ TVar 0 .==. (TVar 1 .->. TVar 1) $ "a" + , TVar 0 .==. (TVar 2 .->. TVar 3) $ "b" + , TVar 2 .==. intType $ "c" + , TVar 3 .==. boolType $ "d" + ] + +test = let (a, b) = solve (solveOptions {uniqueCounter = 4}) cs greedyConstraintSolver + in (b, errorsFromResult a) + +test2 = let (a, b) = solve (solveOptions {uniqueCounter = 4}) cs greedySimpleConstraintSolver + in (b, errorsFromResult a) -} diff --git a/src/Top/Solver/PartitionCombinator.hs b/src/Top/Solver/PartitionCombinator.hs new file mode 100644 --- /dev/null +++ b/src/Top/Solver/PartitionCombinator.hs @@ -0,0 +1,41 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +----------------------------------------------------------------------------- + +module Top.Solver.PartitionCombinator where + +import Top.Types +import Top.Solver +import Top.Ordering.Tree +import qualified Data.Map as M + +type Chunks constraint = [Chunk constraint] +type Chunk constraint = (ChunkID, Tree constraint) +type ChunkID = Int + +solveChunkConstraints :: + (M.Map Int (Scheme Predicates) -> constraint -> constraint) -> -- function to update the type scheme variables + ConstraintSolver constraint info -> -- constraint solver to solve the constraints in a chunk + (Tree constraint -> [constraint]) -> -- function to flatten the constraint tree + Chunks constraint -> ConstraintSolver constraint info + +solveChunkConstraints update (ConstraintSolver f) flattening chunks = + ConstraintSolver (\os _ -> + let rec options [] = (emptyResult (uniqueCounter options), noLogEntries) + rec options ((_, tree) : rest) = + let constraintList = flattening tree + (result, entries) + | null constraintList = + (emptyResult (uniqueCounter options), noLogEntries) + | otherwise = + f options constraintList + newOption = options { uniqueCounter = uniqueFromResult result } + schemeMap = typeschemesFromResult result + newRest = [ (chunkID, fmap (update schemeMap) t) | (chunkID, t) <- rest ] + (resultRec, entriesRec) = rec newOption newRest + in (result `combineResults` resultRec, entries `mappend` entriesRec) + in rec os chunks) diff --git a/src/Top/Solver/SwitchCombinator.hs b/src/Top/Solver/SwitchCombinator.hs new file mode 100644 --- /dev/null +++ b/src/Top/Solver/SwitchCombinator.hs @@ -0,0 +1,29 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +----------------------------------------------------------------------------- + +module Top.Solver.SwitchCombinator where + +import Top.Interface.Basic +import Top.Solver + +-- |The first solver is used to solve the constraint set. If this fails (at least one +-- error is returned), then the second solver takes over. +(|>>|) :: ConstraintSolver constraint info -> ConstraintSolver constraint info -> ConstraintSolver constraint info +ConstraintSolver f |>>| ConstraintSolver g = ConstraintSolver $ \options constraints -> + let (result1, logs1) = f options constraints + (result2, logs2) = g options constraints + p (_, ErrorLabel s) = s /= "ambiguous predicate" -- temporary* + p _ = True + switchLog = singleEntry 5 "CombinationSolver: Switching to second solver" + in if not (any p (errorsFromResult result1)) + then (result1, logs1) + else (result2, logs1 `mappend` switchLog `mappend` logs2) + +-- * For now, ignore the ambiguous predicate messages that are returned. They are not shown anyway. +-- These error messages are returned because of the mismatch between the constraints that are generated +-- by the Helium compiler, and the constraints as they are in the Top constraint solver. diff --git a/src/Top/Solver/TypeGraph.hs b/src/Top/Solver/TypeGraph.hs new file mode 100644 --- /dev/null +++ b/src/Top/Solver/TypeGraph.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE OverlappingInstances, UndecidableInstances, FlexibleContexts #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Solver.TypeGraph where + +import Top.Solver +import Top.Constraint +import Top.Constraint.Information +import Top.Implementation.General +import Top.Implementation.Basic +import Top.Implementation.Overloading +import Top.Implementation.TypeInference +import Top.Implementation.TypeGraphSubstitution +import Top.Implementation.TypeGraph.Heuristic +import Top.Monad.Select + +type TG info = BasicMonad (TGS info) +type TGS info = And ( Fix (BasicState info) ) + ( And ( Simple (TIState info) ) + ( And ( Simple (TypeGraphState info) ) + ( Simple (OverloadingState info) ) + ) + ) + +solveTypeGraph :: (Solvable constraint (TG info), TypeConstraintInfo info) + => TG info () -> SolveOptions -> [constraint] -> TG info (SolveResult info) +solveTypeGraph m options cs = + do initialize cs options >> m + onlySolveConstraints cs + solveResult + +typegraphConstraintSolver :: (TypeConstraintInfo info, Solvable constraint (TG info)) + => PathHeuristics info -> ConstraintSolver constraint info +typegraphConstraintSolver hs = + let setHeuristics = deselect (modify (\tgs -> tgs { heuristics = hs })) + in makeConstraintSolver (solveTypeGraph setHeuristics) + +typegraphConstraintSolverDefault :: (TypeConstraintInfo info, Solvable constraint (TG info)) + => ConstraintSolver constraint info +typegraphConstraintSolverDefault = + makeConstraintSolver (solveTypeGraph (return ())) + +--- +{- +cs = [ TVar 0 .==. (TVar 1 .->. TVar 1) $ "a" + , TVar 0 .==. (TVar 2 .->. TVar 3) $ "b" + , TVar 2 .==. intType $ "c" + , TVar 3 .==. boolType $ "d" + ] + +test = let (a, b) = solve (solveOptions {uniqueCounter = 4}) cs typegraphConstraintSolverDefault + in (b, errorsFromResult a) -} diff --git a/src/Top/Types.hs b/src/Top/Types.hs new file mode 100644 --- /dev/null +++ b/src/Top/Types.hs @@ -0,0 +1,22 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +-- +-- A collection of type utilities. +-- +----------------------------------------------------------------------------- + +module Top.Types (module Export) where + +import Top.Types.Primitive as Export +import Top.Types.Substitution as Export +import Top.Types.Quantification as Export +import Top.Types.Qualification as Export +import Top.Types.Synonym as Export +import Top.Types.Unification as Export +import Top.Types.Classes as Export +import Top.Types.Schemes as Export +import Top.Types.Kinds as Export diff --git a/src/Top/Types/Classes.hs b/src/Top/Types/Classes.hs new file mode 100644 --- /dev/null +++ b/src/Top/Types/Classes.hs @@ -0,0 +1,204 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +-- +-- Type classes and the standard reduction instances. A part of the code +-- was taken from the paper "Typing Haskell in Haskell". +-- +----------------------------------------------------------------------------- + +module Top.Types.Classes where + +import Top.Types.Primitive +import Top.Types.Substitution +import Top.Types.Unification +import Top.Types.Synonym +import Top.Types.Qualification +import Control.Monad +import qualified Data.Map as M + +---------------------------------------------------------------------- +-- * Class predicates + +type Predicates = [Predicate] +data Predicate = Predicate String Tp deriving Eq + +instance Show Predicate where + show (Predicate s tp) = if priorityOfType tp == 2 + then s ++ " " ++ show tp + else s ++ " (" ++ show tp ++ ")" + +instance Substitutable Predicate where + sub |-> (Predicate s tp) = Predicate s (sub |-> tp) + ftv (Predicate _ tp) = ftv tp + +instance HasTypes Predicate where + getTypes (Predicate _ tp) = [tp] + changeTypes f (Predicate s tp) = Predicate s (f tp) + +instance ShowQualifiers Predicate + +---------------------------------------------------------------------- +-- * Class environments and instances + +type ClassEnvironment = M.Map String Class +type Class = ([String], Instances) +type Instances = [Instance] +type Instance = (Predicate, Predicates) + +-- |The empty class environment +emptyClassEnvironment :: ClassEnvironment +emptyClassEnvironment = M.empty + +matchPredicates :: OrderedTypeSynonyms -> Predicate -> Predicate -> Maybe MapSubstitution +matchPredicates synonyms (Predicate s1 t1) (Predicate s2 t2) + | s1 == s2 = case mguWithTypeSynonyms synonyms (freezeVariablesInType t1) t2 of + Left _ -> Nothing + Right (_, s) -> Just (M.map unfreezeVariablesInType s) + | otherwise = Nothing + +insertInstance :: String -> Instance -> ClassEnvironment -> ClassEnvironment +insertInstance className inst env = + case M.lookup className env of + Nothing -> M.insert className ([], [inst]) env + Just (parents, insts) -> M.insert className (parents, inst:insts) env + +---------------------------------------------------------------------- +-- * Class environment + +inClassEnvironment :: String -> ClassEnvironment -> Bool +inClassEnvironment = M.member + +superclassPaths :: String -> String -> ClassEnvironment -> [[String]] +superclassPaths from to cs + | from == to = [[to]] + | otherwise = [ from : path | sc <- superclasses from cs, path <- superclassPaths sc to cs ] + +-- |For example, Eq is a superclass of Ord +superclasses :: String -> ClassEnvironment -> [String] +superclasses s cs = maybe [] fst (M.lookup s cs) + +instances :: String -> ClassEnvironment -> Instances +instances s cs = maybe [] snd (M.lookup s cs) + +---------------------------------------------------------------------- +-- * Head normal form + +inHeadNormalForm :: Predicate -> Bool +inHeadNormalForm (Predicate _ tp) = hnf tp + where hnf (TVar _) = True + hnf (TCon _) = False + hnf (TApp t _) = hnf t + +listToHeadNormalForm :: OrderedTypeSynonyms -> ClassEnvironment -> Predicates -> Maybe Predicates +listToHeadNormalForm synonyms classes ps = + do pss <- mapM (toHeadNormalForm synonyms classes) ps + return (concat pss) + +toHeadNormalForm :: OrderedTypeSynonyms -> ClassEnvironment -> Predicate -> Maybe Predicates +toHeadNormalForm synonyms classes p + | inHeadNormalForm p = Just [p] + | otherwise = do ps <- byInstance synonyms classes p + listToHeadNormalForm synonyms classes ps + +---------------------------------------------------------------------- +-- * Entailment + +bySuperclass :: ClassEnvironment -> Predicate -> Predicates +bySuperclass classes p@(Predicate s tp) = + p : concat [ bySuperclass classes (Predicate s' tp) | s' <- superclasses s classes ] + +byInstance :: OrderedTypeSynonyms -> ClassEnvironment -> Predicate -> Maybe Predicates +byInstance synonyms classes p@(Predicate s _) = + let tryInstance (p',list) = do sub <- matchPredicates synonyms p p' + Just (sub |-> list) + in msum [ tryInstance it | it <- instances s classes ] + +entail :: OrderedTypeSynonyms -> ClassEnvironment -> Predicates -> Predicate -> Bool +entail synonyms classes ps p = + scEntail classes ps p || + case byInstance synonyms classes p of + Nothing -> False + Just qs -> all (entail synonyms classes ps) qs + +entailList :: OrderedTypeSynonyms -> ClassEnvironment -> Predicates -> Predicates -> Bool +entailList synonyms classes ps = all (entail synonyms classes ps) + +scEntail :: ClassEnvironment -> Predicates -> Predicate -> Bool +scEntail classes ps p = any (p `elem`) (map (bySuperclass classes) ps) + +---------------------------------------------------------------------- +-- * Context reduction + +newtype ReductionError a = ReductionError a + deriving Show + +contextReduction :: OrderedTypeSynonyms -> ClassEnvironment -> Predicates -> + (Predicates, [ReductionError Predicate]) +contextReduction synonyms classes ps = + let op p (a,b) = case toHeadNormalForm synonyms classes p of + Just qs -> (qs++a,b) + Nothing -> (a,ReductionError p : b) + (predicates, errors) = foldr op ([], []) ps + + loop rs [] = rs + loop rs (x:xs) | scEntail classes (rs++xs) x = loop rs xs + | otherwise = loop (x:rs) xs + + in (loop [] predicates, errors) + +associatedContextReduction :: OrderedTypeSynonyms -> ClassEnvironment -> [(Predicate, a)] -> + ([(Predicate,a)], [ReductionError (Predicate, a)]) +associatedContextReduction synonyms classes ps = + let op (predicate, a) (reduced, es) = + case toHeadNormalForm synonyms classes predicate of + Just qs -> ([(p,a) | p <- qs]++reduced,es) + Nothing -> (reduced,ReductionError (predicate, a) : es) + (predicates, errors) = foldr op ([], []) ps + + loop rs [] = rs + loop rs (q:qs) | entailed = loop rs qs + | otherwise = loop (q:rs) qs + where entailed = scEntail classes (map fst (rs++qs)) (fst q) + + in (loop [] predicates, errors) + +---------------------------------------------------------------------- +-- * Standard class environment + +-- This environment is only used at three places: +-- o MiscErrors.ag +-- o Warnings.ag +-- o Collect.ag (initialization in import environment) +standardClasses :: ClassEnvironment +standardClasses = M.fromList $ + + -- only two instances for Num: Int and Float + ( "Num", + ( ["Eq","Show"] -- superclasses + , [ (Predicate "Num" intType , []) -- instances + , (Predicate "Num" floatType, []) + ] + ) + ) : + ( "Enum", ([], [ (Predicate "Enum" tp, []) | tp <- [voidType, charType, intType, floatType, boolType]]) + ) : + -- Eq, Ord and Show all have the same instances + [ ("Eq" , ([] , makeInstances "Eq" )) + , ("Ord", (["Eq"], makeInstances "Ord" )) + , ("Show", ([], makeInstances "Show")) + ] + + where + makeInstances className = + let basicTypes = [intType, floatType, boolType, charType] + makeTupleInstance i = + ( Predicate className (tupleType [ TVar n | n <- [1..i] ]) + , [ Predicate className (TVar n) | n <- [1..i] ] + ) + in (Predicate className (listType (TVar 0)), [Predicate className (TVar 0)]) -- instance for Lists + : [ (Predicate className tp, []) | tp <- basicTypes ] + ++ map makeTupleInstance (0 : [2..10]) diff --git a/src/Top/Types/Kinds.hs b/src/Top/Types/Kinds.hs new file mode 100644 --- /dev/null +++ b/src/Top/Types/Kinds.hs @@ -0,0 +1,46 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +-- +-- Kinds can be represented by a type. +-- +----------------------------------------------------------------------------- + +module Top.Types.Kinds where + +import Top.Types.Primitive +import Top.Types.Substitution +import Top.Types.Quantification +import Top.Types.Schemes + +type Kind = Tp +type Kinds = [Kind] +type KindScheme = TpScheme + +-- |Star is the kind of all values. +star :: Kind +star = TCon "*" + +-- |In traditional kind inference systems, a kind cannot contain variables. +-- At some point in the inference process the kind variables are defaulted +-- to star. +defaultToStar :: Kind -> Kind +defaultToStar kind = + let sub = listToSubstitution [ (i, star) | i <- ftv kind ] + in sub |-> kind + +-- |A function to show kinds. +showKind :: Kind -> String +showKind kind = + let sub = listToSubstitution [ (i, TCon ('k':show i)) | i <- ftv kind ] + in show (sub |-> kind) + +showKindScheme :: KindScheme -> String +showKindScheme scheme = + let sub = listToSubstitution + $ [ (i, TCon ('k':show j)) | (i, j) <- zip (quantifiers scheme) [1 :: Int ..] ] + ++ [ (i, TCon ("_k"++show i)) | i <- ftv scheme ] + in show (sub |-> unquantify scheme) diff --git a/src/Top/Types/Primitive.hs b/src/Top/Types/Primitive.hs new file mode 100644 --- /dev/null +++ b/src/Top/Types/Primitive.hs @@ -0,0 +1,252 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +-- +-- This module contains a data type to represent (plain) types, some basic +-- functionality for types, and an instance for Show. +-- +----------------------------------------------------------------------------- + +module Top.Types.Primitive where + +import Data.List (union, isPrefixOf) +import Data.Char (isDigit, isSpace) + +----------------------------------------------------------------------------- +-- * Data type definition + +type Tps = [Tp] +-- |A data type to represent monotypes. Note that 'Type' is already in use +-- in the Unified Haskell Architecture (UHA) which is used in the Helium compiler +data Tp = TVar Int -- ^The type variables are numbered. + | TCon String -- ^A type constant is represented by a string. + | TApp Tp Tp -- ^The application of two Top.Types. Not all types that can be + -- constructed are well-formed. + deriving (Eq, Ord) + +---------------------------------------------------------------------- +-- * Common types + +intType, charType, floatType, boolType, stringType :: Tp +intType = TCon "Int" +charType = TCon "Char" +floatType = TCon "Float" +boolType = TCon "Bool" +stringType = TCon "String" + +infixr 5 .->. +-- |Constructs a function type from one type to another. This operator is +-- left associative. +(.->.) :: Tp -> Tp -> Tp +t1 .->. t2 = TApp (TApp (TCon "->") t1) t2 + +-- |For instance, @(listType intType)@ represents @[Int]@ +listType :: Tp -> Tp +listType = TApp (TCon "[]") + +-- |For instance, @(ioType boolType)@ represents @(IO Bool)@ +ioType :: Tp -> Tp +ioType = TApp (TCon "IO") + +-- |A cathesian product of zero or more Top.Types. For instance, +-- @(tupleType [])@ represents @()@, and @(tupleType [charType, stringType])@ +-- represents @(Char,String)@ +tupleType :: Tps -> Tp +tupleType tps = let name | null tps = "()" + | otherwise = "("++replicate (length tps-1) ','++")" + in foldl TApp (TCon name) tps + +-- |The unit type. A special instance of of tuple type. +voidType :: Tp +voidType = tupleType [] + +---------------------------------------------------------------------- +-- * Basic functionality + +-- |Returns the list of type variables of a type. (no duplicates) +variablesInType :: Tp -> [Int] +variablesInType tp = case tp of + TVar i -> [i] + TCon _ -> [] + TApp t1 t2 -> variablesInType t1 `union` variablesInType t2 + +-- |Returns the list of type constants of a type. (no duplicates) +constantsInType :: Tp -> [String] +constantsInType tp = case tp of + TVar _ -> [] + TCon s -> [s] + TApp t1 t2 -> constantsInType t1 `union` constantsInType t2 + +-- |Returns the left spine of a type. For instance, if type @t@ +-- is @Either Bool [Int]@, then @leftSpine t@ is @(Either,[Bool,[Int]])@. +leftSpine :: Tp -> (Tp,Tps) +leftSpine = rec [] where + rec tps (TApp t1 t2) = rec (t2:tps) t1 + rec tps tp = (tp,tps) + +-- |Returns the right spine of a function type. For instance, +-- if type @t@ is @Int -> (Bool -> String)@, then @functionSpine t@ +-- is @([Int,Bool],String)@. +functionSpine :: Tp -> (Tps,Tp) +functionSpine = rec [] where + rec tps (TApp (TApp (TCon "->") t1) t2) = rec (t1:tps) t2 + rec tps tp = (reverse tps,tp) + +-- |Returns the right spine of a function type of a maximal length. +functionSpineOfLength :: Int -> Tp -> (Tps, Tp) +functionSpineOfLength i tp = + let (as, a ) = functionSpine tp + (bs, cs) = splitAt i as + in (bs, foldr (.->.) a cs) + +-- |Returns the arity of a type, that is, the number of expected arguments. +arityOfTp :: Tp -> Int +arityOfTp = length . fst . functionSpine + +-- |The priority of a type, primarily used for the insertion of parentheses +-- in pretty printing. +priorityOfType :: Tp -> Int +priorityOfType tp = case leftSpine tp of + (TCon "->",[_,_] ) -> 0 + (_ ,[] ) -> 2 + (TCon "[]",[_] ) -> 2 + (TCon s ,_ ) | isTupleConstructor s -> 2 + _ -> 1 + +-- |All the type variables in a type are frozen by turning them into a type +-- constant. The integer numeral is prefixed with an underscore ('_'). +freezeVariablesInType :: Tp -> Tp +freezeVariablesInType tp = + case tp of + TVar i -> TCon ('_':show i) + TCon s -> TCon s + TApp l r -> TApp (freezeVariablesInType l) (freezeVariablesInType r) + +-- |Recover the type variables that are frozen in a type. +unfreezeVariablesInType :: Tp -> Tp +unfreezeVariablesInType tp = + case tp of + TVar i -> TVar i + TCon ('_':s) | all isDigit s && not (null s) + -> TVar (read s) + TCon s -> TCon s + TApp l r -> TApp (unfreezeVariablesInType l) (unfreezeVariablesInType r) + +---------------------------------------------------------------------- +-- * Predicates on types + +isTVar :: Tp -> Bool +isTVar (TVar _) = True +isTVar _ = False + +isTCon :: Tp -> Bool +isTCon (TCon _) = True +isTCon _ = False + +isTApp :: Tp -> Bool +isTApp (TApp _ _) = True +isTApp _ = False + +isFunctionType :: Tp -> Bool +isFunctionType (TApp (TApp (TCon "->") _) _) = True +isFunctionType _ = False + +isTupleConstructor :: String -> Bool +isTupleConstructor ('(':[]) = False +isTupleConstructor ('(':cs) = all (','==) (init cs) && last cs == ')' +isTupleConstructor _ = False + +isIOType :: Tp -> Bool +isIOType (TApp (TCon "IO") _) = True +isIOType _ = False + +---------------------------------------------------------------------- +-- Show and Read instances + +instance Show Tp where + -- parenthesis are needed when the type must be shown as a part of + -- some other data type + showsPrec prio theType rest = + parIf (prio > 0) (showTp theType) ++ rest + + where + showTp tp = + case leftSpine tp of + (TCon "->",[t1,t2]) -> rec (<1) t1 ++ " -> " ++ rec (const False) t2 + (TVar i ,[] ) -> 'v' : show i + (TCon s ,[] ) -> s + (TCon "[]",[t1] ) -> "[" ++ rec (const False) t1 ++ "]" + (TCon s ,ts ) | isTupleConstructor s -> let ts' = map (rec (const False)) ts + f [] = "" + f xs = foldr1 (\x y -> x++", "++y) xs + in "(" ++ f ts' ++ ")" + (t,ts) -> unwords (map (rec (<2)) (t:ts)) + + rec p t = parIf (p (priorityOfType t)) (showTp t) + parIf True s = "("++s++")" + parIf False s = s + +instance Read Tp where + readsPrec _ = tpParser + +tpParser :: String -> [(Tp, String)] +tpParser = level0 + where + level0 = foldr1 (.->.) <$> seplist (tok "->") level1 + level1 = foldl1 TApp <$> list1 level2 + level2 = ident + <|> (listType <$> bracks level0) + <|> ((\xs -> if length xs == 1 then head xs else tupleType xs) <$> pars (commaList level0)) + + ident xs = + case break (\c -> isSpace c || c `elem` "[]()-,") (dropWhile isSpace xs) of + ([], _) -> [] + (s, xs2) | length s > 1 && "v" `isPrefixOf` s && all isDigit (drop 1 s) + -> [ (TVar (read $ drop 1 s), xs2) ] + | otherwise -> [ (TCon s, xs2) ] + + (p <*> q) xs = [ (f a, xs2) | (f, xs1) <- p xs, (a, xs2) <- q xs1 ] + (f <$> p) xs = [ (f a, xs1) | (a, xs1) <- p xs ] + (p <|> q) xs = p xs ++ q xs + p <* q = const <$> p <*> q + p *> q = flip const <$> p <*> q + succeed a xs = [(a, xs)] + tok s xs = + let ys = dropWhile isSpace xs + in [ (s, drop (length s) ys) | not (null ys), s `isPrefixOf` ys ] + pars p = tok "(" *> p <* tok ")" + bracks p = tok "[" *> p <* tok "]" + list p = ((:) <$> p <*> list p) <|> succeed [] + list1 p = (:) <$> p <*> list p + seplist sep p = (:) <$> p <*> list (sep *> p) + commaList p = seplist (tok ",") p <|> succeed [] + +---------------------------------------------------------------------- +-- The type class HasTypes + +class HasTypes a where + getTypes :: a -> Tps + changeTypes :: (Tp -> Tp) -> a -> a + +instance HasTypes Tp where + getTypes tp = [tp] + changeTypes = ($) + +instance HasTypes a => HasTypes [a] where + getTypes = concatMap getTypes + changeTypes f = map (changeTypes f) + +instance (HasTypes a, HasTypes b) => HasTypes (a, b) where + getTypes (a, b) = getTypes a ++ getTypes b + changeTypes f (a, b) = (changeTypes f a, changeTypes f b) + +instance HasTypes a => HasTypes (Maybe a) where + getTypes = maybe [] getTypes + changeTypes = fmap . changeTypes + +instance (HasTypes a, HasTypes b) => HasTypes (Either a b) where + getTypes = either getTypes getTypes + changeTypes f = either (Left . changeTypes f) (Right . changeTypes f) diff --git a/src/Top/Types/Qualification.hs b/src/Top/Types/Qualification.hs new file mode 100644 --- /dev/null +++ b/src/Top/Types/Qualification.hs @@ -0,0 +1,72 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +-- +-- Qualification of types (for instance, predicates to deal with type classes). +-- +----------------------------------------------------------------------------- + +module Top.Types.Qualification where + +import Top.Types.Primitive +import Top.Types.Substitution +import Data.List + +----------------------------------------------------------------------------- +-- * Qualification + +newtype Qualification q a = Qualification (q, a) + +split :: Qualification q a -> (q, a) +split (Qualification t) = t + +infixr 2 .=>. + +(.=>.) :: q -> a -> Qualification q a +(.=>.) = curry Qualification + +qualifiers :: Qualification q a -> q +qualifiers = fst . split + +unqualify :: Qualification q a -> a +unqualify = snd . split + +qualify :: (Substitutable context, Substitutable q, Substitutable a) => context -> [q] -> a -> Qualification [q] a +qualify context preds tp = + let is = ftv tp \\ ftv context + p = any (`elem` is) . ftv + in (filter p preds .=>. tp) + +instance (Substitutable q, Substitutable a) => Substitutable (Qualification q a) where + sub |-> (Qualification t) = Qualification (sub |-> t) + ftv (Qualification t) = ftv t + +instance (HasTypes q, HasTypes a) => HasTypes (Qualification q a) where + getTypes (Qualification t) = getTypes t + changeTypes f (Qualification t) = Qualification (changeTypes f t) + +instance (ShowQualifiers q, Show a) => Show (Qualification q a) where + show (Qualification (q, a)) = + showContext q ++ show a + +class Show a => ShowQualifiers a where + showQualifiers :: a -> [String] + -- default definition + showQualifiers = (:[]) . show + +showContext :: ShowQualifiers a => a -> String +showContext = showContextSimple . showQualifiers + +showContextSimple :: [String] -> String +showContextSimple [] = "" +showContextSimple [x] = x ++ " => " +showContextSimple xs = "(" ++ intercalate ", " xs ++ ") => " + +instance (ShowQualifiers a, ShowQualifiers b) => ShowQualifiers (a, b) where + showQualifiers (a, b) = showQualifiers a ++ showQualifiers b + +instance ShowQualifiers a => ShowQualifiers [a] where + showQualifiers = concatMap showQualifiers diff --git a/src/Top/Types/Quantification.hs b/src/Top/Types/Quantification.hs new file mode 100644 --- /dev/null +++ b/src/Top/Types/Quantification.hs @@ -0,0 +1,233 @@ +{-# LANGUAGE EmptyDataDecls #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +-- +-- Universal and existential quantification of types +-- +----------------------------------------------------------------------------- + +module Top.Types.Quantification where + +import Top.Types.Primitive +import Top.Types.Substitution +import Data.List +import Data.Maybe +import Utils (internalError) + +----------------------------------------------------------------------------- +-- * Quantification + +newtype Quantification q a = Quantification ([Int], QuantorMap, a) + +type QuantorMap = [(Int, String)] + +withoutQuantors :: Quantification q a -> Bool +withoutQuantors (Quantification (is, _, _)) = null is + +showQuantor :: Show q => Quantification q a -> String +showQuantor = show . f where + f :: Quantification q a -> q + f = internalError "Top.Types.Quantification" "showQuantor" "quantor unknown" + +noQuantifiers :: a -> Quantification q a +noQuantifiers a = Quantification ([], [], a) + +quantifiers :: Quantification q a -> [Int] +quantifiers (Quantification (is, _, _)) = is + +unquantify :: Quantification q a -> a +unquantify (Quantification (_, _, a)) = a + +instance Substitutable a => Substitutable (Quantification q a) where + sub |-> (Quantification (is, qmap, a)) = Quantification (is, qmap, removeDom is sub |-> a) + ftv (Quantification (is, _ , a)) = ftv a \\ is + +instance HasTypes a => HasTypes (Quantification q a) where + getTypes (Quantification (_, _, a)) = getTypes a + changeTypes f (Quantification (is, qmap, a)) = Quantification (is, qmap, changeTypes f a) + +introduceTypeVariables :: Substitutable a => Int -> Quantification q a -> (Int, a) +introduceTypeVariables i (Quantification (qs, _, a)) = + let sub = listToSubstitution (zip qs (map TVar [i..])) + in (i + length qs, sub |-> a) + +introduceSkolemConstants :: Substitutable a => Int -> Quantification q a -> (Int, a) +introduceSkolemConstants i (Quantification (qs, _, a)) = + let sub = listToSubstitution (zip qs (map makeSkolemConstant [i..])) + in (i + length qs, sub |-> a) + +bindTypeVariables :: Substitutable a => [Int] -> a -> Quantification q a +bindTypeVariables is a = Quantification (is `intersect` ftv a, [], a) + +bindSkolemConstants :: HasSkolems a => [Int] -> a -> Quantification q a +bindSkolemConstants scs a = + let scs' = scs `union` allSkolems a + skMap = [ (i, TVar i) | i <- scs' ] + in Quantification (scs', [], changeSkolems skMap a) + +getQuantorMap :: Quantification q a -> QuantorMap +getQuantorMap (Quantification (_, qm, _)) = qm + +----------------------------------------------------------------------------- +-- * Universal quantification + +data Universal +type Forall = Quantification Universal + +instance Show Universal where + show = const "forall" + +instantiate, skolemize :: Substitutable a => Int -> Forall a -> (Int, a) +instantiate = introduceTypeVariables +skolemize = introduceSkolemConstants + +generalize :: (Substitutable context, Substitutable a) => context -> a -> Forall a +generalize context a = + quantify (ftv a \\ ftv context) a + +generalizeAll :: Substitutable a => a -> Forall a +generalizeAll a = quantify (ftv a) a + +quantify :: Substitutable a => [Int] -> a -> Forall a +quantify = bindTypeVariables + +unskolemize :: HasSkolems a => [Int] -> a -> Forall a +unskolemize = bindSkolemConstants + +----------------------------------------------------------------------------- +-- * Existential quantification + +data Existential +type Exists = Quantification Existential + +instance Show Existential where + show = const "exists" + +open, reveal :: Substitutable a => Int -> Exists a -> (Int, a) +open = introduceSkolemConstants +reveal = introduceTypeVariables + +close :: HasSkolems a => [Int] -> a -> Exists a +close = bindSkolemConstants + +unreveal :: Substitutable a => [Int] -> a -> Exists a +unreveal = bindTypeVariables + +----------------------------------------------------------------------------- +-- * Skolemization + +skolemPrefix :: String +skolemPrefix = "_" + +makeSkolemConstant :: Int -> Tp +makeSkolemConstant = TCon . (skolemPrefix++) . show + +fromSkolemString :: String -> Maybe Int +fromSkolemString s + | skolemPrefix `isPrefixOf` s = + Just (read (drop (length skolemPrefix) s)) + | otherwise = Nothing + +skolemizeFTV :: Substitutable a => a -> a +skolemizeFTV a = + let sub = listToSubstitution [ (i, makeSkolemConstant i) | i <- ftv a ] + in sub |-> a + +class HasSkolems a where + allSkolems :: a -> [Int] + changeSkolems :: [(Int, Tp)] -> a -> a + +instance HasSkolems Tp where + allSkolems (TVar _) = [] + allSkolems (TCon s) = case fromSkolemString s of + Just i -> [i] + Nothing -> [] + allSkolems (TApp l r) = allSkolems l `union` allSkolems r + + changeSkolems skMap = rec where + rec tp@(TVar _) = tp + rec tp@(TCon s) = case fromSkolemString s of + Just i -> fromMaybe tp (lookup i skMap) + Nothing -> tp + rec (TApp l r) = TApp (rec l) (rec r) + +instance HasSkolems a => HasSkolems [a] where + allSkolems = foldr (union . allSkolems) [] + changeSkolems skMap = map (changeSkolems skMap) + +----------------------------------------------------------------------------- +-- * Pretty printing + +data ShowQuantorOptions = ShowQuantorOptions + { showTopLevelQuantors :: Bool + , dontUseIdentifiers :: [String] + , variablePrefix :: String + , showAllTheSame :: Bool + , useTheNameMap :: Bool + } + +defaultOptions :: ShowQuantorOptions +defaultOptions = ShowQuantorOptions + { showTopLevelQuantors = False + , dontUseIdentifiers = [] + , variablePrefix = "v" + , showAllTheSame = False + , useTheNameMap = True + } + +showQuantors :: ShowQuantors a => a -> String +showQuantors = showQuantorsWithout (defaultOptions { showTopLevelQuantors = True }) + +-- |This class can deal with the pretty printing of (possibly nested) quantifiers. +class Show a => ShowQuantors a where + showQuantorsWithout :: ShowQuantorOptions -> a -> String + + -- default definition + showQuantorsWithout = const show + +instance ShowQuantors Tp + +instance (Substitutable a, ShowQuantors a, Show q) => Show (Quantification q a) where + show = showQuantorsWithout defaultOptions + +instance (Substitutable a, ShowQuantors a, Show q) => ShowQuantors (Quantification q a) where + showQuantorsWithout options q@(Quantification (is, qmap, a)) = + let + qs = is `intersect` ftv a + quantorText | null qs || not (showTopLevelQuantors options) = "" + | otherwise = unwords (showQuantor q : map (\i -> show (sub |-> TVar i)) qs ++ [". "]) + dontUse = dontUseIdentifiers options + -- find an appropriate name for bound type variables that are in the name map + qmap1 | not (useTheNameMap options) || showAllTheSame options = [] + | otherwise = + let op (rest, donts) (i,n) + | i `elem` qs = let ints = [1..] :: [Int] + s = head [ n ++ extra + | extra <- "" : map show ints + , n ++ extra `notElem` donts + ] + in ((i,s):rest, s:donts) + | otherwise = (rest, donts) + in fst (foldl op ([], dontUse) qmap) + dontUse1 = map snd qmap1 ++ dontUse + -- find a name for the other bound type variables + qmap2 | showAllTheSame options = [] + | otherwise = zip (filter (`notElem` map fst qmap1) qs) (variableList \\ dontUse1) + dontUse2 = map snd qmap2 ++ dontUse1 + frees = ftv a \\ map fst (qmap1 ++ qmap2) + sub = listToSubstitution $ [ (i, TCon s) | (i,s) <- qmap1 ++ qmap2 ] + ++ [ (i, TCon (variablePrefix options ++ show i)) | i <- frees ] + newOptions = options { dontUseIdentifiers = dontUse2 + , showTopLevelQuantors = True + } + in + quantorText ++ showQuantorsWithout newOptions (sub |-> a) + +-- |List of unique identifiers.(a, b, .., z, a1, b1 .., z1, a2, ..) +variableList :: [String] +variableList = [ [x] | x <- ['a'..'z'] ] + ++ [ x:show i | i <- [1 :: Int ..], x <- ['a'..'z'] ] diff --git a/src/Top/Types/Schemes.hs b/src/Top/Types/Schemes.hs new file mode 100644 --- /dev/null +++ b/src/Top/Types/Schemes.hs @@ -0,0 +1,124 @@ +{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +-- +-- A representation of type schemes. A type scheme is a (qualified) type +-- with a number of quantifiers (foralls) in front of it. A partial mapping +-- from type variable (Int) to their name (String) is preserved. +-- +----------------------------------------------------------------------------- + +module Top.Types.Schemes where + +import Top.Types.Primitive +import Top.Types.Quantification +import Top.Types.Qualification +import Top.Types.Substitution +import Top.Types.Synonym +import Top.Types.Unification +import Top.Types.Classes +import Data.List +import qualified Data.Map as M + +---------------------------------------------------------------------- +-- * Type schemes + +-- |A type scheme consists of a list of quantified type variables, a finite map +-- that partially maps these type variables to their original identifier, and a +-- qualified type. +type TpScheme = Forall QType +type QType = Qualification Predicates Tp + +-- |A type class to convert something into a type scheme +class IsTpScheme a where + toTpScheme :: a -> TpScheme + +instance IsTpScheme TpScheme where + toTpScheme = id + +instance IsTpScheme QType where + toTpScheme = noQuantifiers + +instance IsTpScheme Tp where + toTpScheme = noQuantifiers . ([] .=>.) + +---------------------------------------------------------------------- +-- * Basic functionality for types and type schemes + +-- |Determine the arity of a type scheme. +arityOfTpScheme :: TpScheme -> Int +arityOfTpScheme = arityOfTp . unqualify . unquantify + +genericInstanceOf :: OrderedTypeSynonyms -> ClassEnvironment -> TpScheme -> TpScheme -> Bool +genericInstanceOf synonyms classes scheme1 scheme2 = + let -- monomorphic type variables are treated as constants + s1 = skolemizeFTV scheme1 + s2 = skolemizeFTV scheme2 + -- substitution to fix the type variables in the first type scheme + sub = listToSubstitution (zip (quantifiers s1) [ TCon ('+':show i) | i <- [0 :: Int ..]]) + (ps1, tp1) = split (sub |-> unquantify s1) + (ps2, tp2) = split (snd (instantiate 123456789 s2)) + in case mguWithTypeSynonyms synonyms tp1 tp2 of + Left _ -> False + Right (_,sub2) -> entailList synonyms classes ps1 (sub2 |-> ps2) + +-- |Is the type scheme overloaded (does it contain predicates)? +isOverloaded :: TpScheme -> Bool +isOverloaded = not . null . qualifiers . unquantify + +makeScheme :: [Int] -> Predicates -> Tp -> TpScheme +makeScheme monos preds tp = + let is = ftv tp \\ monos + p = any (`elem` is) . ftv + in quantify is (filter p preds .=>. tp) + +instantiateWithNameMap :: Int -> TpScheme -> (Int, Predicates, Tp) -- get rid of this function. +instantiateWithNameMap unique (Quantification (qs,nm,qtp)) = + let sub = listToSubstitution [ (i,TCon s) | (i,s) <- nm, i `elem` qs ] + (u, qtp') = instantiate unique (Quantification (qs \\ map fst nm, [], sub |-> qtp)) + (ps, tp) = split qtp' + in (u, ps, tp) + +instance (ShowQualifiers q, Show a) => ShowQuantors (Qualification q a) + +-- |A sigma is a type scheme or a type scheme variable +type Scheme qs = Forall (Qualification qs Tp) + +data Sigma qs = SigmaVar SigmaVar + | SigmaScheme (Scheme qs) +type SigmaVar = Int + +instance (ShowQualifiers qs, Substitutable qs) => Show (Sigma qs) where + show (SigmaVar i) = 's':show i + show (SigmaScheme s) = show s + +instance Substitutable qs => Substitutable (Sigma qs) where + _ |-> sv@(SigmaVar _) = sv + sub |-> (SigmaScheme s) = SigmaScheme (sub |-> s) + + ftv (SigmaVar _) = [] + ftv (SigmaScheme s) = ftv s + +instance (Substitutable qs, ShowQualifiers qs) => ShowQuantors (Sigma qs) where + showQuantorsWithout options sigma = + case sigma of + SigmaVar _ -> show sigma + SigmaScheme ts -> showQuantorsWithout options ts + +-- |A substitution for type scheme variables +type TpSchemeMap = M.Map SigmaVar TpScheme + +type SigmaPreds = Sigma Predicates + +class IsSigmaPreds a where + toSigmaPreds :: a -> SigmaPreds + +instance IsSigmaPreds SigmaPreds where toSigmaPreds = id +instance IsSigmaPreds TpScheme where toSigmaPreds = SigmaScheme . toTpScheme +instance IsSigmaPreds QType where toSigmaPreds = SigmaScheme . toTpScheme +instance IsSigmaPreds Tp where toSigmaPreds = SigmaScheme . toTpScheme +instance IsSigmaPreds Int where toSigmaPreds = SigmaVar diff --git a/src/Top/Types/Substitution.hs b/src/Top/Types/Substitution.hs new file mode 100644 --- /dev/null +++ b/src/Top/Types/Substitution.hs @@ -0,0 +1,179 @@ +{-# LANGUAGE ExistentialQuantification, TypeSynonymInstances, FlexibleInstances #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +-- +-- This module contains a data type to represent (plain) types, some basic +-- functionality for types, and an instance for Show. +-- +----------------------------------------------------------------------------- + +module Top.Types.Substitution where + +import Top.Types.Primitive +import Data.List (union, (\\), nub) +import qualified Data.Map as M +import qualified Data.Set as S +import Utils (internalError) + +---------------------------------------------------------------------- +-- * Substitutions and substitutables + +infix 4 |-> + +class Substitution s where + lookupInt :: Int -> s -> Tp -- lookup the type of a type variable in a substitution + removeDom :: [Int] -> s -> s -- remove from the domain of the substitution + restrictDom :: [Int] -> s -> s -- restrict the domain of the substitution + dom :: s -> [Int] -- domain of substitution + cod :: s -> Tps -- co-domain of substitution + +class Substitutable a where + (|->) :: Substitution s => s -> a -> a -- apply substitution + ftv :: a -> [Int] -- free type variables + +-- |The next type variable that is not free (default is zero) +nextFTV :: Substitutable a => a -> Int +nextFTV a = case ftv a of + [] -> 0 + is -> maximum is + 1 + +---------------------------------------------------------------------- +-- * Substitution instances + +-- |A substitution represented by a finite map. +type MapSubstitution = M.Map Int Tp + +instance Substitution MapSubstitution where + + lookupInt i = M.findWithDefault (TVar i) i + removeDom = flip (foldr M.delete) + restrictDom is = let set = S.fromList is + in M.filterWithKey (\i _ -> S.member i set) + + dom = M.keys + cod = M.elems + +emptySubst :: MapSubstitution +emptySubst = M.empty + +-- |Compose two finite map substitutions: safe. +-- Note for 'M.union': bindings in right argument shadow those in the left +(@@) :: MapSubstitution -> MapSubstitution -> MapSubstitution +fm1 @@ fm2 = fm1 `M.union` M.map (\t -> fm1 |-> t) fm2 + +-- |Compose two finite map substitutions: quick and dirty! +(@@@) :: MapSubstitution -> MapSubstitution -> MapSubstitution +(@@@) = M.union + +singleSubstitution :: Int -> Tp -> MapSubstitution +singleSubstitution = M.singleton + +listToSubstitution :: [(Int,Tp)] -> MapSubstitution +listToSubstitution = M.fromList + +-- |A fixpoint is computed when looking up the target of a type variable in this substitution. +-- Combining two substitutions is cheap, whereas a lookup is more expensive than the +-- normal finite map substitution. +newtype FixpointSubstitution = FixpointSubstitution (M.Map Int Tp) + +instance Substitution FixpointSubstitution where + lookupInt i original@(FixpointSubstitution fm) = + case M.lookup i fm of + Just tp | tp == TVar i -> TVar i + | otherwise -> original |-> tp + Nothing -> TVar i + removeDom is (FixpointSubstitution fm) = FixpointSubstitution (M.filterWithKey (\i _ -> i `notElem` is) fm) + restrictDom is (FixpointSubstitution fm) = let js = M.keys fm \\ is + in FixpointSubstitution (M.filterWithKey (\i _ -> i `notElem` js) fm) + dom (FixpointSubstitution fm) = M.keys fm + cod (FixpointSubstitution fm) = M.elems fm + +-- |The empty fixpoint substitution +emptyFPS :: FixpointSubstitution +emptyFPS = FixpointSubstitution M.empty + +-- |Combine two fixpoint substitutions that are disjoint +disjointFPS :: FixpointSubstitution -> FixpointSubstitution -> FixpointSubstitution +disjointFPS (FixpointSubstitution fm1) (FixpointSubstitution fm2) = + let notDisjoint = internalError "Substitution" "disjointFPS" "the two fixpoint substitutions are not disjoint" + in FixpointSubstitution (M.unionWith notDisjoint fm1 fm2) + +---------------------------------------------------------------------- +-- * Wrapper for substitutions + +wrapSubstitution :: Substitution substitution => substitution -> WrappedSubstitution +wrapSubstitution substitution = + WrappedSubstitution substitution + ( lookupInt + , removeDom + , restrictDom + , dom + , cod + ) + +data WrappedSubstitution = + forall a . Substitution a => + WrappedSubstitution a + ( Int -> a -> Tp + , [Int] -> a -> a + , [Int] -> a -> a + , a -> [Int] + , a -> Tps + ) + +instance Substitution WrappedSubstitution where + lookupInt i (WrappedSubstitution x (f,_,_,_,_)) = f i x + removeDom is (WrappedSubstitution x (_,f,_,_,_)) = wrapSubstitution (f is x) + restrictDom is (WrappedSubstitution x (_,_,f,_,_)) = wrapSubstitution (f is x) + dom (WrappedSubstitution x (_,_,_,f,_)) = f x + cod (WrappedSubstitution x (_,_,_,_,f)) = f x + +---------------------------------------------------------------------- +-- * Substitutables instances + +instance Substitutable Tp where + sub |-> tp = + case tp of + TVar i -> lookupInt i sub + TCon _ -> tp + TApp t1 t2 -> TApp (sub |-> t1) (sub |-> t2) + ftv tp = + case tp of + TVar i -> [i] + TCon _ -> [] + TApp t1 t2 -> ftv t1 `union` ftv t2 + +instance Substitutable a => Substitutable [a] where + sub |-> as = map (sub |->) as + ftv = foldr (union . ftv) [] + +instance (Substitutable a, Substitutable b) => Substitutable (a, b) where + sub |-> (a, b) = (sub |-> a, sub |-> b) + ftv (a, b) = ftv a `union` ftv b + +instance Substitutable a => Substitutable (Maybe a) where + sub |-> ma = fmap (sub |->) ma + ftv = maybe [] ftv + +instance (Substitutable a, Substitutable b) => Substitutable (Either a b) where + sub |-> x = either (Left . (sub |->)) (Right . (sub |->)) x + ftv = either ftv ftv + +freezeFTV :: Substitutable a => a -> a +freezeFTV a = + let sub = listToSubstitution [ (i, TCon ('_':show i)) | i <- ftv a ] + in sub |-> a + +allTypeVariables :: HasTypes a => a -> [Int] +allTypeVariables = ftv . getTypes + +allTypeConstants :: HasTypes a => a -> [String] +allTypeConstants = + let f (TVar _) = [] + f (TCon s) = [s] + f (TApp l r) = f l ++ f r + in nub . concatMap f . getTypes diff --git a/src/Top/Types/Synonym.hs b/src/Top/Types/Synonym.hs new file mode 100644 --- /dev/null +++ b/src/Top/Types/Synonym.hs @@ -0,0 +1,142 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +-- +-- This module contains type synonyms to represent type synonyms. A collection +-- of type synonyms can always be ordered, since (mutually) recursive type +-- synonyms are not permitted. The ordering of type synonyms must be determined +-- to find a minimal number of unfold steps to make two types syntactically +-- equivalent. +-- +----------------------------------------------------------------------------- + +module Top.Types.Synonym where + +import Top.Types.Primitive +import Top.Types.Substitution hiding (lookupInt) +import Utils (internalError) +import Data.Maybe +import Data.Graph (scc, buildG) +import Data.Tree (flatten) +import qualified Data.Map as M + +---------------------------------------------------------------------- +-- * Type synonyms + +-- |A (unordered) collection of type synonyms is represented by a finite map of +-- strings (the name of the type synonym) to pairs that have an int +-- (the number of arguments of the type synonym) and a function. +type TypeSynonyms = M.Map String (Int, Tps -> Tp) +-- |An ordering of type synonyms maps a name of a type synonym to +-- a position in the ordering. +type TypeSynonymOrdering = M.Map String Int +-- |An (unordered) collection of type synonyms, together with an ordering. +type OrderedTypeSynonyms = (TypeSynonymOrdering, TypeSynonyms) + +---------------------------------------------------------------------- +-- * Utility functions + +-- |An empty collection of ordered type synonyms. +noOrderedTypeSynonyms :: OrderedTypeSynonyms +noOrderedTypeSynonyms = (M.empty, M.empty) + +-- |A string is a list of characters +stringAsTypeSynonym :: OrderedTypeSynonyms +stringAsTypeSynonym = (M.singleton "String" 0, M.singleton "String" (0, \_ -> listType charType)) + +-- |Order a collection of type synonyms, and return this ordering paired with +-- sets of mutually recursive type synonyms that are detected. +getTypeSynonymOrdering :: TypeSynonyms -> (TypeSynonymOrdering, [[String]]) +getTypeSynonymOrdering synonyms = + let + (nameTable, intTable) = let keys = M.keys synonyms + in ( M.fromList (zip keys [0..]) + , M.fromList (zip [0..] keys) + ) + + err = internalError "Top.Types.Synonyms" "getTypeSynonymOrdering" "error in lookup table" + lookupName n = fromMaybe err (M.lookup n nameTable) + lookupInt i = fromMaybe err (M.lookup i intTable) + + edges = let op s1 (arity, function) es = + let i1 = lookupName s1 + cs = constantsInType (function (map TVar [0 .. arity - 1])) + add s2 = case M.lookup s2 nameTable of + Just i2 -> (:) (i2,i1) + Nothing -> id + in foldr add es cs + in M.foldrWithKey op [] synonyms + + graph = buildG (0, M.size synonyms - 1) edges + list = map flatten (scc graph) + + (ordering, recursive, _) = + let op ints (os, rs, counter) = + case ints of + [int] | (int, int) `notElem` edges -- correct type synonym + -> (M.insert (lookupInt int) counter os, rs, counter + 1) + _ -> (os, map lookupInt ints : rs, counter) + in foldr op (M.empty, [], 0) list + in + (ordering, recursive) + +isPhantomTypeSynonym :: OrderedTypeSynonyms -> String -> Bool +isPhantomTypeSynonym (_, xs) s = + case M.lookup s xs of + Nothing -> False + Just (i, f) -> + let is = take i [0..] + tp = f (map TVar is) + free = ftv tp + in any (`notElem` free) is + +---------------------------------------------------------------------- +-- * Expansion of a type + +-- |Fully expand a type in a recursive way. +expandType :: TypeSynonyms -> Tp -> Tp +expandType synonyms tp = + let (x,xs) = leftSpine (expandTypeConstructor synonyms tp) + in foldl TApp x (map (expandType synonyms) xs) + +-- |Fully expand the top-level type constructor. +expandTypeConstructor :: TypeSynonyms -> Tp -> Tp +expandTypeConstructor synonyms tp = + maybe tp (expandTypeConstructor synonyms) (expandTypeConstructorOneStep synonyms tp) + +-- |Fully expand the top-level type constructor. +expandToplevelTC :: OrderedTypeSynonyms -> Tp -> Maybe Tp +expandToplevelTC (_, synonyms) = + fmap (expandTypeConstructor synonyms) . expandTypeConstructorOneStep synonyms + +-- |Try to expand the top-level type constructor one step. +expandTypeConstructorOneStep :: TypeSynonyms -> Tp -> Maybe Tp +expandTypeConstructorOneStep synonyms tp = + case leftSpine tp of + (TCon s, tps) -> case M.lookup s synonyms of + Just (i, f) | i == length tps -> Just (f tps) + | otherwise -> internalError "Top.Types.Synonyms" + "expandTypeConstructorOneStep" + "invalid arity of type synonym" + Nothing -> Nothing + _ -> Nothing + +-- |Try to expand the top-level type constructor of one of the two paired Top.Types. If both +-- top-level type constructors can be expanded, then the type synonym thast appears first +-- in the ordering is expanded. +expandOneStepOrdered :: OrderedTypeSynonyms -> (Tp, Tp) -> Maybe (Tp, Tp) +expandOneStepOrdered (ordering, synonyms) (t1,t2) = + let f tp = case fst (leftSpine tp) of + TCon s -> M.lookup s ordering + _ -> Nothing + expand tp = fromMaybe err (expandTypeConstructorOneStep synonyms tp) + err = internalError "Top.Types.Synonyms" "expandOneStep" "invalid set of OrderedTypeSynonyms" + in case (f t1, f t2) of + (Just i1, Just i2) | i1 <= i2 -> Just (expand t1, t2) + | otherwise -> Just (t1, expand t2) + (Just _ , Nothing) -> Just (expand t1, t2) + (Nothing, Just _ ) -> Just (t1, expand t2) + _ -> Nothing diff --git a/src/Top/Types/Unification.hs b/src/Top/Types/Unification.hs new file mode 100644 --- /dev/null +++ b/src/Top/Types/Unification.hs @@ -0,0 +1,124 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +-- +-- A unification algorithm for types, which can take a list of (ordered) +-- type synonyms into account. +-- +----------------------------------------------------------------------------- + +module Top.Types.Unification where + +import Top.Types.Substitution +import Top.Types.Primitive +import Top.Types.Synonym +import qualified Data.Map as M +import Utils (internalError) + +-- |There are two reasons why two types cannot be unified: either two (different) type constants clash (they +-- should be the same), or a type variable should be unified with a composed type that contains this same +-- type variable. +data UnificationError + = ConstantClash String String + | InfiniteType Int + deriving (Show,Eq) + +-- |The most general unification (substitution) of two types. +mgu :: Tp -> Tp -> Either UnificationError MapSubstitution +mgu t1 t2 = + case mguWithTypeSynonyms noOrderedTypeSynonyms t1 t2 of + Left uError -> Left uError + Right (_, s) -> Right s + +-- Expand type synonyms 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 exansions were necessary +mguWithTypeSynonyms :: OrderedTypeSynonyms -> Tp -> Tp -> Either UnificationError (Bool, MapSubstitution) +mguWithTypeSynonyms typesynonyms = rec emptySubst + + where + rec sub t1 t2 = + case (leftSpine t1, leftSpine t2) of + ((TVar i,[]), _) -> recVar sub i t2 + (_, (TVar i,[])) -> recVar sub i t1 + ((TCon s, ss), (TCon t, tt)) + | s == t && not (isPhantomTypeSynonym typesynonyms s) -> + recList sub ss tt + | otherwise -> + case expandOneStepOrdered typesynonyms (t1, t2) of + Just (t1', t2') -> + case rec sub t1' t2' of + Left uError -> Left uError + Right (_, sub') -> Right (True, sub') + Nothing -> Left (ConstantClash s t) + + _ -> case (t1, t2) of + (TApp l1 r1, TApp l2 r2) -> recList sub [l1, r1] [l2, r2] + _ -> internalError "Top.Types.Unification" "mguWithTypeSynonyms" "illegal type" + + recVar sub i tp = + case M.lookup i sub of + Just t2 -> + case rec sub tp t2 of + Right (True,sub') -> + let mtp = equalUnderTypeSynonyms typesynonyms (sub' |-> tp) (sub' |-> t2) + in case mtp of + Just newTP -> Right (True,singleSubstitution i newTP @@ removeDom [i] sub') + Nothing -> internalError "Top.Types.Unification" "mguWithTypeSynonyms" "illegal types" + answer -> answer + Nothing -> + case sub |-> tp of + TVar j | i == j -> Right (False, sub) + tp' | i `elem` ftv tp' -> Left (InfiniteType i) + | otherwise -> Right (False, singleSubstitution i tp' @@ sub) + + recList sub [] [] = Right (False,sub) + recList sub (s:ss) (t:tt) = + case rec sub s t of + Left uError -> Left uError + Right (b,sub') -> + case recList sub' ss tt of + Left uError -> Left uError + Right (b',sub'') -> Right (b || b', sub'') + recList _ _ _ = + internalError "Top.Types.Unification" "mguWithTypeSynonyms" "kinds do not match" + +-- |Find the most general type for two types that are equal under type synonyms +-- (i.e., the least number of expansions) +equalUnderTypeSynonyms :: OrderedTypeSynonyms -> Tp -> Tp -> Maybe Tp +equalUnderTypeSynonyms typesynonyms t1 t2 = + case (leftSpine t1,leftSpine t2) of + ((TVar i,[]),(TVar _,[])) -> Just (TVar i) + ((TCon s,ss),(TCon t,tt)) + | s == t && not (isPhantomTypeSynonym typesynonyms s) -> + do let f = uncurry (equalUnderTypeSynonyms typesynonyms) + xs <- mapM f (zip ss tt) + Just (foldl TApp (TCon s) xs) + | otherwise -> + do (t1', t2') <- expandOneStepOrdered typesynonyms (t1, t2) + equalUnderTypeSynonyms typesynonyms t1' t2' + + _ -> Nothing + +-- |Given a set of (ordered) type synonyms, can two types be unified? +unifiable :: OrderedTypeSynonyms -> Tp -> Tp -> Bool +unifiable typesynonyms t1 t2 = + case mguWithTypeSynonyms typesynonyms t1 t2 of + Left _ -> False + Right _ -> True + +-- |Same as unifiable, but takes as input a list of types +unifiableList :: OrderedTypeSynonyms -> Tps -> Bool +unifiableList typesynonyms (t1:t2:ts) = + case mguWithTypeSynonyms typesynonyms t1 t2 of + Left _ -> False + Right (_, sub) -> unifiableList typesynonyms (sub |-> (t2:ts)) +unifiableList _ _ = True diff --git a/src/Top/Util/Embedding.hs b/src/Top/Util/Embedding.hs new file mode 100644 --- /dev/null +++ b/src/Top/Util/Embedding.hs @@ -0,0 +1,41 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +----------------------------------------------------------------------------- + +module Top.Util.Embedding where + +data Embedding a b = Embedding { getE :: a -> b, changeE :: (b -> b) -> a -> a } + +setE :: Embedding a b -> b -> a -> a +setE e = changeE e . const + +withE :: Embedding a b -> (b -> c) -> a -> c +withE e f = f . getE e + +------------------------------ +-- useful embeddings + +idE :: Embedding a a +idE = Embedding { getE = id, changeE = id } + +fstE :: Embedding (a, b) a +fstE = Embedding { getE = fst, changeE = \f (a, b) -> (f a, b) } + +sndE :: Embedding (a, b) b +sndE = Embedding { getE = snd, changeE = \f (a, b) -> (a, f b) } + +------------------------------ +-- compositions of embeddings + +composeE :: Embedding a b -> Embedding b c -> Embedding a c +composeE e1 e2 = Embedding { getE = getE e2 . getE e1, changeE = changeE e1 . changeE e2 } + +fromFstE :: Embedding a c -> Embedding (a, b) c +fromFstE = composeE fstE + +fromSndE :: Embedding b c -> Embedding (a, b) c +fromSndE = composeE sndE diff --git a/src/Top/Util/Empty.hs b/src/Top/Util/Empty.hs new file mode 100644 --- /dev/null +++ b/src/Top/Util/Empty.hs @@ -0,0 +1,30 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +----------------------------------------------------------------------------- + +module Top.Util.Empty where + +------------------------------------------------------------------------ +-- * Empty type class + +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 + +instance Empty a => Empty (Either a b) where + empty = Left empty diff --git a/src/Top/Util/Option.hs b/src/Top/Util/Option.hs new file mode 100644 --- /dev/null +++ b/src/Top/Util/Option.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE RankNTypes #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Top.Util.Option where + +import Control.Monad.State + +option :: a -> String -> Option a +option a s = Option { defaultValue = a, currentValue = a, optionDescription = s } + +data Option a = Option { defaultValue :: a, currentValue :: a, optionDescription :: String } +data OptionAccess m a = Access { getOption :: m a, setOption :: a -> m () } + +ignoreOption :: Monad m => Option a -> OptionAccess m a +ignoreOption value = + Access { getOption = return (currentValue value), setOption = const $ return () } + +optionAccessTrans :: (forall a . m1 a -> m2 a) -> OptionAccess m1 b -> OptionAccess m2 b +optionAccessTrans f oa = + Access { getOption = f (getOption oa), setOption = f . setOption oa } + +useOption :: MonadState s m => (s -> Option a) -> (Option a -> s -> s) -> OptionAccess m a +useOption getter setter = + let f b x = setter ((getter x) { currentValue = b }) x + in Access { getOption = gets (currentValue . getter), setOption = modify . f } + +instance (Show a, Eq a) => Show (Option a) where + show a = + let extra | currentValue a == defaultValue a = " (default)" + | otherwise = "" + in optionDescription a ++ ": " ++ show (currentValue a) ++ extra + +instance Functor Option where + fmap f a = a { defaultValue = f (defaultValue a), currentValue = f (currentValue a) } diff --git a/src/TopSolver.hs b/src/TopSolver.hs new file mode 100644 --- /dev/null +++ b/src/TopSolver.hs @@ -0,0 +1,558 @@ +{-# LANGUAGE UndecidableInstances, OverlappingInstances, FlexibleInstances #-} +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : non-portable (requires extensions) +----------------------------------------------------------------------------- + +module Main where + +import Text.ParserCombinators.Parsec +import qualified Text.ParserCombinators.Parsec.Token as P +import qualified Text.ParserCombinators.Parsec.Language as P +import Top.Constraint +import Top.Types +import Top.Constraint.Information +import Top.Constraint.Qualifier +import Top.Constraint.Equality +import Top.Constraint.Polymorphism (PolymorphismConstraint(..)) +import Top.Interface.TypeInference +import Top.Solver +import Top.Solver.TypeGraph +import Utils (internalError) +import Data.Char (isDigit, isLower) +import Data.List (intercalate, intersperse) +import Data.Maybe +import qualified Data.Map as M +import qualified Data.Set as S +import System.Environment (getArgs) + +--------------------------------------------------------------------- +-- * Top logo + +logo :: [String] +logo = [ "__ __|" + , " | _ \\ _ \\" + , " _|\\___/ .__/" + , " _|" + ] + +--------------------------------------------------------------------- +-- * Top constraint information + +newtype TopInfo = TopInfo [(String, String)] + +instance Show TopInfo where + show (TopInfo xs) + | null xs = "[]" + | otherwise = snd (last xs) + +addTopInfo :: String -> String -> TopInfo -> TopInfo +addTopInfo s1 s2 (TopInfo xs) = TopInfo ((s1, s2) : xs) + +instance TypeConstraintInfo TopInfo where + ambiguousPredicate p = addTopInfo "ambiguous predicate" (show p) + unresolvedPredicate p = addTopInfo "unresolved predicate" (show p) + equalityTypePair pair = addTopInfo "type pair" (show pair) + parentPredicate p = addTopInfo "parent predicate" (show p) + escapedSkolems is = addTopInfo "escaped skolems" (show is) + neverDirective tuple = addTopInfo "never directive" (show tuple) + closeDirective tuple = addTopInfo "close directive" (show tuple) + disjointDirective t1 t2 = addTopInfo "disjoint directive" (show (t1, t2)) + +instance PolyTypeConstraintInfo TopInfo where + instantiatedTypeScheme s = addTopInfo "instantiated type scheme" (show s) + skolemizedTypeScheme s = addTopInfo "skolemized type scheme" (show s) + +--------------------------------------------------------------------- +-- * Top constraints + +type TopQualifiers = Predicates +type TopConstraint = ConstraintSum EqualityConstraint + (ConstraintSum PolymorphismConstraint ExtraConstraint) + TopInfo + +class IsTopConstraint a where + toTopCon :: a -> TopConstraint + +instance IsTopConstraint (EqualityConstraint TopInfo) where + toTopCon = SumLeft + +instance IsTopConstraint (PolymorphismConstraint TopInfo) where + toTopCon = SumRight . SumLeft + +instance IsTopConstraint (ExtraConstraint TopInfo) where + toTopCon = SumRight . SumRight + +--------------------------------------------------------------------- +-- * Top solve monad + +-- type TopExtraState = () --(DependencyState TopInfo, (ImplicitParameterState TopInfo, SubtypingState TopInfo)) +type TopSolve = TG TopInfo --TypeGraphX TopInfo TopQualifiers TopExtraState + {- +instance HasDep TopSolve TopInfo where + depGet = do (_, (_, (_, (x1, _)))) <- getX ; return x1 + depPut x1 = do (a, (b, (c, (_, xr)))) <- getX ; putX (a, (b, (c, (x1, xr)))) + +instance HasIP TopSolve TopInfo where + ipGet = do (_, (_, (_, (_, (x2, _ ))))) <- getX ; return x2 + ipPut x2 = do (a, (b, (c, (x1, (_, xr))))) <- getX ; putX (a, (b, (c, (x1, (x2, xr))))) + +instance HasST TopSolve TopInfo where + stGet = do (_, (_, (_, (_, (_, x3))))) <- getX ; return x3 + stPut x3 = do (a, (b, (c, (x1, (x2, _))))) <- getX ; putX (a, (b, (c, (x1, (x2, x3))))) -} + +--------------------------------------------------------------------- +-- * Top lexer + +lexer :: P.TokenParser () +lexer = P.makeTokenParser + ( P.haskellStyle + { P.reservedOpNames = ["==", "::", "<=", "=>", ":=", "~>", "<:" ] + , P.reservedNames = ["forall", "Generalize", "Instantiate", "Skolemize", "Implicit", + "Prove", "Assume", "MakeConsistent", "LogState", "Stop", + "Declare", {- "Enter", "Leave", "ContextReduction",-} + "Class", "Instance", "Never", "Close", + "Disjoint", "Default" ] + }) + +runLex :: Parser (Constraints TopSolve, Int) -> String -> IO () +runLex p + = run (do { whiteSpace + ; x <- p + ; eof + ; return x + }) + +whiteSpace, comma, dot :: CharParser () () +identifier :: CharParser () String +parens, brackets :: CharParser () a -> CharParser () a +reserved, reservedOp :: String -> CharParser () () + +whiteSpace = P.whiteSpace lexer +comma = void (P.comma lexer) +dot = void (P.dot lexer) +parens = P.parens lexer +brackets = P.brackets lexer +identifier = P.identifier lexer +reserved = P.reserved lexer +reservedOp = P.reservedOp lexer + +--------------------------------------------------------------------- +-- * Top parser and main function + +main :: IO () +main = do args <- getArgs + case args of + [filename] -> + do content <- readFile filename + runLex pStatements content + _ -> do putStrLn "Incorrect number of arguments for topsolver" + putStrLn "Usage: topsolver " + +run :: Parser (Constraints TopSolve, Int) -> String -> IO () +run p input = + case parse p "" input of + Left err -> + do putStr "parse error at " + print err + Right (cset, unique) -> + do putStrLn (unlines logo) + let result :: SolveResult TopInfo + options = solveOptions { uniqueCounter = unique, typeSynonyms = stringAsTypeSynonym } + (result, logm) = solve options cset typegraphConstraintSolverDefault + + print logm + + putStrLn . concat $ + "Substitution: " : intersperse ", " + [ show (i, lookupInt i (substitutionFromResult result)) + | i <- dom (substitutionFromResult result) + ] + + case errorsFromResult result of + [] -> putStrLn "(No errors)" + es -> let nice (info, lab) = + let TopInfo xs = addTopInfo "label" (show lab) info + in "{" ++ intercalate ", " [ a++"="++b | (a, b) <- xs] ++ "}" + in do putStr (unlines (map nice es)) + putStrLn ("(Failed with "++show (length es)++" errors)") + +pStatements :: Parser (Constraints TopSolve, Int) +pStatements = + do xs <- many pStatement + let vars = S.filter (isLower . head) . S.unions . map (either fst fst) $ xs + varmap = M.fromList (zip (S.elems vars) [0..]) + g (Left (_,f)) = liftConstraint (f varmap) + g (Right (_, f)) = f varmap + return (map g xs, S.size vars) + +pStatement :: Parser (Either (Result TopConstraint) (Result (Constraint TopSolve))) +pStatement = + tryList (map (liftM Right) decl ++ [ liftM Left pConstraint ]) + where + decl = [ pOperation {-, pSubtypingRule, pClassDecl, pInstanceDecl, pNeverDecl + , pCloseDecl, pDisjointDecl, pDefaultDecl -} + ] + +--------------------------------------------------------------------- +-- * Top constraint parser + +pConstraint :: Parser (Result TopConstraint) +pConstraint = + do f <- tryList $ + change pEquality : + map change + [ pGeneralize, pInstantiate, pExplicit, pSkolemize, pImplicit + ] ++ + map change + [ pProve, pAssume + ] + info <- pInfo + let (list, fun) = f info + return (S.fromList list, fun) + + where + change parser = + do g <- parser + return $ \info -> + let (a, b) = g info + in (a, toTopCon . b) + + pEquality = + do t1 <- pType + reservedOp "==" + t2 <- pType + return $ \info -> + ( allTypeConstants t1 ++ allTypeConstants t2 + , \varMap -> Equality (applyVarMap varMap t1) (applyVarMap varMap t2) info + ) + + pGeneralize = + do sv <- pSigmaVar + reservedOp ":=" + reserved "Generalize" + (monos, tp) <- parens pMonosType + return $ \info -> + ( sv : allTypeConstants monos ++ allTypeConstants tp + , \varMap -> Generalize (fromMaybe (-1) $ M.lookup sv varMap) (applyVarMap varMap monos, applyVarMap varMap tp) info + ) + + pInstantiate = + do tp <- pType + reservedOp ":=" + reserved "Instantiate" + sigma <- parens pSigma + return $ \info -> + ( allTypeConstants tp ++ either toList allTypeConstants sigma + , \varMap -> Instantiate (applyVarMap varMap tp) (makeSigma varMap sigma) info + ) + + -- explicit instance constraint = instantiate + pExplicit = + do tp <- pType + reservedOp "::" + sigma <- pSigma + return $ \info -> + ( allTypeConstants tp ++ either toList allTypeConstants sigma + , \varMap -> Instantiate (applyVarMap varMap tp) (makeSigma varMap sigma) info + ) + + pSkolemize = + do tp <- pType + reservedOp ":=" + reserved "Skolemize" + (monos, sigma) <- parens $ + do ms <- brackets (commas identifier) + comma + sigma <- pSigma + return (map TCon ms, sigma) + return $ \info -> + ( allTypeConstants tp ++ allTypeConstants monos ++ either toList allTypeConstants sigma + , \varMap -> Skolemize (applyVarMap varMap tp) (applyVarMap varMap monos, makeSigma varMap sigma) info + ) + + pProve = + do reserved "Prove" + q <- parens pPredicate + return $ \info -> + ( allTypeConstants q + , \varMap -> Prove (applyVarMap varMap q) info + ) + + pAssume = + do reserved "Assume" + q <- parens pPredicate + return $ \info -> + ( allTypeConstants q + , \varMap -> Assume (applyVarMap varMap q) info + ) + + pImplicit = + do t1 <- pType + reservedOp ":=" + reserved "Implicit" + (monos, t2) <- parens pMonosType + return $ \info -> + ( allTypeConstants t1 ++ allTypeConstants monos ++ allTypeConstants t2 + , \varMap -> Implicit (applyVarMap varMap t1) (applyVarMap varMap monos, applyVarMap varMap t2) info + ) + +--------------------------------------------------------------------- +-- * Top operation parser + +pOperation :: Parser (Result (Constraint TopSolve)) +pOperation = + let ops = [ --("Enter" , enterGroup) + --, ("Leave" , do qsInfo <- doContextReduction; (_ :: TopQualifiers) <- removeAnnotation qsInfo ; leaveGroup) + ("MakeConsistent" , makeConsistent) + --, ("ContextReduction", do qsInfo <- doContextReduction; (_ :: TopQualifiers) <- removeAnnotation qsInfo; return ()) + -- , ("LogState" , logState) + -- , ("Stop" , do logState; error "***** Stop reached *****") + ] + f (s, a) = do reserved s + return (S.empty, const (operation s a)) + in tryList (map f ops) + +--------------------------------------------------------------------- +-- * Top subtyping rule parser + {- +pSubtypingRule :: Parser (Result (Constraint TopSolve)) +pSubtypingRule = + do reserved lexer "Declare" + (xs, x) <- parens lexer (pContext pSubtyping pSubtyping) + info <- pInfo + let rule = SubtypingRule xs x + vars = filter (isLower . head) . nub . allTypeConstants $ rule + varmap = zip vars [0..] + return $ ([], \_ -> Constraint + (declareSubtypingRule (applyVarMap varmap rule) info, return True, "Declare "++show rule)) -} + +--------------------------------------------------------------------- +-- * Top class/instance declaration parser +{- +pClassDecl :: Parser (Result (Constraint TopSolve)) +pClassDecl = + do reserved lexer "Class" + tuple@(supers, className) <- pContext (identifier lexer) (identifier lexer) + + let f :: TIState info -> TIState info + f s = s { classenv = g (classenv s) } + g = M.insertWith (\(s1,is1) (s2,is2) -> (s1 `union` s2,is1 `union` is2)) className (supers, []) + + return ([], \_ -> operation ("Class "++show tuple) (deselect (modify f))) + +pInstanceDecl :: Parser (Result (Constraint TopSolve)) +pInstanceDecl = + do reserved lexer "Instance" + tuple@(ps, p@(Predicate className _)) <- pContext pPredicate pPredicate + + let vars = filter (isLower . head) . nub . allTypeConstants $ (ps, p) + varmap = zip vars [0..] + tuple' = applyVarMap varmap (p, ps) + + f :: TIState info -> TIState info + f s = s { classenv = g (classenv s) } + g = M.insertWith (\(s1,is1) (s2,is2) -> (s1 `union` s2,is1 `union` is2)) className ([], [tuple']) + + return ([], \_ -> operation ("Instance "++show tuple) (deselect (modify f))) + +pNeverDecl :: Parser (Result (Constraint TopSolve)) +pNeverDecl = + do reserved lexer "Never" + p <- pPredicate + info <- pInfo + + let vars = filter (isLower . head) . nub . allTypeConstants $ p + varmap = zip vars [0..] + p' = applyVarMap varmap p + + return ([], \_ -> operation ("Never " ++ show p ++ " : {" ++ show info ++ "}") (addNeverDirective (p', info))) + +pCloseDecl :: Parser (Result (Constraint TopSolve)) +pCloseDecl = + do reserved lexer "Close" + s <- identifier lexer + info <- pInfo + + return ([], \_ -> operation ("Close " ++ s ++ " : {" ++ show info ++ "}") (addCloseDirective (s, info))) + +pDisjointDecl :: Parser (Result (Constraint TopSolve)) +pDisjointDecl = + do reserved lexer "Disjoint" + ss <- commas (identifier lexer) + info <- pInfo + + return ([], \_ -> operation ("Disjoint " ++ show ss ++ " : {" ++ show info ++ "}") (addDisjointDirective (ss, info))) + +pDefaultDecl :: Parser (Result (Constraint TopSolve)) +pDefaultDecl = + do reserved lexer "Default" + className <- identifier lexer + typeList <- + let single = pType >>= \tp -> return [tp] + more = parens lexer (commas pType) + in tryList [more, single] + info <- pInfo + return ([], \_ -> operation + ("Default " ++ className ++ " (" ++ concat (intersperse "," (map show typeList)) ++ ") : {" ++ show info ++ "}") + ( addDefaultDirective (className, (typeList, info)))) -} + +--------------------------------------------------------------------- +-- * Other parsers + +pInfo :: Parser TopInfo +pInfo = tryList [ withInfo, withoutInfo ] + where + withInfo = + do reservedOp ":" + s <- manyTill anyChar (do { void (char '\n') ; return () } <|> eof) + whiteSpace + return (TopInfo [("msg", s)]) + withoutInfo = + do reservedOp ";" + whiteSpace + return (TopInfo [("msg", "")]) + +pContext :: Parser a -> Parser b -> Parser ([a], b) +pContext p1 p2 = + do as <- tryList [ listContext, singletonContext, emptyContext] + b <- p2 + return (as, b) + where + emptyContext = + return [] + singletonContext = + do a <- p1 + reservedOp "=>" + return [a] + listContext = + do as <- parens (commas p1) + reservedOp "=>" + return as + +pSigma :: Parser (Either String (Scheme TopQualifiers)) +pSigma = try (do s <- pSigmaVar; return (Left s)) + <|> (do s <- pTypeScheme; return (Right s)) + +pSigmaVar :: Parser String +pSigmaVar = do s <- identifier + case s of + 's' : rest | all isDigit rest -> return s + _ -> fail "" + +pTypeScheme :: Parser (Scheme TopQualifiers) +pTypeScheme = do qs <- option [] $ + do reserved "forall" + xs <- many1 identifier + dot + return xs + (pss, tp) <- pContext pOneQualifier pType + let sub = M.fromList (zip qs [10000..]) + return (quantify (M.elems sub) (applyVarMap sub (concat pss) .=>. applyVarMap sub tp)) + +pQualifierList :: Parser TopQualifiers +pQualifierList = + tryList [ liftM concat (parens (commas pOneQualifier)) + , pOneQualifier + ] + +pOneQualifier :: Parser TopQualifiers +pOneQualifier = tryList + [ liftM return pPredicate + --, pDependency >>= (return . toTopQual) + --, pImplicitParameter >>= (return . toTopQual) + --, pSubtyping >>= (return . toTopQual) + , parens pOneQualifier + ] + +pPredicate :: Parser Predicate +pPredicate = + do s <- identifier + tp <- pType2 + return (Predicate s tp) + +{- pDependency :: Parser Dependency +pDependency = + do s <- identifier lexer + symbol lexer "." + t1 <- pType + reservedOp lexer "~>" + t2 <- pType + return (Dependency s t1 t2) -} + +{-pImplicitParameter :: Parser ImplicitParameter +pImplicitParameter = + do reservedOp lexer "?" + s <- identifier lexer + reservedOp lexer "::" + tp <- pType + return (ImplicitParameter s tp) -} + +{- pSubtyping :: Parser Subtyping +pSubtyping = + do t1 <- pType + reservedOp lexer "<:" + t2 <- pType + return (t1 :<: t2) -} + +pType :: Parser Tp +pType = do left <- pType1 + option left $ + do reservedOp "->" + right <- pType + return (left .->. right) + +pType1 :: Parser Tp +pType1 = do tps <- many1 pType2 + return (foldl1 TApp tps) + +pType2 :: Parser Tp +pType2 = tryList [ + do s <- identifier + return (TCon s) + , do tps <- parens (commas pType) + case tps of + [tp] -> return tp + _ -> return (tupleType tps) + , do tp <- brackets pType + return (listType tp) + ] + +pMonosType :: Parser ([Tp], Tp) +pMonosType = do + ms <- brackets (commas identifier) + comma + tp <- pType + return (map TCon ms, tp) + +--------------------------------------------------------------------- +-- * Miscellaneous + +type VarMap = M.Map String Int +type Result a = (S.Set String, VarMap -> a) + +applyVarMap :: HasTypes a => VarMap -> a -> a +applyVarMap varmap = + let f tp = + case tp of + TApp l r -> TApp (f l) (f r) + TCon s -> maybe (TCon s) TVar (M.lookup s varmap) + TVar _ -> tp + in changeTypes f + +commas :: Parser a -> Parser [a] +commas = (`sepBy` comma) + +tryList :: [Parser a] -> Parser a +tryList = foldr1 (<|>) . map try + +toList :: a -> [a] +toList a = [a] + +makeSigma :: VarMap -> Either String (Scheme TopQualifiers) -> Sigma TopQualifiers +makeSigma vm (Left s) = let err = internalError "TopSolver.hs" "makeSigma" "sigma var not in variable map" + in SigmaVar (fromMaybe err $ M.lookup s vm) +makeSigma vm (Right s) = SigmaScheme (applyVarMap vm s) diff --git a/src/Utils.hs b/src/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Utils.hs @@ -0,0 +1,18 @@ +----------------------------------------------------------------------------- +-- | License : GPL +-- +-- Maintainer : helium@cs.uu.nl +-- Stability : provisional +-- Portability : portable +----------------------------------------------------------------------------- + +module Utils (internalError) where + +internalError :: String -> String -> String -> a +internalError moduleName functionName message = + error . unlines $ + [ "" + , "INTERNAL ERROR - " ++ message + , "** Module : " ++ moduleName + , "** Function : " ++ functionName + ]