packages feed

Top (empty) → 1.7

raw patch · 53 files changed

+7285/−0 lines, 53 filesdep +basedep +containersdep +mtlsetup-changed

Dependencies added: base, containers, mtl, parsec

Files

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