diff --git a/COPYING b/COPYING new file mode 100644 --- /dev/null +++ b/COPYING @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The GNU General Public License is a free, copyleft license for +software and other kinds of works. + + The licenses for most software and other practical works are designed +to take away your freedom to share and change the works. By contrast, +the GNU General Public License is intended to guarantee your freedom to +share and change all versions of a program--to make sure it remains free +software for all its users. We, the Free Software Foundation, use the +GNU General Public License for most of our software; it applies also to +any other work released this way by its authors. You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +them if you wish), that you receive source code or can get it if you +want it, that you can change the software or use pieces of it in new +free programs, and that you know you can do these things. + + To protect your rights, we need to prevent others from denying you +these rights or asking you to surrender the rights. Therefore, you have +certain responsibilities if you distribute copies of the software, or if +you modify it: responsibilities to respect the freedom of others. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must pass on to the recipients the same +freedoms that you received. You must make sure that they, too, receive +or can get the source code. And you must show them these terms so they +know their rights. + + Developers that use the GNU GPL protect your rights with two steps: +(1) assert copyright on the software, and (2) offer you this License +giving you legal permission to copy, distribute and/or modify it. + + For the developers' and authors' protection, the GPL clearly explains +that there is no warranty for this free software. For both users' and +authors' sake, the GPL requires that modified versions be marked as +changed, so that their problems will not be attributed erroneously to +authors of previous versions. + + Some devices are designed to deny users access to install or run +modified versions of the software inside them, although the manufacturer +can do so. This is fundamentally incompatible with the aim of +protecting users' freedom to change the software. The systematic +pattern of such abuse occurs in the area of products for individuals to +use, which is precisely where it is most unacceptable. Therefore, we +have designed this version of the GPL to prohibit the practice for those +products. If such problems arise substantially in other domains, we +stand ready to extend this provision to those domains in future versions +of the GPL, as needed to protect the freedom of users. + + Finally, every program is threatened constantly by software patents. +States should not allow patents to restrict development and use of +software on general-purpose computers, but in those that do, we wish to +avoid the special danger that patents applied to a free program could +make it effectively proprietary. To prevent this, the GPL assures that +patents cannot be used to render the program non-free. + + The precise terms and conditions for copying, distribution and +modification follow. + + TERMS AND CONDITIONS + + 0. Definitions. + + "This License" refers to version 3 of the GNU General Public License. + + "Copyright" also means copyright-like laws that apply to other kinds of +works, such as semiconductor masks. + + "The Program" refers to any copyrightable work licensed under this +License. Each licensee is addressed as "you". "Licensees" and +"recipients" may be individuals or organizations. + + To "modify" a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of an +exact copy. The resulting work is called a "modified version" of the +earlier work or a work "based on" the earlier work. + + A "covered work" means either the unmodified Program or a work based +on the Program. + + To "propagate" a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + + To "convey" a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user through +a computer network, with no transfer of a copy, is not conveying. + + An interactive user interface displays "Appropriate Legal Notices" +to the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + + 1. Source Code. + + The "source code" for a work means the preferred form of the work +for making modifications to it. "Object code" means any non-source +form of a work. + + A "Standard Interface" means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + + The "System Libraries" of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +"Major Component", in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + + The "Corresponding Source" for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. + + The Corresponding Source need not include anything that users +can regenerate automatically from other parts of the Corresponding +Source. + + The Corresponding Source for a work in source code form is that +same work. + + 2. Basic Permissions. + + All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + + You may make, run and propagate covered works that you do not +convey, without conditions so long as your license otherwise remains +in force. You may convey covered works to others for the sole purpose +of having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + + Conveying under any other circumstances is permitted solely under +the conditions stated below. Sublicensing is not allowed; section 10 +makes it unnecessary. + + 3. Protecting Users' Legal Rights From Anti-Circumvention Law. + + No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + + When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such circumvention +is effected by exercising rights under this License with respect to +the covered work, and you disclaim any intention to limit operation or +modification of the work as a means of enforcing, against the work's +users, your or third parties' legal rights to forbid circumvention of +technological measures. + + 4. Conveying Verbatim Copies. + + You may convey verbatim copies of the Program's source code as you +receive it, in any medium, provided that you conspicuously and +appropriately publish on each copy an appropriate copyright notice; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + + You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + + 5. Conveying Modified Source Versions. + + You may convey a work based on the Program, or the modifications to +produce it from the Program, in the form of source code under the +terms of section 4, provided that you also meet all of these conditions: + + a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + + b) The work must carry prominent notices stating that it is + released under this License and any conditions added under section + 7. This requirement modifies the requirement in section 4 to + "keep intact all notices". + + c) You must license the entire work, as a whole, under this + License to anyone who comes into possession of a copy. This + License will therefore apply, along with any applicable section 7 + additional terms, to the whole of the work, and all its parts, + regardless of how they are packaged. This License gives no + permission to license the work in any other way, but it does not + invalidate such permission if you have separately received it. + + d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your + work need not make them do so. + + A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +"aggregate" if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + + 6. Conveying Non-Source Forms. + + You may convey a covered work in object code form under the terms +of sections 4 and 5, provided that you also convey the +machine-readable Corresponding Source under the terms of this License, +in one of these ways: + + a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium + customarily used for software interchange. + + b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a + written offer, valid for at least three years and valid for as + long as you offer spare parts or customer support for that product + model, to give anyone who possesses the object code either (1) a + copy of the Corresponding Source for all the software in the + product that is covered by this License, on a durable physical + medium customarily used for software interchange, for a price no + more than your reasonable cost of physically performing this + conveying of source, or (2) access to copy the + Corresponding Source from a network server at no charge. + + c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This + alternative is allowed only occasionally and noncommercially, and + only if you received the object code with such an offer, in accord + with subsection 6b. + + d) Convey the object code by offering access from a designated + place (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) + that supports equivalent copying facilities, provided you maintain + clear directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + + e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + + A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + + A "User Product" is either (1) a "consumer product", which means any +tangible personal property which is normally used for personal, family, +or household purposes, or (2) anything designed or sold for incorporation +into a dwelling. In determining whether a product is a consumer product, +doubtful cases shall be resolved in favor of coverage. For a particular +product received by a particular user, "normally used" refers to a +typical or common use of that class of product, regardless of the status +of the particular user or of the way in which the particular user +actually uses, or expects or is expected to use, the product. A product +is a consumer product regardless of whether the product has substantial +commercial, industrial or non-consumer uses, unless such uses represent +the only significant mode of use of the product. + + "Installation Information" for a User Product means any methods, +procedures, authorization keys, or other information required to install +and execute modified versions of a covered work in that User Product from +a modified version of its Corresponding Source. The information must +suffice to ensure that the continued functioning of the modified object +code is in no case prevented or interfered with solely because +modification has been made. + + If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + + The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or updates +for a work that has been modified or installed by the recipient, or for +the User Product in which it has been modified or installed. Access to a +network may be denied when the modification itself materially and +adversely affects the operation of the network or violates the rules and +protocols for communication across the network. + + Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + 7. Additional Terms. + + "Additional permissions" are terms that supplement the terms of this +License by making exceptions from one or more of its conditions. +Additional permissions that are applicable to the entire Program shall +be treated as though they were included in this License, to the extent +that they are valid under applicable law. If additional permissions +apply only to part of the Program, that part may be used separately +under those permissions, but the entire Program remains governed by +this License without regard to the additional permissions. + + When you convey a copy of a covered work, you may at your option +remove any additional permissions from that copy, or from any part of +it. (Additional permissions may be written to require their own +removal in certain cases when you modify the work.) You may place +additional permissions on material, added by you to a covered work, +for which you have or can give appropriate copyright permission. + + Notwithstanding any other provision of this License, for material you +add to a covered work, you may (if authorized by the copyright holders of +that material) supplement the terms of this License with terms: + + a) Disclaiming warranty or limiting liability differently from the + terms of sections 15 and 16 of this License; or + + b) Requiring preservation of specified reasonable legal notices or + author attributions in that material or in the Appropriate Legal + Notices displayed by works containing it; or + + c) Prohibiting misrepresentation of the origin of that material, or + requiring that modified versions of such material be marked in + reasonable ways as different from the original version; or + + d) Limiting the use for publicity purposes of names of licensors or + authors of the material; or + + e) Declining to grant rights under trademark law for use of some + trade names, trademarks, or service marks; or + + f) Requiring indemnification of licensors and authors of that + material by anyone who conveys the material (or modified versions of + it) with contractual assumptions of liability to the recipient, for + any liability that these contractual assumptions directly impose on + those licensors and authors. + + All other non-permissive additional terms are considered "further +restrictions" within the meaning of section 10. If the Program as you +received it, or any part of it, contains a notice stating that it is +governed by this License along with a term that is a further +restriction, you may remove that term. If a license document contains +a further restriction but permits relicensing or conveying under this +License, you may add to a covered work material governed by the terms +of that license document, provided that the further restriction does +not survive such relicensing or conveying. + + If you add terms to a covered work in accord with this section, you +must place, in the relevant source files, a statement of the +additional terms that apply to those files, or a notice indicating +where to find the applicable terms. + + Additional terms, permissive or non-permissive, may be stated in the +form of a separately written license, or stated as exceptions; +the above requirements apply either way. + + 8. Termination. + + You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + + However, if you cease all violation of this License, then your +license from a particular copyright holder is reinstated (a) +provisionally, unless and until the copyright holder explicitly and +finally terminates your license, and (b) permanently, if the copyright +holder fails to notify you of the violation by some reasonable means +prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + + Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + + 9. Acceptance Not Required for Having Copies. + + You are not required to accept this License in order to receive or +run a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + + 10. Automatic Licensing of Downstream Recipients. + + Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + + An "entity transaction" is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + + You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + + 11. Patents. + + A "contributor" is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's "contributor version". + + A contributor's "essential patent claims" are all patent claims +owned or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, "control" includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + + Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + + In the following three paragraphs, a "patent license" is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To "grant" such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + + If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. "Knowingly relying" means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + + If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + + A patent license is "discriminatory" if it does not include within +the scope of its coverage, prohibits the exercise of, or is +conditioned on the non-exercise of one or more of the rights that are +specifically granted under this License. You may not convey a covered +work if you are a party to an arrangement with a third party that is +in the business of distributing software, under which you make payment +to the third party based on the extent of your activity of conveying +the work, and under which the third party grants, to any of the +parties who would receive the covered work from you, a discriminatory +patent license (a) in connection with copies of the covered work +conveyed by you (or copies made from those copies), or (b) primarily +for and in connection with specific products or compilations that +contain the covered work, unless you entered into that arrangement, +or that patent license was granted, prior to 28 March 2007. + + Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + + 12. No Surrender of Others' Freedom. + + If conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot convey a +covered work so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you may +not convey it at all. For example, if you agree to terms that obligate you +to collect a royalty for further conveying from those to whom you convey +the Program, the only way you could satisfy both those terms and this +License would be to refrain entirely from conveying the Program. + + 13. Use with the GNU Affero General Public License. + + Notwithstanding any other provision of this License, you have +permission to link or combine any covered work with a work licensed +under version 3 of the GNU Affero General Public License into a single +combined work, and to convey the resulting work. The terms of this +License will continue to apply to the part which is the covered work, +but the special requirements of the GNU Affero General Public License, +section 13, concerning interaction through a network will apply to the +combination as such. + + 14. Revised Versions of this License. + + The Free Software Foundation may publish revised and/or new versions of +the GNU General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + + Each version is given a distinguishing version number. If the +Program specifies that a certain numbered version of the GNU General +Public License "or any later version" applies to it, you have the +option of following the terms and conditions either of that numbered +version or of any later version published by the Free Software +Foundation. If the Program does not specify a version number of the +GNU General Public License, you may choose any version ever published +by the Free Software Foundation. + + If the Program specifies that a proxy can decide which future +versions of the GNU General Public License can be used, that proxy's +public statement of acceptance of a version permanently authorizes you +to choose that version for the Program. + + Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + + 15. Disclaimer of Warranty. + + THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY +APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT +HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY +OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM +IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF +ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. Limitation of Liability. + + IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS +THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY +GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE +USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF +DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD +PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), +EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF +SUCH DAMAGES. + + 17. Interpretation of Sections 15 and 16. + + If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +state the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + + Copyright (C) + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see . + +Also add information on how to contact you by electronic and paper mail. + + If the program does terminal interaction, make it output a short +notice like this when it starts in an interactive mode: + + Copyright (C) + This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the appropriate +parts of the General Public License. Of course, your program's commands +might be different; for a GUI interface, you would use an "about box". + + You should also get your employer (if you work as a programmer) or school, +if any, to sign a "copyright disclaimer" for the program, if necessary. +For more information on this, and how to apply and follow the GNU GPL, see +. + + The GNU General Public License does not permit incorporating your program +into proprietary programs. If your program is a subroutine library, you +may consider it more useful to permit linking proprietary applications with +the library. If this is what you want to do, use the GNU Lesser General +Public License instead of this License. But first, please read +. diff --git a/Language/Symantic.hs b/Language/Symantic.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic.hs @@ -0,0 +1,17 @@ +module Language.Symantic + ( module Language.Symantic.Typing + , module Language.Symantic.Compiling + , module Language.Symantic.Interpreting + , module Language.Symantic.Transforming + -- * Re-exports for convenience. + , module Language.Symantic.Grammar.Fixity + , module Language.Symantic.Grammar.Meta + ) where + +import Language.Symantic.Typing +import Language.Symantic.Compiling +import Language.Symantic.Interpreting +import Language.Symantic.Transforming + +import Language.Symantic.Grammar.Fixity +import Language.Symantic.Grammar.Meta diff --git a/Language/Symantic/Compiling.hs b/Language/Symantic/Compiling.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Compiling.hs @@ -0,0 +1,14 @@ +-- | Compiling terms. +module Language.Symantic.Compiling + ( module Language.Symantic.Compiling.Term + , module Language.Symantic.Compiling.Module + , module Language.Symantic.Compiling.Grammar + , module Language.Symantic.Compiling.Beta + , module Language.Symantic.Compiling.Read + ) where + +import Language.Symantic.Compiling.Term +import Language.Symantic.Compiling.Module +import Language.Symantic.Compiling.Grammar +import Language.Symantic.Compiling.Beta +import Language.Symantic.Compiling.Read diff --git a/Language/Symantic/Compiling/Beta.hs b/Language/Symantic/Compiling/Beta.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Compiling/Beta.hs @@ -0,0 +1,80 @@ +-- | Beta-reduction of 'Term's. +module Language.Symantic.Compiling.Beta where + +import Control.Arrow (left) +import qualified Data.Kind as K + +import Language.Symantic.Grammar +import Language.Symantic.Typing +import Language.Symantic.Compiling.Term + +-- | Term application: apply second given 'TermT' to the first, +-- applying embedded 'TeSym's, or return an error. +betaTerm :: + forall src ss es vs fun arg. + Inj_Source (TypeVT src) src => + Constable (->) => + Term src ss es vs (fun::K.Type) -> + Term src ss es vs (arg::K.Type) -> + Either (Error_Beta src) (TermT src ss es vs) +betaTerm (Term qf tf (TeSym te_fun)) (Term qa ta (TeSym te_arg)) = + case tf of + TyApp _ (TyApp _ a2b a2b_a) a2b_b + | Just HRefl <- proj_ConstKiTy @(K (->)) @(->) a2b -> + case a2b_a `eqType` ta of + Nothing -> Left $ Error_Beta_Type_mismatch (TypeVT a2b_a) (TypeVT ta) + Just Refl -> + Right $ + case (proveConstraint qf, proveConstraint qa) of + -- NOTE: remove provable Constraints to keep those smaller. + (Just Dict, Just Dict) -> TermT $ Term (noConstraintLen (lenVars a2b_b)) a2b_b $ + TeSym $ \c -> te_fun c `app` te_arg c + (Just Dict, Nothing) -> TermT $ Term qa a2b_b $ + TeSym $ \c -> te_fun c `app` te_arg c + (Nothing, Just Dict) -> TermT $ Term qf a2b_b $ + TeSym $ \c -> te_fun c `app` te_arg c + (Nothing, Nothing) -> TermT $ Term (qf # qa) a2b_b $ + TeSym $ \c -> te_fun c `app` te_arg c + _ -> Left $ Error_Beta_Term_not_a_function $ TypeVT (qf #> tf) + +-- | Collapse given 'BinTree' of 'TermVT's to compute a resulting 'TermVT', if possible. +betaTerms :: + Inj_Source (TypeVT src) src => + Constable (->) => + BinTree (TermVT src ss es) -> + Either (Error_Beta src) (TermVT src ss es) +betaTerms t = + collapseBT (\acc ele -> do + TermVT (Term qf tf te_fun) <- acc + TermVT (Term qa ta te_arg) <- ele + let (tf', ta') = appendVars tf ta + let (qf', qa') = appendVars qf qa + case unTyFun tf' of + Nothing -> Left $ Error_Beta_Term_not_a_function $ TypeVT tf' + Just (af, _rf) -> do + mgu <- + (Error_Beta_Unify `left`) $ + case (unQualsTy af, unQualsTy ta') of + (TypeK af', TypeK ta'') -> unifyType mempty af' ta'' + let qf'' = subst mgu qf' + let qa'' = subst mgu qa' + let tf'' = subst mgu tf' + let ta'' = subst mgu ta' + TermT (Term qr tr te_res) <- betaTerm (Term qf'' tf'' te_fun) (Term qa'' ta'' te_arg) + normalizeVarsTy (qr #> tr) $ \(TyApp _ (TyApp _ _c qr') tr') -> + Right $ TermVT $ Term qr' tr' te_res + ) (Right <$> t) + +-- * Type 'Error_Beta' +data Error_Beta src + = Error_Beta_Term_not_a_function (TypeVT src) + | Error_Beta_Type_mismatch (TypeVT src) (TypeVT src) + | Error_Beta_Unify (Error_Unify src) + -- ^ Cannot unify the expected 'Type' of the argument of the function, + -- with the 'Type' of the argument. + deriving (Eq, Show) + +instance Inj_Error (Error_Beta src) (Error_Beta src) where + inj_Error = id +instance Inj_Error (Error_Unify src) (Error_Beta src) where + inj_Error = Error_Beta_Unify diff --git a/Language/Symantic/Compiling/Grammar.hs b/Language/Symantic/Compiling/Grammar.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Compiling/Grammar.hs @@ -0,0 +1,370 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE UndecidableInstances #-} +module Language.Symantic.Compiling.Grammar where + +import Control.Arrow (left) +import Control.Monad (void) +import Data.Proxy (Proxy(..)) +import Data.Semigroup (Semigroup(..)) +import Prelude hiding (mod, not, any) +import qualified Data.Char as Char +import qualified Data.Function as Fun +import qualified Data.Map.Strict as Map +import qualified Data.Text as Text + +import Language.Symantic.Grammar +import Language.Symantic.Typing +import Language.Symantic.Compiling.Module + +-- * Class 'Gram_Name' +class + ( Gram_Terminal g + , Gram_Rule g + , Gram_Alt g + , Gram_Try g + , Gram_App g + , Gram_AltApp g + , Gram_RegL g + , Gram_CF g + , Gram_Comment g + , Gram_Op g + ) => Gram_Name g where + g_mod_path :: CF g PathMod + g_mod_path = rule "mod_path" $ + infixrG + (pure <$> g_mod_name) + (op <$ char '.') + where op = (<>) + g_mod_name :: CF g NameMod + g_mod_name = rule "mod_name" $ + (NameMod . Text.pack <$>) $ + (identG `minus`) $ + Fun.const + <$> g_term_keywords + <*. (any `but` g_term_idname_tail) + where + identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail) + headG = unicat $ Unicat Char.UppercaseLetter + + g_term_mod_name :: CF g (Mod NameTe) + g_term_mod_name = rule "term_mod_name" $ + lexeme $ + g_term_mod_idname <+> + parens g_term_mod_opname + g_term_name :: CF g NameTe + g_term_name = rule "term_name" $ + lexeme $ + g_term_idname <+> + parens g_term_opname + + g_term_mod_idname :: CF g (Mod NameTe) + g_term_mod_idname = rule "term_mod_idname" $ + Mod + <$> option [] (try $ g_mod_path <* char '.') + <*> g_term_idname + g_term_idname :: CF g NameTe + g_term_idname = rule "term_idname" $ + (NameTe . Text.pack <$>) $ + (identG `minus`) $ + Fun.const + <$> g_term_keywords + <*. (any `but` g_term_idname_tail) + where + identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail) + headG = unicat $ Unicat_Letter + g_term_idname_tail :: Terminal g Char + g_term_idname_tail = rule "term_idname_tail" $ + unicat Unicat_Letter <+> + unicat Unicat_Number + g_term_keywords :: Reg rl g String + g_term_keywords = rule "term_keywords" $ + choice $ string <$> ["in", "let"] + + g_term_mod_opname :: CF g (Mod NameTe) + g_term_mod_opname = rule "term_mod_opname" $ + Mod + <$> option [] (try $ g_mod_path <* char '.') + <*> g_term_opname + g_term_opname :: CF g NameTe + g_term_opname = rule "term_opname" $ + (NameTe . Text.pack <$>) $ + (symG `minus`) $ + Fun.const + <$> g_term_keysyms + <*. (any `but` g_term_opname_ok) + where + symG = some $ cf_of_Terminal g_term_opname_ok + g_term_opname_ok :: Terminal g Char + g_term_opname_ok = rule "term_opname_ok" $ + choice (unicat <$> + [ Unicat_Symbol + , Unicat_Punctuation + , Unicat_Mark + ]) `but` koG + where + koG = choice (char <$> ['(', ')', '`', '\'', ',', '[', ']']) + g_term_keysyms :: Reg rl g String + g_term_keysyms = rule "term_keysyms" $ + choice $ string <$> ["\\", "->", "=", "@"] + +deriving instance Gram_Name g => Gram_Name (CF g) +instance Gram_Name EBNF +instance Gram_Name RuleEBNF + +-- * Class 'Gram_Term_Type' +class + ( Gram_Terminal g + , Gram_Rule g + , Gram_Alt g + , Gram_AltApp g + , Gram_App g + , Gram_CF g + , Gram_Comment g + , Gram_Name g + , Gram_Type src g + ) => Gram_Term_Type src g where + g_term_abst_decl :: CF g (NameTe, AST_Type src) + g_term_abst_decl = rule "term_abst_decl" $ + parens $ (,) + <$> g_term_name + <* (symbol "::" <+> symbol ":") + -- NOTE: "::" is Haskell compatibility and ":" is another common notation. + <*> g_type + +deriving instance Gram_Term_Type src g => Gram_Term_Type src (CF g) +instance Gram_Source src EBNF => Gram_Term_Type src EBNF +instance Gram_Source src RuleEBNF => Gram_Term_Type src RuleEBNF + +-- ** Type 'Error_Term_Gram' +data Error_Term_Gram + = Error_Term_Gram_Fixity Error_Fixity + | Error_Term_Gram_Term_incomplete + | Error_Term_Gram_Type_applied_to_nothing + | Error_Term_Gram_not_applicable + | Error_Term_Gram_application + | Error_Term_Gram_application_mismatch + | Error_Term_Gram_Module Error_Module + deriving (Eq, Show) + +-- * Class 'Gram_Term' +class + ( Gram_Source src g + , Gram_Error Error_Term_Gram g + , Gram_Terminal g + , Gram_Rule g + , Gram_Alt g + , Gram_App g + , Gram_AltApp g + , Gram_CF g + , Gram_Comment g + , Gram_Type src g + , Gram_Name g + , Gram_Term_Type src g + , Gram_Term_Atoms src ss g + , Gram_State (Imports, Modules src ss) g + ) => Gram_Term src ss g where + g_term :: CF g (AST_Term src ss) + g_term = rule "term" $ + choice + [ try g_term_abst + , g_term_operators + , g_term_let + ] + g_term_operators :: CF g (AST_Term src ss) + g_term_operators = rule "term_operators" $ + g_catch $ + left Error_Term_Gram_Fixity <$> + g_ops + where + g_ops :: CF g (Either Error_Fixity (AST_Term src ss)) + g_ops = operators g_term_atom g_prefix g_infix g_postfix + g_prefix :: CF g (Unifix, AST_Term src ss -> AST_Term src ss) + g_infix :: CF g (Infix, AST_Term src ss -> AST_Term src ss -> AST_Term src ss) + g_postfix :: CF g (Unifix, AST_Term src ss -> AST_Term src ss) + g_prefix = g_catch $ g_source $ g_get_after $ op_prefix <$> g_prefix_op + g_infix = g_catch $ g_source $ g_get_after $ op_infix <$> g_infix_op + g_postfix = g_catch $ g_source $ g_get_after $ op_postfix <$> g_postfix_op + op_infix + :: Mod NameTe + -> (Imports, Modules src ss) + -> src + -> Either Error_Term_Gram + (Infix, AST_Term src ss -> AST_Term src ss -> AST_Term src ss) + op_infix name (imps, mods) src = do + t <- Error_Term_Gram_Module `left` + lookupDefTerm FixitySing_Infix imps name mods + Right $ (token_fixity t,) $ \a b -> + (BinTree0 (token_term t src) `BinTree2` a) `BinTree2` b + op_prefix, op_postfix + :: Mod NameTe + -> (Imports, Modules src ss) + -> src + -> Either Error_Term_Gram + ( Unifix + , AST_Term src ss -> AST_Term src ss ) + op_prefix name (imps, mods) src = do + t <- Error_Term_Gram_Module `left` + lookupDefTerm FixitySing_Prefix imps name mods + Right $ (token_fixity t,) $ \a -> + BinTree0 (token_term t src) `BinTree2` a + op_postfix name (imps, mods) src = do + t <- Error_Term_Gram_Module `left` + lookupDefTerm FixitySing_Postfix imps name mods + Right $ (token_fixity t,) $ \a -> + BinTree0 (token_term t src) `BinTree2` a + g_postfix_op :: CF g (Mod NameTe) + g_postfix_op = rule "term_op_postfix" $ + lexeme $ + g_backquote *> g_term_mod_idname <+> -- <* (cf_of_Terminal $ Gram.Term (pure ' ') `but` g_backquote) + g_term_mod_opname + g_infix_op :: CF g (Mod NameTe) + g_infix_op = rule "term_op_infix" $ + lexeme $ + between g_backquote g_backquote g_term_mod_idname <+> + try (Fun.const <$> g_term_mod_opname <*> (string " " <+> string "\n")) <+> + pure (Mod [] " ") + g_prefix_op :: CF g (Mod NameTe) + g_prefix_op = rule "term_op_prefix" $ + lexeme $ + g_term_mod_idname <* g_backquote <+> + g_term_mod_opname + g_backquote :: Gram_Terminal g' => g' Char + g_backquote = char '`' + + g_term_atom :: CF g (AST_Term src ss) + g_term_atom = rule "term_atom" $ + choice $ + {-(try ( + g_source $ + (\typ src -> BinTree0 $ inj_EToken src $ Token_Term_Type typ) + <$ char '@' <*> g_type) :) $ + -} + (try <$> g_term_atomsR @_ @_ @ss) <> + [ try $ + g_catch $ g_source $ g_get_after $ + (\m (imps, mods) src -> + case lookupDefTerm FixitySing_Infix imps m mods of + Right t -> Right $ BinTree0 $ token_term t src + Left err -> + case m of + [] `Mod` n -> Right $ BinTree0 $ Token_Term_Var src n + _ -> Left $ Error_Term_Gram_Module err + ) <$> g_term_mod_name + , g_term_group + ] + g_term_group :: CF g (AST_Term src ss) + g_term_group = rule "term_group" $ parens g_term + g_term_abst :: CF g (AST_Term src ss) + g_term_abst = rule "term_abst" $ + g_source $ + ((\(xs, te) src -> + foldr (\(x, ty_x) -> + BinTree0 . Token_Term_Abst src x ty_x) te xs) <$>) $ + g_term_abst_args_body + (symbol "\\" *> some g_term_abst_decl <* symbol "->") + g_term + g_term_abst_args_body + :: CF g [(NameTe, AST_Type src)] + -> CF g (AST_Term src ss) + -> CF g ([(NameTe, AST_Type src)], AST_Term src ss) + -- g_term_abst_args_body args body = (,) <$> args <*> body + g_term_abst_args_body cf_args cf_body = + g_state_before $ + (\a b (imps::Imports, mods::Modules src ss) -> ((imps, mods), (a, b))) + <$> g_state_after ((<$> cf_args) $ \args (imps::Imports, Modules mods) -> + ((imps, Modules $ Map.alter (setArgs args) [] mods), args)) + <*> cf_body + where + setArgs args = \case + Nothing -> Just $ moduleEmpty {module_infix = insArg mempty args} + Just mod -> Just $ mod + { module_prefix = delArg (module_prefix mod) args + , module_infix = insArg (module_infix mod) args + , module_postfix = delArg (module_postfix mod) args + } + delArg :: ModuleFixy src ss Unifix -> [(NameTe, _a)] -> ModuleFixy src ss Unifix + delArg = foldr $ \(n, _) -> Map.delete n + insArg :: ModuleFixy src ss Infix -> [(NameTe, _a)] -> ModuleFixy src ss Infix + insArg = foldr $ \(n, _) -> + Map.insert n Tokenizer + { token_term = (`Token_Term_Var` n) + , token_fixity = infixN5 + } + g_term_let :: CF g (AST_Term src ss) + g_term_let = rule "term_let" $ + g_source $ + (\name args bound body src -> + BinTree0 $ + Token_Term_Let src name + (foldr (\(x, ty_x) -> + BinTree0 . Token_Term_Abst src x ty_x) bound args) body) + <$ symbol "let" + <*> g_term_name + <*> many g_term_abst_decl + <* symbol "=" + <*> g_term + <* symbol "in" + <*> g_term + +deriving instance + ( Gram_Term src ss g + , Gram_Term_Atoms src ss (CF g) + ) => Gram_Term src ss (CF g) +instance + ( Gram_Term_Atoms src ss EBNF + , Gram_Source src EBNF + ) => Gram_Term src ss EBNF +instance + ( Gram_Term_Atoms src ss RuleEBNF + , Gram_Source src RuleEBNF + ) => Gram_Term src ss RuleEBNF + +-- ** Class 'Gram_Term_Atoms' +type Gram_Term_Atoms src ss g = Gram_Term_AtomsR src ss ss g + +-- *** Class 'Gram_Term_AtomsR' +class Gram_Term_AtomsR src (ss::[*]) (rs::[*]) g where + g_term_atomsR :: [CF g (AST_Term src ss)] +instance Gram_Term_AtomsR src ss '[] g where + g_term_atomsR = [] +instance + ( Gram_Term_AtomsFor src ss g t + , Gram_Term_AtomsR src ss rs g + ) => Gram_Term_AtomsR src ss (Proxy t ': rs) g where + g_term_atomsR = + g_term_atomsFor @_ @_ @_ @t <> + g_term_atomsR @_ @_ @rs + +-- *** Class 'Gram_Term_AtomsFor' +class Gram_Term_AtomsFor src ss g t where + g_term_atomsFor :: [CF g (AST_Term src ss)] + g_term_atomsFor = [] + +gram_term + :: forall g. + ( Gram_Term () '[Proxy (->), Proxy Integer] g + ) => [CF g ()] +gram_term = + [ voiD g_term + , voiD g_term_operators + , voiD g_term_atom + , voiD g_term_group + , voiD g_term_abst + , void (g_term_abst_decl::CF g (NameTe, AST_Type ())) + , voiD g_term_let + , void g_term_mod_name + , void g_term_name + , void g_term_idname + , void $ cf_of_Terminal g_term_idname_tail + , void $ cf_of_Reg g_term_keywords + , void g_term_mod_opname + , void g_term_opname + , void $ cf_of_Terminal g_term_opname_ok + , void $ cf_of_Reg g_term_keysyms + ] where + voiD :: CF g (AST_Term () '[Proxy (->), Proxy Integer]) -> CF g () + voiD = (() <$) diff --git a/Language/Symantic/Compiling/Module.hs b/Language/Symantic/Compiling/Module.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Compiling/Module.hs @@ -0,0 +1,383 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE UndecidableInstances #-} +module Language.Symantic.Compiling.Module where + +import Data.Bool (not) +import Data.Map.Strict (Map) +import Data.Semigroup (Semigroup(..)) +import Data.Set (Set) +import Data.String (IsString(..)) +import Data.Text (Text) +import Prelude hiding (mod, not, any) +import qualified Data.Kind as K +import qualified Data.Map.Strict as Map + +import Language.Symantic.Grammar +import Language.Symantic.Typing +import Language.Symantic.Compiling.Term + +-- * Type 'Mod' +data Mod a = Mod PathMod a + deriving (Eq, Functor, Ord, Show) + +-- ** Type 'PathMod' +type PathMod = [NameMod] + +-- ** Type 'NameMod' +newtype NameMod = NameMod Text + deriving (Eq, Ord, Show) +instance IsString NameMod where + fromString = NameMod . fromString + +-- * Class 'ModuleFor' +class ModuleFor src ss s where + moduleFor :: (PathMod, Module src ss) + moduleFor = ([], moduleEmpty) + +-- * Type 'Imports' +newtype Imports = Imports (Map PathMod (Map PathMod FilterImports)) + deriving (Eq, Show) +type FilterImports = Maybe (Set NameTe) + +importQualifiedAs :: PathMod -> Modules src ss -> Imports +importQualifiedAs as (Modules mods) = Imports $ Map.fromList [(as, Nothing <$ mods)] + +-- * Type 'Modules' +newtype Modules src ss + = Modules + { modules :: Map PathMod (Module src ss) + } deriving (Eq, Show) + +unionModules :: Modules src ss -> Modules src ss -> Either Error_Module (Modules src ss) +unionModules mx@(Modules x) my@(Modules y) = + case check x y of + Just err -> Left err + Nothing -> Right $ unionModulesUnchecked mx my + where + check :: + Map PathMod (Module src ss) -> + Map PathMod (Module src ss) -> + Maybe Error_Module + check x' y' = + case Map.intersectionWith (,) x' y' of + xy | null xy -> Nothing + xy -> + let errs = + Map.filter (not . null) $ + (<$> xy) $ \(a, b) -> + inter a b module_prefix <> + inter a b module_infix <> + inter a b module_postfix in + case errs of + e | null e -> Nothing + e -> Just $ Error_Module_colliding_Term e + where + inter a b f = Map.keysSet $ Map.intersection (f a) (f b) + +unionModulesUnchecked :: Modules src ss -> Modules src ss -> Modules src ss +unionModulesUnchecked (Modules x) (Modules y) = + Modules $ Map.unionWith (<>) x y + +-- ** Type 'Error_Module' +data Error_Module + = Error_Module_colliding_Term (Map PathMod (Set NameTe)) + | Error_Module_ambiguous (Mod NameTe) (Map PathMod NameTe) + | Error_Module_missing PathMod + | Error_Module_missing_Term (Mod NameTe) + deriving (Eq, Show) + +-- ** Type 'Module' +data Module src ss + = Module + { module_prefix :: ModuleFixy src ss Unifix + , module_infix :: ModuleFixy src ss Infix + , module_postfix :: ModuleFixy src ss Unifix + } deriving (Eq, Show) + +module_fixity :: FixitySing fixy -> Module src ss -> ModuleFixy src ss fixy +module_fixity = \case + FixitySing_Prefix -> module_prefix + FixitySing_Infix -> module_infix + FixitySing_Postfix -> module_postfix + +moduleEmpty :: Module src ss +moduleEmpty = Module + { module_prefix = mempty + , module_infix = mempty + , module_postfix = mempty + } + +moduleWhere :: forall src ss. Source src => PathMod -> [DefTerm src ss] -> (PathMod, Module src ss) +moduleWhere mod lst = + (mod,) Module + { module_infix = mk $ \(n `WithFixity` fixy := t) -> + case fixy of + Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermAVT t))] + _ -> [] + , module_prefix = mk $ \(n `WithFixity` fixy := t) -> + case fixy of + Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermAVT t))] + _ -> [] + , module_postfix = mk $ \(n `WithFixity` fixy := t) -> + case fixy of + Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermAVT t))] + _ -> [] + } + where + mk :: + (DefTerm src ss -> [(NameTe, Tokenizer fixy src ss)]) -> + Map NameTe (Tokenizer fixy src ss) + mk = Map.fromList . (`foldMap` lst) + +-- *** Type 'ModuleFixy' +type ModuleFixy src ss fixy = Map NameTe (Tokenizer fixy src ss) + +instance Semigroup (Module src ss) where + x <> y = + Module + { module_prefix = module_prefix x <> module_prefix y + , module_infix = module_infix x <> module_infix y + , module_postfix = module_postfix x <> module_postfix y + } + +-- ** Type 'Tokenizer' +data Tokenizer fixy src ss + = Tokenizer + { token_fixity :: fixy + , token_term :: src -> Token_Term src ss + } +instance (Source src, Eq fixy) => Eq (Tokenizer fixy src ss) where + Tokenizer fx x == Tokenizer fy y = fx == fy && (x noSource) == (y noSource) +instance Source src => Show (Tokenizer fixy src ss) where + show (Tokenizer _fx x) = show (x noSource) + +-- ** Type 'Token_Term' +data Token_Term src ss + = Token_Term (TermAVT src ss) + | Token_TermVT (TermVT src ss '[]) + | Token_Term_Abst src NameTe (AST_Type src) (AST_Term src ss) + | Token_Term_Var src NameTe + | Token_Term_Let src NameTe (AST_Term src ss) (AST_Term src ss) + | Token_Term_App src + -- deriving (Eq, Show) +instance Source src => Eq (Token_Term src ss) where + Token_Term x == Token_Term y = x == y + Token_TermVT x == Token_TermVT y = x == y + Token_Term_Abst _ nx ax rx == Token_Term_Abst _ ny ay ry = nx == ny && ax == ay && rx == ry + Token_Term_Var _ x == Token_Term_Var _ y = x == y + Token_Term_Let _ nx ax rx == Token_Term_Let _ ny ay ry = nx == ny && ax == ay && rx == ry + Token_Term_App _ == Token_Term_App _ = True + _ == _ = False +instance Source src => Show (Token_Term src ss) where + showsPrec p (Token_Term x) = + showParen (p >= 10) $ + showString "Token_Term" . + showChar ' ' . showsPrec 10 x + showsPrec p (Token_TermVT x) = + showParen (p >= 10) $ + showString "Token_TermVT" . + showChar ' ' . showsPrec 10 x + showsPrec p (Token_Term_Abst _ n a r) = + showParen (p >= 10) $ + showString "Token_Term_Abst" . + showChar ' ' . showsPrec 10 n . + showChar ' ' . showsPrec 10 a . + showChar ' ' . showsPrec 10 r + showsPrec p (Token_Term_Var _ x) = + showParen (p >= 10) $ + showString "Token_Term_Var" . + showChar ' ' . showsPrec 10 x + showsPrec p (Token_Term_Let _ n a r) = + showParen (p >= 10) $ + showString "Token_Term_Let" . + showChar ' ' . showsPrec 10 n . + showChar ' ' . showsPrec 10 a . + showChar ' ' . showsPrec 10 r + showsPrec _p (Token_Term_App _) = showString "Token_Term_App" + +-- ** Type 'NameTe' +newtype NameTe = NameTe Text + deriving (Eq, Ord, Show) +instance IsString NameTe where + fromString = NameTe . fromString + +-- * Type 'CtxTy' +-- | /Typing context/ +-- accumulating at each /lambda abstraction/ +-- the 'Type' of the introduced variable. +-- It is built top-down from the closest +-- including /lambda abstraction/ to the farest. +data CtxTy src (ts::[K.Type]) where + CtxTyZ :: CtxTy src '[] + CtxTyS :: NameTe + -> Type src '[] t + -> CtxTy src ts + -> CtxTy src (t ': ts) +infixr 5 `CtxTyS` + +appendCtxTy + :: CtxTy src ts0 + -> CtxTy src ts1 + -> CtxTy src (ts0 ++ ts1) +appendCtxTy CtxTyZ c = c +appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c' + + + +-- ** Type 'AST_Term' +-- | /Abstract Syntax Tree/ of 'Token_Term'. +type AST_Term src ss = BinTree (Token_Term src ss) + +-- * Class 'Inj_Modules' +type Inj_Modules src ss + = Inj_ModulesR src ss ss + +inj_Modules :: + forall src ss. + Inj_Modules src ss => + Either Error_Module (Modules src ss) +inj_Modules = inj_ModulesR @_ @_ @ss + +-- ** Class 'Inj_ModulesR' +class Inj_ModulesR src (ss::[*]) (rs::[*]) where + inj_ModulesR :: Either Error_Module (Modules src ss) +instance Inj_ModulesR src ss '[] where + inj_ModulesR = Right $ Modules mempty +instance + ( ModuleFor src ss s + , Inj_ModulesR src ss rs + ) => Inj_ModulesR src ss (Proxy s ': rs) where + inj_ModulesR = do + x <- inj_ModulesR @_ @_ @rs + let (n, m) = moduleFor @_ @_ @s + Modules (Map.singleton n m) `unionModules` x + +-- * Type 'DefTerm' +data DefTerm src ss + = forall vs t. + (:=) (WithFixity NameTe) + (forall ts. Term src ss ts vs t) + +-- | Lookup given 'Mod' 'NameTe' into the 'Infix' 'TermDef' of given 'Modules'. +-- +-- NOTE: 'Token_Term_App' is returned for the space 'NameTe'. +lookupDefTerm :: + forall src ss fixy. + FixitySing fixy -> + Imports -> + Mod NameTe -> + Modules src ss -> + Either Error_Module (Tokenizer fixy src ss) +lookupDefTerm FixitySing_Infix _is ([] `Mod` " ") _ms = + Right $ Tokenizer + { token_term = Token_Term_App @src @ss + , token_fixity = Infix (Just AssocL) 9 + } +lookupDefTerm fixy (Imports is) mn@(m `Mod` n) (Modules mods) = + let mod_fixy = module_fixity fixy in + case Map.lookup m is of + Nothing -> + maybe (Left $ Error_Module_missing m) Right (Map.lookup m mods) >>= + maybe (Left $ Error_Module_missing_Term mn) Right . + Map.lookup n . mod_fixy + Just ims -> + let look = + -- n matches amongst ims + (`Map.mapMaybeWithKey` ims) $ \im _ft -> -- TODO: filter NameTe + Map.lookup im mods >>= + Map.lookup n . mod_fixy >>= + Just . Map.singleton n in + case Map.minView look of + Nothing -> Left $ Error_Module_missing_Term mn + Just (r, rs) | null rs -> Right $ snd $ Map.findMin r + | otherwise -> Left $ Error_Module_ambiguous mn $ fst . Map.findMin <$> look + +-- | Delete given 'Mod' 'NameTe' into given 'Modules'. +deleteDefTerm :: Mod NameTe -> Modules src ss -> Modules src ss +deleteDefTerm (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms + where del mod = mod + { module_prefix = Map.delete n $ module_prefix mod + , module_infix = Map.delete n $ module_infix mod + , module_postfix = Map.delete n $ module_postfix mod + } + +-- | Delete given 'Mod' 'NameTe' into 'module_infix's of given 'Modules'. +deleteDefTermInfix :: Mod NameTe -> Modules src ss -> Modules src ss +deleteDefTermInfix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms + where del mod = mod{module_infix = Map.delete n $ module_infix mod} + +-- | Delete given 'Mod' 'NameTe' into 'module_prefix's of given 'Modules'. +deleteDefTermPrefix :: Mod NameTe -> Modules src ss -> Modules src ss +deleteDefTermPrefix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms + where del mod = mod{module_prefix = Map.delete n $ module_prefix mod} + +-- | Delete given 'Mod' 'NameTe' into 'module_postfix's of given 'Modules'. +deleteDefTermPostix :: Mod NameTe -> Modules src ss -> Modules src ss +deleteDefTermPostix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms + where del mod = mod{module_postfix = Map.delete n $ module_postfix mod} + +insertDefTerm :: + forall src ss. + Source src => + Mod (DefTerm src ss) -> Modules src ss -> Modules src ss +insertDefTerm (m `Mod` (n `WithFixity` fixy := t)) (Modules ms) = + Modules $ Map.insert m (insertFixity ins fixy moduleEmpty) ms + where + ins :: fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx + ins fx = Map.insert n $ Tokenizer fx $ Token_Term . setSource (TermAVT t) + +insertTermVT :: + forall src ss. + Source src => + Mod (TermVT src ss '[]) -> NameTe -> Fixity -> + Modules src ss -> Modules src ss +insertTermVT (m `Mod` t) n fixy (Modules ms) = + Modules $ Map.insert m (insertFixity ins fixy moduleEmpty) ms + where + ins :: fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx + ins fx = Map.insert n $ Tokenizer fx $ Token_TermVT . setSource t + +insertFixity :: + (forall fx. fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx) -> + Fixity -> Module src ss -> Module src ss +insertFixity ins fx mod = + case fx of + Fixity1 uni@Prefix{} -> mod {module_prefix = ins uni $ module_prefix mod} + Fixity2 inf@Infix{} -> mod {module_infix = ins inf $ module_infix mod} + Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod} + +-- ** Type 'WithFixity' +data WithFixity a + = WithFixity a Fixity + deriving (Eq, Show) +instance IsString (WithFixity NameTe) where + fromString a = WithFixity (fromString a) (Fixity2 infixN5) + +withInfix :: a -> Infix -> WithFixity a +withInfix a inf = a `WithFixity` Fixity2 inf +withInfixR :: a -> Precedence -> WithFixity a +withInfixR a p = a `WithFixity` Fixity2 (infixR p) +withInfixL :: a -> Precedence -> WithFixity a +withInfixL a p = a `WithFixity` Fixity2 (infixL p) +withInfixN :: a -> Precedence -> WithFixity a +withInfixN a p = a `WithFixity` Fixity2 (infixN p) +withInfixB :: a -> (Side, Precedence) -> WithFixity a +withInfixB a (lr, p) = a `WithFixity` Fixity2 (infixB lr p) +withPrefix :: a -> Precedence -> WithFixity a +withPrefix a p = a `WithFixity` Fixity1 (Prefix p) +withPostfix :: a -> Precedence -> WithFixity a +withPostfix a p = a `WithFixity` Fixity1 (Postfix p) + +-- ** Type 'FixitySing' +data FixitySing fixy where + FixitySing_Prefix :: FixitySing Unifix + FixitySing_Infix :: FixitySing Infix + FixitySing_Postfix :: FixitySing Unifix +deriving instance Eq (FixitySing fixy) +deriving instance Show (FixitySing fixy) diff --git a/Language/Symantic/Compiling/Read.hs b/Language/Symantic/Compiling/Read.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Compiling/Read.hs @@ -0,0 +1,233 @@ +{-# LANGUAGE GADTs #-} +module Language.Symantic.Compiling.Read where + +import Control.Arrow (left) +import qualified Data.Kind as K + +import Language.Symantic.Grammar +import Language.Symantic.Typing + +import Language.Symantic.Compiling.Term +import Language.Symantic.Compiling.Module +import Language.Symantic.Compiling.Beta + +-- * Type 'ReadTerm' +-- | Convenient type alias for 'readTerm' and related functions. +type ReadTerm src ss ts = + Source src => + Inj_Source (TypeVT src) src => + Inj_Source (KindK src) src => + Inj_Source (AST_Type src) src => + Constable (->) => + Name2Type src -> + CtxTy src ts -> + AST_Term src ss -> + Either (Error_Term src) (TermVT src ss ts) + +-- | Read a 'TermVT' from and 'AST_Term'. +readTerm :: forall src ss ts. ReadTerm src ss ts +readTerm n2t ctxTy ast = do + ts <- go ctxTy `traverse` ast + inj_Error `left` betaTerms ts + where + go :: + forall ts'. + CtxTy src ts' -> + Token_Term src ss -> + Either (Error_Term src) (TermVT src ss ts') + go _ts (Token_Term (TermAVT te)) = Right $ TermVT te + go _ts (Token_TermVT te) = Right $ liftTermVT te + go ts (Token_Term_Var _src name) = teVar name ts + go _ts (Token_Term_App _src) = Right $ TermVT teApp + go ts (Token_Term_Abst _src name_arg ast_ty_arg ast_body) = do + TypeVT ty_arg <- inj_Error `left` readType n2t ast_ty_arg + when_EqKind (inj_Kind @K.Type) (kindOf ty_arg) $ \Refl -> + case lenVars ty_arg of + LenS{} -> Left $ Error_Term_polymorphic $ TypeVT ty_arg + LenZ | (TypeK qa, TypeK ta) <- unQualTy ty_arg -> do + TermVT (Term qr tr (TeSym res)) <- readTerm n2t (CtxTyS name_arg ta ts) ast_body + let (qa', qr') = appendVars qa qr + let (ta', tr') = appendVars ta tr + Right $ + case (proveConstraint qa', proveConstraint qr') of + -- NOTE: remove provable Constraints to keep those smaller. + (Just Dict, Just Dict) -> TermVT $ + Term (noConstraintLen (lenVars tr')) (ta' ~> tr') $ + TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c) + (Just Dict, Nothing) -> TermVT $ + Term qr' (ta' ~> tr') $ + TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c) + (Nothing, Just Dict) -> TermVT $ + Term qa' (ta' ~> tr') $ + TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c) + (Nothing, Nothing) -> TermVT $ + Term (qa' # qr') (ta' ~> tr') $ + TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c) + go ts (Token_Term_Let _src name ast_arg ast_body) = do + TermVT (Term qa ta (TeSym arg)) <- readTerm n2t ts ast_arg + case lenVars ta of + LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta) + LenZ -> do + TermVT (Term qr tr (TeSym res)) <- readTerm n2t (CtxTyS name ta ts) ast_body + let (qa', qr') = appendVars qa qr + let tr' = allocVarsL (lenVars ta) tr + Right $ + case (proveConstraint qa', proveConstraint qr') of + -- NOTE: remove provable Constraints to keep those smaller. + (Just Dict, Just Dict) -> TermVT $ + Term (noConstraintLen (lenVars tr')) tr' $ + TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c) + (Just Dict, Nothing) -> TermVT $ + Term qr' tr' $ + TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c) + (Nothing, Just Dict) -> TermVT $ + Term qa' tr' $ + TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c) + (Nothing, Nothing) -> TermVT $ + Term (qa' # qr') tr' $ + TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c) + +teVar :: + forall ss src ts. + Source src => + NameTe -> CtxTy src ts -> Either (Error_Term src) (TermVT src ss ts) +teVar name CtxTyZ = Left $ Error_Term_unknown name +teVar name (CtxTyS n ty _) | n == name = + Right $ TermVT $ Term noConstraint ty $ + TeSym $ \(te `CtxTeS` _) -> te +teVar name (CtxTyS _n _typ ts') = do + TermVT (Term q t (TeSym te)) <- teVar @ss name ts' + Right $ TermVT $ Term q t $ + TeSym $ \(_ `CtxTeS` ts) -> te ts + +teApp :: + Source src => Constable (->) => + Term src ss ts '[Proxy (a::K.Type), Proxy (b::K.Type)] (() #> ((a -> b) -> a -> b)) +teApp = + Term noConstraint ((a ~> b) ~> a ~> b) $ + TeSym $ const apply + where + a :: Source src => Type src '[Proxy a, Proxy b] (a::K.Type) + a = tyVar "a" $ varZ + b :: Source src => Type src '[Proxy a, Proxy b] (b::K.Type) + b = tyVar "b" $ VarS varZ + +-- | Reduce number of 'Token_Term_App' in given 'AST_Term' by converting them into 'BinTree2'. +-- +-- NOTE: 'Token_Term_App' exists only to handle unifix operators applied to arguments. +reduceTeApp :: AST_Term src ss -> AST_Term src ss +reduceTeApp (BinTree2 x y) = + case reduceTeApp x of + BinTree0 Token_Term_App{} `BinTree2` x' -> reduceTeApp x' `BinTree2` reduceTeApp y + _ -> reduceTeApp x `BinTree2` reduceTeApp y +reduceTeApp (BinTree0 (Token_Term_Abst src n ty te)) = BinTree0 $ Token_Term_Abst src n ty (reduceTeApp te) +reduceTeApp (BinTree0 (Token_Term_Let src n bo te)) = BinTree0 $ Token_Term_Let src n (reduceTeApp bo) (reduceTeApp te) +reduceTeApp x@BinTree0{} = x + +-- ** Type 'ReadTermCF' +-- | Like 'ReadTerm', but 'CtxTe'-free. +-- +-- Useful in 'readTermWithCtx' to help GHC's type solver, which +-- "Cannot instantiate unification variable with a type involving foralls". +newtype ReadTermCF src ss + = ReadTermCF + { unReadTermCF :: forall ts. ReadTerm src ss ts } + +-- | Like 'readTerm' but with given context, and no more. +readTermWithCtx :: + Foldable f => + Source src => + Inj_Source (TypeVT src) src => + Inj_Source (KindK src) src => + Inj_Source (AST_Type src) src => + Constable (->) => + f (NameTe, TermT src ss '[] '[]) -> + Name2Type src -> + AST_Term src ss -> + Either (Error_Term src) (TermVT src ss '[]) +readTermWithCtx env = + readTermWithCtxClose $ + readTermWithCtxPush env readTerm + +-- | Like 'readTerm' but with given context. +readTermWithCtxPush :: + Foldable f => + f (NameTe, TermT src ss '[] '[]) -> + (forall ts'. ReadTerm src ss ts') -> + ReadTerm src ss ts +readTermWithCtxPush env readTe = + unReadTermCF $ foldr + (\t (ReadTermCF r) -> ReadTermCF $ readTermWithCtxPush1 t r) + (ReadTermCF readTe) env + +-- | Like 'readTerm' but with given 'TermT' pushed onto 'CtxTy' and 'CtxTe'. +readTermWithCtxPush1 :: + (NameTe, TermT src ss '[] '[]) -> + (forall ts'. ReadTerm src ss ts') -> + ReadTerm src ss ts +readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe n2t ctxTy ast = do + TermVT (Term q t (TeSym te)) <- readTe n2t (CtxTyS n (qn #> tn) ctxTy) ast + case proveConstraint qn of + Nothing -> Left $ Error_Term_proofless $ TypeVT qn + Just Dict -> + Right $ TermVT $ Term q t $ TeSym $ \c -> + let cte = qual qn $ te_n CtxTeZ in + te $ cte `CtxTeS` c + +-- | Close a 'ReadTerm' context. +readTermWithCtxClose :: + (forall ts'. ReadTerm src ss ts') -> + Source src => + Inj_Source (TypeVT src) src => + Inj_Source (KindK src) src => + Inj_Source (AST_Type src) src => + Constable (->) => + Name2Type src -> + AST_Term src ss -> + Either (Error_Term src) (TermVT src ss '[]) +readTermWithCtxClose readTe n2t = readTe n2t CtxTyZ + +-- * Type 'Error_Term' +data Error_Term src + = Error_Term_unknown NameTe + | Error_Term_polymorphic (TypeVT src) + | Error_Term_qualified (TypeVT src) + | Error_Term_proofless (TypeVT src) + | Error_Term_Type (Error_Type src) + | Error_Term_Beta (Error_Beta src) + {- Error_Term_Con_Type (Con_Type src ss) -} + {- Error_Term_Con_Kind (Con_Kind src) -} + deriving (Eq, Show) +instance Inj_Error (Error_Type src) (Error_Term src) where + inj_Error = Error_Term_Type +instance Inj_Error (Error_Beta src) (Error_Term src) where + inj_Error = Error_Term_Beta +instance Inj_Error (Con_Kind src) (Error_Term src) where + inj_Error = Error_Term_Type . inj_Error + +-- * Type 'SrcTe' +-- | A 'Source' usable when using 'readTerm'. +data SrcTe inp ss + = SrcTe_Less + | SrcTe_Input (Span inp) + | SrcTe_AST_Term (AST_Term (SrcTe inp ss) ss) + | SrcTe_AST_Type (AST_Type (SrcTe inp ss)) + | SrcTe_Kind (KindK (SrcTe inp ss)) + | SrcTe_Type (TypeVT (SrcTe inp ss)) + | SrcTe_Term + deriving (Eq, Show) + +type instance Source_Input (SrcTe inp ss) = inp + +instance Source (SrcTe inp ss) where + noSource = SrcTe_Less +instance Inj_Source (Span inp) (SrcTe inp ss) where + inj_Source = SrcTe_Input +instance Inj_Source (AST_Term (SrcTe inp ss) ss) (SrcTe inp ss) where + inj_Source = SrcTe_AST_Term +instance Inj_Source (AST_Type (SrcTe inp ss)) (SrcTe inp ss) where + inj_Source = SrcTe_AST_Type +instance Inj_Source (KindK (SrcTe inp ss)) (SrcTe inp ss) where + inj_Source = SrcTe_Kind +instance Inj_Source (TypeVT (SrcTe inp ss)) (SrcTe inp ss) where + inj_Source = SrcTe_Type diff --git a/Language/Symantic/Compiling/Term.hs b/Language/Symantic/Compiling/Term.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Compiling/Term.hs @@ -0,0 +1,285 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Language.Symantic.Compiling.Term where + +import Data.Maybe (isJust) +import Data.Semigroup (Semigroup(..)) +import qualified Data.Kind as K +import qualified Data.Set as Set +import qualified Data.Text as Text + +import Language.Symantic.Grammar +import Language.Symantic.Interpreting +import Language.Symantic.Transforming.Trans +import Language.Symantic.Typing + +-- * Type 'Term' +data Term src ss ts vs (t::K.Type) where + Term :: Type src vs q + -> Type src vs t + -> TeSym ss ts (q #> t) + -> Term src ss ts vs (q #> t) +instance Source src => Eq (Term src ss ts vs t) where + Term qx tx _ == Term qy ty _ = qx == qy && tx == ty +instance Source src => Show (Term src ss ts vs t) where + showsPrec p (Term q t _te) = showsPrec p (q #> t) + +-- Source +type instance SourceOf (Term src ss ts vs t) = src +instance Source src => Sourced (Term src ss ts vs t) where + sourceOf (Term _q t _te) = sourceOf t + setSource (Term q t te) src = Term q (setSource t src) te + +-- Const +instance ConstsOf (Term src ss ts vs t) where + constsOf (Term q t _te) = constsOf q `Set.union` constsOf t + +-- Var +type instance VarsOf (Term src ss ts vs t) = vs +instance LenVars (Term src ss ts vs t) where + lenVars (Term _q t _te) = lenVars t +instance AllocVars (Term src ss ts) where + allocVarsL len (Term q t te) = Term (allocVarsL len q) (allocVarsL len t) te + allocVarsR len (Term q t te) = Term (allocVarsR len q) (allocVarsR len t) te + +-- Fam +instance ExpandFam (Term src ss ts vs t) where + expandFam (Term q t te) = Term (expandFam q) (expandFam t) te + +-- Type +instance Inj_Source (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where + typeOf t = typeOfTerm t `source` TermT t + +typeOfTerm :: Source src => Term src ss ts vs t -> Type src vs t +typeOfTerm (Term q t _) = q #> t + +-- ** Type 'TermT' +-- | 'Term' with existentialized 'Type'. +data TermT src ss ts vs = forall t. TermT (Term src ss ts vs t) +instance Source src => Show (TermT src ss ts vs) where + showsPrec p (TermT t) = showsPrec p t + +-- ** Type 'TermVT' +-- | 'Term' with existentialized 'Var's and 'Type'. +data TermVT src ss ts = forall vs t. TermVT (Term src ss ts vs t) +instance Source src => Eq (TermVT src ss ts) where + TermVT x == TermVT y = + case appendVars x y of + (Term qx' tx' _, Term qy' ty' _) -> + isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty') +instance Source src => Show (TermVT src ss ts) where + showsPrec p (TermVT t) = showsPrec p t +type instance SourceOf (TermVT src ss ts) = src +instance Source src => Sourced (TermVT src ss ts) where + sourceOf (TermVT t) = sourceOf t + setSource (TermVT t) src = TermVT $ setSource t src + +liftTermVT :: TermVT src ss '[] -> TermVT src ss ts +liftTermVT (TermVT (Term q t (TeSym te))) = + TermVT $ Term q t $ + TeSym $ \_c -> te CtxTeZ + +-- ** Type 'TermAVT' +-- | Like 'TermVT', but 'CtxTe'-free. +data TermAVT src ss = forall vs t. TermAVT (forall ts. Term src ss ts vs t) +type instance SourceOf (TermAVT src ss) = src +instance Source src => Sourced (TermAVT src ss) where + sourceOf (TermAVT t) = sourceOf t + setSource (TermAVT t) src = TermAVT (setSource t src) +instance Source src => Eq (TermAVT src ss) where + TermAVT x == TermAVT y = + case appendVars x y of + (Term qx' tx' _, Term qy' ty' _) -> + isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty') +instance Source src => Show (TermAVT src ss) where + showsPrec p (TermAVT t) = showsPrec p t + +-- * Type 'TeSym' +-- | Symantic of a 'Term'. +newtype TeSym ss ts (t::K.Type) + = TeSym + ( forall term. + Syms ss term => + Sym_Lambda term => + QualOf t => + CtxTe term ts -> term (UnQualOf t) + ) + +-- | Like 'TeSym', but 'CtxTe'-free +-- and using 'inj_Sym' to be able to use 'Sym'@ (@'Proxy'@ s)@ inside. +teSym :: + forall s ss ts t. + Inj_Sym ss s => + (forall term. Sym (Proxy s) term => Sym_Lambda term => QualOf t => term (UnQualOf t)) -> + TeSym ss ts t +teSym t = inj_Sym @s (TeSym $ const t) + +-- ** Type family 'QualOf' +-- | Qualification +type family QualOf (t::K.Type) :: Constraint where + QualOf (q #> t) = q -- (q # QualOf t) + QualOf t = (()::Constraint) + +-- ** Type family 'UnQualOf' +-- | Unqualification +type family UnQualOf (t::K.Type) :: K.Type where + UnQualOf (q #> t) = t -- UnQualOf t + UnQualOf t = t + +-- | Return 'K.Constraint' and 'K.Type' part of given 'Type'. +unQualTy :: + Source src => + Type src vs (t::K.Type) -> + ( TypeK src vs K.Constraint + , TypeK src vs K.Type ) +unQualTy (TyApp _ (TyApp _ c q) t) + | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) c + = (TypeK q, TypeK t) +unQualTy t = (TypeK $ noConstraintLen (lenVars t), TypeK t) + +-- | Remove 'K.Constraint's from given 'Type'. +unQualsTy :: Source src => Type src vs (t::kt) -> TypeK src vs kt +unQualsTy (TyApp _ (TyApp _ c _q) t) + | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) c + = unQualsTy t +unQualsTy (TyApp src f a) + | TypeK f' <- unQualsTy f + , TypeK a' <- unQualsTy a + = TypeK $ TyApp src f' a' +unQualsTy t = TypeK t + +-- * Type 'CtxTe' +-- | GADT for an /interpreting context/: +-- accumulating at each /lambda abstraction/ +-- the @term@ of the introduced variable. +data CtxTe (term::K.Type -> K.Type) (hs::[K.Type]) where + CtxTeZ :: CtxTe term '[] + CtxTeS :: term t + -> CtxTe term ts + -> CtxTe term (t ': ts) +infixr 5 `CtxTeS` + +-- ** Type 'TermDef' +-- | Convenient type alias for defining 'Term'. +type TermDef s vs t = forall src ss ts. Source src => Inj_Sym ss s => Term src ss ts vs t + +-- ** Type family 'Sym' +type family Sym (s::K.Type) :: {-term-}(K.Type -> K.Type) -> Constraint + +-- ** Type family 'Syms' +type family Syms (ss::[K.Type]) (term:: K.Type -> K.Type) :: Constraint where + Syms '[] term = () + Syms (s ': ss) term = (Sym s term, Syms ss term) + +-- ** Type 'Inj_Sym' +-- | Convenient type synonym wrapping 'Inj_SymP' +-- applied on the correct 'Index'. +type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s + +-- | Inject a given /symantic/ @s@ into a list of them, +-- by returning a function which given a 'TeSym' on @s@ +-- returns the same 'TeSym' on @ss@. +inj_Sym :: + forall s ss ts t. + Inj_Sym ss s => + TeSym '[Proxy s] ts t -> + TeSym ss ts t +inj_Sym = inj_SymP @(Index ss (Proxy s)) + +-- *** Class 'Inj_SymP' +class Inj_SymP p ss s where + inj_SymP :: TeSym '[Proxy s] ts t -> TeSym ss ts t +instance Inj_SymP Zero (Proxy s ': ss) (s::k) where + inj_SymP (TeSym te) = TeSym te +instance Inj_SymP p ss s => Inj_SymP (Succ p) (not_s ': ss) s where + inj_SymP (te::TeSym '[Proxy s] ts t) = + case inj_SymP @p te :: TeSym ss ts t of + TeSym te' -> TeSym te' + +-- * Class 'Sym_Lambda' +class Sym_Lambda term where + -- | /Function application/. + apply :: term ((a -> b) -> a -> b) + default apply :: Sym_Lambda (UnT term) => Trans term => term ((a -> b) -> a -> b) + apply = trans apply + + -- | /Lambda application/. + app :: term (a -> b) -> (term a -> term b); infixr 0 `app` + default app :: Sym_Lambda (UnT term) => Trans term => term (arg -> res) -> term arg -> term res + app = trans2 app + + -- | /Lambda abstraction/. + lam :: (term a -> term b) -> term (a -> b) + default lam :: Sym_Lambda (UnT term) => Trans term => (term arg -> term res) -> term (arg -> res) + lam f = trans $ lam (unTrans . f . trans) + + -- | Convenient 'lam' and 'app' wrapper. + let_ :: term var -> (term var -> term res) -> term res + let_ x f = lam f `app` x + + -- | /Lambda abstraction/ beta-reducable without duplication + -- (i.e. whose variable is used once at most), + -- mainly useful in compiled 'Term's + -- whose symantics are not a single 'term' + -- but a function between 'term's, + -- which happens because those are more usable when used as an embedded DSL. + lam1 :: (term a -> term b) -> term (a -> b) + default lam1 :: Sym_Lambda (UnT term) => Trans term => (term a -> term b) -> term (a -> b) + lam1 = lam + + -- | /Qualification/. + -- + -- Workaround used in 'readTermWithCtx'. + qual :: proxy q -> term t -> term (q #> t) + default qual :: Sym_Lambda (UnT term) => Trans term => proxy q -> term t -> term (q #> t) + qual q = trans1 (qual q) + +lam2 :: Sym_Lambda term => (term a -> term b -> term c) -> term (a -> b -> c) +lam3 :: Sym_Lambda term => (term a -> term b -> term c -> term d) -> term (a -> b -> c -> d) +lam4 :: Sym_Lambda term => (term a -> term b -> term c -> term d -> term e) -> term (a -> b -> c -> d -> e) +lam2 f = lam1 $ lam1 . f +lam3 f = lam1 $ lam2 . f +lam4 f = lam1 $ lam3 . f + +-- Interpreting +instance Sym_Lambda Eval where + apply = Eval ($) + app = (<*>) + lam f = Eval (unEval . f . Eval) + lam1 = lam + qual _q (Eval t) = Eval $ Qual t + let_ x f = f x -- NOTE: like flip ($) +instance Sym_Lambda View where + apply = View $ \_po _v -> "($)" + app (View a1) (View a2) = View $ \po v -> + parenInfix po op $ + a1 (op, SideL) v <> " " <> a2 (op, SideR) v + where op = infixN 10 + lam f = View $ \po v -> + let x = "x" <> Text.pack (show v) in + parenInfix po op $ + "\\" <> x <> " -> " <> + unView (f (View $ \_po _v -> x)) (op, SideL) (succ v) + where op = infixN 1 + lam1 = lam + qual _q (View t) = View t -- TODO: maybe print q + let_ x f = + View $ \po v -> + let x' = "x" <> Text.pack (show v) in + parenInfix po op $ + "let" <> " " <> x' <> " = " + <> unView x (infixN 0, SideL) (succ v) <> " in " + <> unView (f (View $ \_po _v -> x')) (op, SideL) (succ v) + where op = infixN 1 +instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (Dup r1 r2) where + apply = dup0 @Sym_Lambda apply + app = dup2 @Sym_Lambda app + lam f = dup_1 lam_f `Dup` dup_2 lam_f + where lam_f = lam f + lam1 = lam + qual q = dup1 @Sym_Lambda (qual q) diff --git a/Language/Symantic/Interpreting.hs b/Language/Symantic/Interpreting.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Interpreting.hs @@ -0,0 +1,10 @@ +-- | Interpreting terms. +module Language.Symantic.Interpreting + ( module Language.Symantic.Interpreting.Eval + , module Language.Symantic.Interpreting.Dup + , module Language.Symantic.Interpreting.View + ) where + +import Language.Symantic.Interpreting.Eval +import Language.Symantic.Interpreting.Dup +import Language.Symantic.Interpreting.View diff --git a/Language/Symantic/Interpreting/Dup.hs b/Language/Symantic/Interpreting/Dup.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Interpreting/Dup.hs @@ -0,0 +1,51 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +-- | Interpreter to duplicate the representation of an expression +-- in order to evaluate it with different interpreters. +-- +-- NOTE: this is a more verbose, less clear, +-- and maybe less efficient alternative +-- to maintaining the universal polymorphism of @term@ +-- at parsing time as done with 'Term'; +-- it is mainly here for the sake of curiosity. +module Language.Symantic.Interpreting.Dup where + +-- | Interpreter's data. +data Dup term1 term2 a + = Dup + { dup_1 :: term1 a + , dup_2 :: term2 a + } + +dup0 + :: (cl r, cl s) + => (forall term. cl term => term a) + -> Dup r s a +dup0 f = f `Dup` f + +dup1 + :: (cl r, cl s) + => (forall term. cl term => term a -> term b) + -> Dup r s a + -> Dup r s b +dup1 f (a1 `Dup` a2) = + f a1 `Dup` f a2 + +dup2 + :: (cl r, cl s) + => (forall term. cl term => term a -> term b -> term c) + -> Dup r s a + -> Dup r s b + -> Dup r s c +dup2 f (a1 `Dup` a2) (b1 `Dup` b2) = + f a1 b1 `Dup` f a2 b2 + +dup3 + :: (cl r, cl s) + => (forall term. cl term => term a -> term b -> term c -> term d) + -> Dup r s a + -> Dup r s b + -> Dup r s c + -> Dup r s d +dup3 f (a1 `Dup` a2) (b1 `Dup` b2) (c1 `Dup` c2) = + f a1 b1 c1 `Dup` f a2 b2 c2 diff --git a/Language/Symantic/Interpreting/Eval.hs b/Language/Symantic/Interpreting/Eval.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Interpreting/Eval.hs @@ -0,0 +1,34 @@ +-- | Interpreter to evaluate a term as a host-term. +module Language.Symantic.Interpreting.Eval where + +import Control.Monad + +-- * Type 'Eval' + +-- | Interpreter's data. +newtype Eval a = Eval { unEval :: a } +instance Functor Eval where + fmap f (Eval a) = Eval (f a) +instance Applicative Eval where + pure = Eval + (Eval f) <*> (Eval a) = Eval (f a) +instance Monad Eval where + return = Eval + (Eval a) >>= f = f a + +-- | Interpreter. +eval :: Eval a -> a +eval = unEval + +-- ** Constructors +eval0 :: a -> Eval a +eval0 = Eval + +eval1 :: (a -> b) -> Eval a -> Eval b +eval1 = liftM + +eval2 :: (a -> b -> c) -> Eval a -> Eval b -> Eval c +eval2 = liftM2 + +eval3 :: (a -> b -> c -> d) -> Eval a -> Eval b -> Eval c -> Eval d +eval3 = liftM3 diff --git a/Language/Symantic/Interpreting/View.hs b/Language/Symantic/Interpreting/View.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Interpreting/View.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE UndecidableInstances #-} +-- | Interpreter to serialize an expression into a 'Text'. +module Language.Symantic.Interpreting.View where + +import Data.Text (Text) +import qualified Data.Text as Text +import Prelude hiding (Integral(..)) + +import Language.Symantic.Grammar + +-- * Type 'View' + +-- | Interpreter's data. +newtype View a + = View + { unView -- Inherited attribuctx: + :: (Infix, Side) + -> DepthLam + -- Synthetised attribuctx: + -> Text + } +type DepthLam = Int +instance Show (View a) where + show = Text.unpack . view + +-- | Interpreter. +view :: View a -> Text +view r = unView r (infixN0, SideL) 0 + +-- ** Constructors +view0 :: Text -> View a +view0 name = View $ \_op _v -> name + +view1 :: Text -> View a1 -> View a +view1 name (View a1) = View $ \po v -> + parenInfix po op $ + Text.intercalate " " + [ name + , a1 (op, SideL) v + ] + where op = infixN 10 + +view2 :: Text -> View a1 -> View a2 -> View a +view2 name (View a1) (View a2) = + View $ \po v -> + parenInfix po op $ + Text.intercalate " " + [ name + , a1 (op, SideL) v + , a2 (op, SideL) v + ] + where op = infixN 10 + +view3 :: Text -> View a1 -> View a2 -> View a3 -> View a +view3 name (View a1) (View a2) (View a3) = + View $ \po v -> + parenInfix po op $ + Text.intercalate " " + [ name + , a1 (op, SideL) v + , a2 (op, SideL) v + , a3 (op, SideL) v + ] + where op = infixN 10 + +viewInfix :: Text -> Infix -> View a1 -> View a2 -> View a +viewInfix name op (View a1) (View a2) = + View $ \po v -> + parenInfix po op $ + Text.intercalate " " + [ a1 (op, SideL) v + , name + , a2 (op, SideR) v + ] diff --git a/Language/Symantic/Transforming.hs b/Language/Symantic/Transforming.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Transforming.hs @@ -0,0 +1,8 @@ +-- | Transforming terms. +module Language.Symantic.Transforming + ( module Language.Symantic.Transforming.Trans + , module Language.Symantic.Transforming.Beta + ) where + +import Language.Symantic.Transforming.Trans +import Language.Symantic.Transforming.Beta diff --git a/Language/Symantic/Transforming/Beta.hs b/Language/Symantic/Transforming/Beta.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Transforming/Beta.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE GADTs #-} +-- | Interpreter to beta-reduce static lambdas +-- introduced only because of the compiling machinery +-- (hence preserving lambdas put by the user). +module Language.Symantic.Transforming.Beta where + +import Language.Symantic.Transforming.Trans +import Language.Symantic.Compiling.Term + +-- * Type 'BetaT' +-- | The annotation here is if a lambda is known statically, +-- and so can be applied if given an argument, +-- Moreover, it only does this beta-reduction if the lambda +-- has been introduced by the compiling phase +-- (which happens when a symantic method is a function +-- between 'term's instead of being only a 'term') +-- (i.e. 'lam1' is used, not 'lam') +data BetaT term a where + BetaT_Unk :: term a -> BetaT term a + BetaT_Lam1 :: (BetaT term a -> BetaT term b) -> BetaT term (a -> b) + +instance Sym_Lambda term => Trans (BetaT term) where + type UnT (BetaT term) = term + trans = BetaT_Unk + unTrans (BetaT_Unk t) = t + unTrans (BetaT_Lam1 f) = lam1 $ unTrans . f . trans + +-- | 'lam1' adds annotations, 'app' uses it +instance Sym_Lambda term => Sym_Lambda (BetaT term) where + lam1 = BetaT_Lam1 -- NOTE: only 'lam1' introduces 'BetaT_Lam1', not 'lam'. + app (BetaT_Lam1 f) = f + app f = trans2 app f + let_ x f = trans $ let_ (unTrans x) (unTrans . f . trans) + +-- | Transformer +betaT :: Trans (BetaT term) => BetaT term a -> term a +betaT = unTrans diff --git a/Language/Symantic/Transforming/Trans.hs b/Language/Symantic/Transforming/Trans.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Transforming/Trans.hs @@ -0,0 +1,39 @@ +module Language.Symantic.Transforming.Trans where + +-- | +-- * 'trans' is generally not /surjective/ +-- * 'unTrans' is not /injective/ +-- * 'unTrans' . 'trans' == 'id' +-- * 'trans' . 'unTrans' /= 'id' +-- +-- NOTE: @DefaultSignatures@ can be used +-- when declaring a symantic type class +-- to provide default definition of the methods: +-- implementing their identity transformation +-- in order to avoid boilerplate code +-- when writting 'Trans' instances which +-- do not need to alterate those methods. +class Trans tr where + -- | Return the underlying @tr@ of the transformer. + type UnT tr :: * -> * + + -- | Lift a tr to the transformer's. + trans :: UnT tr a -> tr a + -- | Unlift a tr from the transformer's. + unTrans :: tr a -> UnT tr a + + -- | Identity transformation for a unary symantic method. + trans1 :: (UnT tr a -> UnT tr b) -> (tr a -> tr b) + trans1 f = trans . f . unTrans + + -- | Identity transformation for a binary symantic method. + trans2 + :: (UnT tr a -> UnT tr b -> UnT tr c) + -> (tr a -> tr b -> tr c) + trans2 f t1 t2 = trans $ f (unTrans t1) (unTrans t2) + + -- | Identity transformation for a ternary symantic method. + trans3 + :: (UnT tr a -> UnT tr b -> UnT tr c -> UnT tr d) + -> (tr a -> tr b -> tr c -> tr d) + trans3 f t1 t2 t3 = trans $ f (unTrans t1) (unTrans t2) (unTrans t3) diff --git a/Language/Symantic/Typing.hs b/Language/Symantic/Typing.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing.hs @@ -0,0 +1,24 @@ +-- | Typing terms. +module Language.Symantic.Typing + ( module Language.Symantic.Typing.List + , module Language.Symantic.Typing.Peano + , module Language.Symantic.Typing.Kind + , module Language.Symantic.Typing.Variable + , module Language.Symantic.Typing.Type + , module Language.Symantic.Typing.Grammar + , module Language.Symantic.Typing.Document + , module Language.Symantic.Typing.Read + , module Language.Symantic.Typing.Show + , module Language.Symantic.Typing.Unify + ) where + +import Language.Symantic.Typing.List +import Language.Symantic.Typing.Peano +import Language.Symantic.Typing.Kind +import Language.Symantic.Typing.Variable +import Language.Symantic.Typing.Type +import Language.Symantic.Typing.Grammar +import Language.Symantic.Typing.Document +import Language.Symantic.Typing.Read +import Language.Symantic.Typing.Show +import Language.Symantic.Typing.Unify diff --git a/Language/Symantic/Typing/Document.hs b/Language/Symantic/Typing/Document.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing/Document.hs @@ -0,0 +1,177 @@ +{-# LANGUAGE PolyKinds #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Language.Symantic.Typing.Document where + +import Data.Function (id) +import Data.Map.Strict (Map) +import Data.Semigroup (Semigroup(..)) +import Data.Set (Set) +import Data.Text (Text) +import Data.Typeable +import qualified Data.List as L +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set +import qualified Data.Text as T + +import qualified Language.Symantic.Document as D +import Language.Symantic.Grammar +import Language.Symantic.Typing.Kind +import Language.Symantic.Typing.Variable +import Language.Symantic.Typing.Type + +-- * Type 'Config_Doc_Type' +newtype Config_Doc_Type + = Config_Doc_Type + { config_Doc_Type_vars_numbering :: Bool + -- ^ Style of /type variables/: + -- + -- * if 'True': use name and position (as in @a0@ then @a1@) + -- * if 'False': use name, and a counter when names collide (as in @a@ then @a1@) + -- + -- NOTE: if the name is empty, a 'freshName' is taken from 'poolNames'. + } + +config_doc_type :: Config_Doc_Type +config_doc_type = + Config_Doc_Type + { config_Doc_Type_vars_numbering = True } + +docType :: + forall src vs t d. + Semigroup d => + D.Doc_Text d => + D.Doc_Color d => + Config_Doc_Type -> + Precedence -> + Type src vs t -> d +docType conf pr ty = + let (v2n, _) = var2Name conf mempty ty in + go v2n (infixB SideL pr, SideL) ty + where + go :: + forall x. + (Map IndexVar Name) -> -- names of variables + (Infix, Side) -> + Type src vs x -> d + go _v2n _po c + | Just HRefl <- proj_ConstKiTy @Constraint @() c = D.textH "()" + go _v2n _po (TyConst _src _vs c) = D.stringH $ show c + go v2n _po (TyVar _src _n v) = + let iv = indexVar v in + case Map.lookup iv v2n of + Nothing -> error "[BUG] docType: variable name missing" + Just n -> D.textH n + go v2n _po (TyApp _ (TyConst _ _ f@Const{}) a) + | Just HRefl <- proj_ConstKi @(K []) @[] f = + "[" <> go v2n (infixB SideL 0, SideL) a <> "]" + go v2n po (TyApp _ (TyApp _ (TyConst _ _ f@Const{}) a) b) + | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a + , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f = + go v2n po b + | Just (Fixity2 op) <- fixityOf f = + (if needsParenInfix po op then D.paren else id) $ + go v2n (op, SideL) a <> + prettyConst f <> + go v2n (op, SideR) b + where + d_op = D.yellower + unParen ('(':s) | ')':s' <- reverse s = reverse s' + unParen s = s + prettyConst :: forall k c. Const src (c::k) -> d + prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = D.space <> d_op "=>" <> D.space + prettyConst c | Just HRefl <- proj_ConstKi @(K (#)) @(#) c = d_op "," <> D.space + prettyConst c | Just HRefl <- proj_ConstKi @(K (,)) @(,) c = d_op "," <> D.space + prettyConst c@Const{} + | r <- typeRepTyCon (typeRep c) + , tyConName r =="#~" + , tyConModule r =="Language.Symantic.Typing.Type" + -- XXX: module name must be in sync with where (#~) is defined. + -- NOTE: cannot use 'proj_ConstKi' here + -- because (#~) has a polymorphic kind. + = D.space <> d_op "~" <> D.space + | otherwise = D.space <> d_op (D.stringH $ unParen $ show c) <> D.space + go v2n po (TyApp _src f a) = + let op = infixL 11 in + (if needsParenInfix po op then D.paren else id) $ + go v2n (op, SideL) f <> + D.space <> + go v2n (op, SideR) a + go v2n po (TyFam _src _len fam args) = + let op = infixL 11 in + (if needsParenInfix po op then D.paren else id) $ + D.stringH (show fam) <> + foldlTys (\t acc -> + D.space <> go v2n (op, SideL) t <> acc + ) args D.empty + +docTypes :: + forall src vs ts d. + Semigroup d => + D.Doc_Text d => + D.Doc_Color d => + Config_Doc_Type -> + Types src vs ts -> d +docTypes conf tys = + d_op (D.charH '[') <> go tys <> d_op (D.charH ']') + where + d_op = D.yellower + go :: forall xs. Types src vs xs -> d + go TypesZ = D.empty + go (TypesS t0 (TypesS t1 ts)) = + docType conf 10 t0 <> + d_op (D.charH ',') <> D.space <> + docType conf 10 t1 <> + go ts + go (TypesS t ts) = docType conf 10 t <> go ts + +-- | Return a 'Map' associating a distinct 'Name' +-- for all the variables of the given 'Type'. +var2Name :: + Config_Doc_Type -> + (Map IndexVar Name, Names) -> + Type src vs t -> + (Map IndexVar Name, Names) +var2Name _cfg st TyConst{} = st +var2Name cfg st@(v2n, ns) (TyVar _src (NameVar n) v) = + let iv = indexVar v in + case Map.lookup iv v2n of + Just{} -> st + Nothing -> + let n' = + if config_Doc_Type_vars_numbering cfg && not (T.null n) + then n <> T.pack (show iv) + else freshifyName ns n in + let v2n' = Map.insert iv n' v2n in + let ns' = Set.insert n' ns in + (v2n', ns') +var2Name cfg st (TyApp _src f a) = var2Name cfg (var2Name cfg st f) a +var2Name cfg st (TyFam _src _len _fam as) = foldlTys (flip $ var2Name cfg) as st + +-- ** Type 'Name' +type Name = Text +type NameHint = Name +type Names = Set Name + +-- | Return given 'Name' renamed a bit to avoid +-- conflicting with any given 'Names'. +freshifyName :: Names -> Name -> Name +freshifyName ns "" = freshName ns +freshifyName ns n = + let ints = [1..] :: [Int] in + L.head + [ fresh + | suffix <- "" : (show <$> ints) + , fresh <- [n <> T.pack suffix] + , fresh `Set.notMember` ns + ] + +freshName :: Names -> Name +freshName ns = L.head $ poolNames L.\\ Set.toList ns + +-- | Infinite list of unique 'Name's: +-- @a, b, .., z, a1, b1 .., z1, a2, ..@ +poolNames :: [Name] +poolNames = + [ T.singleton n | n <- ['a'..'z'] ] <> + [ T.pack (n:show i) | n <- ['a'..'z'] + , i <- [1 :: Int ..] ] diff --git a/Language/Symantic/Typing/Grammar.hs b/Language/Symantic/Typing/Grammar.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing/Grammar.hs @@ -0,0 +1,134 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Language.Symantic.Typing.Grammar where + +import Control.Applicative (Applicative(..)) +import Data.List (foldl1') +import Data.String (IsString(..)) +import Data.Text (Text) +import qualified Data.Char as Char + +import Language.Symantic.Grammar +import Language.Symantic.Typing.Variable + +-- * Type 'NameTy' +newtype NameTy = NameTy Text + deriving (Eq, Ord, Show) +instance IsString NameTy where + fromString = NameTy . fromString + +-- ** Type 'NameConst' +type NameConst = NameTy + +-- ** Type 'NameFam' +type NameFam = NameTy + +-- * Type 'AST_Type' +-- | /Abstract Syntax Tree/ of 'Token_Type'. +type AST_Type src = BinTree (Token_Type src) -- (EToken src '[Proxy K.Type]) + +-- ** Type 'Token_Type' +data Token_Type src + = Token_Type_Const (At src NameTy) + | Token_Type_Var (At src NameVar) + -- deriving (Eq, Show) +instance Source src => Eq (Token_Type src) where + Token_Type_Const (At _ x) == Token_Type_Const (At _ y) = x == y + Token_Type_Var (At _ x) == Token_Type_Var (At _ y) = x == y + _ == _ = False +instance Source src => Show (Token_Type src) where + showsPrec p (Token_Type_Const (At _ x)) = + showParen (p >= 10) $ + showString "Token_Type_Const" . + showChar ' ' . showsPrec 10 x + showsPrec p (Token_Type_Var (At _ x)) = + showParen (p >= 10) $ + showString "Token_Type_Var" . + showChar ' ' . showsPrec 10 x + +-- * Class 'Gram_Type' +-- | Read an 'AST_Type' from a textual source. +class + ( Gram_Source src g + , Gram_Terminal g + , Gram_Rule g + , Gram_Alt g + , Gram_Try g + , Gram_App g + , Gram_AltApp g + , Gram_CF g + , Gram_Comment g + , Gram_Op g + ) => Gram_Type src g where + g_type :: CF g (AST_Type src) + g_type = rule "type" $ g_type_fun + g_type_fun :: CF g (AST_Type src) + g_type_fun = rule "type_fun" $ + infixrG g_type_list (g_source $ op <$ symbol "->") + where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src "(->)") + -- TODO: maybe not harcoding g_type_list and g_type_tuple2 + g_type_list :: CF g (AST_Type src) + g_type_list = rule "type_list" $ + g_source $ inside mk + (symbol "[") (optional g_type) (symbol "]") + (const <$> g_type_tuple2) + where + mk Nothing src = tok src + mk (Just a) src = BinTree2 (tok src) a + tok src = BinTree0 $ Token_Type_Const $ At src "[]" + g_type_tuple2 :: CF g (AST_Type src) + g_type_tuple2 = rule "type_tuple2" $ + try (parens (infixrG (g_type) (g_source $ op <$ symbol ","))) <+> (g_type_app) + where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src "(,)") + g_type_app :: CF g (AST_Type src) + g_type_app = rule "type_app" $ + foldl1' BinTree2 <$> some (g_type_atom) + g_type_atom :: CF g (AST_Type src) + g_type_atom = rule "type_atom" $ + try (parens g_type) <+> + g_type_name_const <+> + g_type_name_var <+> + g_type_symbol + g_type_name_const :: CF g (AST_Type src) + g_type_name_const = rule "type_name_const" $ + lexeme $ g_source $ + (\n ns src -> BinTree0 $ Token_Type_Const $ At src $ fromString $ n:ns) + <$> unicat (Unicat Char.UppercaseLetter) + <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number]) + g_type_name_var :: CF g (AST_Type src) + g_type_name_var = rule "type_name_var" $ + lexeme $ g_source $ + (\n ns src -> BinTree0 $ Token_Type_Var $ At src $ fromString $ n:ns) + <$> unicat (Unicat Char.LowercaseLetter) + <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number]) + g_type_symbol :: CF g (AST_Type src) + g_type_symbol = rule "type_symbol" $ + g_source $ (mk <$>) $ + parens $ many $ cf_of_Terminal $ choice g_ok `but` choice g_ko + where + mk s src = BinTree0 $ Token_Type_Const $ At src (fromString $ "(" ++ s ++ ")") + g_ok = unicat <$> + [ Unicat_Symbol + , Unicat_Punctuation + , Unicat_Mark + ] + g_ko = char <$> ['(', ')', '`'] + +deriving instance Gram_Type src g => Gram_Type src (CF g) +instance Gram_Source src EBNF => Gram_Type src EBNF +instance Gram_Source src RuleEBNF => Gram_Type src RuleEBNF + +-- | List of the rules of 'Gram_Type'. +gram_type :: Gram_Type () g => [CF g (AST_Type ())] +gram_type = + [ g_type + , g_type_fun + , g_type_list + , g_type_tuple2 + , g_type_app + , g_type_atom + , g_type_name_const + , g_type_name_var + , g_type_symbol + ] diff --git a/Language/Symantic/Typing/Kind.hs b/Language/Symantic/Typing/Kind.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing/Kind.hs @@ -0,0 +1,142 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE UndecidableInstances #-} +module Language.Symantic.Typing.Kind where + +import Data.Type.Equality (TestEquality(..), (:~:)(..)) +import qualified Data.Kind as K + +import Language.Symantic.Grammar + +-- * Type 'Kind' +-- | Singleton for kind types. +data Kind src k where + KiType :: src -> Kind src K.Type + KiConstraint :: src -> Kind src K.Constraint + KiFun :: src -> Kind src ka -> Kind src kb -> Kind src (ka -> kb) +infixr 5 `KiFun` + +type instance SourceOf (Kind src k) = src +instance Source src => Sourced (Kind src k) where + sourceOf (KiType src) = src + sourceOf (KiConstraint src) = src + sourceOf (KiFun src _a _b) = src + + setSource (KiType _loc) src = KiType src + setSource (KiConstraint _loc) src = KiConstraint src + setSource (KiFun _loc a b) src = KiFun src a b + +instance Show (Kind src k) where + show KiType{} = "*" + show KiConstraint{} = "Constraint" + show (KiFun _src a b) = "(" ++ show a ++ " -> " ++ show b ++ ")" +instance TestEquality (Kind src) where + testEquality = eqKind + +eqKind :: Kind xs x -> Kind ys y -> Maybe (x:~:y) +eqKind KiType{} KiType{} = Just Refl +eqKind KiConstraint{} KiConstraint{} = Just Refl +eqKind (KiFun _xs xa xb) (KiFun _ys ya yb) + | Just Refl <- eqKind xa ya + , Just Refl <- eqKind xb yb + = Just Refl +eqKind _ _ = Nothing + +-- * Type 'K' +type K (t::kt) = kt + +-- * Class 'KindOf' +-- | Return the 'Kind' of something. +class KindOf (a::kt -> K.Type) where + kindOf :: a t -> Kind (SourceOf (a t)) kt + +-- * Type 'Inj_Kind' +-- | Implicit 'Kind'. +-- +-- NOTE: GHC-8.0.1's bug +-- makes it fail to properly build an implicit 'Kind', +-- this can however be worked around by having the class instances +-- work on a data type 'Ty' instead of 'Data.K.Type', +-- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'Inj_KindP'. +class (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k where +instance (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k + +inj_Kind :: + forall k src. + Source src => + Inj_Kind k => + Kind src k +inj_Kind = inj_KindP @(Ty_of_Type k) (noSource @src) + +-- ** Type 'Inj_KindP' +class Inj_KindP k where + inj_KindP :: src -> Kind src (Type_of_Ty k) +instance Inj_KindP K.Constraint where + inj_KindP = KiConstraint +instance Inj_KindP Ty where + inj_KindP = KiType +instance (Inj_KindP a, Inj_KindP b) => Inj_KindP (a -> b) where + inj_KindP src = KiFun src (inj_KindP @a src) (inj_KindP @b src) + +-- ** Type 'Ty' +-- | FIXME: workaround to be removed when +-- +-- will be fixed. +data Ty + +-- ** Type family 'Ty_of_Type' +-- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here, +-- this notably disables the expansion of 'Ty_of_Type'@ Any@. +type family Ty_of_Type (t::K.Type) :: K.Type +type instance Ty_of_Type K.Type = Ty +type instance Ty_of_Type K.Constraint = K.Constraint +type instance Ty_of_Type (a -> b) = Ty_of_Type a -> Ty_of_Type b + +-- ** Type family 'Type_of_Ty' +-- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here, +-- this notably disables the expansion of 'Type_of_Ty'@ Any@. +type family Type_of_Ty (t::K.Type) :: K.Type +type instance Type_of_Ty Ty = K.Type +type instance Type_of_Ty K.Constraint = K.Constraint +type instance Type_of_Ty (a -> b) = Type_of_Ty a -> Type_of_Ty b + +-- * Type 'KindK' +-- | Existential for 'Kind'. +data KindK src = forall k. KindK (Kind src k) +instance Eq (KindK src) where + KindK x == KindK y + | Just _ <- eqKind x y = True + _x == _y = False +instance Show (KindK src) where + show (KindK x) = show x + +-- * Type 'Con_Kind' +data Con_Kind src + = Con_Kind_Eq (KindK src) (KindK src) + | Con_Kind_Arrow (KindK src) + deriving (Eq, Show) + +when_EqKind + :: Inj_Error (Con_Kind src) err + => Kind src x + -> Kind src y + -> ((x :~: y) -> Either err ret) -> Either err ret +when_EqKind x y k = + case x `eqKind` y of + Just Refl -> k Refl + Nothing -> Left $ inj_Error $ Con_Kind_Eq (KindK x) (KindK y) + +when_KiFun :: + Inj_Error (Con_Kind src) err => + Inj_Source (KindK src) src => + Kind src x -> + (forall a b. (x :~: (a -> b)) -> + Kind src a -> + Kind src b -> + Either err ret) -> + Either err ret +when_KiFun x k = + case x of + KiFun _src a b -> k Refl (a `source` KindK x) (b `source` KindK x) + _ -> Left $ inj_Error $ Con_Kind_Arrow (KindK x) diff --git a/Language/Symantic/Typing/List.hs b/Language/Symantic/Typing/List.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing/List.hs @@ -0,0 +1,110 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE UndecidableInstances #-} +-- | List utilities at the type-level. +module Language.Symantic.Typing.List where + +import GHC.Exts (Constraint) + +import Language.Symantic.Typing.Peano + +-- ** Type 'Index' +-- | Return the position of a type within a list of them. +-- This is useful to work around @OverlappingInstances@. +type family Index xs x where + Index (x ': xs) x = Zero + Index (not_x ': xs) x = Succ (Index xs x) + +-- * Type family @(++)@ +type family (++) xs ys where + '[] ++ ys = ys + -- xs ++ '[] = xs + (x ': xs) ++ ys = x ': xs ++ ys +infixr 5 ++ + +-- * Type family 'Concat' +type family Concat (xs::[[k]]) :: [k] where + Concat '[] = '[] + Concat (x ': xs) = x ++ Concat xs + +-- * Type family 'Concat_Constraints' +type family Concat_Constraints (cs::[Constraint]) :: Constraint where + Concat_Constraints '[] = () + Concat_Constraints (c ': cs) = (c, Concat_Constraints cs) + +-- * Type family 'DeleteAll' +type family DeleteAll (x::k) (xs::[k]) :: [k] where + DeleteAll x '[] = '[] + DeleteAll x (x ': xs) = DeleteAll x xs + DeleteAll x (y ': xs) = y ': DeleteAll x xs + +-- * Type family 'Head' +type family Head (xs::[k]) :: k where + Head (x ': _xs) = x + +-- * Type family 'Tail' +type family Tail (xs::[k]) :: [k] where + Tail (_x ': xs) = xs + +{- +-- * Type family 'Map' +type family Map (f::a -> b) (cs::[a]) :: [b] where + Map f '[] = '[] + Map f (c ': cs) = f c ': Map f cs +-} + +-- * Type family 'Nub' +type family Nub (xs::[k]) :: [k] where + Nub '[] = '[] + Nub (x ': xs) = x ': Nub (DeleteAll x xs) + +{- +-- * Type family 'L' +type family L (xs::[k]) :: Nat where + L '[] = 'Z + L (x ': xs) = 'S (L xs) + +-- ** Class 'Inj_L' +class Inj_L (as::[k]) where + inj_L :: SNat (L as) +instance Inj_L '[] where + inj_L = SNatZ +instance Inj_L as => Inj_L (a ': as) where + inj_L = SNatS (inj_L @_ @as) +-} + +-- * Type 'Len' +data Len (xs::[k]) where + LenZ :: Len '[] + LenS :: Len xs -> Len (x ': xs) + +instance Show (Len vs) where + showsPrec _p = showsPrec 10 . intLen + +addLen :: Len a -> Len b -> Len (a ++ b) +addLen LenZ b = b +addLen (LenS a) b = LenS $ addLen a b + +shiftLen :: + forall t b a. + Len a -> + Len (a ++ b) -> + Len (a ++ t ': b) +shiftLen LenZ b = LenS b +shiftLen (LenS a) (LenS b) = LenS $ shiftLen @t @b a b + +intLen :: Len xs -> Int +intLen = go 0 + where + go :: Int -> Len xs -> Int + go i LenZ = i + go i (LenS l) = go (1 + i) l + +-- ** Class 'Inj_Len' +class Inj_Len (vs::[k]) where + inj_Len :: Len vs +instance Inj_Len '[] where + inj_Len = LenZ +instance Inj_Len as => Inj_Len (a ': as) where + inj_Len = LenS inj_Len diff --git a/Language/Symantic/Typing/Peano.hs b/Language/Symantic/Typing/Peano.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing/Peano.hs @@ -0,0 +1,84 @@ +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -fno-warn-missing-methods #-} +-- | Natural numbers inductivey defined at the type-level, and of kind @*@. +module Language.Symantic.Typing.Peano where + +import Data.Type.Equality + +-- * Types 'Zero' and 'Succ' +data Zero +data Succ p + +-- ** Type synonyms for a few numbers +type P0 = Zero +type P1 = Succ P0 +type P2 = Succ P1 +type P3 = Succ P2 +-- ... + +-- * Type 'SPeano' +-- | Singleton for 'Zero' and 'Succ'. +data SPeano p where + SZero :: SPeano Zero + SSucc :: SPeano p -> SPeano (Succ p) +instance TestEquality SPeano where + testEquality SZero SZero = Just Refl + testEquality (SSucc x) (SSucc y) + | Just Refl <- testEquality x y + = Just Refl + testEquality _ _ = Nothing + +-- * Type 'IPeano' +-- | Implicit construction of 'SPeano'. +class IPeano p where + ipeano :: SPeano p +instance IPeano Zero where + ipeano = SZero +instance IPeano p => IPeano (Succ p) where + ipeano = SSucc ipeano + +-- * Type 'EPeano' +data EPeano where + EPeano :: SPeano p -> EPeano +instance Eq EPeano where + EPeano x == EPeano y = + case testEquality x y of + Just _ -> True + _ -> False +instance Show EPeano where + show (EPeano x) = show (integral_from_peano x::Integer) + +-- * Interface with 'Integral' +integral_from_peano :: Integral i => SPeano p -> i +integral_from_peano SZero = 0 +integral_from_peano (SSucc x) = 1 + integral_from_peano x + +peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret +peano_from_integral 0 k = k SZero +peano_from_integral i k | i > 0 = + peano_from_integral (i - 1) $ \p -> k (SSucc p) +peano_from_integral _ _ = error "peano_from_integral" + +{- +-- | /Type-level natural number/, inductively defined. +data Nat + = Z + | S Nat + +data SNat n where + SNatZ :: SNat 'Z + SNatS :: SNat n -> SNat ('S n) +instance Show (SNat n) where + showsPrec _p = showsPrec 10 . intNat + +intNat :: SNat n -> Int +intNat = go 0 + where + go :: Int -> SNat n -> Int + go i SNatZ = i + go i (SNatS n) = go (1 + i) n + +type family (+) (a::Nat) (b::Nat) :: Nat where + 'Z + b = b + 'S a + b = 'S (a + b) +-} diff --git a/Language/Symantic/Typing/Read.hs b/Language/Symantic/Typing/Read.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing/Read.hs @@ -0,0 +1,121 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE PolyKinds #-} +module Language.Symantic.Typing.Read where + +import Data.Map.Strict (Map) +import Data.Typeable +import qualified Data.Map.Strict as Map +import qualified Data.Text as Text + +import Language.Symantic.Grammar +import Language.Symantic.Typing.List +import Language.Symantic.Typing.Kind +import Language.Symantic.Typing.Type +import Language.Symantic.Typing.Show () +import Language.Symantic.Typing.Grammar +import Language.Symantic.Typing.Variable + +-- | Read a 'Type' from an 'AST_Type', given its 'Vars'. +readType :: + Inj_Source (KindK src) src => + Inj_Source (TypeVT src) src => + Inj_Source (AST_Type src) src => + Name2Type src -> + AST_Type src -> + Either (Error_Type src) (TypeVT src) +readType cs ast | EVars vs <- readVars (EVars VarsZ) ast = do + TypeT ty <- readTyVars cs vs ast + Right $ TypeVT ty + +-- | Read a 'Type' from an 'AST_Type', given its 'Vars'. +readTyVars :: + forall vs src. + Inj_Source (KindK src) src => + Inj_Source (TypeVT src) src => + Inj_Source (AST_Type src) src => + Name2Type src -> + Vars src vs -> + AST_Type src -> + Either (Error_Type src) (TypeT src vs) +readTyVars cs vs ast@(BinTree0 (Token_Type_Const (At _src name))) = + readTyName cs (inj_Source ast) (lenVars vs) name +readTyVars _cs vs ast@(BinTree0 (Token_Type_Var (At _src name))) = + case lookupVars name vs of + Just (EVar v) -> Right $ TypeT $ TyVar (inj_Source ast) name v + Nothing -> error "[BUG] readTyVars: lookupVars failed" +readTyVars cs vs ast@(ast_x `BinTree2` ast_y) = do + TypeT ty_x <- readTyVars cs vs ast_x + TypeT ty_y <- readTyVars cs vs ast_y + when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b -> + when_EqKind ki_x_a (kindOf ty_y) $ \Refl -> + Right $ TypeT $ TyApp (inj_Source ast) ty_x ty_y + +-- | Lookup a 'TyConst' or 'Type' synonym +-- associated with given 'NameTy' in given 'Name2Type', +-- building it for a @vs@ of given 'Len'. +readTyName :: + Source src => + Name2Type src -> src -> Len vs -> NameTy -> + Either (Error_Type src) (TypeT src vs) +readTyName cs src len name = + case Map.lookup name cs of + Just (TypeTLen t) -> Right $ t len + Nothing -> Left $ Error_Type_Constant_unknown $ At src name + +-- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'. +readVars :: Source src => EVars src -> AST_Type src -> EVars src +readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (At _src name))) = + case lookupVars name vs of + Just{} -> evs + Nothing -> do + let kv = KiType noSource + let vs' = VarsS name kv vs + EVars vs' +readVars evs BinTree0{} = evs +readVars evs (BinTree2 x y) = + readVars (readVars evs x) y + +-- * Type 'Name2Type' +type Name2Type src = Map NameTy (TypeTLen src) + +-- ** Type 'TypeTLen' +-- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built. +-- +-- Useful to build a 'Name2Type' which can be used +-- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'. +newtype TypeTLen src = TypeTLen (forall vs. Len vs -> TypeT src vs) +instance Source src => Eq (TypeTLen src) where + TypeTLen x == TypeTLen y = x LenZ == y LenZ +instance Source src => Show (TypeTLen src) where + showsPrec p (TypeTLen t) = showsPrec p $ t LenZ + +-- ** Class 'Inj_Name2Type' +-- | Derive a 'Name2Type' from the given type-level list +-- of 'Proxy'-fied /type constants/. +class Inj_Name2Type cs where + inj_Name2Type :: Source src => Name2Type src +instance Inj_Name2Type '[] where + inj_Name2Type = Map.empty +instance + ( Inj_KindP (Ty_of_Type (K c)) + , K c ~ Type_of_Ty (Ty_of_Type (K c)) + , Constable c + , Inj_Name2Type cs + ) => Inj_Name2Type (Proxy c ': cs) where + inj_Name2Type = + Map.insert + (NameTy $ Text.pack $ show $ typeRep (Proxy @c)) + (TypeTLen $ \len -> TypeT $ TyConst noSource len $ + inj_ConstKi @(K c) @c $ + inj_KindP @(Ty_of_Type (K c)) noSource) $ + inj_Name2Type @cs + +-- * Type 'Error_Type' +data Error_Type src + = Error_Type_Constant_unknown (At src NameTy) + | Error_Type_Con_Kind (Con_Kind src) + deriving (Eq, Show) +instance Inj_Error (Error_Type src) (Error_Type src) where + inj_Error = id +instance Inj_Error (Con_Kind src) (Error_Type src) where + inj_Error = Error_Type_Con_Kind diff --git a/Language/Symantic/Typing/Show.hs b/Language/Symantic/Typing/Show.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing/Show.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE PolyKinds #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Language.Symantic.Typing.Show where + +import Data.Semigroup ((<>)) +import qualified Data.Text.Lazy as TL +import qualified Data.Text.Lazy.Builder as TLB + +import qualified Language.Symantic.Document as D +import Language.Symantic.Grammar +import Language.Symantic.Typing.Type +import Language.Symantic.Typing.Document + +showType :: Config_Doc_Type -> Type src vs t -> String +showType conf ty = TL.unpack $ TLB.toLazyText $ D.plain $ docType conf 0 ty + +showTypeS :: Config_Doc_Type -> Precedence -> Type src vs t -> ShowS +showTypeS conf pr ty s = s <> TL.unpack (TLB.toLazyText $ D.plain $ docType conf pr ty) + +showTypes :: Config_Doc_Type -> Types src vs ts -> String +showTypes conf tys = TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys) + +showTypesS :: Config_Doc_Type -> Types src vs ts -> ShowS +showTypesS conf tys s = s <> TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys) + +instance Source src => Show (Type src vs t) where + showsPrec = showTypeS config_doc_type +instance Source src => Show (TypeK src vs kt) where + showsPrec p (TypeK t) = showsPrec p t +instance Source src => Show (TypeVT src) where + showsPrec p (TypeVT t) = showsPrec p t +instance Source src => Show (TypeT src vs) where + showsPrec p (TypeT t) = showsPrec p t +instance Source src => Show (Types src vs ts) where + showsPrec _ = showTypesS config_doc_type diff --git a/Language/Symantic/Typing/Type.hs b/Language/Symantic/Typing/Type.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing/Type.hs @@ -0,0 +1,806 @@ +{-# language ConstraintKinds #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE LiberalTypeSynonyms #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Language.Symantic.Typing.Type + ( module Language.Symantic.Typing.Type + , Proxy(..) + , (:~:)(..) + , (:~~:)(..) + , K.Constraint + ) where + +import Control.Applicative (Alternative(..)) +import Data.Maybe (isJust) +import Data.Proxy +import Data.Semigroup ((<>)) +import Data.Set (Set) +import Data.Type.Equality +import Data.Typeable +import qualified Data.Kind as K +import qualified Data.Set as Set + +import Language.Symantic.Grammar +import Language.Symantic.Typing.List +import Language.Symantic.Typing.Kind +import Language.Symantic.Typing.Variable + +-- * Type 'Type' +data Type (src::K.Type) (vs::[K.Type]) (t::kt) where + TyConst :: src -> Len vs + -> Const src c + -> Type src vs c + TyApp :: src -> Type src vs f + -> Type src vs a + -> Type src vs (f a) + -- NOTE: @f a@ decomposition made possible + -- at the cost of requiring @TypeInType@. + TyVar :: src -> NameVar + -> Var src vs v + -> Type src vs v + TyFam :: src -> Len vs + -> Const src fam + -> Types src vs hs + -> Type src vs (Fam fam hs) + {- + TyPi :: src -> Type src (arg ': vs) res + -> Type (Pi arg res) src vs + TyQuant :: src -> NameHint + -> Kind src kv + -> (forall (v::kv). Type src vs v -> TypeK src vs k) + -> Type src vs (h::k) + TyEq :: src -> Type x src vs + -> Type y src vs + -> Type (x #~ y) src vs + -} + +instance Source src => Eq (Type src vs t) where + x == y = isJust $ eqType x y +instance Inj_Source (TypeVT src) src => TestEquality (Type src vs) where + testEquality = eqType + +type instance SourceOf (Type src vs t) = src +instance Source src => Sourced (Type src vs t) where + sourceOf (TyConst src _l _c) = src + sourceOf (TyApp src _f _a) = src + sourceOf (TyVar src _n _v) = src + sourceOf (TyFam src _l _f _as) = src + + setSource (TyConst _src l c) src = TyConst src l c + setSource (TyApp _src f a) src = TyApp src f a + setSource (TyVar _src n v) src = TyVar src n v + setSource (TyFam _src l f as) src = TyFam src l f as + +instance Inj_Source (TypeVT src) src => KindOf (Type src vs) where + kindOf t = kindOfType t `source` TypeVT t + +instance ConstsOf (Type src vs t) where + constsOf (TyConst _src _len c) = Set.singleton $ ConstC c + constsOf TyVar{} = Set.empty + constsOf (TyApp _src f a) = constsOf f `Set.union` constsOf a + constsOf (TyFam _src _len fam as) = constsOf fam `Set.union` constsOf as + +type instance VarsOf (Type src vs t) = vs +instance LenVars (Type src vs t) where + lenVars (TyConst _src len _c) = len + lenVars (TyApp _src f _a) = lenVars f + lenVars (TyVar _src _n v) = lenVars v + lenVars (TyFam _src l _f _as) = l +instance UsedVarsOf (Type src vs t) where + usedVarsOf vs TyConst{} k = k vs + usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k + usedVarsOf vs (TyApp _src f a) k = + usedVarsOf vs f $ \vs' -> + usedVarsOf vs' a k + usedVarsOf vs (TyVar _src _n v) k = + case insertUsedVars v vs of + Nothing -> k vs + Just vs' -> k vs' +instance VarOccursIn (Type src vs t) where + varOccursIn v (TyVar _src _n v') | Just{} <- v `eqVarKi` v' = False + varOccursIn _v TyVar{} = False + varOccursIn _v TyConst{} = False + varOccursIn v (TyApp _src f a) = varOccursIn v f || varOccursIn v a + varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as +instance AllocVars (Type src) where + allocVarsL len (TyConst src l c) = TyConst src (addLen len l) c + allocVarsL len (TyApp src f a) = TyApp src (allocVarsL len f) (allocVarsL len a) + allocVarsL len (TyVar src n v) = TyVar src n $ allocVarsL len v + allocVarsL len (TyFam src l f as) = TyFam src (addLen len l) f $ allocVarsL len `mapTys` as + + allocVarsR len (TyConst src l c) = TyConst src (addLen l len) c + allocVarsR len (TyApp src f a) = TyApp src (allocVarsR len f) (allocVarsR len a) + allocVarsR len (TyVar src n v) = TyVar src n $ allocVarsR len v + allocVarsR len (TyFam src l f as) = TyFam src (addLen l len) f $ allocVarsR len `mapTys` as + +-- | Like 'TyConst', but using 'noSource' and 'inj_Const'. +-- +-- FIXME: remove @kc@ when GHC's #12933 is fixed. +tyConst :: + forall kc (c::kc) src vs. + Source src => + Inj_Len vs => + Constable c => + Inj_KindP (Ty_of_Type kc) => + Type_of_Ty (Ty_of_Type kc) ~ kc => + Type src vs c +tyConst = TyConst noSource inj_Len inj_Const + -- NOTE: The forall brings @c@ first in the type variables, + -- which is convenient to use @TypeApplications@. + +-- | Like 'TyConst', but using 'noSource' and 'inj_Const'. +-- +-- FIXME: remove @kc@ when GHC's #12933 is fixed. +tyConstLen :: + forall kc (c::kc) src vs. + Source src => + Constable c => + Inj_KindP (Ty_of_Type kc) => + Type_of_Ty (Ty_of_Type kc) ~ kc => + Len vs -> + Type src vs c +tyConstLen len = TyConst noSource len inj_Const + +-- | Like 'TyApp', but using 'noSource'. +tyApp :: + Source src => + Type src vs f -> + Type src vs a -> + Type src vs (f a) +tyApp = TyApp noSource +infixl 9 `tyApp` + +-- | Like 'TyVar', but using 'noSource'. +tyVar :: + Source src => + NameVar -> + Var src vs v -> + Type src vs v +tyVar = TyVar noSource + +-- | Like 'TyFam', but using 'noSource'. +-- +-- FIXME: remove @kc@ when GHC's #12933 is fixed. +tyFam :: + forall kc (c::kc) as vs src. + Source src => + Inj_Len vs => + Constable c => + Inj_KindP (Ty_of_Type kc) => + Type_of_Ty (Ty_of_Type kc) ~ kc => + Types src vs as -> + Type src vs (Fam c as) +tyFam = TyFam noSource inj_Len (inj_Const @c) + +-- | Qualify a 'Type'. +tyQual :: + Source src => + Type src vs q -> + Type src vs t -> + (Qual q -> + Type src vs t -> + Type src vs (q #> t)) -> + Type src vs (q #> t) +tyQual q t f = + case proveConstraint q of + Just Dict -> f Dict t + Nothing -> q #> t +infix 1 `tyQual` + +-- ** Type 'TypeK' +-- | Existential 'Type' of a known 'Kind'. +data TypeK src vs kt = forall (t::kt). TypeK (Type src vs t) +type instance SourceOf (TypeK src vs ki) = src +type instance VarsOf (TypeK src vs ki) = vs +instance Source src => Eq (TypeK src vs ki) where + TypeK x == TypeK y = isJust $ eqType x y + +-- ** Type 'TypeT' +-- | Existential for 'Type'. +data TypeT src vs = forall t. TypeT (Type src vs t) +type instance SourceOf (TypeT src vs) = src +type instance VarsOf (TypeT src vs) = vs +instance Source src => Eq (TypeT src vs) where + TypeT x == TypeT y = isJust $ eqTypeKi x y + +-- ** Type 'TypeVT' +-- | Existential polymorphic 'Type'. +data TypeVT src = forall vs t. TypeVT (Type src vs t) +type instance SourceOf (TypeVT src) = src +instance Source src => Eq (TypeVT src) where + TypeVT x == TypeVT y = + let (x', y') = appendVars x y in + isJust $ eqTypeKi x' y' + +-- * Type 'Const' +-- | /Type constant/. +data Const src (c::kc) where + Const :: Constable c + => Kind src kc + -> Const src (c::kc) + +type instance SourceOf (Const src c) = src +instance ConstsOf (Const src c) where + constsOf = Set.singleton . ConstC +instance Inj_Source (ConstC src) src => KindOf (Const src) where + kindOf c@(Const kc) = kc `source` ConstC c + +kindOfConst :: Const src (t::kt) -> Kind src kt +kindOfConst (Const kc) = kc + +-- ** Class 'Constable' +class + ( Typeable c + , FixityOf c + , ClassInstancesFor c + , TypeInstancesFor c + ) => Constable c +instance + ( Typeable c + , FixityOf c + , ClassInstancesFor c + , TypeInstancesFor c + ) => Constable c + +-- ** Class 'ConstsOf' +-- | Return the 'Const's used by something. +class ConstsOf a where + constsOf :: a -> Set (ConstC (SourceOf a)) + +-- ** Class 'FixityOf' +-- | Return the 'Fixity' of something. +class FixityOf (c::kc) where + fixityOf :: proxy c -> Maybe Fixity + fixityOf _c = Nothing +instance FixityOf (c::K.Type) +instance FixityOf (c::K.Constraint) + +-- Show +instance Show (Const src c) where + showsPrec p c@Const{} = showsPrec p $ typeRep c + +-- ** Type 'ConstC' +data ConstC src + = forall c. ConstC (Const src c) +instance Eq (ConstC src) where + ConstC x == ConstC y = isJust $ x `eqConstKi` y +instance Ord (ConstC src) where + ConstC x `compare` ConstC y = x `ordConst` y + +-- * Type '(->)' +-- | The function 'Type' @(->)@, +-- with an infix notation more readable. +(~>) :: + Source src => + Constable (->) => + Type src vs a -> + Type src vs b -> + Type src vs (a -> b) +(~>) a b = (tyConstLen @(K (->)) @(->) (lenVars a) `tyApp` a) `tyApp` b +infixr 0 ~> +instance FixityOf (->) where + fixityOf _c = Just $ Fixity2 $ infixR 0 +{- NOTE: defined in Lib.Function +instance ClassInstancesFor (->) +instance TypeInstancesFor (->) +-} + +-- ** Type family 'FunArg' +type family FunArg (fun::K.Type) :: K.Type where + FunArg (q #> f) = FunArg f + FunArg (a -> b) = a + +-- ** Type family 'FunRes' +type family FunRes (fun::K.Type) :: K.Type where + FunRes (q #> f) = FunRes f + FunRes (a -> b) = b + +-- | Return, when the given 'Type' is a function, +-- the argument of that function. +unTyFun :: + forall t src tys. + Inj_Source (TypeVT src) src => + Constable (->) => + Type src tys t -> + Maybe ( Type src tys (FunArg t) + , Type src tys (FunRes t) ) +unTyFun ty_ini = go ty_ini + where + go :: + Type src tys x -> + Maybe ( Type src tys (FunArg x) + , Type src tys (FunRes x) ) + go (TyApp _ (TyApp _ (TyConst _ _ f) a) b) + | Just HRefl <- proj_ConstKi @(K (->)) @(->) f + = Just ((a `source` TypeVT ty_ini), (b `source` TypeVT ty_ini)) + go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b) + | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f + = go b + go TyApp{} = Nothing + go TyConst{} = Nothing + go TyVar{} = Nothing + go TyFam{} = Nothing + +-- ** Type @(#>)@ +-- | /Type constant/ to qualify a 'Type'. +newtype (#>) (q::K.Constraint) (a::K.Type) = Qual (q => a) +instance FixityOf (#>) where + fixityOf _c = Just $ Fixity2 $ infixR 0 +instance ClassInstancesFor (#>) +instance TypeInstancesFor (#>) + +(#>) :: + Source src => + Type src vs a -> + Type src vs b -> + Type src vs (a #> b) +(#>) a b = (tyConstLen @(K (#>)) @(#>) (lenVars a) `tyApp` a) `tyApp` b +infixr 0 #> + -- NOTE: should actually be (-1) + -- to compose well with @infixr 0 (->)@ + -- but this is not allowed by GHC. + +-- ** Class @(#)@ +-- | 'K.Constraint' union. +class (x, y) => x # y +instance (x, y) => x # y +instance FixityOf (#) where + fixityOf _c = Just $ Fixity2 $ infixB SideL 0 +instance ClassInstancesFor (#) where + proveConstraintFor _c (TyApp _ (TyApp _ c q0) q1) + | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) c + , Just Dict <- proveConstraint q0 + , Just Dict <- proveConstraint q1 + = Just Dict + proveConstraintFor _c _q = Nothing +instance TypeInstancesFor (#) + +(#) :: + Source src => + Type src vs qx -> + Type src vs qy -> + Type src vs (qx # qy) +(#) a b = (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b +infixr 2 # + +noConstraint :: + Source src => + Inj_Len vs => + Type src vs (()::K.Constraint) +noConstraint = tyConstLen @K.Constraint @(()::K.Constraint) inj_Len + +noConstraintLen :: + Source src => + Len vs -> + Type src vs (()::K.Constraint) +noConstraintLen = tyConstLen @K.Constraint @(()::K.Constraint) + +instance ClassInstancesFor (()::K.Constraint) where + proveConstraintFor _c q + | Just HRefl <- proj_ConstKiTy @K.Constraint @(()::K.Constraint) q + = Just Dict + proveConstraintFor _c _q = Nothing +instance TypeInstancesFor (()::K.Constraint) + +-- ** Class @(#~)@ +-- | /Type equality/ 'K.Constraint'. +class (x ~ y) => x #~ y +instance (x ~ y) => x #~ y +instance FixityOf (#~) where + fixityOf _ = Just $ Fixity2 $ infixB SideL 0 +instance + ( Inj_Kind k + , Typeable k + ) => ClassInstancesFor ((#~)::k -> k -> K.Constraint) where + proveConstraintFor _c (TyApp _ (TyApp _ c a) b) + | Just HRefl <- proj_ConstKiTy @(k -> k -> K.Constraint) @(#~) c + , Just Refl <- eqType a b + = Just Dict + proveConstraintFor _c _q = Nothing +instance TypeInstancesFor (#~) + +(#~) :: + forall k a b src vs. + Source src => + Typeable k => + Inj_Kind k => + Type src vs (a :: k) -> + Type src vs (b :: k) -> + Type src vs (a #~ b) +(#~) a b = (tyConstLen @(K (#~)) @(#~) (lenVars a) `tyApp` a) `tyApp` b +infixr 2 #~ + +{- +const_EqTy :: + forall k src. + Source src => + Typeable k => + Inj_Kind k => + Const src ((#~)::k -> k -> K.Constraint) +const_EqTy = inj_Const @(#~) +-} + +-- | /Type equality/. +eqType :: + Source src => + Type src tys (x::k) -> + Type src tys (y::k) -> + Maybe (x:~:y) +eqType x y | Just HRefl <- eqTypeKi x y = Just Refl +eqType _x _y = Nothing + +-- | /Heterogeneous type equality/: +-- return two proofs when two 'Type's are equals: +-- one for the type and one for the kind. +eqTypeKi :: + Source src => + Type src tys (x::kx) -> + Type src tys (y::ky) -> + Maybe (x:~~:y) +eqTypeKi (TyConst _sx _lx x) (TyConst _sy _ly y) = eqConstKi x y +eqTypeKi (TyVar _sx _nx x) (TyVar _sy _ny y) = eqVarKi x y +eqTypeKi (TyApp _sx fx ax) (TyApp _sy fy ay) + | Just HRefl <- eqTypeKi fx fy + , Just HRefl <- eqTypeKi ax ay + = Just HRefl +eqTypeKi (TyFam _ _lx fx ax) (TyFam _ _ly fy ay) + | Just HRefl <- eqConstKi fx fy + , Just HRefl <- eqTypes ax ay + = Just HRefl +-- NOTE: 'TyFam' is expanded as much as possible. +eqTypeKi x@TyFam{} y = eqTypeKi (expandFam x) y +eqTypeKi x y@TyFam{} = eqTypeKi x (expandFam y) +eqTypeKi _x _y = Nothing + +eqTypes :: + Source src => + Types src tys x -> + Types src tys y -> + Maybe (x:~~:y) +eqTypes TypesZ TypesZ = Just HRefl +eqTypes (x `TypesS` sx) (y `TypesS` sy) + | Just HRefl <- eqTypeKi x y + , Just HRefl <- eqTypes sx sy + = Just HRefl +eqTypes _x _y = Nothing + +-- *** Comparison +-- | Compare two 'Type's. +ordType :: + Source src => + Type src tys (x::kx) -> + Type src tys (y::ky) -> + Ordering +-- NOTE: 'TyFam' is expanded as much as possible. +ordType (TyFam _ _lx fx ax) (TyFam _ _ly fy ay) = ordConst fx fy <> ordTypes ax ay +ordType x@TyFam{} y = ordType (expandFam x) y +ordType x y@TyFam{} = ordType x (expandFam y) +ordType (TyConst _sx _lx x) (TyConst _sy _ly y) = ordConst x y +ordType TyConst{} _y = LT +ordType _x TyConst{} = GT +ordType (TyVar _sx _kx x) (TyVar _sy _ky y) = ordVarKi x y +ordType TyVar{} _y = LT +ordType _x TyVar{} = GT +ordType (TyApp _sx fx xx) (TyApp _sy fy xy) = ordType fx fy <> ordType xx xy +-- ordType TyApp{} _y = LT +-- ordType _x TyApp{} = GT + +ordTypes :: + Source src => + Types src tys x -> + Types src tys y -> + Ordering +ordTypes TypesZ TypesZ = EQ +ordTypes TypesZ TypesS{} = LT +ordTypes TypesS{} TypesZ = GT +ordTypes (x `TypesS` sx) (y `TypesS` sy) = ordType x y <> ordTypes sx sy + +-- * Type 'Qual' +-- | Captures the proof of a 'K.Constraint' +-- (and its dictionaries when it contains type classes): +-- pattern matching on the 'Dict' constructor +-- brings the 'K.Constraint' into scope. +data Qual q where + Dict :: q => Qual q + +-- ** Class 'ClassInstancesFor' +class ClassInstancesFor c where + proveConstraintFor + :: Source src + => proxy c + -> Type src vs q + -> Maybe (Qual q) + proveConstraintFor _c _q = Nothing + +proveConstraint :: Source src => Type src vs q -> Maybe (Qual q) +proveConstraint q = foldr proj Nothing $ constsOf q + where proj (ConstC c@Const{}) = (<|> proveConstraintFor c q) + +-- ** Injection +inj_Const :: + forall c src. + Source src => + Constable c => + Inj_KindP (Ty_of_Type (K c)) => + Type_of_Ty (Ty_of_Type (K c)) ~ K c => + Const src c +inj_Const = Const $ inj_KindP @(Ty_of_Type (K c)) noSource + +inj_ConstKi :: + forall kc c src. + Source src => + Constable c => + Kind src kc -> + Const src (c::kc) +inj_ConstKi = Const + +-- ** Projection +{- XXX: not working because of GHC's #12933 +proj_ConstKi :: + forall c u src. + Constable c => + (K c ~ Type_of_Ty (Ty_of_Type (K c))) => + Inj_Kind (K c) => + Const src u -> + Maybe (c :~~: u) +proj_ConstKi (Const ku) = do + Refl <- eqKind ku $ inj_Kind @(K c) @() + Refl :: u:~:c <- eqT + Just HRefl +-} + +-- | Like 'proj_ConstKi', but with kind equality already known. +proj_Const :: + forall c u src. + Typeable c => + Const src u -> + Maybe (c :~: u) +proj_Const Const{} = eqT + +-- | Like 'proj_Const', but on a 'Type'. +proj_ConstTy :: + forall c u src vs. + Typeable c => + Type src vs u -> + Maybe (c :~: u) +proj_ConstTy (TyConst _src _len Const{}) = eqT +proj_ConstTy _ = Nothing + +-- | XXX: 'proj_ConstKi' must be given the @kc@ kind explicitely, +-- when used multiple times in the same pattern match, +-- because of GHC's #12933. +proj_ConstKi :: + forall kc (c::kc) u src. + Typeable c => + (kc ~ Type_of_Ty (Ty_of_Type kc)) => + Inj_KindP (Ty_of_Type kc) => + Const src u -> + Maybe (c :~~: u) +proj_ConstKi (Const ku) = do + Refl <- eqKind ku $ inj_KindP @(Ty_of_Type kc) () + Refl :: u:~:c <- eqT + Just HRefl + +-- | Like 'proj_ConstKi', but on a 'Type'. +proj_ConstKiTy :: + forall kc (c::kc) u src vs. + Typeable c => + (kc ~ Type_of_Ty (Ty_of_Type kc)) => + Inj_KindP (Ty_of_Type kc) => + Type src vs u -> + Maybe (c :~~: u) +proj_ConstKiTy (TyConst _src _len c) = proj_ConstKi c +proj_ConstKiTy _ = Nothing + +eqConst :: + Const src_x (x::k) -> + Const src_y (y::k) -> + Maybe (x:~:y) +eqConst (Const _kx) (Const _ky) = eqT +instance Eq (Const src c) where + x == y = isJust $ eqConstKi x y +instance Ord (Const src c) where + compare = ordConst + +eqConstKi :: + forall src_x src_y kx ky x y. + Const src_x (x::kx) -> + Const src_y (y::ky) -> + Maybe (x:~~:y) +eqConstKi (Const kx) (Const ky) + | Just Refl <- eqKind kx ky + , Just (Refl::x:~:y) <- eqT + = Just HRefl +eqConstKi _x _y = Nothing + +ordConst :: + forall src_x src_y kx ky x y. + Const src_x (x::kx) -> + Const src_y (y::ky) -> + Ordering +ordConst x@Const{} y@Const{} = + typeRep x `compare` typeRep y + +normalizeQualsTy :: + Source src => + Type src tys (t::kt) -> + TypeK src tys kt +normalizeQualsTy = go + where + go :: + Source src => + Type src tys (a::ka) -> + TypeK src tys ka + -- (q0, q1) + go (TyApp s1 (TyApp s0 f q0) q1) + | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) f + , TypeK q0' <- go q0 + , TypeK q1' <- go q1 = + case (proveConstraint q0', proveConstraint q1') of + (Just{}, Just{}) -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q0 + (Just{}, Nothing) -> TypeK q1' + (Nothing, Just{}) -> TypeK q0' + (Nothing, Nothing) -> + case q0' `ordType` q1' of + LT -> TypeK $ TyApp s1 (TyApp s0 f q0') q1' + EQ -> TypeK $ q0' + GT -> TypeK $ TyApp s0 (TyApp s1 f q1') q0' + -- q0 => (q1 => t) + go (TyApp s1 (TyApp s0 f0@(TyConst sf0 lf0 _) q0) (TyApp s2 (TyApp s3 f1 q1) t)) + | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f0 + , Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f1 + , TypeK q0' <- go q0 + , TypeK q1' <- go q1 = + case (proveConstraint q0', proveConstraint q1') of + (Just{}, Just{}) -> TypeK t + (Just{}, Nothing) -> TypeK $ TyApp s2 (TyApp s3 f1 q1) t + (Nothing, Just{}) -> TypeK $ TyApp s1 (TyApp s0 f0 q0) t + (Nothing, Nothing) -> + case q0' `ordType` q1' of + LT -> + let q0q1 = TyApp s2 (TyApp s0 (TyConst sf0 lf0 $ inj_Const @(#)) q0') q1' in + TypeK $ TyApp s2 (TyApp s3 f1 q0q1) t + EQ -> TypeK $ TyApp s2 (TyApp s3 f1 q1') t + GT -> + let q1q0 = TyApp s0 (TyApp s2 (TyConst sf0 lf0 $ inj_Const @(#)) q1') q0' in + TypeK $ TyApp s2 (TyApp s3 f1 q1q0) t + -- q => t + go (TyApp _sa (TyApp _sq (TyConst _sc _lc c) q) t) + | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = + case proveConstraint q of + Just{} -> go t + Nothing + | TypeK q' <- go q + , TypeK t' <- go t + -> TypeK $ q' #> t' + -- q + go q + | Just Refl <- KiConstraint () `eqKind` kindOfType q + = case proveConstraint q of + Just{} -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q + Nothing -> TypeK q + go (TyApp src f a) + | TypeK f' <- go f + , TypeK a' <- go a + = TypeK $ TyApp src f' a' + go t@TyFam{} = go (expandFam t) + go t@TyConst{} = TypeK t + go t@TyVar{} = TypeK t + +-- * Type family 'Fam' +-- | Apply the /type family/ selected by @fam@ +-- to a list of types (within a 'Proxy'). +-- +-- | NOTE: |Fam|'s 'Kind' MUST be the same than @fam@'s. +type family Fam (fam::k) (hs::[K.Type]) :: k +-- type family FamKi fam :: K.Type + +-- ** Class 'TypeInstancesFor' +class TypeInstancesFor (c::kc) where + expandFamFor + :: Source src + => proxy c + -> Len vs + -> Const src fam + -> Types src vs ts + -> Maybe (Type src vs (Fam fam ts)) + expandFamFor _c _len _fam _as = Nothing + +-- ** Class 'ExpandFam' +class ExpandFam a where + expandFam :: Source (SourceOf a) => a -> a +instance ExpandFam (Type src vs t) where + expandFam t@TyConst{} = t + expandFam t@TyVar{} = t + expandFam (TyApp src f a) = TyApp src (expandFam f) (expandFam a) + expandFam t@(TyFam _src len fam as) = + case foldr proj Nothing $ constsOf fam `Set.union` constsOf as of + Nothing -> t + Just t' -> expandFam t' + where proj (ConstC c@Const{}) = (<|> expandFamFor c len fam as) + -- XXX: this can loop… + +-- | Like 'kindOf' but keep the old 'Source'. +kindOfType :: Type src vs (t::kt) -> Kind src kt +kindOfType (TyConst _src _l c) = kindOfConst c +kindOfType (TyApp _src f _a) = + case kindOfType f of + KiFun _src_kf _kx kf -> kf +kindOfType (TyVar _src _n v) = kindOfVar v +kindOfType (TyFam _src _len fam _as) = kindOfConst fam + +-- | Remove unused 'Var's from ther context. +normalizeVarsTy :: + Type src vs (t::kt) -> + (forall vs'. Type src vs' (t::kt) -> ret) -> ret +normalizeVarsTy ty k = + usedVarsOf UsedVarsZ ty $ \vs -> + k $ goTy vs ty + where + goTy :: + UsedVars src vs vs' -> + Type src vs t -> + Type src vs' t + goTy vs (TyConst src _len c) = TyConst src (lenVars vs) c + goTy vs (TyApp src f a) = TyApp src (goTy vs f) (goTy vs a) + goTy vs (TyVar src n v) = + case v `lookupUsedVars` vs of + Nothing -> error "[BUG] normalizeVarsTy: impossible lookup fail" + Just v' -> TyVar src n v' + goTy vs (TyFam src _len fam as) = TyFam src (lenVars vs) fam $ goTys vs as + + goTys :: + UsedVars src vs vs' -> + Types src vs ts -> + Types src vs' ts + goTys _vs TypesZ = TypesZ + goTys vs (TypesS t ts) = + goTy vs t `TypesS` + goTys vs ts + +-- * Type 'Types' +data Types src vs (ts::[K.Type]) where + TypesZ :: Types src vs '[] + TypesS :: Type src vs t + -> Types src vs ts + -> Types src vs (Proxy t ': ts) +infixr 5 `TypesS` + +type instance SourceOf (Types src vs ts) = src +instance ConstsOf (Types src vs ts) where + constsOf TypesZ = Set.empty + constsOf (TypesS t ts) = constsOf t `Set.union` constsOf ts +type instance VarsOf (Types src vs ts) = vs +instance UsedVarsOf (Types src vs ts) where + usedVarsOf vs TypesZ k = k vs + usedVarsOf vs (TypesS t ts) k = + usedVarsOf vs t $ \vs' -> + usedVarsOf vs' ts k +instance VarOccursIn (Types src vs ts) where + varOccursIn _v TypesZ = False + varOccursIn v (TypesS t ts) = varOccursIn v t || varOccursIn v ts + +mapTys :: + (forall kt (t::kt). Type src vs t -> Type src vs' t) -> + Types src vs ts -> + Types src vs' ts +mapTys _f TypesZ = TypesZ +mapTys f (TypesS t ts) = f t `TypesS` mapTys f ts + +foldlTys :: + (forall k (t::k). Type src vs t -> acc -> acc) -> + Types src vs ts -> acc -> acc +foldlTys _f TypesZ acc = acc +foldlTys f (TypesS t ts) acc = foldlTys f ts (f t acc) + +-- * Class 'TypeOf' +class TypeOf a where + typeOf :: a t -> Type (SourceOf (a t)) (VarsOf (a t)) t diff --git a/Language/Symantic/Typing/Unify.hs b/Language/Symantic/Typing/Unify.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing/Unify.hs @@ -0,0 +1,221 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Language.Symantic.Typing.Unify where + +import Data.Map.Strict (Map) +import Data.Semigroup (Semigroup(..)) +import Unsafe.Coerce (unsafeCoerce) +import qualified Data.Map.Strict as Map + +import Language.Symantic.Grammar +import Language.Symantic.Typing.Variable +import Language.Symantic.Typing.Kind +import Language.Symantic.Typing.Type +import Language.Symantic.Typing.Show () + +-- * Type 'Subst' +-- | /Type variable substitution/. +-- +-- WARNING: a 'Subst' MUST be without loops, and fully expanded. +newtype Subst src vs + = Subst (Map IndexVar (VT src vs)) +deriving instance Source src => Show (Subst src vs) +instance Semigroup (Subst src vs) where + (<>) = unionSubst +instance Monoid (Subst src vs) where + mempty = Subst Map.empty + mappend = (<>) + +-- | Unify two 'Subst's. +-- +-- NOTE: the union is left-biased: in case of duplicate 'Var's, +-- it keeps the one from the first 'Subst' given. +-- +-- NOTE: the first 'Subst' given is applied to the second (with 'subst'), +-- this way each 'Var' directly maps to an expanded 'Type', +-- so that, when using the resulting 'Subst', +-- there is no need to apply it multiple times +-- until there is no more substitution to be done. +unionSubst :: Subst src vs -> Subst src vs -> Subst src vs +unionSubst sx@(Subst x) (Subst y) = Subst $ x `Map.union` ((\(VT v r) -> VT v $ subst sx r) <$> y) + +-- * Type 'VT' +-- | A 'Var' and a 'Type' existentialized over their type index. +data VT src vs = forall t. VT (Var src vs t) (Type src vs t) +deriving instance Source src => Show (VT src vs) + +insertSubst :: Var src vs v -> Type src vs v -> Subst src vs -> Subst src vs +insertSubst v t (Subst s) = Subst $ Map.insert (indexVar v) (VT v t) s + +lookupSubst :: Var src vs v -> Subst src vs -> Maybe (Type src vs v) +lookupSubst v (Subst s) + | Just (VT v' t) <- Map.lookup (indexVar v) s + , Just HRefl <- v `eqVarKi` v' + = Just t +lookupSubst _v _m = Nothing + +-- * Class 'Substable' +class Substable a where + -- | Like 'substVar', but without the /occurence check/. + substVarUnsafe :: + src ~ SourceOf a => + vs ~ VarsOf a => + Var src vs v -> Type src vs v -> a -> a + -- | Substitute all the 'Var's which have a match in given 'Subst'. + subst :: + src ~ SourceOf a => + vs ~ VarsOf a => + Subst src vs -> a -> a +instance Substable (Type src vs t) where + substVarUnsafe _v _r t@TyConst{} = t + substVarUnsafe v r (TyApp src f a) = + TyApp src + (substVarUnsafe v r f) + (substVarUnsafe v r a) + substVarUnsafe v r t@(TyVar _src _n vt) = + case v `eqVarKi` vt of + Just HRefl -> r + Nothing -> t + substVarUnsafe v r (TyFam src len fam as) = + TyFam src len fam $ substVarUnsafe v r as + + subst _s t@TyConst{} = t + subst s (TyApp src f a) = TyApp src (subst s f) (subst s a) + subst (Subst s) t@(TyVar _src _n v) = + case indexVar v `Map.lookup` s of + Nothing -> t + Just (VT vr r) -> + case v `eqVarKi` vr of + Nothing -> error "[BUG] subst: kind mismatch" + Just HRefl -> r + subst s (TyFam src len fam as) = TyFam src len fam $ subst s as +instance Substable (Types src vs ts) where + substVarUnsafe _v _r TypesZ = TypesZ + substVarUnsafe v r (TypesS t ts) = + substVarUnsafe v r t `TypesS` + substVarUnsafe v r ts + subst _s TypesZ = TypesZ + subst s (TypesS t ts) = subst s t `TypesS` subst s ts + +-- | Substitute the given 'Var' by the given 'Type', +-- returning 'Nothing' if this 'Type' contains +-- the 'Var' (occurence check). +substVar :: + src ~ SourceOf a => + vs ~ VarsOf a => + Source src => VarOccursIn a => Substable a => + Var src vs v -> Type src vs v -> a -> Maybe a +substVar v r t = + if v `varOccursIn` r + then Nothing -- NOTE: occurence check + else Just $ substVarUnsafe v r t + +-- ** Type 'Error_Unify' +-- | Reasons why two 'Type's cannot be unified. +data Error_Unify src + = Error_Unify_Var_loop IndexVar (TypeVT src) + -- ^ /occurence check/: a 'Var' is unified with a 'Type' + -- which contains this same 'Var'. + | Error_Unify_Const_mismatch (TypeVT src) (TypeVT src) + -- ^ Two 'TyConst's should be the same, but are different. + | Error_Unify_Kind_mismatch (KindK src) (KindK src) + -- ^ Two 'Kind's should be the same, but are different. + | Error_Unify_Kind (Con_Kind src) + -- ^ Two 'Kind's mismatch. + | Error_Unify_mismatch (TypeVT src) (TypeVT src) + -- ^ Cannot unify those two 'Type's. + +deriving instance Source src => Eq (Error_Unify src) +deriving instance Source src => Show (Error_Unify src) + +instance Inj_Error (Error_Unify src) (Error_Unify src) where + inj_Error = id +instance Inj_Error (Con_Kind src) (Error_Unify src) where + inj_Error = Error_Unify_Kind + +-- | Return the left spine of a 'Type': +-- the root 'Type' and its 'Type' parameters, +-- from the left to the right. +spineTy :: + forall src vs t. + Source src => + Inj_Source (TypeVT src) src => + Type src vs t -> + (TypeT src vs, [TypeT src vs]) +spineTy typ = go [] typ + where + go :: forall x. [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs]) + go ctx (TyApp _ (TyApp _ (TyConst _ _ c) _q) t) + | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c + = go ctx t -- NOTE: skip the constraint @q@. + go ctx (TyApp _src f a) = go (TypeT (a `source` TypeVT typ) : ctx) f + go ctx t = (TypeT (t `source` TypeVT typ), ctx) + +{- +spineTy + :: Type src ctx ss cs (t::k) + -> (forall kx (x::kx) xs. Type src ctx ss cs x -> Types src ctx ss cs xs -> ret) + -> ret +spineTy = go TypesZ + where + go :: Types src ctx ss cs hs + -> Type src ctx ss cs (t::k) + -> (forall kx (x::kx) xs. Type src ctx ss cs x -> Types src ctx ss cs xs -> ret) + -> ret + go ctx (TyApp _src f a) k = go (a `TypesS` ctx) f k + go ctx (Term x _te) k = go ctx x k + go ctx (TyAny x) k = go ctx x k + go ctx t k = k t ctx +-} + +-- | Return the /most general unification/ of two 'Type's, when it exists. +unifyType :: + forall ki (x::ki) (y::ki) vs src. + Inj_Source (TypeVT src) src => + Inj_Error (Con_Kind src) (Error_Unify src) => + Subst src vs -> + Type src vs (x::ki) -> + Type src vs (y::ki) -> + Either (Error_Unify src) (Subst src vs) +unifyType vs x y = + let k = kindOfType x in + case (spineTy x, spineTy y) of + ((TypeT hx, px), (TypeT hy, py)) -> + case (hx, hy) of + (TyVar _ _n vx, _) | Just Refl <- k `eqKind` kindOfVar vx -> goVar vs vx y + (_, TyVar _ _n vy) | Just Refl <- k `eqKind` kindOfVar vy -> goVar vs vy x + (TyConst _sx _lx cx, TyConst _sy _ly cy) + | Just HRefl <- cx `eqConstKi` cy -> goList vs px py + | otherwise -> Left $ Error_Unify_Const_mismatch (TypeVT hx) (TypeVT hy) + _ -> + case (x, y) of + (TyApp _ fx ax, TyApp _ fy ay) -> + goList vs + [TypeT fx, TypeT ax] + [TypeT fy, TypeT ay] + _ -> Left $ Error_Unify_mismatch (TypeVT x) (TypeVT y) + where + goVar :: + forall k (a::k) (b::k) vs'. + Subst src vs' -> Var src vs' a -> Type src vs' b -> + Either (Error_Unify src) (Subst src vs') + goVar vs' va b = + case va `lookupSubst` vs' of + Just a -> unifyType vs' b a + Nothing -> + case vs' `subst` b of + TyVar _src _kb vb | Just HRefl <- va `eqVarKi` vb -> Right vs' + b' | va `varOccursIn` b' -> Left $ Error_Unify_Var_loop (indexVar va) (TypeVT b') + | Refl :: a :~: b <- unsafeCoerce Refl -> + Right $ insertSubst va b' mempty <> vs' + goList :: + forall vs'. + Subst src vs' -> [TypeT src vs'] -> [TypeT src vs'] -> + Either (Error_Unify src) (Subst src vs') + goList vs' [] [] = Right vs' + goList vs' (TypeT a:as) (TypeT b:bs) = + when_EqKind (kindOfType a) (kindOfType b) $ \Refl -> + unifyType vs' a b >>= \vs'' -> goList vs'' as bs + goList _vs _a _b = error "[BUG] unifyType: kinds mismatch" diff --git a/Language/Symantic/Typing/Variable.hs b/Language/Symantic/Typing/Variable.hs new file mode 100644 --- /dev/null +++ b/Language/Symantic/Typing/Variable.hs @@ -0,0 +1,223 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE UndecidableInstances #-} +module Language.Symantic.Typing.Variable where + +import Data.Proxy (Proxy(..)) +import Data.String (IsString(..)) +import Data.Text (Text) +import Data.Type.Equality ((:~:)(..)) +import qualified Data.Kind as K + +import Language.Symantic.Grammar +import Language.Symantic.Typing.List +import Language.Symantic.Typing.Kind + +-- | /Heterogeneous propositional equality/: +-- like (:~:) but prove also that the kinds are equal. +data (:~~:) (a::ka) (b::kb) where + HRefl :: a :~~: a + +-- * Type 'Var' +-- | A /type variable/, indexed amongst a type-level list. +-- @v@ is wrapped within a 'Proxy' to have a kind-heterogeneous list. +data Var src (vs::[K.Type]) (v::kv) where + VarZ :: Kind src kv + -> Len (Proxy (v::kv) ': vs) + -> Var src (Proxy (v::kv) ': vs) (v::kv) + VarS :: Var src vs v + -> Var src (not_v ': vs) v +infixr 5 `VarS` +type instance SourceOf (Var src vs t) = src +instance Show (Var src tys v) where + showsPrec p v = showsPrec p (indexVar v) +instance Inj_Source (EVar src vs) src => KindOf (Var src vs) where + kindOf v = kindOfVar v `source` EVar v +instance LenVars (Var src vs v) where + lenVars (VarZ _k l) = l + lenVars (VarS v) = LenS (lenVars v) +instance AllocVars (Var src) where + allocVarsL LenZ v = v + allocVarsL (LenS len) v = VarS $ allocVarsL len v + + allocVarsR len (VarZ k l) = VarZ k (addLen l len) + allocVarsR len (VarS v) = VarS $ allocVarsR len v + +varZ :: + forall src vs kv (v::kv). + Source src => + Inj_Len vs => + Inj_Kind kv => + Var src (Proxy v ': vs) v +varZ = VarZ inj_Kind inj_Len + +-- | Return the 'Kind' of given 'Var'. +kindOfVar :: Var src vs (v::kv) -> Kind src kv +kindOfVar (VarZ k _l) = k +kindOfVar (VarS v) = kindOfVar v + +-- ** Comparison +eqVar :: Var xs vs x -> Var ys vs y -> Maybe (x:~:y) +eqVar VarZ{} VarZ{} = Just Refl +eqVar (VarS x) (VarS y) = eqVar x y +eqVar _ _ = Nothing + +eqVarKi :: Var xs vs x -> Var ys vs y -> Maybe ((x::kx) :~~: (y::ky)) +eqVarKi VarZ{} VarZ{} = Just HRefl +eqVarKi (VarS x) (VarS y) = eqVarKi x y +eqVarKi _ _ = Nothing + +ordVarKi :: Var xs vs x -> Var ys vs y -> Ordering +ordVarKi VarZ{} VarZ{} = EQ +ordVarKi VarZ{} VarS{} = LT +ordVarKi VarS{} VarZ{} = GT +ordVarKi (VarS x) (VarS y) = ordVarKi x y + +-- * Type 'EVar' +-- | Existential 'Var'. +data EVar src vs = forall v. EVar (Var src vs v) + +-- ** Type 'IndexVar' +-- | Index of a 'Var'. +type IndexVar = Int +indexVar :: Var src vs v -> Int +indexVar VarZ{} = 0 +indexVar (VarS v) = 1 + indexVar v + +-- * Class 'LenVars' +-- | Return the 'Len' of the 'Var' context. +class LenVars a where + lenVars :: a -> Len (VarsOf a) + +-- * Class 'AllocVars' +-- | Allocate 'Var's in a 'Var' context, +-- either to the left or to the right. +class AllocVars (a::[K.Type] -> k -> K.Type) where + allocVarsL :: Len len -> a vs x -> a (len ++ vs) x + allocVarsR :: Len len -> a vs x -> a (vs ++ len) x + +appendVars :: + AllocVars a => + AllocVars b => + LenVars (a vs_x x) => + LenVars (b vs_y y) => + VarsOf (a vs_x x) ~ vs_x => + VarsOf (b vs_y y) ~ vs_y => + a vs_x (x::kx) -> + b vs_y (y::ky) -> + ( a (vs_x ++ vs_y) x + , b (vs_x ++ vs_y) y ) +appendVars x y = + ( allocVarsR (lenVars y) x + , allocVarsL (lenVars x) y + ) + +-- * Type 'NameVar' +newtype NameVar = NameVar Text + deriving (Eq, Ord, Show) +instance IsString NameVar where + fromString = NameVar . fromString + +-- * Class 'VarOccursIn' +-- | Test whether a given 'Var' occurs within something. +class VarOccursIn a where + varOccursIn :: Var src (VarsOf a) v -> a -> Bool + +-- * Type family 'VarsOf' +-- | Return the 'Var' context of something. +type family VarsOf a :: [K.Type] +type instance VarsOf (Var src vs v) = vs +type instance VarsOf (UsedVars src vs vs') = vs' + +-- * Type 'Vars' +-- | Growable list of 'Var's. +data Vars src vs where + VarsZ :: Vars src '[] + VarsS :: NameVar -> + Kind src kv -> + Vars src vs -> + Vars src (Proxy (v::kv) ': vs) +type instance VarsOf (Vars src vs) = vs +instance LenVars (Vars src vs) where + lenVars VarsZ = LenZ + lenVars (VarsS _n _kv vs) = LenS $ lenVars vs + +lookupVars :: + NameVar -> + Vars src vs -> + Maybe (EVar src vs) +lookupVars _n VarsZ = Nothing +lookupVars n (VarsS n' kv vs) = + if n == n' + then Just $ EVar $ VarZ kv (LenS $ lenVars vs) + else (\(EVar v) -> EVar $ VarS v) <$> lookupVars n vs + +insertVars :: + NameVar -> + Kind src k -> + Vars src vs -> + (forall vs'. Vars src vs' -> ret) -> ret +insertVars n kv vs k = + case lookupVars n vs of + Just{} -> k vs -- TODO: check kind? + Nothing -> k $ VarsS n kv vs + +-- ** Type 'EVars' +-- | Existential 'Vars'. +data EVars src = forall vs. EVars (Vars src vs) + +-- * Type 'UsedVars' +-- | List of 'Var's, used to change the context of a 'Var' +-- when removing unused 'Var's. +data UsedVars src vs vs' where + UsedVarsZ :: UsedVars src vs '[] + UsedVarsS :: Var src vs (v::k) -> + UsedVars src vs vs' -> + UsedVars src vs (Proxy v ': vs') +instance LenVars (UsedVars src vs vs') where + lenVars UsedVarsZ = LenZ + lenVars (UsedVarsS _v vs) = LenS $ lenVars vs + +lookupUsedVars :: + Var src vs v -> + UsedVars src vs vs' -> + Maybe (Var src vs' v) +lookupUsedVars _v UsedVarsZ = Nothing +lookupUsedVars v (UsedVarsS v' vs) = + case v `eqVarKi` v' of + Just HRefl -> Just $ VarZ (kindOfVar v) (LenS $ lenVars vs) + Nothing -> VarS <$> lookupUsedVars v vs + +insertUsedVars :: + Var src vs v -> + UsedVars src vs vs' -> + Maybe (UsedVars src vs (Proxy v ': vs')) +insertUsedVars v vs = + case lookupUsedVars v vs of + Just{} -> Nothing + Nothing -> Just $ UsedVarsS v vs + +-- ** Class 'UsedVarsOf' +class UsedVarsOf a where + usedVarsOf :: + UsedVars (SourceOf a) (VarsOf a) vs -> a -> + (forall vs'. UsedVars (SourceOf a) (VarsOf a) vs' -> ret) -> ret + +-- * Type 'UnProxy' +type family UnProxy (x::K.Type) :: k where + UnProxy (Proxy x) = x + +{- +-- ** Type family 'V' +type family V (vs::[K.Type]) (i::Nat) :: k where + V (v ': vs) 'Z = UnProxy v + V (not_v ': vs) ('S i) = V vs i + +-- ** Type family 'KV' +type family KV (vs::[K.Type]) (i::Nat) :: K.Type where + KV (Proxy v ': vs) 'Z = K v + KV (not_v ': vs) ('S i) = KV vs i +-} diff --git a/symantic.cabal b/symantic.cabal new file mode 100644 --- /dev/null +++ b/symantic.cabal @@ -0,0 +1,289 @@ +author: Julien Moutinho +bug-reports: Julien Moutinho +build-type: Simple +cabal-version: >= 1.24 +category: Language +description: + __Description__ + . + This is an experimental library for composing, parsing, typing, compiling, transforming and interpreting + a custom DSL (Domain-Specific Language) expressing + a subset of GHC's Haskell type system: + . + * /first class functions/ (aka. /lambdas/), + * chosen /monomorphic types/ (like 'Bool' or 'Maybe'), + * chosen /rank-1 polymorphic types/ (like @(@'Maybe'@ a)@), + * chosen /type class instances/, + * chosen /type family instances/, + * and chosen /type constraints/; + . + where "chosen X" means declared in Haskell + and selected when composing the DSL. + . + In particular, this library is currently not able to: + . + * do /type inferencing/ for the argument of /lambdas/ + (they must all be explicitely annotated, aka. /Church-style/), + * do /pattern matching/ (aka. /case/) (but /Church-encoding/ functions are often enough), + * do /rank-N polymorphic types/ (aka. /non-prenex forall/, like @(forall s. ST s a) -> a@). + . + And by itself, the DSL is only able to define new terms to be interpreted, + no new types, or other type-level structures. + . + __Warning__ + . + Please be aware that despite its using of powerful ideas from clever people, + this remains a FUND-LESS SINGLE-PERSON EXPERIMENTAL LIBRARY. + Meaning that it IS NOT heavily tested and documented, + DOES NOT have a strong commitment to preserving backward compatibility, + MAY FAIL to comply with the , + and CAN die without notice. + You've been warned. + . + __Use cases__ + . + The main goal of this library is to enable the runtime interpretation of terms, + type-checked according to some types defined at composing-time (ie. GHC's compile-time). + . + Using a DSL enables to limit expressiveness in order to ease analysis. + Here the idea is that the more complex logic shall remain written in Haskell, + and then this library used to project an interface into a DSL + (using GHC's Haskell as a FFI (Foreign Function Interface)). + This in order to give runtime users the flexibility + to write programs not requiring a full-blown Haskell compiler, + yet enabling enough flexibility to let them express complex needs + with a reasonably advanced type-safe way + and a controlled environment of primitives. + . + Typical use cases: + . + * Enabling runtime users to enter some Haskell-like expressions + (maybe with a more convenient syntax wrt. the domain problem) + without using at runtime all the heavy machinery and ecosystem of GHC + (eg. by using ), + but still leaning on primitive functions coded in GHC's Haskell. + * Limiting those expressions to be built from well-controlled expressions only. + * Run some analyzes/optimizations on those well-controlled expressions. + . + __Usage__ + . + Please pick in + a few specific @Lib/*.hs@ files near what you want to do + and the corresponding @Lib\/*/Test.hs@ file, + if any in the , + to learn by examples how to use this library. + . + Those @Lib\/*/Test.hs@ files use as parser + (see @Grammar/Megaparsec.hs@) and a default grammar somehow sticking to Haskell's, + but staying context-free (so in particular: insensitive to the indentation), + and supporting prefix and postfix operators. + This grammar — itself written as a symantic embedded DSL + with — + can be reused to build other ones, is not bound to a specific parser, + and can produce its own EBNF rendition. + . + __Acknowledgements__ + . + This library would probably be much worse than it is + without the following seminal works: + . + * by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. + * by Richard A. Eisenberg. + . + __Main ideas__ + . + * __Symantic DSL__. + Terms are encoded in the way (aka. the /symantic/ way) + which leverages the /type class/ system of Haskell — instead of using /data types/ — to form an embedded DSL. + More specifically, a /class/ encodes the /syntax/ of terms (eg. 'Sym_Bool') + and its /class instances/ on a dedicated type encodes their /semantics/ + (eg. @(Sym_Bool Eval)@ interprets a term as a value of its type + in the host language ('Bool' in Haskell here), + or @(Sym_Bool View)@ interprets a term as a textual rendition, etc.). + + DSL are then composed/extended by selecting those symantic /classes/ + (and in an embedded DSL those could even be automatically inferred, + when @NoMonomorphismRestriction@ is on). + Otherwise, when using symantics for a non-embedded DSL + — the whole point of this library — the /classes/ composing the DSL + are selected manually at GHC's compile-time, + through the /type-level list/ @ss@ given to 'readTerm'. + + Moreover, those symantic @term@s are parameterized by the type of the value they encode, + in order to get the same type safety as with plain Haskell values. + Hence the symantic /classes/ have the higher kind: @((* -> *) -> Constraint)@ + instead of just @(* -> Constraint)@. + + Amongst those symantics, 'Sym_Lambda' introduces /lambda abstractions/ by an higher-order approach, + meaning that they directly reuse GHC's internal machinery + to abstract or instantiate variables, + which I think is by far the most efficient and simplest way of doing it + (no (generalized or not) DeBruijn encoding + like in 's @Monad@s). + + * __Singleton for any type__. + To typecheck terms using a @(@'Type'@ src vs t)@ which acts as a /singleton type/ + for any Haskell /type index/ @t@ of any kind, + which is made possible with the dependant Haskell extensions: + especially @TypeFamilies@, @GADTs@ and @TypeInType@. + + * __Type constants using 'Typeable'__. + /Type constant/ could be introduced by indexing them amongst a /type-level list/, + but since they are /monomorphic types/, using 'Typeable' simplifies + the machinery, and is likely more space/time efficient, including at GHC-compile-time. + + * __Type variables using a type-level list__. + Handling /type variables/ is done by indexing them amongst a @vs@ /type-level list/, + where each /type variable/ is wrapped inside a @Proxy@ to handle different kinds. + Performing a substitution (in 'substVar') preserves the /type index/ @t@, + which is key for preserving any associated 'Term'. + Unifying /type variables/ is done with 'unsafeCoerce' (in 'unifyType'), + which I think is necessary and likely safe. + + -- NOTE: no longer used. + -- * __Extensible data type__. + -- To inject a type into a /type-level list/ + -- or project a /type-level list/ onto a type, + -- to compose an /extensible data type/ + -- (eg. the 'Token' @GADT@ gathering the 'TokenT' /data instances/, + -- that a parser can build and then give to 'compile'). + -- This type-level programming requires @UndecidableInstances@, + -- but not @OverlappingInstances@. + -- + -- There is a similarity with + -- + -- (see for instance + -- or ). + -- Those also enable to compose a DSL using some machinery + -- based upon (co)free(r) (co)monads and (cata|ana)morphisms. + -- Which library fits best your problem domain and brain is for you to judge :) + -- On that topic, see also: + -- . + -- + -- Here, I just came up using /type-level lists/ by hacking + -- 's @Elem@. + . + __Main extensions__ + . + * @AllowAmbiguousTypes@ for avoiding a lot of uses of 'Proxy'. + * @ConstraintKinds@ for /type lists/ to contain 'Constraint's, + or reifying any 'Constraint' as an explicit dictionary 'Dict', + or defining /type synonym/ of /type classes/, + or merging /type constraints/. + * @DataKinds@ for type-level data structures (eg. /type-level lists/). + * @DefaultSignatures@ for providing identity transformations of terms, + and thus avoid boilerplate code when a transformation + does not need to alter all semantics. + Almost as explained in . + * @GADTs@ for knowing types by pattern-matching terms, + or building terms by using type classes. + * @PolyKinds@ for avoiding a lot of uses of 'Proxy'. + * @Rank2Types@ or @ExistentialQuantification@ for parsing @GADT@s. + * @TypeApplications@ for having a more concise syntax + to build 'Type' (eg. 'tyConst'@ @\@Bool). + * @TypeFamilies@ for type-level programming. + * @TypeInType@ (introduced in GHC 8.0.1) + for 'Type' to also bind a kind equality for the type @t@ it encodes. + Which makes the /type application/ ('TyApp') + give us an /arrow kind/ for the Haskell /type constructor/ + it applies an Haskell type to, releaving me from tricky workarounds. + * @UndecidableInstances@ for type-level programming that may never terminate. + . + __Bugs__ + . + There are some of them hidding in there, + and the whole thing is far from being perfect… + Your comments, problem reports, or questions, are welcome! + You have my email address, so… just send me some emails :] + . + __To do__ + . + * Study to which point /type inferencing/ is doable, + now that 'Type' is powerful enough to contain 'TyVar's. + * Study to which point error messages can be improved, + now that there is a 'Source' carried through all 'Kind's or 'Type's, + it should enable some nice reports. + Still, a lot of work and testing remain to be done, + and likely some ideas to find too… + * Add more terms in . + * Add more transformations. + * Study how to integrate types into the module system. + * Study where to put @INLINE@, @INLINEABLE@ or @SPECIALIZE@ pragmas. + * Study how to support /rank-N polymorphic types/, + special cases can likely use the /boxed polymorphism/ workaround, + but even if GHC were supporting /impredicative types/, + I'm currently clueless about how to do this. +extra-source-files: +extra-tmp-files: +-- homepage: +license: GPL-3 +license-file: COPYING +maintainer: Julien Moutinho +name: symantic +stability: experimental +synopsis: Library for Typed Tagless-Final Higher-Order Composable DSL +tested-with: GHC==8.0.2 +-- PVP: +-+------- breaking API changes +-- | | +----- non-breaking API additions +-- | | | +--- code changes with no API change +version: 6.0.0.20170623 + +Source-Repository head + location: git://git.autogeree.net/symantic + type: git + +Library + default-extensions: + DataKinds + DefaultSignatures + FlexibleContexts + FlexibleInstances + LambdaCase + MultiParamTypeClasses + NamedFieldPuns + OverloadedStrings + Rank2Types + ScopedTypeVariables + StandaloneDeriving + TupleSections + TypeApplications + TypeFamilies + TypeOperators + ghc-options: -Wall + -fno-warn-tabs + default-language: Haskell2010 + exposed-modules: + Language.Symantic + Language.Symantic.Compiling + Language.Symantic.Compiling.Beta + Language.Symantic.Compiling.Grammar + Language.Symantic.Compiling.Module + Language.Symantic.Compiling.Read + Language.Symantic.Compiling.Term + Language.Symantic.Interpreting + Language.Symantic.Interpreting.Dup + Language.Symantic.Interpreting.Eval + Language.Symantic.Interpreting.View + Language.Symantic.Transforming + Language.Symantic.Transforming.Beta + Language.Symantic.Transforming.Trans + Language.Symantic.Typing + Language.Symantic.Typing.Document + Language.Symantic.Typing.Grammar + Language.Symantic.Typing.Kind + Language.Symantic.Typing.List + Language.Symantic.Typing.Peano + Language.Symantic.Typing.Read + Language.Symantic.Typing.Show + Language.Symantic.Typing.Type + Language.Symantic.Typing.Unify + Language.Symantic.Typing.Variable + build-depends: + base >= 4.6 && < 5 + , containers + , ghc-prim + , mono-traversable + , symantic-grammar + , symantic-document + , transformers + , text